specification overtaking [S]:noexit

(* ====================================================================== *)
(* Type definitions *)

library Boolean, NaturalNumber endlib

type CarId is 
   sorts CarId
   opns
        volvo (*! constructor *),
        saab (*! constructor *),
        bmw (*! constructor *) :-> CarId
endtype

(* Position type *)

type Position is Boolean, NaturalNumber 
   sorts Position
   opns
        Head (*! constructor *),
        Middle (*! constructor *),
        Tail (*! constructor *) : -> Position
        ord (*! implementedby ORD_Position *) : Position -> Nat
        _<>_ (*! implementedby NE_Position *) : Position, Position -> Bool
   eqns
        forall x, y, z  : Position
        ofsort Nat
                ord (Tail)   = 0;
                ord (Middle) = succ (0);
                ord (Head)   = succ (succ (0));
        ofsort Bool
                x <> y = ord(x) ne ord(y);
endtype

(* Type to specify direction of PDUs being sent *)

type SENDdirection is 
   sorts SENDdirection
   opns
        snd (*! constructor *),
        rcv (*! constructor *) :-> SENDdirection
endtype

(* Service Primitives *)

type SAPsort is
   sorts SAPsort
   opns
        ot_req (*! constructor *),
        ot_ind (*! constructor *),
        ot_begin (*! constructor *),
        ot_end (*! constructor *),
        ot_resp_no (*! constructor *),
        ot_resp_ok (*! constructor *),
        ot_conf_ok (*! constructor *) :-> SAPsort
endtype

(* Protocol Data Units *)

type PDUSORT is
   sorts PDUsort
   opns
        p_ot_req (*! constructor *),
        p_ot_conf_ok (*! constructor *) : -> PDUsort
endtype

(* Port type for communication medium *)

type M_Port is Boolean
   sorts M_Port
   opns
        F_Tail (*! constructor *),
        F_Middle (*! constructor *),
        F_Head (*! constructor *),
        B_Tail (*! constructor *),
        B_Middle (*! constructor *),
        B_Head (*! constructor *) :-> M_Port
endtype

(* Port type for overtaking communication medium *)

type Ot_Port is
   sorts Ot_Port
   opns
        ot_Tail (*! constructor *),
        ot_Middle (*! constructor *),
        ot_Head (*! constructor *) :-> Ot_Port
endtype

(* ====================================================================== *)
(* Behavioural specification *)

behaviour
        hide M, OT in
        (
        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)
        )
                |[M, OT]|
        (
        Medium [M]
                |||
        Overtake_Medium [OT]
        )

where

(* ---------------------------------------------------------------------- *)
(* Lossy Point-to-Point medium *)

process Medium [M]:noexit :=
        M_Channel [M] (F_Tail, B_Middle) ||| M_Channel [M] (F_Middle, B_Head)
endproc

process M_Channel [M] (P1:M_Port, P2:M_Port):noexit :=
        hide medium_loss in
           M !P1 !snd ?pdu:PDUsort;
                (   M !P2 !rcv !pdu;  M_Channel [M] (P1, P2)
                 [] medium_loss; M_Channel [M] (P1, P2))
        [] M !P2 !snd ?pdu:PDUsort;
                (   M !P1 !rcv !pdu;  M_Channel [M] (P1, P2)
                 [] medium_loss; M_Channel [M] (P1, P2))
endproc

(* ---------------------------------------------------------------------- *)
(* Perfect Overtaking medium *)

process Overtake_Medium [OT]:noexit :=
        Ot_Channel [OT] (ot_Tail, ot_Middle)
                |||
        Ot_Channel [OT] (ot_Middle, ot_Head)
endproc

process Ot_Channel [OT] (P1:Ot_Port, P2:Ot_Port):noexit :=
        OT !P1 ?c_B:M_Port ?c_Op:Ot_Port ?c_pos:Position;
        OT !P2 !c_B ?s_F:M_Port !c_Op ?s_Op:Ot_Port !c_pos ?s_pos:Position;
        OT !P1 !s_F !s_Op !s_pos;
        Ot_Channel [OT] (P1, P2)
endproc

(* ---------------------------------------------------------------------- *)
(* Vehicle *)

process Vehicle [S, M, OT] (F:M_Port, B:M_Port, Op:Ot_Port, pos:Position, car:CarId):noexit :=
           S !ot_req !car !pos [pos <> Head]; Client [S, M, OT] (F, B, Op, pos, car)
        [] Server [S, M, OT] (F, B, Op, pos, car)
endproc

(* Client *)

process Client [S, M, OT] (F:M_Port, B:M_Port, Op:Ot_Port, pos:Position, car:CarId):noexit :=
        hide client_timer in
           M !F !snd !p_ot_req;
                ((* time out *)
                    client_timer !car;
                        Client [S, M, OT] (F, B, Op, pos, car)
                 [] (* or positive acknowledgement *)
                    M !F !rcv !p_ot_conf_ok;
                        (* Overtaking starts! *)
                        S !ot_begin !car !pos;
                        OT !Op !B !Op !pos;
                        OT !Op ?s_F:M_Port ?s_Op:Ot_Port ?s_pos:Position;
                        S !ot_end !car !pos;
                        Vehicle [S, M, OT] (s_F, F, s_Op, s_pos, car))

        (* We ignore "old" confirmation messages *)
        [] M !F !rcv !p_ot_conf_ok; Client [S, M, OT] (F, B, Op, pos, car)
endproc

(* Server *)

process Server [S, M, OT] (F:M_Port, B:M_Port, Op:Ot_Port, pos:Position, car:CarId):noexit :=
        M !B !rcv !p_ot_req [pos <> Tail];
                Server_Query [S, M, OT] (F, B, Op, pos, car)
endproc

process Server_Query [S, M, OT] (F:M_Port, B:M_Port, Op:Ot_Port, pos:Position, car:CarId):noexit :=
        S !ot_ind !car !pos; ( S !ot_resp_no !car !pos; Server [S, M, OT] (F, B, Op, pos, car)
                        [] S !ot_resp_ok !car !pos;
                           Server_Answer [S, M, OT] (F, B, Op, pos, car))
endproc

process Server_Answer [S, M, OT] (F:M_Port, B:M_Port, Op:Ot_Port, pos:Position, car:CarId):noexit :=
           M !B !snd !p_ot_conf_ok; Server_Ok [S, M, OT] (F, B, Op, pos, car)
        [] M !B !rcv !p_ot_req; Server_Query [S, M, OT] (F, B, Op, pos, car)
endproc

process Server_Ok [S, M, OT] (F:M_Port, B:M_Port, Op:Ot_Port, pos:Position, car:CarId):noexit :=
        OT !Op ?c_B:M_Port !F ?c_Op:Ot_Port !Op ?c_pos:Position !pos;
                 Vehicle [S, M, OT] (B, c_B, c_Op, c_pos, car)
        [] M !B !rcv !p_ot_req; Server_Query [S, M, OT] (F, B, Op, pos, car)
endproc

endspec