XDI analysis of RGD Arbiter

Processing AND/IF input stream:
-----------------------------------------------------------------------------
  2> (AND/IF_1.0
  3> (NFA 
  4>      (NAME  RGD Arbiter)
  5>      (INTERPRETATION Verhoeff/XDI)
  6>      (NOTE Generated by digg v1.0)
  7>      (SYMBOLS 
  8>               (r0 INPUT)
  9>               (d0 INPUT)
 10>               (r1 INPUT)
 11>               (d1 INPUT)
 12>               (g0 OUTPUT)
 13>               (g1 OUTPUT)
 14>      )
 15>      (STATES 
 16>         (0 BOX INITIAL)
 17>         (1 TRANSIENT)
 18>         (2 TRANSIENT)
 19>         (3 TRANSIENT)
 20>         (4 BOX)
 21>         (5 BOX)
 22>         (6 BOX)
 23>         (7 BOX)
 24>         (8 BOX)
 25>         (9 BOX)
 26>         (10 BOX)
 27>         (11 BOX)
 28>      )
 29>      (TRANSITIONS
 30>          (0 1 r0)
 31>          (0 2 r1)
 32>          (1 3 r1)
 33>          (1 9 g0)
 34>          (2 3 r0)
 35>          (2 4 g1)
 36>          (3 7 g0)
 37>          (3 5 g1)
 38>          (4 5 r0)
 39>          (4 6 r1)
 40>          (4 0 d1)
 41>          (5 8 r1)
 42>          (5 1 d1)
 43>          (6 8 r0)
 44>          (6 2 d1)
 45>          (7 11 r0)
 46>          (7 2 d0)
 47>          (8 3 d1)
 48>          (9 10 r0)
 49>          (9 0 d0)
 50>          (9 7 r1)
 51>          (10 1 d0)
 52>          (10 11 r1)
 53>          (11 3 d0)
 54>      )
 55> ))
-----------------------------------------------------------------------------

Statistics

6 symbols:

4 input and 2 output

12 states:

0 demanding, 9 indifferent and 3 transient

24 transitions:

20 input and 4 output

Automorphisms (symmetries)

0:	r0	d0	r1	d1	g0	g1
0:	r1	d1	r0	d0	g1	g0

Finest Semi-independent Partition

/ r0 d0 g0 / r1 d1 g1 /

Choice, Order Dependence, Nondeterminism

• Maximally Transient
• No Disabling Inputs (Z^inp)
• Disabling outputs (Z^out) in state(s):

  3

• Order-Independent input (Y^inp)
• Order-Independent output (Y^out)
• Output refusal sets do NOT propagate backward over inputs in state(s):

  1 2

• Output Non-Deterministic

Distances

All states are reachable from the initial state:
[ + == 9 < distance < +inf , . == distance = +inf ]

											1	1
	0	1	2	3	4	5	6	7	8	9	0	1
0:	0	1	1	2	2	3	3	3	4	2	3	4

Initial state reachable from all states.
All states reachable from all other states.

Shortest paths from initial state:

0:
1:	r0
2:	r1
3:	r0 r1
4:	r1 g1
5:	r0 r1 g1
6:	r1 g1 r1
7:	r0 r1 g0
8:	r0 r1 g1 r1
9:	r0 g0
10:	r0 g0 r0
11:	r0 r1 g0 r0

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]

Autocomparison Matrix

There are no state pairs (x,y) where x refines y outside the diagonal.

XDI Validity

'RGD Arbiter' is a valid XDI specification.