#define QSIZ	4

mtype = { send, resend, ack, nack };

chan sr = [QSIZ] of { mtype, bit };
chan rs = [QSIZ] of { mtype };

proctype sender (chan in, out)
{
  bit sbit;	/* bit to send */
  mtype resp;	/* response received */

  do
  ::	if
	:: sbit = 0;	/* pick bit to send at random */
	:: sbit = 1;
	fi;
	out ! send(sbit);
	do
	::	in ? resp;
		if
		:: resp == ack -> break;	/* ok */
		:: else -> out ! resend(sbit);
		fi
	od
  od
}

proctype receiver (chan in, out)
{
  bit rbit;

  do
  :: in ? _, rbit;	/* throw away tag, keep just bit */
     if
     :: out ! ack;	/* acknowledge or not at random */
     :: out ! nack;
     fi
  od
}


init {
  run sender(rs, sr);
  run receiver(sr, rs);
}