module inres_protocol_int_6 is

------------------------------------------------------------------------------
-- type definitions
------------------------------------------------------------------------------

type DecNumb is
   0, s (x:DecNumb)
   with ==, !=, <
   -- the LOTOS operations 2, 3, 4, <=, >=, and > have not been translated to
   -- LNT, because they are never called
end type

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

function 1 : DecNumb is
   return s (0)
end function

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

type ISDU is
   data1 -- data2 to data5 have been suppressed
end type

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

type Sequencenumber is
   0, 1
   with ==, !=
end type

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

function succ (x:Sequencenumber) : Sequencenumber is
   case x in
      0 -> return 1
   |  1 -> return 0
   end case
end function

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

type SP is
   ICONreq, ICONconf, IDISind, ICONind, ICONresp, IDISreq,
   IDATreq (data:ISDU), IDATind (data:ISDU)
   -- the LOTOS functions isICONreq(), isICONconf(), isIDISind(), isIDATreq(),
   -- isIDATind(), isICONind(), isICONresp(), isIDISreq(), and data() have not
   -- been translated to LNT, because they are never called
end type

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

type IPDU is
   CR, CC, DR,
   DT (f:Sequencenumber, d:ISDU),
   AK (f:Sequencenumber)
   -- the LOTOS functions isCR(), isCC(), isDT(), isAK(), isDR(), data(), and
   -- num() have not been translated to LNT, because they are never called
end type

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

type MSP is
   MDATreq (d:IPDU),
   MDATind (d:IPDU)
end type

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

function isMDATreq (m:MSP) : Bool is
   case m in
      MDATreq (any IPDU) -> return true
   |  any -> return false
   end case
end function

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

function isMDATind (m:MSP) : Bool is
   case m in
      MDATind (any IPDU) -> return true
   |  any -> return false
   end case
end function

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

function data (m:MSP) : IPDU is
   var d:IPDU in
      case m in
         MDATreq (d) -> return d
      |  MDATind (d) -> return d
      end case
   end var
end function

------------------------------------------------------------------------------
-- channel definitions
------------------------------------------------------------------------------

channel LOSS_CHANNEL is
   ()
end channel

channel MSAP_CHANNEL is
   (m:MSP)
end channel

channel ISAP_CHANNEL is
   (s:SP)
end channel

------------------------------------------------------------------------------
-- process definitions
------------------------------------------------------------------------------

process MAIN [ISAPini, ISAPres:ISAP_CHANNEL] is
   hide MSAP1, MSAP2:MSAP_CHANNEL, LOSS:LOSS_CHANNEL in
      par
         MSAP1, LOSS -> Station_Ini [ISAPini, MSAP1, LOSS] (1 of DecNumb)
         -- maximum number of transmissions equal to 1
      ||
         MSAP1, MSAP2, LOSS -> Medium [MSAP1, MSAP2, LOSS]
      ||
         MSAP2 -> Station_Res [MSAP2, ISAPres]
      end par
   end hide
end process

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

process Medium [MSAP1, MSAP2:MSAP_CHANNEL, LOSS:LOSS_CHANNEL] is
   par
      Channel_with_loss [MSAP1, MSAP2, LOSS]
   ||
      Channel_without_loss [MSAP2, MSAP1]
   end par
end process

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

process Channel_with_loss [a, b:MSAP_CHANNEL, LOSS:LOSS_CHANNEL] is
   var d:MSP in
      loop
         a (?d) where isMDATreq (d);
         alt
            b (MDATind (data (d)))
         []
            LOSS
         end alt
      end loop
   end var
end process

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

process Channel_without_loss [a, b:MSAP_CHANNEL] is
   var d:MSP in
      loop
         a (?d) where isMDATreq (d);
         b (MDATind (data (d)))
      end loop
   end var
end process

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

process Station_Ini [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL,
                     LOSS:LOSS_CHANNEL] (max:DecNumb) is
   disrupt
      Initiator [ISAP, MSAP, LOSS] (max)
   by
      -- former LOTOS process Disconnection expanded inline
      MSAP (MDATind (DR));
      ISAP (IDISind);
      Station_Ini [ISAP, MSAP, LOSS] (max)
   end disrupt
end process

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

process Initiator [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL, LOSS:LOSS_CHANNEL]
                                                            (max:DecNumb) is
   Connectionphase [ISAP, MSAP, LOSS] (max);
   i; -- LOTOS operator ">>"
   Initiator_Dataphase [ISAP, MSAP, LOSS] (succ (0 of Sequencenumber), max)
end process

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

process Connectionphase [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL,
                                         LOSS:LOSS_CHANNEL] (max:DecNumb) is
   var z:DecNumb in
      -- former LOTOS process Connectrequest expanded inline
      ISAP (ICONreq);
      -- former LOTOS process Connectrequest2 expanded inline
      loop L1 in
         alt
            MSAP (MDATreq (CR));
            -- User errors are ignored
            z := s (0);
            break L1
         []
            MSAP (MDATind (CC))
         []
            var x:SequenceNumber in
               x:= any SequenceNumber;
               MSAP (MDATind (AK (x)))
               -- DR is only accepted by process Disconnection
               -- System errors are ignored
            end var
         end alt
      end loop;
      i; -- LOTOS operator ">>"
      -- former LOTOS process Wait expanded inline
      loop L2 in
         alt
            MSAP (MDATind (CC));
            ISAP (ICONconf);
            assert max != 0;
            z := 0;
            break L2
         []
            var x:Sequencenumber in
               x := any SequenceNumber;
               MSAP (MDATind (AK (x)))
               -- DR is only accepted by process Disconnection
               -- System errors are ignored
            end var
         []
            LOSS;
            if z < max then
               MSAP (MDATreq (CR));
               z := s (z)
            else
               assert z == max;
               ISAP (IDISind);
               break L2
            end if
            -- Timeout
         end alt
      end loop;
      if z == max then
         Connectionphase [ISAP, MSAP, LOSS] (max)
      end if
   end var
end process

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

process Initiator_Dataphase [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL,
                    LOSS:LOSS_CHANNEL] (number:Sequencenumber, max:DecNumb) is
   var z:DecNumb, olddata:ISDU in
      -- former LOTOS process Readytosend expanded inline
      loop L1 in
         alt
            var y:ISDU in
               y := any ISDU;
               ISAP (IDATreq (y));
               MSAP (MDATreq (DT (number, y)));
               z := s (0); -- 1 is the first Sequencenumber
               olddata := y;
               break L1
            end var
         []
            MSAP (MDATind (CC))
         []
            var x:Sequencenumber in
               x:= any SequenceNumber;
               MSAP (MDATind (AK (x)))
            end var
         end alt
      end loop;
      i; -- LOTOS operator ">>"
      -- z is number of sendings. At the beginning z=1
      -- former LOTOS process Sending expanded inline
      loop L2 in
         alt
            var x:Sequencenumber in
               x := any SequenceNumber;
               MSAP (MDATind (AK (x)));
               if x == number then
                  assert max != 0;
                  z := 0;
                  break L2
               elsif z < max then
                  MSAP (MDATreq (DT (number, olddata)));
                  z := s (z)
                  -- The Initiator shall not resend more than max times in case of
                  -- faulty transmission
               else
                  assert z == max;
                  ISAP (IDISind);
                  break L2
               end if
            end var
         []
            MSAP (MDATind (CC))
         []
            LOSS;
            if z < max then
               MSAP (MDATreq (DT (number, olddata)));
               z := s (z)
            else
               assert z == max;
               ISAP (IDISind);
               break L2
            end if
         end alt
      end loop;
      if z == 0 then
         Initiator_Dataphase [ISAP, MSAP, LOSS] (succ (number), max)
      else
         assert z == max;
         Initiator [ISAP, MSAP, LOSS] (max)
      end if
   end var
end process

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

process Station_Res [MSAP:MSAP_CHANNEL, ISAP:ISAP_CHANNEL] is
   -- former LOTOS process Connectrequest expanded inline
   loop L1 in
      alt
         MSAP (MDATind (CR));
         ISAP (ICONind);
         break L1
      []
         var x:Sequencenumber, y:ISDU in
            x := any SequenceNumber;
            y := any ISDU;
            MSAP (MDATind (DT (x, y)))
            -- System errors are ignored
         end var
      end alt
   end loop;
   i; -- LOTOS operator ">>"
   disrupt
      -- former LOTOS process Wait expanded inline
      ISAP (ICONresp);
      -- former LOTOS process Wait2 expanded inline
      loop L2 in
         alt
            MSAP (MDATind (CR))
         []
            var x:Sequencenumber, y:ISDU in
               x := any SequenceNumber;
               y := any ISDU;
               MSAP (MDATind (DT (x, y)))
               -- System errors are ignored
            end var
         []
            MSAP (MDATreq (CC));
            break L2
         end alt
      end loop;
      i; -- LOTOS operator ">>"
      Station_Res_Dataphase [ISAP, MSAP] (succ (1 of Sequencenumber))
   by
      -- former LOTOS process Disconnection expanded inline
      ISAP (IDISreq);
      -- former LOTOS process Disc2 expanded inline
      -- Disc2 allows Responder to reject all IPDUs while it is disconnecting
      loop L3 in
         alt
            MSAP (MDATreq (DR));
            break L3
         []
            MSAP (MDATind (CR))
         []
            var x:Sequencenumber, y:ISDU in
               x := any SequenceNumber;
               y := any ISDU;
               MSAP (MDATind (DT (x, y)))
            end var
         end alt
      end loop;
      Station_Res [MSAP, ISAP]
   end disrupt
end process

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

process Station_Res_Dataphase [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL]
                                                   (number:Sequencenumber) is
   -- number is the last acknowledged Sequencenumber
   alt
      var x:Sequencenumber, y:ISDU in
         x := any SequenceNumber;
         y := any ISDU;
         MSAP (MDATind (DT (x, y)));
         alt
            if x == succ (number) then
               ISAP (IDATind (y));
               Dataphase2 [ISAP, MSAP] (x)
            else
               assert x == number;
               Dataphase2 [ISAP, MSAP] (x)
            end if
         end alt
      end var
   []
      MSAP (MDATind (CR));
      ISAP (ICONind);
      -- former LOTOS process Wait expanded inline
      ISAP (ICONresp);
      Wait2 [ISAP, MSAP]
   end alt
end process

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

process Wait2 [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL] is
   alt
      MSAP (MDATind (CR));
      Wait2 [ISAP, MSAP]
   []
      var x:Sequencenumber, y:ISDU in
         x := any SequenceNumber;
         y := any ISDU;
         MSAP (MDATind (DT (x, y)));
         Wait2 [ISAP, MSAP]
         -- System errors are ignored
      end var
   []
      MSAP (MDATreq (CC));
      Station_Res_Dataphase [ISAP, MSAP] (succ (1 of Sequencenumber))
   end alt
end process

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

process Dataphase2 [ISAP:ISAP_CHANNEL, MSAP:MSAP_CHANNEL] (x:Sequencenumber) is
   alt
      MSAP (MDATreq (AK (x)));
      Station_Res_Dataphase [ISAP, MSAP] (x)
   []
      MSAP (MDATind (CR));
      ISAP (ICONind);
      -- former LOTOS process Wait expanded inline
      ISAP (ICONresp);
      Wait2 [ISAP, MSAP]
   end alt
end process

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

end module