Closed vkhomenko closed 5 years ago
This is addressed by the last example among nondeterministic automata where we explicitly allow this and specify this as union of the marks.
I'm added a not above this in the aforementioned paragraph.
I've just fixed an old typo in the paragraph...
The documentation says:
The INT* used in acc-sig represent the acceptance sets the state or edge belongs to. Since we use transition-based acceptance, when acc-sig is used on a state to declare membership to some acceptance sets, it is syntactic sugar for the membership of all the outgoing transitions to this set. For instance State: 0 {1 3} would states that all transitions leaving state 0 are in acceptance sets 1 and 3.
It is not clear whether acc-sig can be specified on both the state and some of its exit arcs. There are several possibilities: