alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* wrap/python/tests/ltl2tgba.test: Run $srcdir/ltl2tgba.py, not

Browse source 
ltl2tgba.py.
This commit is contained in:
Alexandre Duret-Lutz 2003-08-18 13:55:55 +00:00
parent 2b9f17202c
commit f4e9c1defa
2 changed files with 24 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,4 +1,9 @@
2003-08-15 Alexandre Duret-Lutz <adl@gnu.org> 2003-08-18 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* wrap/python/tests/ltl2tgba.test: Run $srcdir/ltl2tgba.py, not
ltl2tgba.py.
2003-08-15 Alexandre Duret-Lutz <aduret@src.lip6.fr>
This implements Couvreur's FM'99 ltl2tgba translation. This implements Couvreur's FM'99 ltl2tgba translation.
* src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ... * src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ...

36
wrap/python/tests/ltl2tgba.test
View file

@ -5,22 +5,22 @@ set -e
# We don't check the output, but just running these might be enough to # We don't check the output, but just running these might be enough to
# trigger assertions. # trigger assertions.
./run ltl2tgba.py a ./run $srcdir/ltl2tgba.py a
./run ltl2tgba.py 'a U b' ./run $srcdir/ltl2tgba.py 'a U b'
./run ltl2tgba.py 'X a' ./run $srcdir/ltl2tgba.py 'X a'
./run ltl2tgba.py 'a & b & c' ./run $srcdir/ltl2tgba.py 'a & b & c'
./run ltl2tgba.py 'a | b | (c U (d & (g U (h ^ i))))' ./run $srcdir/ltl2tgba.py 'a | b | (c U (d & (g U (h ^ i))))'
./run ltl2tgba.py 'Xa & (b U !a) & (b U !a)' ./run $srcdir/ltl2tgba.py 'Xa & (b U !a) & (b U !a)'
./run ltl2tgba.py 'Fa & Xb & GFc & Gd' ./run $srcdir/ltl2tgba.py 'Fa & Xb & GFc & Gd'
./run ltl2tgba.py 'Fa & Xa & GFc & Gc' ./run $srcdir/ltl2tgba.py 'Fa & Xa & GFc & Gc'
./run ltl2tgba.py 'Fc & X(a | Xb) & GF(a | Xb) & Gc' ./run $srcdir/ltl2tgba.py 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
./run ltl2tgba.py -f a ./run $srcdir/ltl2tgba.py -f a
./run ltl2tgba.py -f 'a U b' ./run $srcdir/ltl2tgba.py -f 'a U b'
./run ltl2tgba.py -f 'X a' ./run $srcdir/ltl2tgba.py -f 'X a'
./run ltl2tgba.py -f 'a & b & c' ./run $srcdir/ltl2tgba.py -f 'a & b & c'
./run ltl2tgba.py -f 'a | b | (c U (d & (g U (h ^ i))))' ./run $srcdir/ltl2tgba.py -f 'a | b | (c U (d & (g U (h ^ i))))'
./run ltl2tgba.py -f 'Xa & (b U !a) & (b U !a)' ./run $srcdir/ltl2tgba.py -f 'Xa & (b U !a) & (b U !a)'
./run ltl2tgba.py -f 'Fa & Xb & GFc & Gd' ./run $srcdir/ltl2tgba.py -f 'Fa & Xb & GFc & Gd'
./run ltl2tgba.py -f 'Fa & Xa & GFc & Gc' ./run $srcdir/ltl2tgba.py -f 'Fa & Xa & GFc & Gc'
./run ltl2tgba.py -f 'Fc & X(a | Xb) & GF(a | Xb) & Gc' ./run $srcdir/ltl2tgba.py -f 'Fc & X(a | Xb) & GF(a | Xb) & Gc'