transparent diamond, normalise

MESSAGES = {0}
NODENAMES = {0,1,2}
N = 3

LIMIT = 2
LIMIT1 = 3

channel in : NODENAMES.MESSAGES
channel out, ring : NODENAMES.NODENAMES.MESSAGES

M0(i) =     STOP 
	|~| (
	   in.i?x -> M1(i,i,x)
        [] ring.i?j?x -> (if (j==i) then M0(i) 
        		  else (out.i.j!x -> M1(i,j,x))))
        
M1(i,j,x) =    ring.((i+1)%N)!j.x -> M0(i)
	    [] ring.i?k?y -> (if (k==i) then M1(i,j,x)
	    		      else out.i.k!y -> ring.((i+1)%N)!j.x -> M1(i,k,y))
	    		     

P0(i,e) =    STOP 
	  |~| (
	     in.i?x -> P1(i,i,x, e)
          [] ring.i?j?x -> (if (j==i) then P0(i,e) 
          		    else out.i.j!x -> P1(i,j,x,e)))
        
P1(i,j,x,e) =    ring.((i+1)%N)!j.x -> P0(i,e)
	      [] ring.i?k?y -> (if (k==i) then P1(i,j,x,e)
	    		        else out.i.k!y -> ring.((i+1)%N)!j.x 
	    		             -> P1(i,k,y,e))
	    		             
Q0(i,e) =    STOP 
	  |~| (
	     in.i?x -> Q1(i,i,x, e+1)
          [] ring.i?j?x -> (if (j==i) then Q0(i,e-1) 
          		    else out.i.j!x -> Q1(i,j,x,e)))
        
Q1(i,j,x,e) =    ring.((i+1)%N)!j.x -> Q0(i,e)
	      [] ring.i?k?y -> (if (k==i) then Q1(i,j,x,e-1)
	    		        else out.i.k!y -> ring.((i+1)%N)!j.x 
	    		             -> Q1(i,k,y,e))


N0(i,e) =    STOP 
	  |~| (
	     (e<LIMIT) & (in.i?x -> N1(i,i,x, e+1))
          [] (true) & ring.i?j?x -> (if (j==i) 
          			     then (if (0<e) then N0(i,e-1) else STOP)
          		             else out.i.j!x -> N1(i,j,x,e)))
        
N1(i,j,x,e) =    ring.((i+1)%N)!j.x -> N0(i,e)
	      [] ring.i?k?y -> (if (k==i) then (if 0<e then N1(i,j,x,e-1)
	      					else STOP)
	    		        else out.i.k!y -> ring.((i+1)%N)!j.x 
	    		             -> N1(i,k,y,e))


NN0(i,e) =    STOP
	  |~| (
	     (e<LIMIT1) & (in.i?x -> NN1(i,i,x, e+1))
          [] ring.i?j?x -> (if (j==i) then (if 0<e then NN0(i,e-1) else STOP)
          		    else out.i.j!x -> NN1(i,j,x,e)))
        
NN1(i,j,x,e) =    ring.((i+1)%N)!j.x -> NN0(i,e)
	      [] ring.i?k?y -> (if (k==i) then (if 0<e then NN1(i,j,x,e-1)
	      					else STOP)
	    		        else out.i.k!y -> ring.((i+1)%N)!j.x 
	    		             -> NN1(i,k,y,e))
	    		             	    		             	    		             	    		             
M = (normalise(diamond((M0(0) [|{|ring.1|}|] M0(1)) \ {|ring.1|}))
      [|{|ring.2,ring.0|}|]
      M0(2))
     \ {|ring.2,ring.0|}
     
P = (normalise(diamond((P0(0,0) [|{|ring.1|}|] P0(1,0)) \ {|ring.1|}))
      [|{|ring.2,ring.0|}|]
      P0(2,0))
     \ {|ring.2,ring.0|}
     
Q = (normalise(diamond((Q0(0,0) [|{|ring.1|}|] Q0(1,0)) \ {|ring.1|}))
      [|{|ring.2,ring.0|}|]
      Q0(2,0))
     \ {|ring.2,ring.0|}

NN = (normalise(diamond((NN0(0,0) [|{|ring.1|}|] NN0(1,0)) \ {|ring.1|}))
      [|{|ring.2,ring.0|}|]
      NN0(2,0))
     \ {|ring.2,ring.0|}
     
RING = (normalise(diamond((N0(0,0) [|{|ring.1|}|] N0(1,0)) \ {|ring.1|}))
      [|{|ring.2,ring.0|}|]
      N0(2,0))
     \ {|ring.2,ring.0|}
     

assert M [FD= P
assert P [FD= NN
assert NN [FD= RING