specification ABP_unreliable [PUT,GET] :noexit

 behaviour

   hide smes0, smes1, rmes0, rmes1, rerror, 
        rack0, rack1, sack0, sack1, serror in
   (
      (
        TRANS [PUT, smes0, smes1, sack0, sack1, serror]
        |||
        RECV  [GET, rmes0, rmes1, rack0, rack1, rerror]
      )
      |[smes0, smes1, rmes0, rmes1, rerror, 
        rack0, rack1, sack0, sack1, serror]|
      (
        Medium [smes0, smes1, rmes0, rmes1, rerror]
        |||
        Medium [rack0, rack1, sack0, sack1, serror]
      )
   )

   where

(* ----------------------------------------------------------------- *)

   process TRANS [PUT, mes0, mes1, ack0, ack1, error] : noexit :=

     PUT;         (* acquiring a new message *)
       TSEND [PUT, mes0, mes1, ack0, ack1, error]

   where

     process TSEND [PUT, mes0, mes1, ack0, ack1, error] : noexit :=

       mes0;             (* sending a 0-message *)
         (
          ack0;          (* control bit correct, alternating bit *)
            TRANS [PUT, mes1, mes0, ack1, ack0, error]
          []
          ack1;          (* incorrect control bit, retry to send *)
            TSEND [PUT, mes0, mes1, ack0, ack1, error]
          []
          error;         (* ack distorted, retry to send *)
            TSEND [PUT, mes0, mes1, ack0, ack1, error]
         )

     endproc

   endproc

(* ----------------------------------------------------------------- *)

   process RECV [GET, mes0, mes1, ack0, ack1, error] : noexit :=

     mes0;               (* correct control bit *)
       GET;              (* output the message  *)
         ack0;           (* sending correct ack *)
           RECV [GET, mes1, mes0, ack1, ack0, error]
     []
     mes1;               (* incorrect control bit *)
       ack1;             (* sending incorrect ack (nack) *)
         RECV [GET, mes0, mes1, ack0, ack1, error]
     []
     error;              (* message distorted *)
       ack1;             (* sending incorrect ack (nack) *)
         RECV [GET, mes0, mes1, ack0, ack1, error]

   endproc

(* ----------------------------------------------------------------- *)

   process Medium [in0, in1, out0, out1, error] : noexit :=

     in0;            (* send 0-message *)
       (
        out0;        (* transmission correct *)
          Medium [in0, in1, out0, out1, error]
        []
        error;       (* message distorted *)
          Medium [in0, in1, out0, out1, error]
       )
     []
     Medium [in1, in0, out1, out0, error] (* alternating channel *)

   endproc

endspec