Encyclopedia of Delay-Insensitive Systems (EDIS)

Context Conditions for XDI Specifications in AND/IF

• Mandatory practices are phrased with the verbs ``shall/must''. Failure to adhere is reported as an error.
• Recommended practices are phrased with the verb ``should''. Failure to adhere is reported as a warning,
• Guidelines are phrased wiht the verb ``may''. Failure to adhere is not reported.

1. The NFA description should contain the option clause

   (INTERPRETATION Verhoeff/XDI)
   

   There should be no option clauses in terms of private lists.

2. Each symbol shall be declared with exactly one of the properties INPUT or OUTPUT. The symbol properties INOUT and EPSILON shall not be used. There should be no symbols with a private type as property.

3. Exactly one state shall be declared with the 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 TOP, TRANSIENT, BOX, DEMANDING, or BOTTOM.

   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 TOP or BOTTOM, it shall be the only state in the NFA and, hence, also have the property INITIAL. 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.

4. There should be no transitions with a private type as propertys.

5. The NFA shall be a deterministic (sometimes also called unambiguous) finite automaton. That is, for every state, its outgoing transitions must be labeled by distinct symbols.

   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

   • the (implicit) TOP state if q has property TOP, or if the symbol has property OUTPUT and q has not property BOTTOM,
   • the (implicit) BOTTOM state, if q has property BOTTOM, or if the symbol has property INPUT and q has not property TOP.

6. Every state shall be reachable, via transitions, from the initial state.

7. Each transient state shall have at least one outgoing output transition. Each demanding state shall have at least one outgoing input transition.

8. The NFA should be minimal, that is, for every pair of distinct states p and q, there exists a trace (see above) t such that the properties of the (possibly implicit) states p' and q', reached via t from p and q respectively, differ.

9. The NFA shall satisfy the Extended JTU Rules capturing delay-insensitivity.

A test suite for XDI specifications written in AND/IF is available to illustrate the rules.