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

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

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