(* 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 *)