Commit 1d30242d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 9be0cd7f
......@@ -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
......
......@@ -51,6 +51,7 @@ TESTS = \
randgen.py \
randltl.ipynb \
relabel.py \
remfin.py \
setxor.py \
testingaut.ipynb
......
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--""")
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment