diff --git a/ChangeLog b/ChangeLog index 723c4665f..15ea3a63b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-07-26 Alexandre Duret-Lutz + + -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 Add some "drop shadow" in ltl2tgba.html. diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index f7512d957..c47a191b4 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -107,7 +107,7 @@ main(int argc, char **argv) if (!*echeck_algo) echeck_algo = "Cou99"; - expect_counter_example = (*opt == 'E'); + expect_counter_example = (*opt == 'e'); output = EmptinessCheck; break; } diff --git a/iface/dve2/dve2check.test b/iface/dve2/dve2check.test index 036f8e965..50aabaf06 100755 --- a/iface/dve2/dve2check.test +++ b/iface/dve2/dve2check.test @@ -39,15 +39,15 @@ for opt in '' '-z'; do # (Don't run the first one using "run 0" because it would take too much # 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)' - 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 # 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 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 # Now check some error messages.