module bitalt_protocol (TYPES, CHANNELS) is

process MAIN [PUT, GET: C_MSG] is
   hide SDT, RDT: C_MSG_BIT, SACK, RACK: C_BIT, SACKe, RDTe: none in
      par
         SDT, SACK, SACKe -> TRANSMITTER [PUT, SDT, SACK, SACKe] (0 of BIT)
      ||
         RDT, RDTe, RACK -> RECEIVER [GET, RDT, RDTe, RACK] (0 of BIT)
      ||   
         SDT, RDT, RDTe -> MEDIUM1 [SDT, RDT, RDTe]
      ||
         RACK, SACK, SACKe -> MEDIUM2 [RACK, SACK, SACKe]
      end par
   end hide
end process

-------------------------------------------------------------------------------

process TRANSMITTER [PUT: C_MSG, SDT: C_MSG_BIT, SACK: C_BIT, SACKe: none]
                    (in var B: BIT) is
   var M: MSG in
      loop
         PUT (?M);              -- obtention of a message
         loop L in
            SDT (M, B);         -- transmission of the message
            alt
               SACK (B);        -- correct control bit
               B := not (B);
               break L
            []
               SACK (not (B))   -- incorrect control bit => retransmission
            []
               SACKe            -- loss indication => retransmission
            []
               i                -- timeout => retransmission
            end alt
         end loop
      end loop
   end var
end process

-------------------------------------------------------------------------------

process RECEIVER [GET: C_MSG, RDT: C_MSG_BIT, RDTe: none, RACK: C_BIT]
                 (in var B: BIT) is
   var M: MSG in
      loop
         alt
            RDT (?M, B);               -- correct control bit
            GET (M);                   -- delivery of the message
            RACK (B);                  -- correct acknowledgement sent
            B := not (B)
         []
            RDT (?any MSG, not (B));   -- incorrect control bit =>
            RACK (not (B))             -- incorrect acknowledgement sent
         []
            RDTe;                      -- loss indication =>
            RACK (not (B))             -- incorrect acknowledgement sent
         []
            i;                         -- timeout =>
            RACK (not (B))             -- incorrect acknowledgement sent
         end alt
      end loop
   end var
end process
   
-------------------------------------------------------------------------------

process MEDIUM1 [SDT, RDT: C_MSG_BIT, RDTe: none] is
   var M: MSG, B: BIT in
      loop
         SDT (?M, ?B);   -- receipt of a message
         alt
            RDT (M, B)   -- correct transmission
         []
            RDTe         -- loss with indication
         []
            i            -- silent loss
         end alt
      end loop
   end var
end process

-------------------------------------------------------------------------------

process MEDIUM2 [RACK, SACK: C_BIT, SACKe: none] is
   var B: BIT in
      loop
         RACK (?B);    -- receipt of an acknowledgement
         alt
            SACK (B)   -- correct transmission
         []
            SACKe      -- loss with indication
         []
            i          -- silent loss
         end alt
      end loop
   end var
end process

end module