chan In	=[0] of { byte };
chan Out =[0] of { byte };

chan s2c =[0] of { byte,bit };
chan c2s =[0] of { byte,bit };
chan r2c =[0] of { byte,bit };
chan c2r =[0] of { byte,bit };

proctype sender() {
    byte msg, seqno=0, ack=0;
    do
    :: In?msg ->
again: do
       :: s2c!msg,seqno ->
          if
          :: c2s?(0,ack) -> break
          :: timeout
          fi
       od;
       if
       :: seqno != ack -> goto again
       :: else -> seqno = 1-seqno
       fi
    od
}


proctype receiver() {
    byte msg,seqno,ack;
    do
    :: do
       :: c2r?msg,ack -> r2c!0,ack;
          if
          :: ack == seqno -> break
          :: else
          fi
       od;
       Out!msg;
       seqno = 1-seqno
    od
}


proctype channel() {
    byte msg,seqno;
    do
    :: s2c?msg,seqno ->
       if
       :: c2r!msg,seqno
       :: skip
       fi
    :: r2c?msg,seqno ->
       if
       :: c2s!msg,seqno
       :: skip
       fi
    od
}



init { atomic {
   run sender();
   run channel();
   run receiver();
} }


#define MAX 3

active proctype producer() {
    byte val;
    do
    :: In!val -> val = (val+1)%MAX
    od
}

active proctype consumer() {
    byte val, exp_val;
    do
    :: Out?val -> assert(val == exp_val);
       exp_val = (exp_val+1)%MAX
    od
}