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.