(* TMDL-to-LOTOS Compiler, version 0.9. *) specification Map2[BusyTone, Dial, OffHook, Tone]: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 ( ConnectionPhase[BusyTone, Dial, OffHook, Tone] ) where process ConnectionPhase[BusyTone, Dial, OffHook, Tone]:noexit := hide CheckDB, RegInit in OffHook; ( RegInit; Tone; Dial; CheckDB; BusyTone; stop (* No recursion *) ) endproc (* Timethread ConnectionPhase *) endspec (* Map Map2 *)