specification ABP [PUT, GET] :noexit

 library ABP endlib

 behaviour

   hide smes, rmes, rerror, rack, sack, serror in
   (
      (
        TRANS [PUT, smes, sack, serror] (0 of BIT)
        |||
        RECV  [GET, rmes, rack, rerror] (0 of BIT)
      )
      |[smes, rmes, rerror, rack, sack, serror]|
      (
        Medium1 [smes, rmes, rerror]
        |||
        Medium2 [rack, sack, serror]
      )
   )

   where

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

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

     PUT ?M:MSG;         (* acquiring a new message *)
        TSEND [PUT, mes, ack, error](B, M) 

   where

     process TSEND [PUT, mes, ack, error] (B:BIT, M:MSG) : noexit :=

       mes !M !B;           (* sending message M with bit B *)
          (
          ack !B;           (* control bit correct, alternating bit *)
             TRANS [PUT, mes, ack, error] (not (B))
          []
          ack !(not (B));   (* incorrect control bit, retry to send *)
             TSEND [PUT, mes, ack, error] (B, M)
          []
          error;            (* ack distorted, retry to send *)
             TSEND [PUT, mes, ack, error] (B, M)
          []
          i;                (* timeout *)
             TSEND [PUT, mes, ack, error] (B, M)
          )

     endproc

   endproc

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

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

      mes ?M:MSG !B;          (* correct control bit *)
         GET !M;              (* output the message  *)
            ack !B;           (* sending correct ack *)
               RECV [GET, mes, ack, error] (not (B))
      []
      mes ?M:MSG !(not (B));  (* incorrect control bit *)
         ack !(not (B));      (* sending incorrect ack (nack) *)
            RECV [GET, mes, ack, error] (B)
      []
      error;                  (* message distorted *)
         ack !(not (B));      (* sending incorrect ack (nack) *)
            RECV [GET, mes, ack, error] (B)
      []
      i;                      (* timeout *)
         ack !(not (B));      (* sending incorrect ack (nack) *)
            RECV [GET, mes, ack, error] (B)

   endproc

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

   process Medium1 [input, output, error] : noexit :=

      input ?M:MSG ?B:BIT;    (* receive the message *)
         (
         output !M !B;        (* transmission correctly *)
            Medium1 [input, output, error]
         []
         error;               (* message distorted *)
            Medium1 [input, output, error]
         []
         i;                   (* lost message *)
            Medium1 [input, output, error]
         )

   endproc

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

   process Medium2 [input, output, error] : noexit :=

      input ?B:BIT;           (* receive the ack/nack message *)
         (
         output !B;           (* transmission correctly *)
            Medium2 [input, output, error]
         []
         error;               (* ack message distorted *)
            Medium2 [input, output, error]
         []
         i;                   (* lost ack message *)
            Medium2 [input, output, error]
         )

   endproc

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

endspec