(* TMDL-to-LOTOS Compiler, version 0.9. *) specification Map5[Answer, BusyTone, Connected, Dial, ErrorDial, HangUp, NoAnswer, OffHook, Ring, Tone, WrongNumber]:noexit library Boolean, NaturalNumber endlib (* Tag ADT definition *) type Tag is Boolean, NaturalNumber sorts Tag opns dummy_val, OK, TOut : -> Tag N : Tag -> Nat _eq_, _ne_ : Tag, Tag ->Bool eqns forall x, y: Tag ofsort Nat N(dummy_val)= 0; (* dummy value *) N(OK) = Succ(N(dummy_val)); N(TOut) = Succ(N(OK)); ofsort Bool x eq y = N(x) eq N(y); x ne y = not(x eq y); endtype behaviour hide AllowHangUp, AskAnswer, Disconnected, EndConnect, EndDial, EndRing, GiveTone, GotAnswer, GotDial in ( ( ConnectionPhase[AllowHangUp, AskAnswer, BusyTone, Connected, EndConnect, EndDial, EndRing, ErrorDial, GiveTone, GotAnswer, GotDial, NoAnswer, OffHook, WrongNumber] |[AllowHangUp, EndConnect]| Disconnecting[AllowHangUp, Disconnected, EndConnect, EndDial, EndRing, HangUp] ) |[AskAnswer, EndDial, EndRing, GiveTone, GotAnswer, GotDial]| ( Answering[Answer, AskAnswer, EndRing, GotAnswer, Ring] ||| Dialing[Dial, EndDial, GiveTone, GotDial, Tone] ) ) where process ConnectionPhase[AllowHangUp, AskAnswer, BusyTone, Connected, EndConnect, EndDial, EndRing, ErrorDial, GiveTone, GotAnswer, GotDial, NoAnswer, OffHook, WrongNumber]:noexit := hide CheckDB, RegInit, Sync_Time_1, Sync_Time_3, TimeOut_0, TimeOut_2 in ( OffHook; ( RegInit; AllowHangUp; GiveTone; ( TimeOut_0; (* Timeout occured *) Sync_Time_1 ! TOut; stop [] GotDial; (* Event occured *) Sync_Time_1 ! OK; stop ) |[Sync_Time_1]| Sync_Time_1 ? TimeGotDial:Tag; ( ( [TimeGotDial eq TOut]-> EndDial; (* Abort event *) ErrorDial; stop (* No recursion *) ) [] ( [TimeGotDial eq OK]-> CheckDB; ( ( WrongNumber; stop (* No recursion *) ) [] ( BusyTone; stop (* No recursion *) ) [] ( AskAnswer; ( TimeOut_2; (* Timeout occured *) Sync_Time_3 ! TimeGotDial ! TOut; stop [] GotAnswer; (* Event occured *) Sync_Time_3 ! TimeGotDial ! OK; stop ) |[Sync_Time_3]| Sync_Time_3 ? TimeGotDial:Tag ? TimeGotAnswer:Tag; ( ( [TimeGotAnswer eq TOut]-> EndRing; (* Abort event *) NoAnswer; stop (* No recursion *) ) [] ( [TimeGotAnswer eq OK]-> Connected; stop (* No recursion *) ) ) ) ) ) ) ) ) [> endconnect; ConnectionPhase[AllowHangUp, AskAnswer, BusyTone, Connected, EndConnect, EndDial, EndRing, ErrorDial, GiveTone, GotAnswer, GotDial, NoAnswer, OffHook, WrongNumber] endproc (* Timethread ConnectionPhase *) (*********************************************) process Disconnecting[AllowHangUp, Disconnected, EndConnect, EndDial, EndRing, HangUp]:noexit := hide Sync_And_4 in AllowHangUp; ( HangUp; ( ( EndConnect; (* Abort event *) Sync_And_4;stop ) |[Sync_And_4]| ( EndDial; (* Abort event *) Sync_And_4;stop ) |[Sync_And_4]| ( EndRing; (* Abort event *) Sync_And_4;stop ) ) |[Sync_And_4]| Sync_And_4; Disconnected; Disconnecting[AllowHangUp, Disconnected, EndConnect, EndDial, EndRing, HangUp] (* End recursion *) ) endproc (* Timethread Disconnecting *) (*********************************************) process Dialing[Dial, EndDial, GiveTone, GotDial, Tone]:noexit := ( GiveTone; ( Tone; Dial; GotDial; stop (* No recursion *) ) ) [> enddial; Dialing[Dial, EndDial, GiveTone, GotDial, Tone] endproc (* Timethread Dialing *) (*********************************************) process Answering[Answer, AskAnswer, EndRing, GotAnswer, Ring]:noexit := ( AskAnswer; ( Ring; Answer; GotAnswer; stop (* No recursion *) ) ) [> endring; Answering[Answer, AskAnswer, EndRing, GotAnswer, Ring] endproc (* Timethread Answering *) endspec (* Map Map5 *)