terminal property

[adl]

We have weak and inherently weak (#22). When discussing with Joachim it seems it would make sense to have something like terminal. All guarantee properties can be expressed by terminal automata. A terminal automaton is an automaton in which all accepting states are true self-loops with no other successor. In practice all these states can be merged into one, so an efficient way to represent the accepting set of such an automaton in memory is just to store the number of the accepting state. If you check a (non-blocking) system against a terminal automaton, you can stop the verification as soon as you hit an accepting state.

It's not clear to me whether we should also have inherently terminal: i.e., a weak automaton in which all accepting SCCs are "complete" (in the sense that they accept any word from any state). This would be consistent with weak/inherently weak, but is there any point?

[xblahoud]

If I understand it correctly, the suggestion is to add possibility to use property: terminal (or weak terminal). I see the arguments as solid and the knowledge whether the automaton is terminal as useful.

[strejcek]

Added.