Test suite for XDI specifications in AND/IF

Each of the following files *.ndf contains one syntactically correct AND/IF 1.0 specification. However, each file *.ndf illustrates some (potential) violation of the rules for XDI specifications. The output of xdi-analyze for file x.ndf is provided in file x.anl.
  1. no-interpretation.ndf (Uninterpreted Wire): this specification has no interpretation clause.
    no-interpretation.anl (output of xdi-analyze): reported as warning.

    double.ndf (Wire and I-Wire): two automata in one AND/IF expression
    double.anl (output of xdi-analyze): reported as warning; only the first NFA section is used.

  2. no-property-symbols.ndf (Wire with undirected symbols): symbols a and b are declared without (direction) property.
    no-property-symbols.anl (output of xdi-analyze): reported as warning; such symbols get property INPUT.

    multi-property-symbols.ndf (Wire with inconsistently directed symbols): symbols a is declared with properties INPUT and OUTPUT.
    multi-property-symbols.anl (output of xdi-analyze): reported as warning; such symbols get property INPUT.

  3. no-initial-state.ndf (Wire without intial state): no state has property INITIAL.
    no-initial-state.anl (output of xdi-analyze): reported as error.

    two-initial-states.ndf (Wire with two initial states): states 0 and 1 have property INITIAL.
    two-initial-states.anl (output of xdi-analyze): reported as warning; only the first INITIAL state is used as such.

    final-state.ndf (Wire with a final state): state 1 has property FINAL.
    final-state.anl (output of xdi-analyze): not reported; property FINAL is ignored.

    no-property-states.ndf (Wire with unlabeled states): state 1 is declared without property.
    no-property-states.anl (output of xdi-analyze): reported as warning; such states get property BOX.

    multi-property-states.ndf (Wire with inconsistently labeled state): state 1 is declared with properities TRANSIENT and BOX.
    multi-property-states.anl (output of xdi-analyze): reported as warning; such states get the `least' of all given properties (BOTTOM < DEMANDING < BOX < TRANSIENT < TOP).

  4. No test cases for transition properties.

  5. ambiguous.ndf (Ambiguous Wire): in state 0 there are two outgoing transitions labeled a.
    ambiguous.anl (output of xdi-analyze): reported as error.

  6. unreachable.ndf (Unreachable): state 2 is not reachable from the initial state.
    unreachable.anl (output of xdi-analyze): all unreachable states are reported (under `Shortest paths from initial state').

  7. inconsistent.ndf (Inconsistent): state 2 is transient and has no outgoing output transition.
    inconsistent.anl (output of xdi-analyze): reported as warning; state property changed to BOX.

  8. non-minimal-wire.ndf (Non-Minimal Wire): state graph not minimal: states 0 and 2 are indistinguishable, as are states 1 and 3.
    non-minimal-wire.anl (output of xdi-analyze): pairs of indistinguishable states are reported (at the end).

  9. stutter.ndf (Stutter-Wire): Rule W is violated, because each a-input is followed by two b-outputs.
    stutter.anl (output of xdi-analyze): reported as violation of Rule W.

    non-X.ndf (Non-X): Rule X is violated in state 0, because ab is a process trace and ba is not.
    non-X.anl (output of xdi-analyze): reported as violation of Rule NS (Neighbor-Swap, which generalizes Rule X).

    non-Y.ndf (Non-Y): Rule Y is violated in state 0, because ab and bac are process traces and abc is not.
    non-Y.anl (output of xdi-analyze): reported as violation of Rule NS (Neighbor-Swap, which generalizes Rule Y).

    non-Z.ndf (Non-Z): Rule Z is violated in state 0, because ab and b are process traces and ba is not.
    non-Z.anl (output of xdi-analyze): reported as violation of Rule NS (Neighbor-Swap, which generalizes Rule Z).

AND/IF errors handled differently: