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

#define CHECKIT

#ifdef CHECKIT
	mtype = { red, white, blue };	/* Wolper's test */
	chan source = [0] of { mtype };
	chan q[2] = [MaxSeq] of { mtype, byte, byte };
	mtype rcvd = white;
	mtype sent = white;
#else
	chan q[2] = [MaxSeq] of { byte, byte };
#endif

active [2] proctype p5()
{	byte	NextFrame, AckExp, FrameExp,
		r, s, nbuf, i;
	chan in, out;
#ifdef CHECKIT
	mtype	ball;
	byte frames[MaxSeq_plus_1];
#endif

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

	xr in;
	xs out;

	do
	:: atomic {
		nbuf < MaxSeq ->
		nbuf++;
#ifdef CHECKIT
		if
		:: _pid%2 -> source?ball
		:: else
		fi;
		frames[NextFrame] = ball;
		out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
		if
		:: _pid%2 -> sent = ball;
		:: else
		fi;
#else
		out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
#endif
#ifdef VERBOSE
		printf("MSC: nbuf: %d\n", nbuf);
#endif
		inc(NextFrame)
	}
#ifdef CHECKIT
	:: atomic { in?ball,r,s ->
#else
	:: atomic { in?r,s ->
#endif
		if
		:: r == FrameExp ->
#ifdef VERBOSE
			printf("MSC: accept %d\n", r);
#endif
#ifdef CHECKIT
			if
			:: _pid%2
			:: else -> rcvd = ball
			fi;
#endif
			inc(FrameExp)
		:: else
#ifdef VERBOSE
			-> printf("MSC: reject\n")
#endif
		fi
	};
	d_step {
	 	do
		:: ((AckExp <= s) && (s <  NextFrame))
		|| ((AckExp <= s) && (NextFrame <  AckExp))
		|| ((s <  NextFrame) && (NextFrame <  AckExp)) ->
			nbuf--;
#ifdef VERBOSE
			printf("MSC: nbuf: %d\n", nbuf);
#endif
			inc(AckExp)
		:: else ->
#ifdef VERBOSE
			printf("MSC: %d %d %d\n", AckExp, s, NextFrame);
#endif
			break
		od;
		skip
	}
	:: timeout ->
	d_step {
		NextFrame = AckExp;
#ifdef VERBOSE
		printf("MSC: timeout\n");
#endif
		i = 1;
		do
		:: i <= nbuf ->
#ifdef CHECKIT
			if
			:: _pid%2 -> ball = frames[NextFrame]
			:: else
			fi;		
			out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
#else
			out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
#endif
			inc(NextFrame);
			i++
		:: else ->
			break
		od;
		i = 0
	}
	od
}
#ifdef CHECKIT
active proctype Source()
{
	do
	:: source!white
	:: source!red -> break
	od;
	do
	:: source!white
	:: source!blue -> break
	od;
end:	do
	:: source!white
	od
}

#define sw	(sent == white)
#define sr	(sent == red)
#define sb	(sent == blue)

#define rw	(rcvd == white)
#define rr	(rcvd == red)
#define rb	(rcvd == blue)

#define LTL	3
#if LTL==1

never {		/* ![](sr -> <> rr) */
		/* the never claim is generated by
			spin -f "![](sr -> <> rr)"
		   and then edited a little for readability
		   the same is true for all others below
		 */
        do
        :: 1
        :: !rr && sr -> goto accept
        od;
accept:
        if
        :: !rr -> goto accept
        fi
}

#endif
#if LTL==2

never {		/* !rr U rb */
	do
        :: !rr
        :: rb -> break	/* move to implicit 2nd state */
        od
}

#endif
#if LTL==3

never {		/* (![](sr -> <> rr)) || (!rr U rb) */

        if
        :: 1 -> goto T0_S5
        :: !rr && sr -> goto accept_S8
        :: !rr -> goto T0_S2
        :: rb -> goto accept_all
        fi;
accept_S8:
        if
        :: !rr -> goto T0_S8
        fi;
T0_S2:
        if
        :: !rr -> goto T0_S2
        :: rb -> goto accept_all
        fi;
T0_S8:
        if
        :: !rr -> goto accept_S8
        fi;
T0_S5:
        if
        :: 1 -> goto T0_S5
        :: !rr && sr -> goto accept_S8
        fi;
accept_all:
        skip
}
#endif

#endif