specification ABP_reliable [PUT,GET] : noexit

  library ABP endlib 

  behaviour

    hide channel,ack in
    (
      TRANS [PUT,channel,ack] (0 of BIT)
      |[channel,ack]|
      RECV  [GET,channel,ack] (0 of BIT)
    )

  where

    process TRANS [PUT,channel,ack](B:BIT): noexit:=

      PUT ?message:MSG;       (* get next message to be sent *)
        channel !message !B;  (* send current message + control bit *)
          ack !B;             (* rendezvouz ack B *)
            TRANS [PUT,channel,ack](not (B))  (* bit alternating *)

    endproc

    process RECV [GET,channel,ack](B:BIT): noexit:=

      channel ?message:MSG !B; (* get current message + rendezvouz bit *)
        GET !message;          (* output message *)
          ack !B;              (* rendezvouz ack B *)
            RECV [GET,channel,ack](not (B))  (* bit alternating *)

    endproc

endspec