minimize_obligation and very-weak automata
Very-weak automata can be complemented by dualization and alternation_removal in O(2^n). So if minimize_obligation()
is called with a very-weak automaton and we don't have a formula or its negation, we should probably complement it ourself.
The following 4-state automaton would be reduced to 3 states if we did that in minimize_obligation()
.
HOA: v1 Start: 0 States: 4 Acceptance: 1 Inf(0)
AP: 2 "v0" "v1" --BODY-- State: 0 "T3_init" [t] 0 [!0 & !1] 1
State: 1 "T2" [0&1] 1 [0&1] 2 [!0&!1] 2 [0&1] 3 [!0&!1] 1
State: 2 "T1" {0} [0&1] 2 State: 3 "all" {0} [t] 3 --END--