missed optimization in to_parity
Here is a case where to_parity()
produces a larger automaton than necessary, because it does not propagate colors before simplifying the acceptance condition.
(However systematically running propagate_marks_here()
before simplify_acceptance_here()
is also going to reveal some cases that are pessimized, for instance cases where two colors are complementary before propagation, but not after. So maybe the rules based on complementary marks in simplify_acceptance_here
need to be more flexible.)
HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
Acceptance: 5 ((Fin(1)|Fin(3)|Fin(4)) | Inf(2) | Inf(0)) & (Inf(0) | Inf(1)) & (Inf(2) | Inf(1))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0&1] 0 {1 3}
[!0&1] 1 {0}
State: 1
[0&1] 1 {2 3 4}
[!0&!1] 0 {1 2}
--END--