module rel_rel_C (DATA) is

-- Improved REL/rel algorithm - FIFO - 3 stations - with crashes - version C

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

process MAIN [GET: GET_CHANNEL, CRASH: CRH_CHANNEL] is
   hide R_T1, R_T2, R_T3: MSG_CHANNEL in
      par R_T1, R_T2, R_T3 in
         Crash_Transmitter [R_T1, R_T2, R_T3]
      ||
         hide R12, R21, R13, R31: MSG_CHANNEL in
            par R12, R21, R13, R31 in
               Receiver_Node [R_T1, R21, R31, R12, R13, GET, CRASH] (1 of ADR)
            ||
               hide R23, R32: MSG_CHANNEL in
                  par
                     Receiver_Node [R_T2, R12, R32, R21, R23, GET, CRASH] (2 of ADR)
                  ||
                     Receiver_Node [R_T3, R13, R23, R31, R32, GET, CRASH] (3 of ADR)
                  end par
               end hide
            end par
         end hide
      end par
   end hide
end process

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

process Receiver_Node [R_T, RR1, RR2, RE1, RE2: MSG_CHANNEL, GET: GET_CHANNEL, CRASH: CRH_CHANNEL] (A: ADR) is
   hide DEPOSE: DEP_CHANNEL in
      par R_T, RR1, RR2, RE1, RE2, DEPOSE, GET, CRASH in
         Receiver_Thread [R_T, RR1, RR2, RE1, RE2, DEPOSE, GET, CRASH] (A)
      ||
         Fail_Receiver [R_T, RR1, RR2, RE1, RE2, DEPOSE, GET, CRASH] (A)
      end par
   end hide
end process

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

process Crash_Transmitter [R_T1, R_T2, R_T3: MSG_CHANNEL] is
   hide CRASH_T: MSG_CHANNEL in
      par R_T1, R_T2, R_T3 in
         Transmitter [R_T1, R_T2, R_T3] (1 of MSG)
      ||
         Fail_Transmitter [R_T1, R_T2, R_T3, CRASH_T]
      end par
   end hide
end process

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

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

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

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

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

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

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

process Fail_Transmitter [R_T1, R_T2, R_T3, CRASH_T: MSG_CHANNEL] is
   loop
      alt
         R_T1 (?any MSG, ?any TYPEMSG)
      []
         R_T2 (?any MSG, ?any TYPEMSG)
      []
         R_T3 (?any MSG, ?any TYPEMSG)
      []
         var M: MSG, T: TYPEMSG in
            alt
               R_T1 (?M, ?T)
            []
               R_T2 (?M, ?T)
            []
               R_T3 (?M, ?T)
            end alt;
            CRASH_T (M, T); 
            stop
         end var
      end alt
   end loop
end process

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

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

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

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

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

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

process Fail_Receiver [RT, RR1, RR2, RE1, RE2: MSG_CHANNEL, DEPOSE: DEP_CHANNEL, GET: GET_CHANNEL, CRASH: CRH_CHANNEL] (in var A: ADR) is
   loop
      alt
         RT (?any MSG, ?any TYPEMSG)
      []
         RR1 (?any MSG, ?any TYPEMSG)
      []
         RR2 (?any MSG, ?any TYPEMSG)
      []
         RE1 (?any MSG, ?any TYPEMSG)
      []
         RE2 (?any MSG, ?any TYPEMSG)
      []
         GET (?A, ?any MSG)
      []
         DEPOSE (?any MSG)
      []
         alt
            RT (?any MSG, ?any TYPEMSG)
         []
            RR1 (?any MSG, ?any TYPEMSG)
         []
            RR2 (?any MSG, ?any TYPEMSG)
         []
            RE1 (?any MSG, ?any TYPEMSG)
         []
            RE2 (?any MSG, ?any TYPEMSG)
         []
            GET (?A, ?any MSG)
         []
            DEPOSE (?any MSG)
         end alt;
         CRASH (A); 
         Ear [RT, RR1, RR2]
      end alt
   end loop
end process

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

process Receiver [RT, RR1, RR2: 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)
            []
               RR1 (?M, FIRST of TYPEMSG)
            []
               RR2 (?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)
            []
               RR1 (?M, SECOND of TYPEMSG)
            []
               RR2 (?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

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

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

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

process Receiver_Thread [R_T, RR1, RR2, RE1, RE2: MSG_CHANNEL, DEPOSE: DEP_CHANNEL, GET: GET_CHANNEL, CRASH: CRH_CHANNEL] (A: ADR) is
   disrupt
      par DEPOSE in
         Receiver [R_T, RR1, RR2, DEPOSE, GET] (A, 1 of MSG, FALSE)
      ||
         Thread [DEPOSE, RE1, RE2]
      end par
   by
      CRASH (A);
      Ear [R_T, RR1, RR2]
   end disrupt
end process

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

end module