(************************************************************************) (* Specification of the Telephone System, modelling the system *) (* described in "The DMS-100 Business Set User's Manual", *) (* Bell Canada Inc. (1988) *) (* *) (* This specification was written by Rezki Boumezbeur as part of *) (* his Master's Thesis at the University of Ottawa (1991). *) (************************************************************************) specification Sample_Telephone [user] :noexit library NaturalNumber,Boolean endlib type Enriched_Nat is NaturalNumber opns _ == _ : Nat, Nat -> Bool _ <> _ : Nat, Nat -> Bool eqns forall m,n:Nat ofsort Bool m == n = m eq n; m <> n = not(m eq n) endtype (* Enriched_Nat *) type Digits is Enriched_Nat,Boolean sorts Digit opns 0,1,2,3,4,5,6,7,8,9 : -> Digit to_nat : Digit -> Nat _ == _ : Digit, Digit -> Bool _ <> _ : Digit, Digit -> Bool eqns forall N,M:Digit ofsort Nat to_nat(0) = 0; to_nat(1) = Succ(to_nat(0)); to_nat(2) = Succ(to_nat(1)); to_nat(3) = Succ(to_nat(2)); to_nat(4) = Succ(to_nat(3)); to_nat(5) = Succ(to_nat(4)); to_nat(6) = Succ(to_nat(5)); to_nat(7) = Succ(to_nat(6)); to_nat(8) = Succ(to_nat(7)); to_nat(9) = Succ(to_nat(8)); ofsort Bool M == N = to_nat(M) == to_nat(N); M <> N = to_nat(M) <> to_nat(N); endtype (* Digits *) type Phone_Num is Digits,Boolean sorts Phone opns num : Digit,Digit,Digit,Digit,Digit,Digit,Digit -> Phone num : Digit,Digit,Digit,Digit,Digit,Digit -> Phone num : Digit,Digit,Digit,Digit,Digit -> Phone num : Digit,Digit,Digit,Digit -> Phone num : Digit,Digit,Digit -> Phone num : Digit,Digit -> Phone num : Digit -> Phone _ == _ : Phone, Phone -> Bool _ <> _ : Phone, Phone -> Bool eqns forall D11,D12,D13,D14,D15,D16,D17,D21,D22, D23,D24,D25,D26,D27 :Digit, M,N:Phone ofsort Bool (D17 == D27) and (D16 == D26) and (D15 == D25) and (D14 == D24) and (D13 == D23) and (D12 == D22) and (D11 == D21) => num(D17,D16,D15,D14,D13,D12,D11) == num(D27,D26,D25,D24,D23,D22,D21) = true; (D17 <> D27) or (D16 <> D26) or (D15 <> D25) or (D14 <> D24) or (D13 <> D23) or (D12 <> D22) or (D11 <> D21) => num(D17,D16,D15,D14,D13,D12,D11) == num(D27,D26,D25,D24,D23,D22,D21) = false; M <> N = not(M == N); ofsort Phone num(D17) = num(0,0,0,0,0,0,D17); num(D16,D17) = num(0,0,0,0,0,D16,D17); num(D15,D16,D17) = num(0,0,0,0,D15,D16,D17); num(D14,D15,D16,D17) = num(0,0,0,D14,D15,D16,D17); num(D13,D14,D15,D16,D17) = num(0,0,D13,D14,D15,D16,D17); num(D12,D13,D14,D15,D16,D17) = num(0,D12,D13,D14,D15,D16,D17); endtype (* Phone_Num *) type Phoneset is Phone_Num,Boolean sorts Phoneset opns empty : -> Phoneset insert: Phone,Phoneset -> Phoneset remove: Phone,Phoneset -> Phoneset isin : Phone,Phoneset -> Bool notin : Phone,Phoneset -> Bool is_empty : Phoneset -> Bool head : Phoneset -> Phone tail : Phoneset -> Phoneset eqns forall x,y:Phone, s:Phoneset ofsort Phoneset remove(x,empty) = empty ; insert(x,insert(x,s)) = insert(x,s); remove(x,insert(x,s)) = s; remove(x,insert(x,empty))= empty ; x <> y => remove(x,insert(y,s)) = insert(y,remove(x,s)); tail(insert(x,s)) = s; tail(empty) = empty; ofsort Bool isin(x,empty) = false; isin(x,insert(y,s))= (x == y) or (isin(x,s)); isin(x,remove(x,s))= false; x <> y => isin(x,remove(y,s))= isin(x,s); notin(x,s) = not(isin(x,s)); is_empty(empty) = true; is_empty(insert(x,s))= false; ofsort Phone head(insert(x,s))= x; endtype (* Phoneset *) type PhonePair is Phone_Num, Boolean sorts PhonePair opns ForPair : Phone,Phone -> PhonePair _==_,_<>_: PhonePair,PhonePair -> Bool eqns forall f1,f2,f3,f4:Phone ofsort Bool ForPair(f1,f2) == ForPair(f3,f4)= (f1 == f3) and (f2 == f4); ForPair(f1,f2) <> ForPair(f3,f4)= (f1 <> f3) or (f2 <> f4); endtype (* PhonePair *) type ForwardPairSet is PhonePair sorts ForwardPairSet opns nopair: -> ForwardPairSet insert: PhonePair,ForwardPairSet-> ForwardPairSet remove: PhonePair,ForwardPairSet-> ForwardPairSet isin : PhonePair,ForwardPairSet-> Bool notin : PhonePair,ForwardPairSet-> Bool ForwardTo: Phone,ForwardPairSet -> Phone eqns forall x,y:PhonePair,s:ForwardPairSet,p1,p2,p3:Phone ofsort ForwardPairSet insert(x,insert(x,s)) = insert(x,s); remove(x,insert(x,s)) = s; remove(x,insert(x,nopair))= nopair ; x <> y => remove(x,insert(y,s))= insert(y,remove(x,s)); ofsort Bool isin(x,nopair) = false; isin(x,insert(y,s))= (x == y) or (isin(x,s)); isin(x,remove(x,s))= false; x <> y => isin(x,remove(y,s)) = isin(x,s); notin(x,s) = not(isin(x,s)); ofsort Phone ForwardTo(p1,insert(ForPair(p1,p2),s))= p2; p1 <> p2 => ForwardTo(p1,insert(ForPair(p2,p3),s))= ForwardTo(p1,s); endtype (* ForwardPairSet *) type key is Boolean sorts key opns OffHook,DialKs,SendVo,HangUp,ReleaseK, HoldK,RiAgK,TransK,ConfK,ForK :-> key _==_,_<>_ : key,key -> Bool eqns forall x,y:key ofsort Bool HoldK == HoldK = true ;HoldK <> HoldK = false; HoldK == TransK= false;HoldK <> TransK= true ; HoldK == ConfK = false;HoldK <> ConfK = true ; TransK== HoldK = false;TransK<> HoldK = true ; TransK== TransK= true ;TransK<> TransK= false; TransK== ConfK = false;TransK<> ConfK = true ; ConfK == HoldK = false;ConfK <> HoldK = true ; ConfK == TransK= false;ConfK <> TransK= true ; ConfK == ConfK = true ;ConfK <> ConfK = false; endtype (* key *) type tone is sorts tone opns Busy_T,Dito_T,Oofs_T, Rano_T,Ring_T :-> tone endtype (* tone *) type signal is Boolean sorts signal opns COAT,CONF,CONFN,CONN,CORE, HOLD,HOLDN,ONRI,RECO,RIAG, TRAN,TRANN,VOICE,DSIN :-> signal _==_,_<>_ : signal,signal -> Bool eqns forall x,y:signal ofsort Bool HOLDN == HOLDN = true ;HOLDN <> HOLDN = false; HOLDN == TRANN = false;HOLDN <> TRANN = true ; HOLDN == CONFN = false;HOLDN <> CONFN = true ; TRANN == HOLDN = false;TRANN <> HOLDN = true ; TRANN == TRANN = true ;TRANN <> TRANN = false; TRANN == CONFN = false;TRANN <> CONFN = true ; CONFN == HOLDN = false;CONFN <> HOLDN = true ; CONFN == TRANN = false;CONFN <> TRANN = true ; CONFN == CONFN = true ;CONFN <> CONFN = false; endtype (* signal *) type special_signal is sorts special_signal opns BUSY,DISC,DITO,FORW,OOFS, RANO,RING :-> special_signal endtype (* special_signal *) (* Behavioural Expressions *) behaviour hide line in Multi_Connections [user,line] |[line]| System_Network [user,line](empty,empty,empty,nopair) where process Multi_Connections [user,line]:noexit:= One_Connection [user,line] ||| i ; Multi_Connections [user,line] where process One_Connection [user,line]:noexit:= Subscribers [user,line] |[line]| Connection_Handler [line] where process Subscribers [user,line]:noexit:= Origination_Side [user,line] ||| Destination_Side [user,line] where process Origination_Side [user,line]:noexit:= user ?N:Phone !OffHook ; (line !N !DITO ; user !N !Dito_T ; ((user !N !DialKs ?CN:Phone ; line !CN !CORE ; exit [> Hang_Up [user,line](N) ) >> line !N !CONN ; User_Talk [user,line](N) [] line ?RN:Phone !OOFS ; user !N !Oofs_T ; Hang_Up [user,line](N) [] line ?RN:Phone !BUSY ?Set:Phoneset ; user !N !Busy_T ; (Hang_Up [user,line](N) [] [N <> RN] -> user !N !RiAgK ; line !N !RIAG ; Ring_Again_Feature [user,line](N,RN) )) [] line !N !BUSY !empty ; user !N !Busy_T ; user !N !HangUp; stop [] line !N !OOFS; user !N !Oofs_T ; user !N !HangUp; stop ) where process Ring_Again_Feature [user,line](N,RN:Phone):noexit:= user !N !HangUp ; (user !N !RiAgK; line !N !DISC ; stop [] line !N !RANO !RN ; user !N !Rano_T ; (user !N !OffHook ; line !N !RIAG ; (line !N !CONN ; User_Talk [user,line](N) [] line !RN !BUSY ?Set:Phoneset ; user !N !Busy_T ; Ring_Again_Feature [user,line](N,RN) ) [] user !N !RiAgK; line !N !DISC ; stop )) endproc (* Ring_Again_Feature *) endproc (* Origination_Side *) process Destination_Side [user,line]:noexit:= (line ?CN:Phone !COAT ; exit(CN) [> stop ) >> accept CN:Phone in Destination_Phone_Ring [user,line](CN) [] Call_Forwarded [user,line](CN) where process Call_Forwarded [user,line](CN:Phone):noexit:= line !CN !FORW ; line ?FN:Phone !FORW ; (line !FN !CORE ; line !FN !COAT ; exit(FN) [> stop ) >> accept FN:Phone in Destination_Phone_Ring [user,line](FN) [] Call_Forwarded [user,line](FN) endproc (* Call_Forwarded *) process Destination_Phone_Ring [user,line](CN:Phone):noexit:= line !CN !RING ; user !CN !Ring_T ; (Ringing [line](CN) [> (user !CN !OffHook ; line !CN !CONN ; User_Talk [user,line](CN) [] line !CN !DISC ; stop ) ) endproc (* Destination_Phone_Ring *) endproc (* Destination_Side *) process User_Talk [user,line](N:Phone):noexit:= Conversation [user,line](N) [> Feature [user,line](N,HoldK,HOLD,HOLDN) [] Feature [user,line](N,TransK,TRAN,TRANN) [] Feature [user,line](N,ConfK,CONF,CONFN) [] User_Termination [user,line](N) endproc (* User_Talk *) process More_Conference [user,line](N:Phone):noexit:= Conversation [user,line](N) [> Feature [user,line](N,ConfK,CONF,CONFN) [] Hang_Up [user,line](N) endproc (* More_Conference *) process Feature [user,line](N:Phone,Key:key,Signal,Note:signal):noexit:= user !N !Key ; (Initiate_Feature [user,line](N,Key,Signal) ||| Additional_Subscriber [user,line](Key) ) [] Party_On_Hold [user,line](N,Note) endproc (* Feature *) process Initiate_Feature [user,line](N:Phone,Key:key,Signal:signal):noexit:= line !N !Signal ; (user !N !DialKs ?TN:Phone ; line !TN !CORE ; exit [> User_Recon [user,line](N,Key) ) >> line ?TN:Phone !BUSY ?Set:Phoneset ; user !N !Busy_T ; User_Recon [user,line](N,Key) [] line ?TN:Phone !OOFS ; user !N !Oofs_T ; User_Recon [user,line](N,Key) [] line !N !CONN ; (Conversation [user,line](N) [> line !N !DSIN ; ([Key == TransK] -> user !N !TransK ; line !N !RECO ; User_Talk [user,line](N) [] [Key <> TransK] -> User_Recon [user,line](N,Key) ) [] [Key == TransK] -> (user !N !TransK ; line !N !RECO ; (Conversation [user,line](N) [> Hang_Up [user,line](N) [] line !N !DSIN ; User_Talk [user,line](N) ) [] user !N !ReleaseK ; Hang_Up [user,line](N) ) [] [Key <> TransK] -> User_Recon [user,line](N,Key) ) endproc (* Initiate_Feature *) process Additional_Subscriber [user,line](Key:key):noexit:= (line ?TN:Phone !COAT ; exit(TN) [> stop ) >> accept TN:Phone in New_Phone_Ring [user,line](Key,TN) [] New_Subscriber_Forward [user,line](Key,TN) where process New_Subscriber_Forward [user,line](Key:key,TN:Phone):noexit:= line !TN !FORW ; (line ?FN:Phone !FORW ; line !FN !CORE ; line !FN !COAT ; exit(FN) [> stop ) >> accept FN:Phone in New_Phone_Ring [user,line](Key,FN) [] New_Subscriber_Forward [user,line](Key,FN) endproc (* New_Subscriber_Forward *) process New_Phone_Ring [user,line](Key:key,TN:Phone):noexit:= line !TN !RING ; user !TN !Ring_T ; (Ringing [line](TN) [> user !TN !OffHook ; line !TN !CONN ; (Conversation [user,line](TN) [> Hang_Up [user,line](TN) [] [Key == ConfK] -> line !TN !RECO ; More_Conference [user,line](TN) [] [Key <> ConfK] -> line !TN !DSIN ; ([Key == TransK] -> User_Talk [user,line](TN) [] [Key == HoldK] -> Hang_Up [user,line](TN) ) ) [] line !TN !DISC ; stop ) endproc (* New_Phone_Ring *) endproc (* Additional_Subscriber *) process Party_On_Hold [user,line](N:Phone,Notify:signal):noexit:= line !N !Notify ; (line !N !RECO ; ([Notify == TRANN] -> (Conversation [user,line](N) [> line !N !DSIN ; User_Talk [user,line](N) [] Hang_Up [user,line](N) ) [] [Notify == CONFN] -> More_Conference [user,line](N) [] [Notify == HOLDN] -> User_Talk [user,line](N) ) [] line !N !DSIN ; line !N !RECO ; User_Talk [user,line](N) [] Hang_Up [user,line](N) ) endproc (* Party_On_Hold *) Process User_Recon [user,line](N:Phone,Key:key):noexit:= user !N !Key ; line !N !RECO ; ([Key <> ConfK] -> User_Talk [user,line](N) [] [Key == ConfK] -> More_Conference [user,line](N) ) endproc (* User_Recon *) process Conversation [user,line](N:Phone):noexit:= user !N !SendVo ; line !N !VOICE ; Conversation [user,line](N) endproc (* Conversation *) process User_Termination [user,line](N:Phone):noexit:= Hang_Up [user,line](N) [] line !N !DSIN ; Hang_Up [user,line](N) endproc (* User_Termination *) process Hang_Up [user,line](N:Phone):noexit:= user !N !HangUp ; line !N !DISC ; stop endproc (* Hang_Up *) endproc(* Subscribers *) process Connection_Handler [line]:noexit:= line ?N:Phone !DITO ; Control_Termination [line](N,empty) [] line ?N:Phone !BUSY !empty ; stop [] line ?N:Phone !OOFS ; stop where process Control_Termination [line](N:Phone,Set:Phoneset):noexit:= (line ?TN:Phone !CORE ; line !TN !COAT ; exit(TN) [> line !N !DISC ; stop ) >> accept TN:Phone in [notin(TN,Set)] -> line !TN !RING ; (Ringing [line](TN) [> (line !TN !CONN ; line !N !CONN ; Control_Conversation [line](N,TN) [] line !N !DISC ; line !TN !DISC ; stop ) ) [] [notin(TN,Set)] -> line !TN !FORW ; line ?FN:Phone !FORW ; Control_Termination [line](N,insert(TN,Set)) [] Unsuccessful_Termination [line](N,TN,Set) endproc (* Control_Termination *) process Unsuccessful_Termination [line](N,TN:Phone,Set:Phoneset):noexit:= line !TN !BUSY !Set ; (line !N !DISC ; stop [] line !N !RIAG; Control_RingAgain [line](N,TN,Set) ) [] line !TN !OOFS ; line !N !DISC ; stop where process Control_RingAgain [line](N,TN:Phone,Set:Phoneset):noexit:= (line !N !DISC ; stop [] [notin(TN,Set)] -> line !N !RANO !TN ; (line !N !RIAG ; ([notin(TN,Set)] -> line !TN !RING ; (Ringing [line](TN) [> (line !TN !CONN ; line !N !CONN ; Control_Conversation [line](N,TN) [] line !N !DISC ; line !TN !DISC ; stop ) ) [] line !TN !BUSY !Set ; Control_RingAgain [line](N,TN,Set) ) [] line !N !DISC ; stop ) ) endproc (* Control_RingAgain *) endproc (* Unsuccessful_Termination *) process Control_Conversation [line](N,RN:Phone):noexit:= Talking [line](N) ||| Talking [line](RN) [> Control_Feature [line](N,RN) [] Control_Feature [line](RN,N) where process Control_Feature [line](N,RN:Phone):noexit:= Control_Hold [line](N,RN) [] Control_Transfer [line](N,RN) [] Control_Conference [line](N,RN) [] Control_Disconnection [line](N,RN) where process Control_Hold [line](N,RN:Phone):noexit:= Control_Feature_Origination [line](N,RN,HOLD,HOLDN) >> accept TN:Phone in Control_Hold_Ring [line](N,RN,TN,empty) [] Control_Hold_Forward [line](N,RN,TN,empty) where process Control_Hold_Forward [line](N,RN,TN:Phone,Set:Phoneset):noexit:= Control_Forward_Origination [line](N,RN,TN,Set) >> accept FN:Phone,NewSet:Phoneset in Control_Hold_Ring [line](N,RN,FN,NewSet) [] Control_Hold_Forward [line](N,RN,FN,NewSet) endproc (* Control_Hold_Forward *) process Control_Hold_Ring [line](N,RN,TN:Phone,Set:Phoneset):noexit:= [notin(TN,Set)] -> line !TN !RING ; (Ringing [line](TN) [> line !TN !CONN ; line !N !CONN ; ((Talking [line](N) ||| Talking [line](TN) ) [> (line !N !RECO ; line !TN !DSIN ; line !TN !DISC ; (line !RN !RECO ; Control_Conversation [line](N,RN) [] Control_Disconnection [line](RN,N) ) [] line !TN !DISC ; line !N !DSIN ; Reconnection [line](N,RN) ) ) [] line !N !RECO ; line !TN !DISC ; (line !RN !RECO ; Control_Conversation [line](N,RN) [] Control_Disconnection [line](RN,N) ) ) [] Unsuccessful_Feature_Termination [line](N,RN,TN,Set) endproc (* Control_Hold_Ring *) endproc (* Control_Hold *) process Control_Transfer [line](N,RN:Phone):noexit:= Control_Feature_Origination [line](N,RN,TRAN,TRANN) >> accept TN:Phone in Control_Transfer_Ring [line](N,RN,TN,empty) [] Control_Transfer_Forward [line](N,RN,TN,empty) where process Control_Transfer_Forward [line](N,RN,TN:Phone,Set:Phoneset):noexit:= Control_Forward_Origination [line](N,RN,TN,Set) >> accept FN:Phone,NewSet:Phoneset in Control_Transfer_Ring [line](N,RN,FN,NewSet) [] Control_Transfer_Forward [line](N,RN,FN,NewSet) endproc (* Control_Transfer_Forward *) process Control_Transfer_Ring [line](N,RN,TN:Phone,Set:Phoneset):noexit:= [notin(TN,Set)] -> line !TN !RING ; (Ringing [line](TN) [> line !TN !CONN ; line !N !CONN ; (Talking [line](N) ||| Talking [line](TN) [> line !N !RECO ; (line !RN !RECO ; (Talking [line](N) ||| Talking [line](RN) ||| Talking [line](TN) [> (Special_Control [line](RN,TN,N) [] Special_Control [line](N,TN,RN) [] Special_Control [line](N,RN,TN) ) ) [] line !RN !DISC ; Control_Conversation [line](N,TN) ) [] line !TN !DISC ; line !N !DSIN ; Reconnection [line](N,RN) [] line !N !DISC ; line !TN !DSIN ; (line !RN !DSIN ; line !RN !RECO ; Control_Conversation [line](RN,TN) [] Control_Disconnection [line](RN,TN) ) ) [] line !N !RECO ; line !TN !DISC ; (line !RN !RECO ; Control_Conversation [line](N,RN) [] Control_Disconnection [line](RN,N) ) ) [] Unsuccessful_Feature_Termination [line](N,RN,TN,Set) endproc (* Control_Transfer_Ring *) endproc (* Control_Transfer *) process Special_Control [line](N1,N2,DN:Phone):noexit:= line !DN !DISC ; line !N1 !DSIN ; line !N2 !DSIN ; Control_Conversation [line](N1,N2) endproc (* Special_Control *) process Control_Conference [line](N,RN:Phone):noexit:= Control_Feature_Origination [line](N,RN,CONF,CONFN) >> accept TN:Phone in Control_Conference_Ring [line](N,RN,TN,empty) [] Control_Conference_Forward [line](N,RN,TN,empty) where process Control_Conference_Forward [line](N,RN,TN:Phone,Set:Phoneset):noexit:= Control_Forward_Origination [line](N,RN,TN,Set) >> accept FN:Phone,NewSet:Phoneset in Control_Conference_Ring [line](N,RN,FN,NewSet) [] Control_Conference_Forward [line](N,RN,FN,NewSet) endproc (* Control_Conference_Forward *) process Control_Conference_Ring [line](N,RN,TN:Phone,Set:Phoneset):noexit := [notin(TN,Set)] -> line !TN !RING ; (Ringing [line](TN) [> line !TN !CONN ; line !N !CONN ; (Talking [line](N) ||| Talking [line](TN) [> line !N !RECO ; (line !RN !RECO ; line !TN !RECO ; (On_Conference [line](N) ||| On_Conference [line](RN) ||| On_Conference [line](TN) ) [] line !RN !DISC ; Control_Conversation [line](N,TN) ) [] line !TN !DISC ; line !N !DSIN ; Reconnection [line](N,RN) ) [] line !N !RECO ; line !TN !DISC ; (line !RN !RECO ; Control_Conversation [line](N,RN) [] Control_Disconnection [line](RN,N) ) ) [] Unsuccessful_Feature_Termination [line](N,RN,TN,Set) endproc (* Control_Conference_Ring *) endproc (* Control_Conference *) process Control_Feature_Origination [line](N,RN:Phone,Sign,Note:signal):exit(Phone):= line !N !Sign ; line !RN !Note ; (line ?TN:Phone !CORE ; line !TN !COAT ; exit(TN) [> Reconnection [line](N,RN) ) endproc (* Control_Feature_Origination *) process Control_Forward_Origination [line](N,RN,TN:Phone,Set:Phoneset):exit(Phone,Phoneset):= [notin(TN,Set)] -> line !TN !FORW ; (line ?FN:Phone !FORW ; line !FN !CORE ; line !FN !COAT ; exit (FN,insert(TN,Set)) [> Reconnection [line](N,RN) ) endproc (* Control_Forward_Origination *) process Reconnection [line](N,RN:Phone):noexit:= line !N !RECO ; (line !RN !RECO ; Control_Conversation [line](N,RN) [] Control_Disconnection [line](RN,N) ) endproc (* Reconnection *) process Unsuccessful_Feature_Termination [line](N,RN,TN:Phone,Set:Phoneset):noexit:= line !TN !BUSY !Set ; Reconnection [line](N,RN) [] line !TN !OOFS ; Reconnection [line](N,RN) endproc (* Unsuccessful_Feature_Termination *) endproc (* Control_Feature *) endproc (* Control_Conversation *) process On_Conference [line](N:Phone):noexit:= Talking [line](N) [> line !N !DISC ; stop [] Add_Conf [line](N) endproc (* On_Conference *) process Add_Conf [line](N:Phone):noexit:= line !N !CONF ; (line ?TN:Phone !CORE ; line !TN !COAT ; exit(TN) [> line !N !RECO ; On_Conference [line](N) ) >> accept TN:Phone in Control_MoreConference_Ring [line](N,TN,empty) [] Control_MoreConference_Forward [line](N,TN,empty) where process Control_MoreConference_Forward [line](N,TN:Phone,Set:Phoneset):noexit:= [notin(TN,Set)] -> line !TN !FORW ; (line ?FN:Phone !FORW ; line !FN !CORE ; line !FN !COAT ; exit (FN,insert(TN,Set)) [> line !N !RECO ; On_Conference [line](N) ) >> accept FN:Phone,NewSet:Phoneset in Control_MoreConference_Ring [line](N,FN,NewSet) [] Control_MoreConference_Forward [line](N,FN,NewSet) endproc (* Control_MoreConference_Forward *) process Control_MoreConference_Ring [line](N,TN:Phone,Set:Phoneset):noexit:= [notin(TN,Set)] -> line !TN !RING ; (Ringing [line](TN) [> line !TN !CONN ; line !N !CONN ; (Talking [line](N) ||| Talking [line](TN) [> line !N !RECO ; line !TN !RECO ; (On_Conference [line](N) ||| On_Conference [line](TN) ) [] line !TN !DISC ; line !N !DSIN ; line !N !RECO ; On_Conference [line](N) ) [] line !N !RECO ; line !TN !DISC ; On_Conference [line](N) ) [] line !TN !BUSY !Set ; line !N !RECO ; On_Conference [line](N) [] line !TN !OOFS ; line !N !RECO ; On_Conference [line](N) endproc (* Control_MoreConference_Ring *) endproc (* Add_Conf *) process Talking [line](N:Phone):noexit:= line !N !VOICE ; Talking [line](N) endproc (* Talking *) process Control_Disconnection [line](N,RN:Phone):noexit:= line !N !DISC ; line !RN !DSIN ; line !RN !DISC ; stop endproc (* Control_Disconnection *) endproc (* Connection_Handler *) process Ringing [line](N:Phone):noexit:= line !N !ONRI ; Ringing [line](N) endproc (* Ringing *) endproc (* One_Connection *) endproc (* Multi_Connections*) process System_Network [user,line](BusySet,ServiceSet,ForwardSet:Phoneset,ForwardPairs:ForwardPairSet):noexit:= user ?N:Phone ; ([notin(N,ServiceSet)] -> System_Network [user,line](BusySet,insert(N,ServiceSet),ForwardSet,ForwardPairs) [] [isin(N,ServiceSet) and notin(N,BusySet)] -> System_Network [user,line](BusySet,remove(N,ServiceSet),ForwardSet,ForwardPairs) [] [isin(N,BusySet)] -> System_Network [user,line](BusySet,ServiceSet,ForwardSet,ForwardPairs) ) [] Forward_Feature [user,line](ServiceSet,BusySet,ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone ?sign:signal ; System_Network [user,line](BusySet,ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !DITO [ notin(N,BusySet) and isin(N,ServiceSet) ] ; System_Network [user,line](insert(N,BusySet),ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !RING [ notin(N,BusySet) and isin(N,ServiceSet) and notin(N,ForwardSet) ] ; System_Network [user,line](insert(N,BusySet),ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !BUSY ?Set:Phoneset [ isin(N,BusySet) or isin(N,Set) ] ; System_Network [user,line](BusySet,ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !OOFS [ notin(N,ServiceSet) ] ; System_Network [user,line](BusySet,ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !DISC [ isin(N,BusySet) ] ; System_Network [user,line](remove(N,BusySet),ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !RANO ?TN:Phone [ notin(TN,BusySet) ] ; System_Network [user,line](BusySet,ServiceSet,ForwardSet,ForwardPairs) [] line ?N:Phone !FORW [ isin(N,ForwardSet) and isin(N,ServiceSet) and notin(N,BusySet) ] ; line !ForwardTo(N,ForwardPairs) !FORW ; System_Network [user,line](BusySet,ServiceSet,ForwardSet,ForwardPairs) where process Forward_Feature [user,line](ServiceSet1,BusySet,ServiceSet,ForwardSet:Phoneset,ForwardPairs:ForwardPairSet):noexit:= [not(is_empty(ServiceSet1))] -> (Forward_Feature2[user,line](head(ServiceSet1),BusySet,ServiceSet,ForwardSet,ForwardPairs) [] Forward_Feature [user,line](tail(ServiceSet1),BusySet,ServiceSet,ForwardSet,ForwardPairs) ) where process Forward_Feature2 [user,line](N:Phone,BusySet,ServiceSet,ForwardSet:Phoneset,ForwardPairs:ForwardPairSet):noexit:= [notin(N,ForwardSet) and notin(N,BusySet)] -> user !N !ForK ?FN:Phone; System_Network [user,line](BusySet,ServiceSet,insert(N,ForwardSet),insert(ForPair(N,FN),ForwardPairs)) [] [isin(N,ForwardSet) and notin(N,BusySet) ] -> user !N !ForK; System_Network [user,line](BusySet,ServiceSet,remove(N,ForwardSet),remove(ForPair(N,ForwardTo(N,ForwardPairs)),ForwardPairs)) endproc (* Forward_Feature2 *) endproc (* Forward_Feature *) endproc (* System_Network *) endspec (* Sample_Telephone *)