XDI comparison of C and COUNTER3

Processing AND/IF input stream:
-----------------------------------------------------------------------------
  2> (AND/IF_1.0
  3> (NFA 
  4>      (NAME C)
  5>      (INTERPRETATION Verhoeff/XDI)
  6>      (NOTE Generated by digg v1.0)
  7>      (SYMBOLS 
  8>               (a INPUT)
  9>               (p OUTPUT)
 10>               (q OUTPUT)
 11>      )
 12>      (STATES 
 13>         (0 BOX INITIAL)
 14>         (1 TRANSIENT)
 15>         (2 BOX)
 16>         (3 TRANSIENT)
 17>         (4 BOX)
 18>         (5 TRANSIENT)
 19>      )
 20>      (TRANSITIONS
 21>          (0 1 a)
 22>          (1 2 p)
 23>          (2 3 a)
 24>          (3 4 p)
 25>          (4 5 a)
 26>          (5 0 q)
 27>      )
 28> ))
-----------------------------------------------------------------------------

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 COUNTER3)
 16>     (SYMBOLS
 17>       (a INPUT)
 18>       (p OUTPUT)
 19>       (q OUTPUT)
 20>     )
 21>     (STATES
 22>       (0 INITIAL)
*** Line 22: XDI Warning: definition of state '0' has no (valid) progress properties. Assuming 'box' property
 23>       (1)
*** Line 23: XDI Warning: definition of state '1' has no (valid) progress properties. Assuming 'box' property
 24>       (2)
*** Line 24: XDI Warning: definition of state '2' has no (valid) progress properties. Assuming 'box' property
 25>       (3)
*** Line 25: XDI Warning: definition of state '3' has no (valid) progress properties. Assuming 'box' property
 26>       (4)
*** Line 26: XDI Warning: definition of state '4' has no (valid) progress properties. Assuming 'box' property
 27>       (5)
*** Line 27: XDI Warning: definition of state '5' has no (valid) progress properties. Assuming 'box' property
 28>     )
 29>     (TRANSITIONS
 30>       (0 1 a)
 31>       (1 2 p)
 32>       (2 3 a)
 33>       (3 4 p)
 34>       (4 5 a)
 35>       (5 0 q)
 36>     )
 37>   )
 38> )
-----------------------------------------------------------------------------

(AND/IF_1.0 
(NFA 
     (NAME C)
     (INTERPRETATION Verhoeff/XDI)
     (NOTE Generated by digg v1.0)
     (SYMBOLS 
         COUNTER3: warning: unknown interpretation 'Ebergen/VERDECT' ignored. Assuming 'Verhoeff/XDI'
COUNTER3: 1 warning, 0 errors.

Alphabets

'C' and 'COUNTER3' have comparable alphabets

Joint Reachability

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

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

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,	\ ,
(1,1):	1,	\ ,	a
(2,2):	2,	\ ,	a p
(3,3):	3,	\ ,	a p a
(4,4):	4,	\ ,	a p a p
(5,5):	5,	\ ,	a p a p a

Distribution of distances from initial pair

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

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

Comparison

'C' refines 'COUNTER3'.

Comparison Matrix:

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

'C' is NOT refined by 'COUNTER3':

(1[],1\/)
(3[],3\/)
(5[],5\/)

Comparison Matrix:

	0	1	2	3	4	5
0:	1	1	1	1	1	1
1:	0	0	0	0	0	0
2:	1	1	1	1	1	1
3:	0	0	0	0	0	0
4:	1	1	1	1	1	1
5:	0	0	0	0	0	0