From ad93f875912b03eeb98ad831e0b4ed59450dc45a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 28 Jan 2011 12:11:20 +0100 Subject: [PATCH] Fixup minimize_monitor(). * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding incorrect monitor if the input tgba is not deterministic. * src/tgbatest/ltl2tgba.test: Add test case. --- ChangeLog | 8 ++++++++ src/tgbaalgos/minimize.cc | 2 +- src/tgbatest/ltl2tgba.test | 8 ++++++++ 3 files changed, 17 insertions(+), 1 deletion(-) diff --git a/ChangeLog b/ChangeLog index 44856bfe9..9eca3324c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-01-28 Alexandre Duret-Lutz + + Fixup minimize_monitor(). + + * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding + incorrect monitor if the input tgba is not deterministic. + * src/tgbatest/ltl2tgba.test: Add test case. + 2011-01-27 Alexandre Duret-Lutz Report formulas that are both safety and guarantee. diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 8d97dc8dd..5ba3c1c14 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -504,7 +504,7 @@ namespace spot // non_final contain all states. // final is empty: there is no acceptance condition - state_set(a, non_final); + state_set(det_a, non_final); return minimize_dfa(det_a, final, non_final); } diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 1b9f8e027..682455559 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -104,3 +104,11 @@ grep 'states: 5$' stdout ../ltl2tgba -ks -Rm -f "$f" > stdout grep 'transitions: 0$' stdout grep 'states: 1$' stdout + +# Make sure a monitor for F(a & F(b)) accepts everything. +run 0 ../ltl2tgba -ks -f "$f" | grep ' ->' > stdout +cat >expected < 1 + 1 -> 1 [label="1\n"] +EOF +cmp stdout expected