is_terminal, acceptance marks on transiant transitions, and terminal co-Büchi automata
It seems our definition of terminal automata is incorrect, as it allows transiant transitions to be accepting. A proper definition should be that an automaton is terminal if it accept any word that has a prefix passing through an accepting transition.
Our implementation of
is_terminal should be fixed, as well as the various definitions of terminal automata. I think the definition of the HOA format is wrong as well.
Also I would like to see a test case calling
is_terminal on a terminal co-Büchi automaton, and I'm wondering what
scc_filter do on such automata.