The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
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?)