module overtaking is ------------------------------------------------------------------------------- -- Type definitions ------------------------------------------------------------------------------- type CarId is volvo, saab, bmw end type ------------------------------------------------------------------------------- -- Position type type Position is Head, Middle, Tail with <> end type ------------------------------------------------------------------------------- -- Type to specify direction of PDUs being sent type SENDdirection is snd, rcv end type ------------------------------------------------------------------------------- -- Service Primitives type SAPsort is ot_req, ot_ind, ot_begin, ot_end, ot_resp_no, ot_resp_ok, ot_conf_ok end type ------------------------------------------------------------------------------- -- Protocol Data Units type PDUSORT is p_ot_req, p_ot_conf_ok end type ------------------------------------------------------------------------------- -- Port type for communication medium type M_Port is F_Tail, F_Middle, F_Head, B_Tail, B_Middle, B_Head end type ------------------------------------------------------------------------------- -- Port type for overtaking communication medium type Ot_Port is ot_Tail, ot_Middle, ot_Head end type ------------------------------------------------------------------------------- -- Channel definitions ------------------------------------------------------------------------------- channel NONE_CHAN is () end channel ------------------------------------------------------------------------------- channel C_CHAN is (car:CarId) end channel ------------------------------------------------------------------------------- channel S_CHAN is (sap:SAPsort, car:CarId, pos:Position) end channel ------------------------------------------------------------------------------- channel M_CHAN is (m:M_Port, dir:SENDdirection, p_ot:PDUSORT) end channel ------------------------------------------------------------------------------- channel OT_CHAN is (ot1:Ot_Port, m:M_Port, ot2:Ot_Port, pos:Position), (ot1:Ot_Port, m1, m2:M_Port, ot2, ot3:Ot_Port, pos1, pos2:Position) end channel ------------------------------------------------------------------------------- -- Behavioural specification ------------------------------------------------------------------------------- process MAIN [S:S_CHAN] is hide M:M_CHAN, OT:OT_CHAN in par M, OT -> par Vehicle [S, M, OT] (F_Tail, B_Tail, ot_Tail, Tail, Volvo) || Vehicle [S, M, OT] (F_Middle, B_Middle, ot_Middle, Middle, Saab) || Vehicle [S, M, OT] (F_Head, B_Head, ot_Head, Head, BMW) end par || M -> Medium [M] || OT -> Overtake_Medium [OT] end par end hide end process ------------------------------------------------------------------------------- -- Lossy Point-to-Point medium process Medium [M:M_CHAN] is par M_Channel [M] (F_Tail, B_Middle) || M_Channel [M] (F_Middle, B_Head) end par end process process M_Channel [M:M_CHAN] (P1:M_Port, P2:M_Port) is hide medium_loss:NONE_CHAN in var pdu:PDUsort in loop select M (P1, snd, ?pdu); select M (P2, rcv, pdu) [] medium_loss end select [] M (P2, snd, ?pdu); select M (P1, rcv, pdu) [] medium_loss end select end select end loop end var end hide end process ------------------------------------------------------------------------------- -- Perfect Overtaking medium process Overtake_Medium [OT:OT_CHAN] is par Ot_Channel [OT] (ot_Tail, ot_Middle) || Ot_Channel [OT] (ot_Middle, ot_Head) end par end process process Ot_Channel [OT:OT_CHAN] (P1:Ot_Port, P2:Ot_Port) is var c_B, s_F:M_Port, c_Op, s_Op:Ot_Port, c_pos, s_pos:Position in loop OT (P1, ?c_B, ?c_Op, ?c_pos); OT (P2, c_B, ?s_F, c_Op, ?s_Op, c_pos, ?s_pos); OT (P1, s_F, s_Op, s_pos) end loop end var end process ------------------------------------------------------------------------------- -- Vehicle type VehicleState is VehicleInit, Client, Server, Server_Query, Server_Answer, Server_Ok with == end type process Vehicle [S:S_CHAN, M:M_CHAN, OT:OT_CHAN] (in var F:M_Port, in var B:M_Port, in var Op:Ot_Port, in var pos:Position, car:CarId) is var State:VehicleState in State := any VehicleState where (State == VehicleInit) or (State == Server); loop case State in VehicleInit -> S (ot_req, car, pos) where pos <> Head; State := Client | Client -> select M (F, snd, p_ot_req); select -- time out hide client_timer:C_CHAN in client_timer (car); State := Client end hide [] -- or positive acknowledgement M (F, rcv, p_ot_conf_ok); -- Overtaking starts! S (ot_begin, car, pos); OT (Op, B, Op, pos); var s_F:M_Port, s_Op:Ot_Port, s_pos:Position in OT (Op, ?s_F, ?s_Op, ?s_pos); S (ot_end, car, pos); State := any VehicleState where (State == VehicleInit) or (State == Server); B := F; F := s_F; Op := s_Op; pos := s_pos end var end select [] -- We ignore "old" confirmation messages M (F, rcv, p_ot_conf_ok) -- State remains equal to Client end select | Server -> M (B, rcv, p_ot_req) where pos <> Tail; State := Server_Query | Server_Query -> S (ot_ind, car, pos); select S (ot_resp_no, car, pos); State := Server [] S (ot_resp_ok, car, pos); State := Server_Answer end select | Server_Answer -> select M (B, snd, p_ot_conf_ok); State := Server_Ok [] M (B, rcv, p_ot_req); State := Server_Query end select | Server_Ok -> select var c_B:M_Port, c_Op:Ot_Port, c_pos:Position in OT (Op, ?c_B, F, ?c_Op, Op, ?c_pos, pos); State := any VehicleState where (State == VehicleInit) or (State == Server); F := B; B := c_B; Op := c_Op; pos := c_pos end var [] M (B, rcv, p_ot_req); State := Server_Query end select end case end loop end var end process ------------------------------------------------------------------------------- end module