specification POTS_System [S_Usr]:noexit (* written by Mohamed Faci and Bernard Stepien june 1989 *) library Set, Boolean, NaturalNumber endlib type NatSet00 is Set renamedby sortnames NatSet for Set endtype type NatSet0 is NatSet00 actualizedby NaturalNumber using sortnames Nat for Element Bool for FBool endtype type NatSet is NatSet0 endtype type signal is Boolean sorts Sig_Sort opns Offhook_To_Call, Offhook_To_Ans, Hangs_Up, Sends_Msg, Rcves_Msg, Ring, Echo_Ring, Dials, Gets_Tone, Busy_Signal :-> Sig_Sort endtype behaviour ( Connections[S_Usr] || Manage_Users_List [S_Usr]({} of NatSet, {} of NatSet) ) where process Talk_To_Both [S_Usr](Caller, Called : Nat) :noexit:= ( Talk1[S_Usr](Caller, Called) ||| Talk2[S_Usr](Called, Caller) ) endproc (* Talk_To_Both *) process Listen[G_Usr] (This_Side, That_Side : Nat) :noexit:= G_Usr ! This_Side ! Rcves_Msg; stop (* [G_Usr](This_Side, That_Side) *) endproc (* Listen *) process Talk_Listen [S_Usr](Caller, Called : Nat) :noexit:= ( Talk1[S_Usr](Caller, Called) ||| Listen[S_Usr](Called, Caller) ) endproc (* Talk_Listen *) process Talk1[G_Usr] (Caller, Called : Nat) :noexit:= G_Usr ! Caller ! Sends_Msg; Talk_Listen [G_Usr](Caller, Called) endproc (* Talk1 *) process Talk2[G_Usr] (Caller, Called : Nat) :noexit:= G_Usr ! Caller ! Sends_Msg; Talk_Listen [G_Usr](Caller, Called) endproc (* Talk2 *) process User_Talk[G_Usr] (Caller : Nat) :noexit:= G_Usr ! Caller ! Sends_Msg; User_Talk [G_Usr](Caller) endproc (* User_Talk *) process User_Listen[G_Usr] (This_Side : Nat) :noexit:= G_Usr ! This_Side ! Rcves_Msg; User_Listen[G_Usr](This_Side) endproc (* User_Listen *) process User_Talk_Or_Listen[G_Usr] (This_Side : Nat) :noexit:= G_Usr ! This_Side ! Sends_Msg; User_Talk[G_Usr](This_Side) ||| G_Usr ! This_Side ! Rcves_Msg; User_Listen[G_Usr](This_Side) endproc (* User_Talk_Or_Listen *) process Connections[S_Usr]:noexit:= ( Single_Connection[S_Usr] ||| i; Connections[S_Usr] ) where process Single_Connection[S_Usr]:noexit:= ( ( Caller[S_Usr] ||| Called [S_Usr] ) || ( Controller[S_Usr] ) ) where process Caller[S_Usr]:noexit:= ( Pick_Up_Phone_To_Call [S_Usr] >> accept Caller : Nat in ( Establish_Call [S_Usr](Caller) >> User_Talk_Or_Listen [S_Usr](Caller) ) [> User_Hang_Up[S_Usr](Caller) ) where process Establish_Call[S_Usr](Caller :Nat) :exit:= ( ( Request_Call [S_Usr](Caller) >> accept Called : Nat in (* DELETE ----------------- DELETE*) Response_Call[S_Usr](Caller) ) ) where process Response_Call [S_Usr](Caller : Nat) : exit:= ( S_Usr ! Caller ! Echo_Ring; exit (* OR busy alternative *) [] S_Usr ! Caller ! Busy_Signal; stop ) endproc (* Response_Call *) endproc (* Establish_Call *) endproc (* Caller *) process Called [S_Usr] : noexit:= ( Phone_Waits_Ring [S_Usr] >> accept Called: Nat in ( Phone_Answer [S_Usr](Called) >> ( User_Talk_Or_Listen [S_Usr](Called) [> User_Hang_Up [S_Usr](Called) ) ) ) where process Phone_Waits_Ring [S_Usr] :exit (Nat) := ( S_Usr ?Called:Nat !Ring; exit(Called) ) endproc (* Phone_Waits_Ring *) endproc (* Called *) process Controller[S_Usr]: noexit:= ( Pick_Up_Phone_To_Call [S_Usr] >> accept Caller : Nat in Connection_Phase [S_Usr] (Caller) >> accept Called: Nat in Talk_To_Both[S_Usr](Caller, Called) ) [> Controller_Hang_Up[S_Usr] where process Connection_Phase [S_Usr]( Caller: Nat) : exit(Nat) := ( ( Request_Call [S_Usr](Caller) >> accept Called : Nat in ( ( Phone_Rings [S_Usr](Caller, Called) >> ( Phone_Echo_Rings [S_Usr](Caller) >> Phone_Answer [S_Usr](Called) >> exit(Called) ) ) ) ) ) endproc (* Connection_Phase *) endproc (* Controller *) endproc (* Single_Connection *) process Phone_Rings [G_Usr](Caller, Called:Nat) :exit := ( G_Usr !Called !Ring; exit [] G_Usr ! Caller ! Busy_Signal; stop ) endproc (* Phone_Rings *) process Phone_Echo_Rings [G_Usr](Caller:Nat) :exit := ( G_Usr !Caller !Echo_Ring; exit ) endproc (* Phone_Echo_Rings *) process Pick_Up_Phone_To_Call [G_Usr] :exit(Nat):= ( G_Usr ?Caller:Nat !Offhook_To_Call; exit (Caller) ) endproc (* Pick_Up_Phone_To_Call *) process Phone_Answer [S_Usr](Called : Nat) :exit := ( S_Usr ! Called ! Offhook_To_Ans; exit ) endproc (* Phone_Answer *) endproc (* Connections*) process Request_Call[S_Usr](Caller : Nat) : exit(Nat):= ( S_Usr ! Caller ! Gets_Tone; S_Usr ! Caller ! Dials ? Called: Nat ; exit(Called) ) endproc (* Request_Call *) process User_Hang_Up [Any_Usr](User : Nat) : noexit := ( Any_Usr ! User ! Hangs_Up; stop ) endproc (* User_Hang_Up *) process Controller_Hang_Up [Any_Usr] : noexit := ( Any_Usr ? User: Nat ! Hangs_Up; Controller_Hang_Up [Any_Usr] [] i; Any_Usr ? User: Nat ! Hangs_Up; Controller_Hang_Up [Any_Usr] ) endproc (* Controller_Hang_Up *) process Manage_Users_List [S_Usr](E_Set, R_Set : NatSet) :noexit:= ( S_Usr ?Caller:Nat !Offhook_To_Call [Caller NotIn (E_Set Union R_Set)]; Manage_Users_List [S_Usr](Insert(Caller, E_Set), R_Set) [] S_Usr ? Caller:Nat ! Gets_Tone; Manage_Users_List [S_Usr](E_Set, R_Set) [] S_Usr ? Caller:Nat ! Dials ? Called: Nat ; Manage_Users_List [S_Usr](E_Set, Insert(Caller, Insert(Called, R_Set))) [] S_Usr ?Called:Nat !Ring [Called NotIn E_Set]; Manage_Users_List [S_Usr](E_Set, R_Set) [] S_Usr ? Caller:Nat ! Echo_Ring; Manage_Users_List [S_Usr](E_Set, R_Set) [] S_Usr ? Called:Nat ! Offhook_To_Ans; Manage_Users_List [S_Usr](Insert(Called, E_Set), R_Set) [] S_Usr ? Sender_Side:Nat ! Sends_Msg; Manage_Users_List [S_Usr](E_Set, R_Set) [] S_Usr ? Sender_Side:Nat ! Rcves_Msg; Manage_Users_List [S_Usr](E_Set, R_Set) [] S_Usr ?Usr:Nat !Hangs_Up; Manage_Users_List [S_Usr](Remove(Usr, E_Set), Remove(Usr, R_Set)) [] S_Usr ? Caller:Nat ! Busy_Signal; Manage_Users_List [S_Usr](E_Set, R_Set) ) endproc (* Manage_Users_List *) endspec