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.