suboptimal behaviour of simplify_acceptance()
Consider the automaton
HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
Acceptance: 5 (Fin(0) & Fin(3)) & (Fin(1)|Fin(2)|Fin(4))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!0&!1] 0 {0 1 4}
[0&1] 1 {0 2 3}
State: 1
[0&1] 0 {0 2 3}
[0&1] 1 {1}
--END--I'm not sure what is going on with the following simplifications.
Since colors 2 & 3 are identical, I would expect the original condition to be reduced to (Fin(0) & Fin(2)) & (Fin(1)|Fin(2)|Fin(4)) then unit-propagation should reduce this to Fin(0)&Fin(2) and fusing of Fin-conjuncts should simplify this to Fin(1) while adjusting the automaton.
It's not clear to me what rules allow to simplify (Fin(0) & Fin(3)) & (Fin(1)|Fin(2)|Fin(4)) to (Fin(0) & (Fin(1)|Fin(2)|Fin(4)). It this because 3 and 2 are complementary? (Would that be a valid reduction?)