newtrav.lot


LOTOS Specification

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


List of Processes


List of Types


HTML vertion by lot2html (ver. 0.1), Fri Sep 6 11:58:47 1996