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

Fixup minimize_monitor().

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2011-01-28 12:11:20 +01:00
parent dd0f01fe03
commit ad93f87591
3 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-01-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2011-01-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Report formulas that are both safety and guarantee. Report formulas that are both safety and guarantee.

2
src/tgbaalgos/minimize.cc
View file

@ -504,7 +504,7 @@ namespace spot
// non_final contain all states. // non_final contain all states.
// final is empty: there is no acceptance condition // 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); return minimize_dfa(det_a, final, non_final);
} }

8
src/tgbatest/ltl2tgba.test
View file

@ -104,3 +104,11 @@ grep 'states: 5$' stdout
../ltl2tgba -ks -Rm -f "$f" > stdout ../ltl2tgba -ks -Rm -f "$f" > stdout
grep 'transitions: 0$' stdout grep 'transitions: 0$' stdout
grep 'states: 1$' 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 <<EOF
0 -> 1
1 -> 1 [label="1\n"]
EOF
cmp stdout expected