N = 3
DATA = {0}
NODES = {0,1,2}

channel out : NODES.NODES.DATA
channel in : NODES.DATA
channel ring : NODES.NODES.DATA
LIMIT = 3

SYS = ((NODE(0) [| {|ring.1|} |] NODE(1)) 
      [| {| ring.0,ring.2|} |] NODE(2)) \ {| ring |}

NODE(i) = (in.i?x -> NODE_1(i,i,x)
           []
	   ring.i?j.x ->
	      (if (i==j) then NODE(i) else (out.i.j.x -> NODE_1(i,j,x)))
	  )
	  |~| STOP

NODE_1(i,j,x) = ring.(i+1)%N!j.x -> NODE(i)
		[]
		ring.i?k.y ->
		    (if (k==i) then NODE_1(i,j,x)
		     else (out.i.k.y -> ring.(i+1)%N!j.x -> NODE_1(i,k,y)))

-- In the following the condition (s>0) is new introduced,
-- and the internal choice is removed.
-- -------------------------------------------------------
NODE3(i,s) = (if (s<LIMIT) then in.i?x -> NODE3_1(i,i,x,s+1)
	      else STOP
           []
	   ring.i?j.x ->
	      (if (i==j) then (if (s>0) then NODE3(i,s-1) else STOP)
	       else (out.i.j.x -> NODE3_1(i,j,x,s)))
	  )
	  -- |~| STOP

NODE3_1(i,j,x,s) = ring.(i+1)%N!j.x -> NODE3(i,s)
		[]
		ring.i?k.y ->
		    (if (k==i) then (if (s>0) then NODE3_1(i,j,x,s-1) else STOP)
		     else (out.i.k!y -> ring.(i+1)%N!j.x 
			   -> NODE3_1(i,k,y,s)))

SYS3 = ((NODE3(0,0) [| {|ring.1|} |] NODE3(1,0)) 
      [| {| ring.0,ring.2|} |] NODE3(2,0)) \ {| ring |}

NODE2(i,s) = (if (s<2) then in.i?x -> NODE2_1(i,i,x,s+1)
	      else STOP
           []
	   ring.i?j.x ->
	      (if (i==j) then (if (s>0) then NODE2(i,s-1) else STOP)
	       else (out.i.j.x -> NODE2_1(i,j,x,s)))
	  )
	  -- |~| STOP

NODE2_1(i,j,x,s) = ring.(i+1)%N!j.x -> NODE2(i,s)
		[]
		ring.i?k.y ->
		    (if (k==i) then (if (s>0) then NODE2_1(i,j,x,s-1) else STOP)
		     else (out.i.k!y -> ring.(i+1)%N!j.x 
			   -> NODE2_1(i,k,y,s)))

SYS2 = ((NODE2(0,0) [| {|ring.1|} |] NODE2(1,0)) 
      [| {| ring.0,ring.2|} |] NODE2(2,0)) \ {| ring |}


assert SYS2 :[deadlock free]
assert SYS3 :[deadlock free]
-- SYS2 is not a traces refinement of SYS3, why?
assert SYS3 [T= SYS2