module rel_rel_B (DATA, PROC) is -- Improved REL/rel algorithm - FIFO - 2 stations - with crashes - version B ------------------------------------------------------------------------------ process MAIN [GET, CRASH: GET_CHANNEL] is hide R_T1, R_T2: MSG_CHANNEL in par R_T1, R_T2 in Crash_Transmitter [R_T1, R_T2] || hide R1, R2: MSG_CHANNEL in par R1, R2 in hide DEPOSE1: DEP_CHANNEL in par R_T1, R1, R2, GET, CRASH, DEPOSE1 in Receiver_Thread [R_T1, R1, R2, DEPOSE1, GET, CRASH] (1 of ADR) || Fail_Receiver [R_T1, R1, R2, GET, DEPOSE1, CRASH] (1 of ADR) end par end hide || hide DEPOSE2: DEP_CHANNEL in par R_T2, R1, R2, GET, CRASH, DEPOSE2 in Receiver_Thread [R_T2, R2, R1, DEPOSE2, GET, CRASH] (2 of ADR) || Fail_Receiver [R_T2, R2, R1, GET, DEPOSE2, CRASH] (2 of ADR) end par end hide end par end hide end par end hide end process ------------------------------------------------------------------------------ process Crash_Transmitter [R_T1, R_T2: MSG_CHANNEL] is hide CRASH_T: MSG_CHANNEL in par R_T1, R_T2 in Transmitter [R_T1, R_T2] (1 of MSG) || Fail_Transmitter [R_T1, R_T2, CRASH_T] end par end hide end process ------------------------------------------------------------------------------ process Fail_Transmitter [R_T1, R_T2, CRASH_T: MSG_CHANNEL] is loop select R_T1 (?any MSG, ?any TYPEMSG) [] R_T2 (?any MSG, ?any TYPEMSG) [] var M: MSG, T: TYPEMSG in select R_T1 (?M, ?T) [] R_T2 (?M, ?T) end select; CRASH_T (M, T); stop end var end select end loop end process ------------------------------------------------------------------------------ process Receiver_Thread [R_T, Ri, Rj: MSG_CHANNEL, DEPOSE: DEP_CHANNEL, GET, CRASH: GET_CHANNEL] (A: ADR) is disrupt par DEPOSE in Receiver [R_T, Rj, DEPOSE, GET] (A, 1 of MSG, FALSE) || Thread [DEPOSE, Ri] end par by CRASH (A, ?any MSG); Ear [R_T, Rj] end disrupt end process ------------------------------------------------------------------------------ end module