Bug in `spot::dualize()`
The dual of an automaton A should recognize the complement of the language of A.
This is not case on the following simple deterministic parity automaton, built from the LTL formula FGa
.
The word (! a)^w is not recognized by the automaton, nor by its dual.
HOA: v1 States: 2 Start: 0 AP: 1 "a" acc-name: Rabin 1 Acceptance: 2 Fin(0) & Inf(1) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 [0] 1 {1} [!0] 0 State: 1 [0] 1 {1} [!0] 0 {0} --END--