module rel_rel_A (DATA, PROC) is -- Improved REL/rel algorithm - FIFO - 2 stations - with crashes - version A ------------------------------------------------------------------------------ process MAIN [GET, CRASH: GET_CHANNEL] is hide R_T1, R_T2: MSG_CHANNEL in par R_T1, R_T2 in disrupt Transmitter [R_T1, R_T2] (1 of MSG) by i; -- Crash stop end disrupt || Receiver_grp [R_T1, R_T2, GET, CRASH] end par end hide end process ------------------------------------------------------------------------------ process Receiver_grp [R_T1, R_T2: MSG_CHANNEL, GET, CRASH: GET_CHANNEL] is hide R_1, R_2: MSG_CHANNEL in par R_1, R_2 in Receiver_Node [R_T1, R_1, R_2, GET, CRASH] (1 of ADR, 1 of MSG, FALSE) || Receiver_Node [R_T2, R_2, R_1, GET, CRASH] (2 of ADR, 1 of MSG, FALSE) end par end hide end process ------------------------------------------------------------------------------ process Receiver_Node [RT, RE, RR: MSG_CHANNEL, GET, CRASH: GET_CHANNEL] (A:ADR, C:MSG, B:BOOL) is hide DEPOSE: DEP_CHANNEL in par RT, RE, RR, GET, DEPOSE, CRASH in disrupt par DEPOSE in Receiver [RT, RR, DEPOSE, GET] (A, C, B) || Thread [DEPOSE, RE] end par by CRASH (A, ?any MSG); Ear [RT, RR] end disrupt || Fail_Receiver [RT, RE, RR, GET, DEPOSE, CRASH] (A) end par end hide end process ------------------------------------------------------------------------------ end module