/* TOKEN RING SYSTEM */

defproc Exit(inCh,outCh) = 
	select {[outCh=inCh].0; outCh!(inCh).0};

defproc IdleNode(inCh,outCh) = 
	inCh?(newInCh).TokenOwner(newInCh,outCh) 

and TokenOwner(inCh,outCh) = 
        select { 
	     tau.Exit(inCh,outCh);
	     outCh!(outCh).IdleNode(inCh,outCh)};

defproc System = 
	(new l1,l2,l3,l4,l5 in 
	     (IdleNode(l1,l2) | 
	      IdleNode(l2,l3) |
	      IdleNode(l3,l4) | 
	      IdleNode(l4,l5) | 
	      TokenOwner(l5,l1)));

/* PROPERTIES */

check System |= always eventually 0;

/***/

defprop exiting(inl,outl) =
	1 and (((inl != outl) or <>0) and < outl!(inl) > 0);

defprop node(inl,outl) = 
	1 and
	(exiting(inl,outl) or 
	(maxfix X(inLnk).
		((< inLnk?(newInLnk) > X(newInLnk)) 
		or ((<> exiting(inLnk,outl)) 
		   and (< outl!(outl) > X(inLnk)))))
	(inl));

defprop ring = 
	0 or
	(hidden lnk. 
	(minfix Y(x).
		(node(x,lnk) or 
		(hidden y. (node(x,y) | Y(y)))))
	(lnk));

check System |= always ring;