Token Ring System

This simple example shows a system holding a set of nodes that communicate
in a token ring fashion, hence they are connected circularly and they are either
idle and waiting for the token or active while holding the token. Being active in
this case just means that they are able to exit the system or pass along the token.

The structure of the system is determined by the names that are shared between the
nodes, being these processes responsible for updating the links when they intend to
leave the system. Each node receives information in one channel - the input channel -
and emits in another - the output channel. Getting the token is represented by the
reception while emitting stands for passing the token to the next node.

We start off by defining the exit procedure for the nodes. There are two possible
alternate behaviors: if the output channel is the same as the input channel that means
that this is the only node in the ring and therefore there is nothing left to be done;
the other possibility occurs when there is a node waiting for the token, so there is
a possible communication. The emitted information consists of the entry link of the
node that is exiting so that the next node can update it's entry point, something like
a short circuit in the links that existed for the exiting node.

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

We now define the behavior of the nodes starting by the IdleNode that consists
in a process waiting on a reception on it's input channel, being the received
name considered as the new input channel. After the reception the process
symbolically holds the token and hence becomes a TokenOwner. This process
can either make an internal silent action and then exit the system or just pass
the token along, maintaining the linkage information, after which losing the
token and becoming an IdleNode.

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

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

Finally we define the system consisting in a set of five nodes, four idle and
obviously one holding the token, linked in a circular fashion by restricted
names known only to the nodes that hold them as links.

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

On the verification side, we start off by checking to see if our system, for every
configuration, will at some point become the empty system, something along the
lines of is it always possible for the system to terminate.

check System |= always eventually 0;

We now intend to verify that the set of nodes in our system are always connected
circularly. We start off by characterizing the behavior of a node that is exiting,
something that can be precisely expressed by the fact that it is a single point in
space, and it holds either two different names or it can perform an internal action
and become the empty system, and it is willing to emit it's input link on it's output
link and become the empty system.

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

We now characterize a node by saying that it is a single point in space and it
is either an exiting process or it has the possible infinite behavior of receiving
a name and continuing considering this new name as the new input channel,
which captures the behavior of the idle node, or of being able to perform an
internal action after which exiting and an output in the output link carrying the
output channel name and continuing with the same input link, which describes
the active node.

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));

Finally we define the circularity property by stating that it is either the empty system
or it consists of only one node that has it's output connected to it's input, or there
spatially co-exist a node and a chain of nodes with one ore more elements, being
the node connected to the chain which in turn leads back to the initial node.

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

We then check to see if the system holds this property in all possible configurations.

check System |= always ring;