simplify_acc: loop over the simplifications

* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Run the
simplifications in a loop until the condition does not change anymore.
* tests/python/simplacc.py, tests/core/accsimpl.test,
tests/core/remfin.test, tests/python/merge.py,
tests/python/simplacc.py, tests/python/toparity.py: Update expected
results.
* tests/python/automata.ipynb: Update the failing example to a more
interesting one, matching the one in doc/org/autfilt.org.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-16 22:53:09 +02:00
parent b62e1bb13c
commit 102ef04364
7 changed files with 1516 additions and 1209 deletions

View file

@ -57,23 +57,28 @@ for a in auts:
b = spot.simplify_acceptance(a)
assert b.equivalent_to(a)
res.append(str(b.get_acceptance()))
c = spot.simplify_acceptance(b)
assert b.get_acceptance() == c.get_acceptance()
a.set_acceptance(a.num_sets(), a.get_acceptance().complement())
b = spot.simplify_acceptance(a)
assert b.equivalent_to(a)
res.append(str(b.get_acceptance()))
c = spot.simplify_acceptance(b)
assert b.get_acceptance() == c.get_acceptance()
assert res == [
'Inf(0)',
'Fin(0)',
'Inf(1) & Fin(0)',
'Fin(0) & Inf(1)',
'Fin(1) | Inf(0)',
'Inf(1) & (Fin(0) | Inf(2))',
'(Fin(0) | Inf(2)) & Inf(1)',
'Fin(1) | (Fin(2) & Inf(0))',
'(Fin(1) | Inf(2)) & Inf(0)',
'Fin(0) | (Fin(2) & Inf(1))',
'((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4))))',
'(Fin(5) | (Fin(2) & Inf(1))) & (Inf(0) | ((Fin(4) | Inf(3)) & Inf(1)))',
'Inf(1) | Inf(0)',
'Fin(1) & Fin(0)',
'Inf(0)',
'Fin(0)',
]