From 9c922252a66acff5935e2190333a52a2a63289a3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 21 Aug 2015 10:51:29 +0200 Subject: [PATCH] * src/tests/ltl2dstar.test: Fix for recent change to ltlcross. --- src/tests/ltl2dstar.test | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/tests/ltl2dstar.test b/src/tests/ltl2dstar.test index 08e8cd93d..75cf7225c 100755 --- a/src/tests/ltl2dstar.test +++ b/src/tests/ltl2dstar.test @@ -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