module inres_service_int is

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

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

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

type SP is
   ICONreq, ICONind, ICONresp, ICONconf, IDISreq, IDISind, IDATreq, IDATind
end type

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

channel ISAP is
   (Primitive:SP),
   (Primitive:SP, Data:ISDU)
end channel

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

process MAIN [ISAPini, ISAPres:ISAP] is
   par
      ISAPini -> ICEPini [ISAPini]
   ||
      ISAPres -> ICEPres [ISAPres]
   ||
      ISAPini, ISAPres -> EndtoEnd [ISAPini,ISAPres]
   end par
end process

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

process ICEPini [g:ISAP] is
   loop
      disrupt
         -- former LOTOS process ConnectionphaseIni expanded inline
         g (ICONreq);
         g (ICONconf);
         i; -- LOTOS operator ">>"
         -- former LOTOS process DataphaseIni expanded inline
         loop
            g (IDATreq, ?any ISDU)
         end loop
      by
         -- former LOTOS process DisconnectionIni expanded inline
         g (IDISind)
      end disrupt
   end loop
end process

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

process ICEPres [g:ISAP] is
   loop
      -- former LOTOS process ConnectionphaseRes expanded inline
      g (ICONind);
      i; -- LOTOS operator ">>"
      disrupt
         -- former LOTOS process WaitRes expanded inline
         g (ICONresp);
         i; -- LOTOS operator ">>"
         -- former LOTOS process DataphaseRes expanded inline
         loop
            g (IDATind, ?any ISDU)
         end loop
      by
         -- former LOTOS process DisconnectionRes expanded inline
         g (IDISreq)
      end disrupt
   end loop
end process

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

process EndtoEnd [ini,res:ISAP] is
   loop
      alt
         ini (ICONreq);
         alt
            res (ICONind)
         []
            res (IDISreq);
            alt
               ini (IDISind)
            []
               res (ICONind);
               ini (IDISind)
            end alt
         end alt
      []
         var data:ISDU in
            ini (IDATreq, ?data);
            alt
               res (IDATind, data)
            []
               res (IDISreq);
               alt
                  ini (IDISind)
               []
                  res (IDATind, data);
                  ini (IDISind)
               end alt
            end alt
         end var
      []
         res (ICONresp);
         alt
            ini (ICONconf)
         []
            res (IDISreq);
            alt
               ini (IDISind)
            []
               ini (ICONconf);
               ini (IDISind)
            end alt
         end alt
      []
         res (IDISreq);
         ini (IDISind)
      end alt
   end loop
end process

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

end module