Basic Spin Manual「もうひとつの例 (Another Example）」

example.pml

#define MAX	5

mtype = { mesg, ack, nak, err };

proctype sender(chan in_, out)
{	byte o, s, r;

	o=MAX-1;
	do
	:: o = (o+1)%MAX; /* next msg */
again: if
       :: out!mesg(o,s) /* send */
       :: out!err(0,0)  /* distort */
       :: skip       /* or lose */
       fi;
       if
       :: timeout   -> goto again
       :: in_?err(0,0) -> goto again
       :: in_?nak(r,0) -> goto again
       :: in_?ack(r,0) ->
		if
		:: (r == s) -> goto progress
		:: (r != s) -> goto again
		fi
       fi;
progress:	s = 1-s	/* toggle seqno */
	od
}

proctype receiver(chan in_, out)
{	byte i;		/* actual input   */
	byte s;		/* actual seqno   */
	byte es;	/* expected seqno */
	byte ei;	/* expected input */

	do
	:: in_?mesg(i, s) ->
		if
		:: (s == es) ->
			assert(i == ei);
progress:		es = 1 - es;
			ei = (ei + 1)%MAX;
			if
	/* send,   */	:: out!ack(s,0)
	/* distort */	:: out!err(0,0)
	/* or lose */	:: skip
			fi
		:: (s != es) ->
			if
	/* send,   */	:: out!nak(s,0)
	/* distort */	:: out!err(0,0)
	/* or lose */	:: skip
			fi
		fi
	:: in_?err ->
		out!nak(s,0)
	od
}

init {
	chan s_r = [1] of { mtype,byte,byte };
	chan r_s = [1] of { mtype,byte,byte };
	atomic {
		run sender(r_s, s_r);
		run receiver(s_r, r_s)
	}
}