specification ABP_reliable [PUT,GET] : noexit

  behaviour

    hide msg0,msg1,ack0,ack1 in
    (
      TRANS [PUT,msg0,msg1,ack0,ack1]
      |[msg0,msg1,ack0,ack1]|
      RECV  [GET,msg0,msg1,ack0,ack1]
    )

  where

    process TRANS [PUT,msg0,msg1,ack0,ack1]: noexit:=

      PUT;      (* get next message to be sent *)
        msg0;   (* send current message + control bit 0 *)
          ack0; (* wait to get ack0 *)
            TRANS [PUT,msg1,msg0,ack1,ack0]  (* alternating bit *)

    endproc

    process RECV [GET,msg0,msg1,ack0,ack1]: noexit:=

      msg0;     (* wait to receive message + control bit 0 *)
        GET;    (* output the message *)
          ack0; (* send ack0 *)
            RECV [GET,msg1,msg0,ack1,ack0]   (* alternating bit *)

    endproc

endspec