specification ALTERNATING_BIT_PROTOCOL [PUT, GET] : noexit 

library TYPES endlib

behaviour

   hide SDT, RDT, RDTe, RACK, SACK, SACKe in
      (
         (
         TRANSMITTER [PUT, SDT, SACK, SACKe] (0 of BIT)
         |||
         RECEIVER [GET, RDT, RDTe, RACK] (0 of BIT)
         )
      |[SDT, RDT, RDTe, RACK, SACK, SACKe]|
         (
         MEDIUM1 [SDT, RDT, RDTe]
         |||
         MEDIUM2 [RACK, SACK, SACKe]
         )
      )

where

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

   process TRANSMITTER [PUT, SDT, SACK, SACKe] (B:BIT) : noexit :=
      PUT ?M:MSG;             (* obtention of a message *)
         TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
   where
      process TRANSMIT [PUT, SDT, SACK, SACKe] (B:BIT, M:MSG) : noexit :=
         SDT !M !B;           (* transmission of the message *)
            (
            SACK !B;          (* correct control bit *)
               TRANSMITTER [PUT, SDT, SACK, SACKe] (not (B))
            []
            SACK !(not (B));  (* incorrect control bit => retransmission *)
               TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
            []
            SACKe;            (* loss indication => retransmission *)
               TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
            []
            i;                (* timeout => retransmission *)
               TRANSMIT [PUT, SDT, SACK, SACKe] (B, M)
            )
      endproc
   endproc

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

   process RECEIVER [GET, RDT, RDTe, RACK] (B:BIT) : noexit :=
      RDT ?M:MSG !B;          (* correct control bit *)
         GET !M;              (* delivery of the message *)
            RACK !B;          (* correct acknowledgement sent *)
               RECEIVER [GET, RDT, RDTe, RACK] (not (B))
      []
      RDT ?M:MSG !(not (B));  (* incorrect control bit => *)
         RACK !(not (B));     (* incorrect acknowledgement sent *)
            RECEIVER [GET, RDT, RDTe, RACK] (B)
      []
      RDTe;                   (* loss indication => *)
         RACK !(not (B));     (* incorrect acknowledgement sent *)
            RECEIVER [GET, RDT, RDTe, RACK] (B)
      []
      i;                      (* timeout => *)
         RACK !(not (B));     (* incorrect acknowledgement sent *)
            RECEIVER [GET, RDT, RDTe, RACK] (B)
   endproc
   
(*---------------------------------------------------------------------------*)

   process MEDIUM1 [SDT, RDT, RDTe] : noexit :=
      SDT ?M:MSG ?B:BIT;   (* receipt of a message *)
         (
         RDT !M !B;        (* correct transmission *)
            MEDIUM1 [SDT, RDT, RDTe]
         []
         RDTe;             (* loss with indication *)
            MEDIUM1 [SDT, RDT, RDTe]
         []
         i;                (* silent loss *)
            MEDIUM1 [SDT, RDT, RDTe]
         )
   endproc

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

   process MEDIUM2 [RACK, SACK, SACKe] : noexit :=
      RACK ?B:BIT;   (* receipt of an acknowledgement *)
         (
         SACK !B;    (* correct transmission *)
            MEDIUM2 [RACK, SACK, SACKe]
         []
         SACKe;      (* loss with indication *)
            MEDIUM2 [RACK, SACK, SACKe]
         []
         i;          (* silent loss *)
            MEDIUM2 [RACK, SACK, SACKe]
         )
   endproc

endspec