#define MaxSeq	3
#define MaxSeq_plus_1	4
#define inc(x)	x = (x + 1) % (MaxSeq + 1)

chan q[2] = [MaxSeq] of { byte, byte };

active [2] proctype p5()
{	byte	NextFrame, AckExp, FrameExp,
		r, s, nbuf, i;
	chan in, out;

	d_step {
		in = q[_pid];
		out = q[1-_pid]
	};
	xr in;
	xs out;

	do
	:: atomic { nbuf < MaxSeq ->
		nbuf++;
		out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
		printf("MSC: nbuf: %d\n", nbuf);
		inc(NextFrame)
	}
	:: atomic { in?r,s ->
		if
		:: r == FrameExp ->
			printf("MSC: accept %d\n", r);
			inc(FrameExp)
		:: else
			-> printf("MSC: reject\n")
		fi
	};
	d_step {
		do
		:: ((AckExp <= s) && (s <  NextFrame))
		|| ((AckExp <= s) && (NextFrame <  AckExp))
		|| ((s <  NextFrame) && (NextFrame <  AckExp)) ->
			nbuf--;
			printf("MSC: nbuf: %d\n", nbuf);
			inc(AckExp)
		:: else ->
			printf("MSC: %d %d %d\n", AckExp, s, NextFrame);
			break
		od; skip
	}
	:: timeout ->
	d_step {
		NextFrame = AckExp;
		printf("MSC: timeout\n");
		i = 1;
		do
		:: i <= nbuf ->
			out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
			inc(NextFrame);
			i++
		:: else ->
			break
		od; i = 0
	}
	od
}