EDIS: Guide | FAQ | New | Search | Bibliography | Index | Feedback
[EDIS Logo]

Encyclopedia of Delay-Insensitive Systems (EDIS)


Context Conditions for XDI Specifications in AND/IF

XDI specifications can be expressed in AND/IF. Besides the rules for AND/IF, some additional constraints must be satisfied.
  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

  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.


Encyclopedia of Delay-Insensitive Systems
Copyright © 1995-1997 Tom Verhoeff / Tom.Verhoeff@acm.org
Disclaimer