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

* src/tests/ltl2dstar.test: Fix for recent change to ltlcross.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-08-21 10:51:29 +02:00
parent 60bd1400c3
commit 9c922252a6
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tests/ltl2dstar.test
View file

@ -58,17 +58,15 @@ $ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
--csv=out.csv
# A bug in ltlcross <=1.2.5 caused it to not use the complement of the
# negative automaton. So running ltlcross with GFa would check one
# complement (the positive one), but running with FGa would ignore
# the negative complement.
# negative automaton.
$ltlcross -f 'GFa' --verbose \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
test `grep -c 'info: check_empty.*Comp' err` = 1
test `grep -c 'info: check_empty.*Comp' err` = 2
$ltlcross -f 'FGa' --verbose \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
test `grep -c 'info: check_empty.*Comp' err` = 1
test `grep -c 'info: check_empty.*Comp' err` = 2
# Make sure ltldo preserve the Rabin acceptance by default