State-based versus transition-based acceptance

The format currently allow both states and transitions to be put into acceptance sets, and those acceptance sets can be complemented in the acceptance condition.

We need to make the semantics crystal clear as one may wonder what is the complement of a set that contains states and transitions...

The mathematical view is that we have only acceptance sets of transitions.  We then pretend that a state belongs to the acceptance set S iff all its outgoing transitions belong to S.  In this view, the syntax

    State: 1 {2}
      [0] 2
      [!0] 1

is just syntactic sugar for

    State: 1
      [0] 2 {2}
      [!0] 1 {2}

When a complement is considered in the acceptance conditions, it is with respect to all the transitions.  However since if the automaton is only using state-based acceptance, it would be equivalent to make to complement with respect to the states.


We should probably also mention that our support for a mix of state-based or transition-based acceptance is inspired from [the format of LBTT][LBTT format].


  [LBTT format]: http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html "LBTT format for automata"