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

* src/tgbatest/ltl2tgba.test: Test both -l and -f. This should

Browse source 
have been done on 2010-01-30 when the default translation was
changed from -l to -f.
This commit is contained in:
Alexandre Duret-Lutz 2010-11-25 19:59:46 +01:00
parent 0dca4be69d
commit 7627b9673b
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,9 @@
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbatest/ltl2tgba.test: Test both -l and -f. This should
have been done on 2010-01-30 when the default translation was
changed from -l to -f.
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbaalgos/scc.hh: Typos in the documentation. * src/tgbaalgos/scc.hh: Typos in the documentation.
@ -980,7 +986,7 @@
Speedup reduc.test by not spawning one process per formula. Speedup reduc.test by not spawning one process per formula.
* src/ltltest/reduc.cc: Add an option -f to read a lost of * src/ltltest/reduc.cc: Add an option -f to read a lot of
formulae from a file. Running a process for each formula was formulae from a file. Running a process for each formula was
too slow. Also add an option -h to hide reduced formulae. too slow. Also add an option -h to hide reduced formulae.
* src/ltltest/reduc.test: Simplify accordingly. * src/ltltest/reduc.test: Simplify accordingly.

2
src/tgbatest/ltl2tgba.test
View file

@ -29,7 +29,7 @@ set -e
check () check ()
{ {
run 0 ../ltl2tgba "$1" run 0 ../ltl2tgba -l "$1"
run 0 ../ltl2tgba -f "$1" run 0 ../ltl2tgba -f "$1"
run 0 ../ltl2tgba -f -FC "$1" run 0 ../ltl2tgba -f -FC "$1"
} }