(INTERPRETATION Verhoeff/XDI)There should be no option clauses in terms of private lists.
OUTPUT. The symbol properties
EPSILONshall not be used. There should be no symbols with a private type as property.
INITIAL. Thus, we can speak of the initial state of the NFA.
The state property
FINAL should not be used.
Each state shall be declared with exactly one of the properties
There should be no states with a private type as property.
Thus, exactly one state is declared with two properties, viz. the initial state.
If a state has property
it shall be the only state in the NFA and,
hence, also have the property
Furthermore, in such a case, there shall be no transitions declared.
A state may be declared with the same name as a symbol. Guideline: It is recommended that the set of symbol names and the set of state names are disjoint.
Thus, a path, along the transitions, can be uniquely described by giving its starting state and the sequence of symbols on the traversed transitions. That symbol sequence is called the trace of the path.
Conversely, given a state p and a trace t, at most one path can be traversed from p by following the transitions labeled by the symbols in t, in order of appearance. If intermediately a state q is reached and the corresponding symbol a in the trace does not match any of the outgoing transitions of that state q, then the next state is taken to be
A test suite for XDI specifications written in AND/IF is available to illustrate the rules.