From 1d30242d17b6bb3ad17252da76d5c498170644d1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 17 Oct 2015 17:38:45 +0200 Subject: [PATCH] remove_fin: fix bug in remove_fin_det_weak * wrap/python/tests/remfin.py: New file. * wrap/python/tests/Makefile.am: Add it. * src/twaalgos/remfin.cc (remove_fin_det_weak): Purge dead states. --- src/twaalgos/remfin.cc | 1 + wrap/python/tests/Makefile.am | 1 + wrap/python/tests/remfin.py | 37 +++++++++++++++++++++++++++++++++++ 3 files changed, 39 insertions(+) create mode 100644 wrap/python/tests/remfin.py 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--""")