Skip to content

to_weak_alternating() is bugged

This automaton (TGBA) is NOT equivalent to its "weakification" (Gen. co-Büchi). Note that the second one has 73 states and drawing it does not help...

The first one recognizes the word (!a\&b ; a\&!b ; !a\&!b)^\omega, while the second does not. One branch of the corresponding run is 0 \rightarrow 7 \rightarrow 65 \rightarrow 15 \rightarrow 31 \rightarrow 30 \rightarrow 25 \rightarrow 31 (loop). All states in the loop (31, 30, 25) are rejecting.

Edited by Maximilien Colange