diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc index de7ced8be..e65ad92b2 100644 --- a/src/twaalgos/remfin.cc +++ b/src/twaalgos/remfin.cc @@ -462,6 +462,7 @@ namespace spot true, // determinisitic true, // stutter inv. }); + res->purge_dead_states(); scc_info si(res); // We will modify res in place, and the resulting diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 3f5c6442a..905b639d3 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -51,6 +51,7 @@ TESTS = \ randgen.py \ randltl.ipynb \ relabel.py \ + remfin.py \ setxor.py \ testingaut.ipynb diff --git a/wrap/python/tests/remfin.py b/wrap/python/tests/remfin.py new file mode 100644 index 000000000..00ee84042 --- /dev/null +++ b/wrap/python/tests/remfin.py @@ -0,0 +1,37 @@ +import spot + +# This test used to trigger an assertion (or a segfault) +# in scc_filter_states(). +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 1 +AP: 1 "a" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 {0} +[t] 0 +State: 1 +[!0] 0 +[0] 2 +State: 2 +[t] 2 +--END-- +""") +aut.prop_inherently_weak() +aut = spot.dtwa_complement(aut) +aut = spot.scc_filter_states(aut) +assert(aut.to_str('hoa') == """HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: inherently-weak +--BODY-- +State: 0 +[0] 1 +State: 1 +[t] 1 +--END--""")