# define white  0
# define red    1
# define blue   2
# define MAXMSG 4

#define p	Sender@Slabel
#define q	Receiver@Rlabel
#define r	Receiver@Rsuccess 

mtype       = { msg, ack };
chan s_r    = [2] of {mtype , byte, bit};
chan r_s    = [2] of {mtype , bit };
chan source = [0] of {byte};
chan sink   = [0] of {byte};

active proctype Sender() {
    byte data = 0;
    bit sbit, seqno = 0;
    source?data;
    do
    :: s_r ! msg(data, sbit) -> Slabel: skip
    :: (1) -> skip
    :: r_s ? ack(seqno);
           if
           :: seqno == sbit ->
                  sbit = 1 - sbit ;
                  source?data
           :: else
           fi
    od
}

active proctype Receiver() {
    byte recd = 0;
    bit rbit = 1, seqno;
    do
    :: s_r ? msg (recd, seqno) ->
           if
           :: seqno != rbit ->
                Rsuccess: sink!recd;
                rbit = 1 - rbit
           :: else
           fi
    :: r_s ! ack (rbit) -> Rlabel: skip
    :: (1) -> skip
    od
}

active proctype Generator() {
    do
    :: source!white
    :: source!red -> break
    od;
    do
    :: source!white
    :: source!blue -> break
    od;
end: do
    :: source!white
    od
}

active proctype Checker() {
    byte inmsg;
    do
    :: sink?inmsg -> 
        if
        :: (inmsg == red) -> break
        :: else assert(inmsg == white)
        fi
    od;
    do
    :: sink?inmsg -> 
        if
        :: (inmsg == blue) -> break
        :: else assert(inmsg == white)
        fi
    od;
end1: do
    :: sink?inmsg -> 
        assert(inmsg == white)
    od
}

/*
	 * Formula As Typed: ([]  <>  p && []  <>  q) -> []  <>  r
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(([]  <>  p && []  <>  q) -> []  <>  r)
	 * (formalizing violations of the original)
	 */

never {    /* !(([]  <>  p && []  <>  q) -> []  <>  r) */
T0_init:
	if
	:: (! ((r)) && (p) && (q)) -> goto accept_S485
	:: (! ((r)) && (p)) -> goto T2_S485
	:: (! ((r))) -> goto T0_S485
	:: (1) -> goto T0_init
	fi;
accept_S485:
	if
	:: (! ((r))) -> goto T0_S485
	fi;
T2_S485:
	if
	:: (! ((r)) && (q)) -> goto accept_S485
	:: (! ((r))) -> goto T2_S485
	fi;
T0_S485:
	if
	:: (! ((r)) && (p) && (q)) -> goto accept_S485
	:: (! ((r)) && (p)) -> goto T2_S485
	:: (! ((r))) -> goto T0_S485
	fi;
}