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

* src/tgbatest/ltlcounter.test (run): Only construct small

Browse source 
formulae (i.e. n<=2) under valgrind.  The test case is too
slow otherwise.
This commit is contained in:
Alexandre Duret-Lutz 2009-11-05 14:12:47 +01:00
parent 24527d6f99
commit b57fdcb684
2 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2009-11-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbatest/ltlcounter.test (run): Only construct small
formulae (i.e. n<=2) under valgrind. The test case is too
slow otherwise.
2009-11-04 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-11-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix spurious failure of style.test. Fix spurious failure of style.test.

14
src/tgbatest/ltlcounter.test
View file

@ -31,13 +31,15 @@ lcl=$lcdir/LTLcounterLinear.pl
lcc=$lcdir/LTLcounterCarry.pl lcc=$lcdir/LTLcounterCarry.pl
lccl=$lcdir/LTLcounterCarryLinear.pl lccl=$lcdir/LTLcounterCarryLinear.pl
run='run 0'
check_formula() check_formula()
{ {
# First, check the satisfiability of the formula with Spot # First, check the satisfiability of the formula with Spot
run 0 ../ltl2tgba -e -x -f "$1" >/dev/null $run ../ltl2tgba -e -x -f "$1" >/dev/null
# Also check the satisfiability of the degeneralized formula # Also check the satisfiability of the degeneralized formula
run 0 ../ltl2tgba -e -D -x -f "$1" >/dev/null $run ../ltl2tgba -e -D -x -f "$1" >/dev/null
run 0 ../ltl2tgba -e -DS -x -f "$1" >/dev/null $run ../ltl2tgba -e -DS -x -f "$1" >/dev/null
} }
# Kristin Y. Rozier reported that the formulae with n=10 were badly # Kristin Y. Rozier reported that the formulae with n=10 were badly
@ -59,4 +61,10 @@ do
check_formula "$f" check_formula "$f"
f=`"$lccl" $i` f=`"$lccl" $i`
check_formula "$f" check_formula "$f"
# Only run the first two formulae under valgrind,
# it is too slow otherwise.
if test $i = 2; then
run=:
fi
done done