module interface (DATA) is !update "2021-b" (* * Interface for Receiver_Node i, where 1 <= i <= 3, 1 <= j <= 3, 1 <= k <= 3, * i != j, i != k, j != k *) (* * Messages received by a Receiver_Node always verify the following properties: * - They are numbered from 1 to 3 * - "FIRST" type messages are received before "SECOND" type messages * - Messages are received either from the Transmitter or from another * Receiver_Node but a Receiver_Node cannot send a message it has not * received itself from the Transmitter * - The Transmitter and the Receiver_Node can crash at any time and then * stop to send messages *) ------------------------------------------------------------------------------ process INTERFACE [R_Ti, Rji, Rki: MSG_CHANNEL] is par R_Ti, Rji, Rki in par ABS_TRANS [R_Ti] || ABS_REC [Rji] || ABS_REC [Rki] end par || Q [R_Ti, Rji, Rki] (0) end par end process ------------------------------------------------------------------------------ process ABS_TRANS [RT: MSG_CHANNEL] is RT (1 of MSG, FIRST of TYPEMSG); RT (1 of MSG, SECOND of TYPEMSG); RT (2 of MSG, FIRST of TYPEMSG); RT (2 of MSG, SECOND of TYPEMSG); RT (3 of MSG, FIRST of TYPEMSG); RT (3 of MSG, SECOND of TYPEMSG); stop end process ------------------------------------------------------------------------------ process ABS_REC [RR: MSG_CHANNEL] is disrupt RR (1 of MSG, FIRST of TYPEMSG); RR (1 of MSG, SECOND of TYPEMSG); stop by disrupt RR (2 of MSG, FIRST of TYPEMSG); RR (2 of MSG, SECOND of TYPEMSG); stop by RR (3 of MSG, FIRST of TYPEMSG); RR (3 of MSG, SECOND of TYPEMSG); stop end disrupt end disrupt end process ------------------------------------------------------------------------------ process Q [RT, RR1, RR2: MSG_CHANNEL] (in var X: NAT) is var Y: MSG in loop select RR1 (?Y, FIRST of TYPEMSG) where (NAT (Y) == X) or (NAT (Y) == X + 1) [] RR2 (?Y, FIRST of TYPEMSG) where (NAT (Y) == X) or (NAT (Y) == X + 1) [] RR1 (?Y, SECOND of TYPEMSG) where NAT (Y) >= X [] RR2 (?Y, SECOND of TYPEMSG) where NAT (Y) >= X [] RT (?Y, SECOND of TYPEMSG) where NAT (Y) >= X; X := NAT (Y) [] RT (?Y, FIRST of TYPEMSG); use Y end select end loop end var end process ------------------------------------------------------------------------------ end module