Commit 1719287b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

-e means we expect an accepting run.

* iface/dve2/dve2check.cc: Reverse the value of
expect_counter_example with respect to the -e/-E options.
* iface/dve2/dve2check.test: Swap -e and -E.
parent 7aefc190
2011-07-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
-e means we expect an accepting run.
* iface/dve2/dve2check.cc: Reverse the value of
expect_counter_example with respect to the -e/-E options.
* iface/dve2/dve2check.test: Swap -e and -E.
2011-06-26 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-06-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add some "drop shadow" in ltl2tgba.html. Add some "drop shadow" in ltl2tgba.html.
......
...@@ -107,7 +107,7 @@ main(int argc, char **argv) ...@@ -107,7 +107,7 @@ main(int argc, char **argv)
if (!*echeck_algo) if (!*echeck_algo)
echeck_algo = "Cou99"; echeck_algo = "Cou99";
expect_counter_example = (*opt == 'E'); expect_counter_example = (*opt == 'e');
output = EmptinessCheck; output = EmptinessCheck;
break; break;
} }
......
...@@ -39,15 +39,15 @@ for opt in '' '-z'; do ...@@ -39,15 +39,15 @@ for opt in '' '-z'; do
# (Don't run the first one using "run 0" because it would take too much # (Don't run the first one using "run 0" because it would take too much
# time with valgrind.). # time with valgrind.).
../dve2check $opt -e $srcdir/beem-peterson.4.dve \ ../dve2check $opt -E $srcdir/beem-peterson.4.dve \
'!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
run 0 ../dve2check $opt -E $srcdir/beem-peterson.4.dve \ run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
'!G(P_0.wait -> F P_0.CS)' > stdout1 '!G(P_0.wait -> F P_0.CS)' > stdout1
# same formula, different syntax. # same formula, different syntax.
run 0 ../dve2check $opt -E $srcdir/beem-peterson.4.dve \ run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
'!G("P_0 == wait" -> F "P_0 == CS")' > stdout2 '!G("P_0 == wait" -> F "P_0 == CS")' > stdout2
cmp stdout1 stdout2 cmp stdout1 stdout2
run 0 ../dve2check $opt -E $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
done done
# Now check some error messages. # Now check some error messages.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment