XDI comparison of Uninitialized Non-Receptive 1-Bit Variable and VAR

Processing AND/IF input stream:
-----------------------------------------------------------------------------
  1> (AND/IF_1.0
  2>   (NFA
  3>     (NAME Uninitialized Non-Receptive 1-Bit Variable)
  4>     (SYMBOLS 
  5>       (w0 INPUT) (w1 INPUT) (a OUTPUT) (r INPUT)
  6>       (v0 OUTPUT) (v1 OUTPUT)
  7>     )
  8>     (STATES
  9>       (0 INITIAL BOX)
 10>       (2 TRANSIENT)
 11>       (5 TRANSIENT)
 12>       (1 TRANSIENT)
 13>       (3 BOX)
 14>       (6 BOX)
 15>       (4 TRANSIENT)
 16>       (7 TRANSIENT)
 17>     )
 18>     (TRANSITIONS
 19>       (0 2 w0) (0 5 w1) (0 1 r)
 20>       (2 3 a)
 21>       (5 6 a)
 22>       (1 3 v0) (1 6 v1)
 23>       (3 2 w0) (3 5 w1) (3 4 r)
 24>       (6 2 w0) (6 5 w1) (6 7 r)
 25>       (4 3 v0)
 26>       (7 6 v1)
 27>     )
 28>   )
 29> )
-----------------------------------------------------------------------------

Uninitialized Non-Receptive 1-Bit Variable: warning: interpretation not given. Assuming 'Verhoeff/XDI'
Uninitialized Non-Receptive 1-Bit Variable: 1 warning, 0 errors.

Processing AND/IF input stream:
-----------------------------------------------------------------------------
 11> (AND/IF_1.0
 12>   (NFA
 13>     (NOTE Generated by Verdect 2.3A)
 14>     (INTERPRETATION Ebergen/VERDECT)
 15>     (NAME VAR)
 16>     (SYMBOLS
 17>       (w0 INPUT)
 18>       (w1 INPUT)
 19>       (a OUTPUT)
 20>       (r INPUT)
 21>       (v0 OUTPUT)
 22>       (v1 OUTPUT)
 23>     )
 24>     (STATES
 25>       (0 INITIAL)
*** Line 25: XDI Warning: definition of state '0' has no (valid) progress properties. Assuming 'box' property
 26>       (1)
*** Line 26: XDI Warning: definition of state '1' has no (valid) progress properties. Assuming 'box' property
 27>       (2)
*** Line 27: XDI Warning: definition of state '2' has no (valid) progress properties. Assuming 'box' property
 28>       (3)
*** Line 28: XDI Warning: definition of state '3' has no (valid) progress properties. Assuming 'box' property
 29>       (4)
*** Line 29: XDI Warning: definition of state '4' has no (valid) progress properties. Assuming 'box' property
 30>       (5)
*** Line 30: XDI Warning: definition of state '5' has no (valid) progress properties. Assuming 'box' property
 31>       (6)
*** Line 31: XDI Warning: definition of state '6' has no (valid) progress properties. Assuming 'box' property
 32>       (7)
*** Line 32: XDI Warning: definition of state '7' has no (valid) progress properties. Assuming 'box' property
 33>     )
 34>     (TRANSITIONS
 35>       (0 1 r) (0 2 w1) (0 7 w0)
 36>       (1 3 v1) (1 4 v0)
 37>       (2 3 a)
 38>       (3 5 r) (3 2 w1) (3 7 w0)
 39>       (4 6 r) (4 2 w1) (4 7 w0)
 40>       (5 3 v1)
 41>       (6 4 v0)
 42>       (7 4 a)
 43>     )
 44>   )
 45> )
-----------------------------------------------------------------------------

AND/IF_1.0
  (NFA
    (NAME Uninitialized Non-Receptive 1-Bit Variable)
    (SYMBOLS 
      (w0 INPUT) (w1 INPUT) (a OUTPUT) (rVAR: warning: unknown interpretation 'Ebergen/VERDECT' ignored. Assuming 'Verhoeff/XDI'
VAR: 1 warning, 0 errors.

Alphabets

'Uninitialized Non-Receptive 1-Bit Variable' and 'VAR' have comparable alphabets

Joint Reachability

# reachable state pairs = 8
[ + == 9 < distance < +inf , . == distance = +inf ]

	0	1	2	3	4	5	6	7
0:	0	.	.	.	.	.	.	.
2:	.	.	.	.	.	.	.	1
5:	.	.	1	.	.	.	.	.
1:	.	1	.	.	.	.	.	.
3:	.	.	.	.	2	.	.	.
6:	.	.	.	2	.	.	.	.
4:	.	.	.	.	.	.	3	.
7:	.	.	.	.	.	3	.	.

Shortest distances and paths from initial pair

[(s,t)=state pair, d=distance, X\Y=not indiv. min., path=shortest path]

(s,t):	d,	X\Y,	path
(0,0):	0,	\ ,
(2,7):	1,	\ ,	w0
(5,2):	1,	\ ,	w1
(1,1):	1,	\ ,	r
(3,4):	2,	\ ,	w0 a
(6,3):	2,	\ ,	w1 a
(4,6):	3,	\ ,	w0 a r
(7,5):	3,	\ ,	w1 a r

Distribution of distances from initial pair

[d=distance, h=occurrence count, c=cumulative occurrence count]

d:	h	[c]
0:	1	[1]
1:	3	[4]
2:	2	[6]
3:	2	[8]

Comparison

'Uninitialized Non-Receptive 1-Bit Variable' refines 'VAR'.

Comparison Matrix:

	0	1	2	3	4	5	6	7
0:	.	.	.	2	2	.	.	.
2:	1	1	3	1	1	1	1	.
5:	1	1	.	1	1	1	1	3
1:	1	.	1	1	1	1	1	1
3:	.	.	.	2	.	.	.	.
6:	.	.	.	.	2	.	.	.
4:	1	.	1	1	1	1	.	1
7:	1	.	1	1	1	.	1	1

'Uninitialized Non-Receptive 1-Bit Variable' is NOT refined by 'VAR':

(1[],1\/)
(2[],5\/)
(5[],7\/)
(6[],4\/)
(7[],2\/)

Comparison Matrix:

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