(* TMDL-to-LOTOS Compiler, version 0.9. *)

specification TaxiCompany[Tdest, Tnew]:noexit

library
   Boolean, NaturalNumber
endlib

(* Tag ADT definition *)
type Tag is Boolean, NaturalNumber
sorts Tag
opns dummy_val : -> Tag
     N : Tag -> Nat
     _eq_, _ne_ : Tag, Tag ->Bool
eqns forall x, y: Tag
     ofsort Nat
     N(dummy_val)= 0;   (* dummy value *)
     ofsort Bool
     x eq y = N(x) eq N(y);
     x ne y = not(x eq y);
endtype

behaviour

hide Cin, Cout, DaskC, Din, Dout, Phangar, Pready, TCride, TgetinC, TgetoffP, TgetonP, TgetoutC, TPFlight, TPhoneD in

   (
      Traveler[TCride, Tdest, TgetinC, TgetoffP, TgetonP, TgetoutC, Tnew, TPflight, TphoneD]
      |[TCride, TgetinC, TgetoffP, TgetonP, TgetoutC, TPflight, TphoneD]|
      (
         Plane[Phangar, Pready, TgetoffP, TgetonP, TPflight]
         |||
         (
            Dispatcher[DaskC, Din, Dout, TphoneD]
            |[DaskC]|
            Cab[Cin, Cout, DaskC, TCride, TgetinC, TgetoutC]
         )
      )
   )

where

   process Traveler[TCride, Tdest, TgetinC, TgetoffP, TgetonP, TgetoutC, Tnew, TPflight, TphoneD]:noexit :=

   hide Tairport in

      Tnew;
      (
         (
            TphoneD; stop
            |||
            TgetinC;
            TCride;
            TgetoutC;
            Tairport;
            TgetonP;
            TPflight;
            TgetoffP;
            Tdest; Traveler[TCride, Tdest, TgetinC, TgetoffP, TgetonP, TgetoutC, Tnew, TPflight, TphoneD]  (* End recursion *)
         )
      )
   endproc  (* Timethread Traveler *)

   (*********************************************)

   process Dispatcher[DaskC, Din, Dout, TphoneD]:noexit :=

   hide Dfillstats, DlookforC, Dready in

      Din;
      (
         (
            Loop_0[DaskC, Din, Dout, TphoneD, Dfillstats, DlookforC, Dready]>>
            Dout; Dispatcher[DaskC, Din, Dout, TphoneD]  (* End recursion *)
         )
      )

   where
      process Loop_0[DaskC, Din, Dout, TphoneD, Dfillstats, DlookforC, Dready] : exit :=
         TphoneD;
         DlookforC;
         DaskC;
         Dfillstats;
         (
            (
               Dready;
               Loop_0[DaskC, Din, Dout, TphoneD, Dfillstats, DlookforC, Dready]
            )
            []
            (
                     exit  (* Exit Loop *)
            )
         )
      endproc  (* Loop_0 *)

   endproc  (* Timethread Dispatcher *)

   (*********************************************)

   process Cab[Cin, Cout, DaskC, TCride, TgetinC, TgetoutC]:noexit :=

   hide Cgarage, CgoD in

      Cin;
      (
         (
            Loop_1[Cin, Cout, DaskC, TCride, TgetinC, TgetoutC, Cgarage, CgoD]>>
            Cgarage;
            Cout; Cab[Cin, Cout, DaskC, TCride, TgetinC, TgetoutC]  (* End recursion *)
         )
      )

   where
      process Loop_1[Cin, Cout, DaskC, TCride, TgetinC, TgetoutC, Cgarage, CgoD] : exit :=
         DaskC;
         TgetinC;
         TCride;
         TgetoutC;
         (
            (
               CgoD;
               Loop_1[Cin, Cout, DaskC, TCride, TgetinC, TgetoutC, Cgarage, CgoD]
            )
            []
            (
                     exit  (* Exit Loop *)
            )
         )
      endproc  (* Loop_1 *)

   endproc  (* Timethread Cab *)

   (*********************************************)

   process Plane[Phangar, Pready, TgetoffP, TgetonP, TPflight]:noexit :=
      Pready;
      (
         TgetonP;
         TPflight;
         TgetoffP;
         Phangar; Plane[Phangar, Pready, TgetoffP, TgetonP, TPflight]  (* End recursion *)
      )
   endproc  (* Timethread Plane *)

endspec (* Map TaxiCompany *)