module PROC (DATA) is

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

process BigRel [R1, R2: MSG_CHANNEL] (M: MSG) is
   Rel [R1, R2] (M, FIRST);   -- first round send
   i; -- to model the LOTOS operator ">>"
   Rel [R1, R2] (M, SECOND)  -- second round send
end process

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

process Rel [R1, R2: MSG_CHANNEL] (M:MSG, T:TYPEMSG) is
   par
      R1 (M, T)
   ||
      R2 (M, T)
   end par
end process

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

process Transmitter [R_T1, R_T2: MSG_CHANNEL] (M: MSG) is
   BigRel [R_T1, R_T2] (M);
   i; -- to model the LOTOS operator ">>"
   if M == N then
      stop
   else
      Transmitter [R_T1, R_T2] (MSG (NAT (M)  + 1))
   end if
end process

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

process BigRel_R [R: MSG_CHANNEL] (M: MSG) is
   Rel_R [R] (M, FIRST);    -- first round send
   i; -- to model the LOTOS operator ">>"
   Rel_R [R] (M, SECOND)   -- second round send
end process 

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

process Rel_R [R: MSG_CHANNEL] (M:MSG, T:TYPEMSG) is
   R (M, T)
end process

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

process Thread [DEPOSE: DEP_CHANNEL, RR: MSG_CHANNEL] is
   var M: MSG in
      DEPOSE (?M);
      disrupt
         BigRel_R [RR] (M);
         i; -- to model the LOTOS operator ">>"
         stop
      by
         DEPOSE (M); 
         Thread [DEPOSE, RR]
      end disrupt
   end var
end process

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

process Ear [RT, RR: MSG_CHANNEL] is
   loop
      alt
         RT (?any MSG, ?any TYPEMSG)
      []
         RR (?any MSG, ?any TYPEMSG)
      end alt
   end loop
end process

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

process Fail_Receiver [RT, RE, RR: MSG_CHANNEL, GET: GET_CHANNEL, DEPOSE: DEP_CHANNEL, CRASH: GET_CHANNEL] (in var A: ADR) is
   var M: MSG in
      loop
         alt
            RT (?any MSG, ?any TYPEMSG)
         []
            RE (?any MSG, ?any TYPEMSG)
         []
            RR (?any MSG, ?any TYPEMSG)
         []
            GET (?A, ?any MSG)
         []
            DEPOSE (?any MSG)
         []
            alt
               RT (?M, ?any TYPEMSG)
            []
               RE (?M, ?any TYPEMSG)
            []
               RR (?M, ?any TYPEMSG)
            []
               GET (?A, ?M)
            []
               DEPOSE (?M)
            end alt;
            CRASH (A, M);
            Ear [RT, RR]
         end alt
      end loop
   end var
end process

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

process Receiver [RT, RR: MSG_CHANNEL, DEPOSE: DEP_CHANNEL, GET: GET_CHANNEL] (A: ADR, in var C: MSG, in var B: BOOL) is
   var M: MSG in
      loop
         alt
            alt
               RT (?M, FIRST of TYPEMSG)
            []
               RR (?M, FIRST of TYPEMSG)
            end alt;
            if M == C then
               GET (A, M);
               DEPOSE (M);
               C := C <+> 1 of MSG;
               B := FALSE
            end if
         []
            alt
               RT (?M, SECOND of TYPEMSG)
            []
               RR (?M, SECOND of TYPEMSG)
            end alt;
            if (M == (C <-> 1 of MSG)) and (B == FALSE) then
               DEPOSE (M);
               B := TRUE
            end if
         end alt
      end loop
   end var
end process

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

end module