#! /bin/sh
# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.


# Check for the equals visitor

. ./defs || exit 1

# No reduction
run 0 ./reduccmp 'a U b' 'a U b'
run 0 ./reduccmp 'a R b' 'a R b'
run 0 ./reduccmp 'a & b' 'a & b'
run 0 ./reduccmp 'a | b' 'a | b'
run 0 ./reduccmp 'a & (a U b)' 'a & (a U b)'
run 0 ./reduccmp 'a | (a U b)' 'a | (a U b)'

# Syntactic reduction
run 0 ./reduccmp 'a & (!b R !a)' 'false'
run 0 ./reduccmp '(!b R !a) & a' 'false'
#run 0 ./reduccmp '(!b R !a) | a' 'true'
#run 0 ./reduccmp 'a | (!b R !a)' 'true'

run 0 ./reduccmp 'a & (!b R !a) & c' 'false'
run 0 ./reduccmp 'c & (!b R !a) & a' 'false'
#run 0 ./reduccmp 'a | (!b R !a) | c' 'true'
#run 0 ./reduccmp 'c | (!b R !a) | a' 'true'

run 0 ./reduccmp 'a & (b U a)' 'a'
run 0 ./reduccmp '(b U a) & a' 'a'
run 0 ./reduccmp 'a | (b U a)' '(b U a)'
run 0 ./reduccmp '(b U a) | a' '(b U a)'
run 0 ./reduccmp 'a U (b U a)' '(b U a)'

run 0 ./reduccmp 'a & (b U a) & a' 'a'
run 0 ./reduccmp 'a & (b U a) & a' 'a'
run 0 ./reduccmp 'a | (b U a) | a' '(b U a)'
run 0 ./reduccmp 'a | (b U a) | a' '(b U a)'
run 0 ./reduccmp 'a U (b U a)' '(b U a)'


# Basics reduction
run 0 ./reduccmp 'X(true)' 'true'
run 0 ./reduccmp 'X(false)' 'false'
run 0 ./reduccmp 'F(true)' 'true'
run 0 ./reduccmp 'F(false)' 'false'
run 0 ./reduccmp 'G(true)' 'true'
run 0 ./reduccmp 'G(false)' 'false'

run 0 ./reduccmp 'XGF(f)' 'GF(f)'
run 0 ./reduccmp 'FX(a)' 'XF(a)'
run 0 ./reduccmp 'G(a R b)' 'G(b)'
run 0 ./reduccmp 'GX(a)' 'XG(a)'

run 0 ./reduccmp 'X(a) U X(b)' 'X(a U b)'
run 0 ./reduccmp 'X(a) R X(b)' 'X(a R b)'

run 0 ./reduccmp 'Xa & Xb' 'X(a & b)'
run 0 ./reduccmp '(a U b) & (c U b)' '(a & c) U b'
run 0 ./reduccmp '(a R b) & (a R c)' 'a R (b & c)'
run 0 ./reduccmp 'Xa | Xb' 'X(a | b)'
run 0 ./reduccmp '(a U b) | (a U c)' 'a U (b | c)'
run 0 ./reduccmp '(a R b) | (c R b)' '(a | c) R b'

run 0 ./reduccmp 'X(a & GFb)' 'Xa & GFb'
run 0 ./reduccmp 'X(a | GFb)' 'Xa | GFb'
run 0 ./reduccmp 'F(a & GFb)' 'Fa & GFb'
run 0 ./reduccmp 'G(a | GFb)' 'Ga | GFb'

run 0 ./reduccmp 'X(a & GFb & c)' 'X(a & c) & GFb'
run 0 ./reduccmp 'X(a | GFb | c)' 'X(a | c) | GFb'
run 0 ./reduccmp 'F(a & GFb & c)' 'F(a & c) & GFb'
run 0 ./reduccmp 'G(a | GFb | c)' 'G(a | c) | GFb'

# Eventuality and universality class reduction
run 0 ./reduccmp 'FFa' 'Fa'
run 0 ./reduccmp 'FGFa' 'GFa'
run 0 ./reduccmp 'b U Fa' 'Fa'
run 0 ./reduccmp 'b U GFa' 'GFa'
run 0 ./reduccmp 'Ga' 'Ga'
run 0 ./reduccmp 'GFGa' 'FGa'
run 0 ./reduccmp 'b R Ga' 'Ga'
run 0 ./reduccmp 'b R FGa' 'FGa'