XDI analysis of MutualExclusion Element
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity
Processing AND/IF input stream:

1> (AND/IF_1.0
2> (NFA
3> (NAME MutualExclusion Element)
4> (SYMBOLS
5> (r0 INPUT) (a0 OUTPUT) (r1 INPUT) (a1 OUTPUT)
6> )
7>
8> (STATES
9> (0 INITIAL BOX)
10> (1 TRANSIENT)
11> (4 TRANSIENT)
12> (2 BOX)
13> (5 TRANSIENT)
14> (3 TRANSIENT)
15> (6 BOX)
16> (7 TRANSIENT)
17> (8 BOX)
18> (9 BOX)
19> (10 TRANSIENT)
20> (11 TRANSIENT)
21> (12 TRANSIENT)
22> (14 TRANSIENT)
23> (13 TRANSIENT)
24> )
25> (TRANSITIONS
26> (0 1 r0) (0 4 r1)
27> (1 2 a0) (1 5 r1)
28> (4 5 r0) (4 8 a1)
29> (2 3 r0) (2 6 r1)
30> (5 6 a0) (5 9 a1)
31> (3 0 a0) (3 7 r1)
32> (6 7 r0)
33> (7 4 a0) (7 10 a1)
34> (8 9 r0) (8 11 r1)
35> (9 12 r1)
36> (10 8 a0) (10 14 r1)
37> (11 12 r0) (11 0 a1)
38> (12 13 a0) (12 1 a1)
39> (14 11 a0) (14 3 a1)
40> (13 14 r0) (13 2 a1)
41> )
42> )
43> )

MutualExclusion Element: warning: interpretation not given. Assuming 'Verhoeff/XDI'
MutualExclusion Element: 1 warning, 0 errors.

 4 symbols:
 2 input and 2 output
 15 states:
 0 demanding, 5 indifferent and 10 transient
 28 transitions:
 14 input and 14 output
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity

There are 2 automorphisms.
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity

/ r0 a0 / r1 a1 /
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity
 Maximally Transient
 No Disabling Inputs (Z^{inp})
 Disabling outputs (Z^{out}) in state(s):
 5
 OrderIndependent input (Y^{inp})
 OrderIndependent output (Y^{out})
 Output refusal sets do NOT propagate backward over inputs in state(s):
 1 4
 Output NonDeterministic
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity
 All states are reachable from the initial state:
[ + == 9 < distance < +inf , . == distance = +inf ]
           1  1  1  1  1 
 0  1  4  2  5  3  6  7  8  9  0  1  2  4  3 
0:  0  1  1  2  2  3  3  4  2  3  5  3  4  6  5 
Initial state reachable from all states.
All states reachable from all other states.
 Shortest paths from initial state:

0:  
1:  r0 
4:  r1 
2:  r0 a0 
5:  r0 r1 
3:  r0 a0 r0 
6:  r0 a0 r1 
7:  r0 a0 r0 r1 
8:  r1 a1 
9:  r0 r1 a1 
10:  r0 a0 r0 r1 a1 
11:  r1 a1 r1 
12:  r0 r1 a1 r1 
14:  r0 a0 r0 r1 a1 r1 
13:  r0 r1 a1 r1 a0 
 Distribution of distances from initial state:
[d=distance, h=occurrence count, c=cumulative occurrence count] 
d:  h  [ c] 
0:  1  [ 1] 
1:  2  [ 3] 
2:  3  [ 6] 
3:  4  [10] 
4:  2  [12] 
5:  2  [14] 
6:  1  [15] 
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity

There are no state pairs (x,y) where x refines y outside the diagonal.
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity

'MutualExclusion Element' is a valid XDI specification.
Top  Statistics  Automorphisms  Finest Semiindependent Partition  Choice, Order Dependence, Nondeterminism  Distances  Autocomparison  XDI Validity
XDI State Graph Tool, Version 2.0 (Feb 17 1998 20:34:43)
Copyright © 19951997 Eindhoven University of Technology