(******************************************************************)
(* Specification of the CS1 IN Call Model and Services in LOTOS *)
(******************************************************************)
specification IN_System [G, N, Detection_Point, DBRequest] : noexit
library Set, Boolean, DecDigit, NaturalNumber, BasicNaturalNumber endlib
(* type specifying the network adresses of the users *)
type Network_Adress is Boolean, NaturalNumber
sorts network_adress
opns adr1 (*! constructor *),
adr2 (*! constructor *),
adr3 (*! constructor *),
null (*! constructor *) : -> network_adress
_eq_ : network_adress, network_adress -> Bool
_ne_ : network_adress, network_adress -> Bool
to_nat : network_adress -> Nat
eqns forall ad1, ad2 : network_adress
ofsort Nat
to_nat(adr2) = 0 ;
to_nat(adr1) = Succ(to_nat(adr2));
to_nat(null) = Succ(to_nat(adr1));
to_nat(adr3) = Succ(to_nat(null));
ofsort Bool
ad1 eq ad2 = to_nat(ad1) eq to_nat(ad2);
ad1 ne ad2 = to_nat(ad1) ne to_nat(ad2);
endtype
(* end type Network_Adress *)
(* type UsersList defining a list of network users : elements are network_adresses *)
type UsersList is Network_Adress, Boolean
sorts List
opns empty (*! constructor *) : -> List
ADD (*! constructor *) : network_adress, List -> List
REM (*! constructor *) : network_adress, List -> List
InsertL, RemoveL : network_adress, List -> List
_IsIn_, _NotIn_ : network_adress, List -> Bool
ScreenList : network_adress -> List
eqns forall x, y : network_adress,
s, t : List
ofsort List
InsertL(x, empty) = ADD(x, empty);
x eq y => InsertL(x, ADD(y,s)) = ADD(x,s);
x ne y => InsertL(x, ADD(y,s)) = ADD(y, InsertL(x,s));
RemoveL(x, empty) = empty ;
x eq y => RemoveL(x, ADD(y,s)) = s ;
x ne y => RemoveL(x, ADD(y,s)) = ADD(y,RemoveL(x,s)) ;
(*
ScreenList(adr1) = InsertL(adr2, empty);
js*)
ScreenList(adr1) = ADD(adr2, empty);
ScreenList(adr2) = empty;
ScreenList(adr3) = empty;
ScreenList(null) = empty;
ofsort Bool
x IsIn empty = false ;
x eq y => x IsIn ADD(y,s) = true ;
x ne y => x IsIn ADD(y,s) = x IsIn s ;
(*
x NotIn s = not(x IsIn s) ;
*)
x NotIn empty = true ;
x eq y => x NotIn ADD(y,s) = false ;
x ne y => x NotIn ADD(y,s) = x NotIn s ;
endtype
(* End Of List Type Definition *)
(* type DBOperations defining the DataBase operations *)
type DBOperations is Boolean , NaturalNumber
sorts dboperations
opns Consult (*! constructor *),
Add (*! constructor *),
Remove (*! constructor *) : -> dboperations
_eq_ : dboperations, dboperations -> Bool
to_nat : dboperations -> Nat
eqns forall db1, db2 : dboperations
ofsort Nat
to_nat(Consult) = 0;
to_nat(Add) = Succ(to_nat(Consult));
to_nat(Remove) = Succ(to_nat(Add));
ofsort Bool
db1 eq db2 = to_nat(db1) eq to_nat(db2);
endtype
(* end of type DBOperations *)
(* Type Dialled_Number defining the numbers dialled by a user *)
type Dialled_Number is Boolean, Network_Adress, NaturalNumber
sorts dialled_number
opns abv_dn (*! constructor *),
dn1 (*! constructor *),
dn2 (*! constructor *),
dn3 (*! constructor *),
nil (*! constructor *) : -> dialled_number
get_adress : dialled_number -> network_adress
get_translated_number : dialled_number -> dialled_number
_eq_ : dialled_number, dialled_number -> Bool
to_nat : dialled_number -> Nat
eqns forall ad, ad1, ad2 : network_adress, dnum, dnum1, dnum2 :
dialled_number
ofsort network_adress
get_adress(abv_dn) = null;
get_adress(dn2) = adr2;
get_adress(dn1) = adr1;
get_adress(dn3) = adr3;
get_adress(nil) = null;
ofsort Nat
to_nat(abv_dn) = 0 ;
to_nat(dn1) = Succ(to_nat(abv_dn));
to_nat(dn2) = Succ(to_nat(dn1));
to_nat(dn3) = Succ(to_nat(dn2));
to_nat(nil) = Succ(to_nat(dn3));
ofsort dialled_number
get_translated_number(abv_dn) = dn2;
get_translated_number(dn1) = dn1;
get_translated_number(dn2) = dn2;
get_translated_number(dn3) = dn3;
get_translated_number(nil) = nil;
ofsort Bool
dnum1 eq dnum2 = to_nat(dnum1) eq to_nat(dnum2);
endtype
(* end of type Dialled_Number *)
(* type Service_Indicator defining an identifier for each service *)
type Service_Indicator is Boolean, NaturalNumber
sorts service_indicator
opns NO_SERVICE (*! constructor *),
OCS (*! constructor *),
ABD (*! constructor *): -> service_indicator
_eq_ : service_indicator, service_indicator -> Bool
to_nat : service_indicator -> Nat
eqns forall s1, s2 : service_indicator
ofsort Nat
to_nat(NO_SERVICE) = 0;
to_nat(OCS) = Succ(to_nat(NO_SERVICE));
to_nat(ABD) = Succ(to_nat(OCS));
ofsort Bool
s1 eq s2 = to_nat(s1) eq to_nat(s2);
endtype
(* end of type Service_Indicator *)
(* Type Signal *)
type Signal is Boolean, NaturalNumber
sorts Signal
opns OffHookToCall (*! constructor*),
OffHookToAnswer (*! constructor*),
HangsUp (*! constructor*),
Talks (*! constructor*),
RingsFrom (*! constructor*),
StopRing (*! constructor*),
GetRingTone (*! constructor*),
StopRingTone (*! constructor*),
Dials (*! constructor*),
GetTone (*! constructor*),
DisconnectionFailureIndication (*! constructor*),
IndicationTerminationDenied (*! constructor*),
InvalidInformationIndication (*! constructor*),
NoTone (*! constructor*),
TimeOut (*! constructor*),
GetNoAnswerIndication (*! constructor*),
RingTimeOut (*! constructor*),
IdleState (*! constructor*),
GetBusySignal (*! constructor*) : -> Signal
_IsEq_ : Signal, Signal -> Bool
_IsNe_ : Signal, Signal -> Bool
Map : Signal -> Nat
eqns forall x, y: Signal
ofsort Nat
Map (OffHookToCall) = 0;
Map (OffHookToAnswer) = Succ(Map (OffHookToCall));
Map (HangsUp) = Succ(Map (OffHookToAnswer));
Map (Talks) = Succ(Map (HangsUp));
Map (RingsFrom) = Succ(Map (Talks));
Map (StopRing) = Succ(Map (RingsFrom));
Map (GetRingTone) = Succ(Map (StopRing));
Map (StopRingTone) = Succ(Map (GetRingTone));
Map (GetTone) = Succ(Map (StopRingTone));
Map (GetBusySignal) = Succ(Map (GetTone));
Map (DisconnectionFailureIndication) = Succ(Map (GetBusySignal));
Map (IndicationTerminationDenied) = Succ(Map (DisconnectionFailureIndication));
Map (InvalidInformationIndication)= Succ(Map (IndicationTerminationDenied));
Map (NoTone) = Succ(Map (InvalidInformationIndication));
Map (TimeOut) = Succ(Map (NoTone));
Map (GetNoAnswerIndication) = Succ(Map (TimeOut));
Map (RingTimeOut) = Succ(Map (GetNoAnswerIndication));
Map (IdleState) = Succ(Map (RingTimeOut));
ofsort Bool
x IsEq y = Map(x) eq Map(y);
x IsNe y = Map(x) ne Map(y);
endtype
(* end of type Signal *)
(* type Trigger_detection_point defining all the Detection Points *)
type Trigger_detection_point is NaturalNumber, Boolean,
Network_Adress, Service_Indicator
sorts trigger_detection_point
opns Orig_Attempt (*! constructor *),
Orig_Denied (*! constructor *),
Orig_Attempt_Auth (*! constructor *),
Collect_Timeout (*! constructor *),
Collected_Info (*! constructor *),
Analysed_Info (*! constructor *),
Invalid_Info (*! constructor *),
Orig_Auth (*! constructor *),
O_Called_Party_busy (*! constructor *),
O_Abandon (*! constructor *),
O_Term_Seized (*! constructor *),
O_No_Answer (*! constructor *),
O_Answer (*! constructor *),
O_Connection_Failure (*! constructor *),
O_Disconnect (*! constructor *),
O_Disc_Complete (*! constructor *),
Term_Attempt (*! constructor *),
Term_Denied (*! constructor *),
Term_Auth (*! constructor *),
T_Called_Party_Busy (*! constructor *),
T_Term_Seized (*! constructor *),
T_No_Answer (*! constructor *),
T_Answer (*! constructor *),
T_Connection_Failure (*! constructor *),
T_Disconnect (*! constructor *),
T_Disconnect_Complete (*! constructor *),
T_Calling_Party_Abandon (*! constructor *): -> trigger_detection_point
to_nat : trigger_detection_point -> Nat
_eq_ : trigger_detection_point, trigger_detection_point -> Bool
trigger_armed : trigger_detection_point, network_adress, service_indicator -> Bool
eqns
forall t, t1, t2 : trigger_detection_point, adr :network_adress,
serv_ind : service_indicator
ofsort Nat
to_nat(Orig_Attempt) = 0;
to_nat(Orig_Denied) = Succ(to_nat(Orig_Attempt));
to_nat(Orig_Attempt_Auth) = Succ(to_nat(Orig_Denied));
to_nat(Term_Attempt) = Succ(to_nat(Orig_Attempt_Auth));
to_nat(Collected_Info) = Succ(to_nat(Term_Attempt));
to_nat(Invalid_Info) = Succ(to_nat(Collected_Info));
to_nat(Orig_Auth) = Succ(to_nat(Invalid_Info));
to_nat(O_Called_Party_busy) = Succ(to_nat(Orig_Auth));
to_nat(O_Abandon) = Succ(to_nat(O_Called_Party_busy));
to_nat(O_Term_Seized) = Succ(to_nat(O_Abandon));
to_nat(O_No_Answer) = Succ(to_nat(O_Term_Seized));
to_nat(O_Answer) = Succ(to_nat(O_No_Answer));
to_nat(O_Connection_Failure) = Succ(to_nat(O_Answer));
to_nat(O_Disconnect) = Succ(to_nat(O_Connection_Failure));
to_nat(O_Disc_Complete) = Succ(to_nat(O_Disconnect));
to_nat(Collect_Timeout) = Succ(to_nat(O_Disc_Complete));
to_nat(Term_Denied) = Succ(to_nat(Collect_Timeout));
to_nat(Term_Auth) = Succ(to_nat(Term_Denied));
to_nat(T_Called_Party_Busy) = Succ(to_nat(Term_Auth));
to_nat(T_Term_Seized) = Succ(to_nat(T_Called_Party_Busy));
to_nat(T_No_Answer) = Succ(to_nat(T_Term_Seized));
to_nat(T_Answer) = Succ(to_nat(T_No_Answer));
to_nat(T_Connection_Failure) = Succ(to_nat(T_Answer));
to_nat(T_Disconnect) = Succ(to_nat(T_Connection_Failure));
to_nat(T_Disconnect_Complete) = Succ(to_nat(T_Disconnect));
to_nat(T_Calling_Party_Abandon) = Succ(to_nat(T_Disconnect_Complete));
to_nat(Analysed_Info)= Succ(to_nat(T_Calling_Party_Abandon));
ofsort Bool
t1 eq t2 = to_nat(t1) eq to_nat(t2);
ofsort Bool
trigger_armed(t, adr, serv_ind)=
((t eq Analysed_Info) and (adr eq adr1) and (serv_ind eq OCS))
or
((t eq Term_Auth) and (adr eq adr2) and (serv_ind eq ABD));
endtype
(* end of type Trigger_detection_point *)
(*********************************************************************************************************)
(* End of Data Type Definition *)
(*********************************************************************************************************)
(*********************************************************************************************************)
(* Behavioral Part Definition *)
(*********************************************************************************************************)
(* behavior of the specification *)
(* The highest level of the specification is defined by a synchronization of two processes, Connections *)
(* and Update_Data_Base. The process Connections specifies the different connections between IN users *)
(* and the process Update_Data_Base handles all the operations of manipulating the list of busy users *)
behavior
(
Connections [G, N, Detection_Point, DBRequest]
|[N, DBRequest]|
Update_Data_Base [N, DBRequest](empty)
)
where
(* process Connections *)
(* The process is defined by a synchronization between two processes Network_Subscribers and CCF_SSF *)
process Connections [G, N, Detection_Point, DBRequest] : noexit :=
(
Network_Subscribers [G, N, Detection_Point, DBRequest]
|[N, G]|
CCF_SSF [G, N, Detection_Point, DBRequest]
)
endproc (* end of process IN_Network *)
(* process Network_Subscribers *)
process Network_Subscribers [G, N, Detection_Point, DBRequest ]:noexit :=
(
Subscriber [G, N, Detection_Point, DBRequest ](adr1)
|||
Subscriber [G, N, Detection_Point, DBRequest ](adr2)
|||
Subscriber [G, N, Detection_Point, DBRequest ](adr3)
)
endproc (* end of process Network_Subscribers *)
process Subscriber [G, N, Detection_Point, DBRequest ] (adr: network_adress)
:noexit :=
Caller_Side[G, N, Detection_Point, DBRequest ](adr)
[]
Called_Side[G, N, Detection_Point, DBRequest ](adr)
endproc (* end of process Subscriber *)
process Caller_Side[G, N, Detection_Point, DBRequest ] (caller: network_adress)
:noexit :=
N !caller !OffHookToCall;
(
Caller_GetsTone[G, N, Detection_Point, DBRequest ] (caller)
[]
G !caller !NoTone; User_HangsUp[G, N, Detection_Point, DBRequest ] (caller)
[]
User_HangsUp[G, N, Detection_Point, DBRequest ] (caller)
)
endproc
process Caller_GetsTone[G, N, Detection_Point, DBRequest ] (caller: network_adress)
:noexit :=
G !caller !GetTone;
(
Caller_Dials [G, N, Detection_Point, DBRequest ] (caller)
[]
User_HangsUp [G, N, Detection_Point, DBRequest ](caller)
)
endproc
process Caller_Dials [G, N, Detection_Point, DBRequest ] (caller: network_adress)
:noexit :=
G !caller !Dials ?dn: dialled_number ;
(
G !caller !TimeOut; User_HangsUp[G, N, Detection_Point, DBRequest ] (caller)
[]
G !caller !GetBusySignal ; User_HangsUp [G, N,Detection_Point, DBRequest ] (caller)
[]
G !caller !InvalidInformationIndication; User_HangsUp [G, N, Detection_Point, DBRequest] (caller)
[]
G !caller !IndicationTerminationDenied; User_HangsUp [G, N, Detection_Point, DBRequest] (caller)
[]
Caller_GetsRingTone [G, N,Detection_Point, DBRequest ] (caller)
[]
User_HangsUp [G, N, Detection_Point, DBRequest ](caller)
)
endproc
process Caller_GetsRingTone [G, N,Detection_Point, DBRequest ] (caller : network_adress):noexit :=
G !caller !GetRingTone;
(
G !caller !StopRingTone;
(
Talking_session [G, N, Detection_Point, DBRequest ] (caller)
[>
(
G !caller !DisconnectionFailureIndication; User_HangsUp [G, N, Detection_Point, DBRequest ](caller)
[]
User_HangsUp [G, N, Detection_Point, DBRequest ] (caller)
)
[]
G !caller !GetNoAnswerIndication; User_HangsUp [G, N, Detection_Point, DBRequest ](caller)
)
[]
User_HangsUp [G, N, Detection_Point, DBRequest ](caller)
)
endproc
process Talking_session[G, N, Detection_Point, DBRequest ] (user: network_adress)
:noexit :=
G !user !Talks;
Talking_session[G, N, Detection_Point, DBRequest ] (user)
endproc (* end of process Talking_session *)
process User_HangsUp [G, N, Detection_Point, DBRequest ] (user : network_adress)
:noexit :=
G !user !HangsUp;
N !user !IdleState;
Subscriber [G, N, Detection_Point, DBRequest ] (user)
endproc (* end of process User_HangsUp *)
process Called_Side[G, N, Detection_Point, DBRequest ] (called: network_adress)
:noexit :=
N !called !RingsFrom ?caller: network_adress;
(
G !called !OffHookToAnswer;
G !called !StopRingTone;
(
Talking_session [G, N, Detection_Point, DBRequest ] (called)
[>
(
G !called !DisconnectionFailureIndication; User_HangsUp [G, N, Detection_Point, DBRequest ] (called)
[]
User_HangsUp [G, N, Detection_Point, DBRequest ] (called)
)
)
[]
G !called !RingTimeOut;
N !called !IdleState;
Subscriber [G, N, Detection_Point, DBRequest] (called)
[]
N !called !IdleState;
Subscriber [G, N, Detection_Point, DBRequest] (called)
)
[]
N !called !IdleState;
Subscriber [G, N, Detection_Point, DBRequest] (called)
endproc
process CCF_SSF[G, N, Detection_Point, DBRequest ]: noexit :=
N ? caller: network_adress !OffHookToCall;
(
Basic_Call_State_Model[G, N, Detection_Point, DBRequest](caller, nil,null)
|||
CCF_SSF[G, N, Detection_Point, DBRequest ]
)
endproc
(* end of process CCF_SSF *)
process Basic_Call_State_Model[G, N, Detection_Point, DBRequest](caller:network_adress,
dn: dialled_number, called: network_adress): noexit :=
State_Orig_Attempt[G, N, Detection_Point, DBRequest ](caller, dn, called)
endproc
process State_Orig_Attempt[G, N, Detection_Point, DBRequest ](caller:network_adress,
dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Orig_Attempt !caller !called;
(
G !caller !GetTone;
State_Orig_Attempt_Auth [G, N, Detection_Point, DBRequest ](caller, dn,called)
[]
G !caller !NoTone;
State_Orig_Denied[G, N,Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !HangsUp;
State_O_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, called )
)
endproc
process State_Orig_Denied[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Orig_Denied !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_O_Abandon[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !O_Abandon !caller !called;
(
N !caller !IdleState;
stop
)
endproc
process State_Orig_Attempt_Auth[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Orig_Attempt_Auth !caller !called;
(
G !caller !Dials ?dn: dialled_number ;
(
State_Collected_Info[G, N, Detection_Point, DBRequest ](caller, dn, get_adress(dn))
[]
G !caller !TimeOut;
State_Collect_Timeout[G, N, Detection_Point, DBRequest ](caller, dn, get_adress(dn))
[]
G !caller !HangsUp;
State_O_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, get_adress(dn))
)
[]
G !caller !HangsUp;
State_O_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, get_adress(dn))
)
endproc
process State_Collect_Timeout[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Collect_Timeout !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_Collected_Info[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Collected_Info !caller !called;
(
[caller eq adr1]->
(
Detection_Point !OCS;
Originating_Call_Screening[G, N, Detection_Point, DBRequest](caller, dn,called)
)
[]
[caller ne adr1]->
(
State_Analysed_Info[G, N, Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !InvalidInformationIndication;
State_Invalid_Info[G, N, Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !HangsUp;
State_O_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, called)
)
)
endproc
process State_Invalid_Info[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Invalid_Info !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_Analysed_Info[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Analysed_Info !caller !called;
(
[caller eq adr1]->
(
Detection_Point !ABD;
Abbreviated_Dialing[G, N, Detection_Point, DBRequest](caller, dn,called)
)
[]
[not(caller eq adr1)]->
(
State_Orig_Auth[G, N, Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !HangsUp;
State_O_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, called)
)
)
endproc
process State_Orig_Auth[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Orig_Auth !caller !called;
(
State_Term_Attempt[G, N, Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !HangsUp;
State_O_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, called)
)
endproc
process State_Term_Attempt[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Term_Attempt !caller !called;
(
State_Term_Auth[G, N, Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !HangsUp;
State_T_Calling_Party_Abandon[G, N, Detection_Point, DBRequest ](caller, dn, called)
[]
G !caller !IndicationTerminationDenied;
State_Term_Denied[G, N, Detection_Point, DBRequest ](caller, dn, called)
)
endproc
process State_Term_Denied[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Term_Denied !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_T_Calling_Party_Abandon[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_Calling_Party_Abandon !caller !called;
DBRequest !Consult ? BusyList: List;
(
[called IsIn BusyList]->
(
N !called !IdleState;
stop
|||
N !caller !IdleState;
stop
)
[]
[called NotIn BusyList]->
(
N !caller !IdleState;
stop
)
)
endproc
process State_Term_Auth[G, N, Detection_Point, DBRequest ](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !Term_Auth !caller !called;
DBRequest !Consult ? BusyList: List;
(
[called IsIn BusyList]->
State_T_Called_Party_Busy[G, N, Detection_Point, DBRequest ]( caller, dn,called)
[]
[called NotIn BusyList]->
(
G !caller !HangsUp;
State_T_Calling_Party_Abandon[G, N, Detection_Point, DBRequest ](caller,dn, called)
[]
N !called !RingsFrom !caller;
State_T_Term_Seized[G, N, Detection_Point, DBRequest ](caller, dn, called)
)
)
endproc
process State_T_Called_Party_Busy[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_Called_Party_Busy !caller !called;
G !caller !GetBusySignal ;
State_O_Called_Party_Busy[G, N, Detection_Point, DBRequest]( caller, dn, called)
endproc
process State_T_Term_Seized[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_Term_Seized !caller !called;
(
G !caller !GetRingTone;
State_O_Term_Seized[G, N, Detection_Point, DBRequest](caller, dn, called)
[]
G !caller !HangsUp;
State_T_Calling_Party_Abandon[G, N, Detection_Point, DBRequest](caller, dn, called)
)
endproc
process State_O_Called_Party_Busy[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !O_Called_Party_busy !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_O_Term_Seized[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress ): noexit :=
Detection_Point !O_Term_Seized !caller !called;
(
G !called !OffHookToAnswer;
G !called !StopRingTone;
State_T_Answer[G, N, Detection_Point, DBRequest](caller, dn,called)
[]
G !called !RingTimeOut;
State_T_No_Answer[G, N, Detection_Point, DBRequest](caller, dn, called)
[]
G !caller !HangsUp;
State_T_Calling_Party_Abandon[G, N, Detection_Point, DBRequest](caller, dn,called)
)
endproc
process State_T_No_Answer[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_No_Answer !caller !called;
(
N !called !IdleState;
stop
|||
G !caller !StopRingTone;
G !caller !GetNoAnswerIndication ;
State_O_No_Answer[G, N, Detection_Point, DBRequest](caller, dn, called)
)
endproc
process State_O_No_Answer[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !O_No_Answer !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_T_Answer[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_Answer !caller !called;
(
G !caller !StopRingTone;
State_O_Answer[G, N, Detection_Point, DBRequest](caller, dn, called)
)
endproc
process State_O_Answer[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !O_Answer !caller !called;
(
(
Talking_session[G, N, Detection_Point, DBRequest](caller)
|||
Talking_session[G, N, Detection_Point, DBRequest](called)
)
[>
(
G !caller !HangsUp;
State_O_Disconnect[G, N, Detection_Point, DBRequest](caller, dn, called)
[]
G !called !HangsUp;
State_T_Disconnect[G, N, Detection_Point, DBRequest](caller, dn, called)
[]
G !caller !DisconnectionFailureIndication;
State_O_Connection_Failure[G, N, Detection_Point, DBRequest](caller, dn, called)
[]
G !called !DisconnectionFailureIndication;
State_T_Connection_Failure[G, N, Detection_Point, DBRequest](caller, dn,called)
)
)
endproc
process State_O_Connection_Failure[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !O_Connection_Failure !caller !called;
G !called !DisconnectionFailureIndication;
Detection_Point !T_Connection_Failure !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
|||
G !called !HangsUp;
N !called !IdleState;
stop
)
endproc
process State_T_Connection_Failure[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_Connection_Failure !caller !called;
G !caller !DisconnectionFailureIndication;
Detection_Point !O_Connection_Failure !caller !called;
(
G !called !HangsUp;
N !called !IdleState;
stop
|||
G !caller !HangsUp;
N !caller !IdleState;
stop
)
endproc
process State_O_Disconnect[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !O_Disconnect !caller !called;
(
N !caller !IdleState; stop
|||
(
Detection_Point !T_Disconnect !caller !called;
(
G !called !HangsUp;
N !called !IdleState;
stop
)
)
)
endproc
process State_T_Disconnect[G, N, Detection_Point, DBRequest](caller:
network_adress, dn: dialled_number, called: network_adress): noexit :=
Detection_Point !T_Disconnect !caller !called;
(
N !called !IdleState; stop
|||
(
Detection_Point !O_Disconnect !caller !called;
(
G !caller !HangsUp;
N !caller !IdleState;
stop
)
)
)
endproc
process Update_Data_Base [N, DBRequest] (BusyList : List) :noexit :=
(
DBRequest !Consult !BusyList ;
Update_Data_Base[N, DBRequest](BusyList)
[]
N ?caller: network_adress !OffHookToCall [caller NotIn BusyList];
Update_Data_Base[N, DBRequest](InsertL(caller,BusyList))
[]
N ?user: network_adress !IdleState;
Update_Data_Base[N, DBRequest](RemoveL(user, BusyList))
[]
N ?called: network_adress !RingsFrom ?caller: network_adress;
Update_Data_Base[N, DBRequest](InsertL(called,BusyList))
)endproc (* *)
process Launch_Service_at_SCF[G, N, Detection_Point , DBRequest](caller: network_adress, dn:
dialled_number, called: network_adress,ser:service_indicator): noexit:=
[ser eq OCS] ->
Originating_Call_Screening[G, N, Detection_Point, DBRequest](caller, dn,called)
[]
[ser eq ABD] ->
Abbreviated_Dialing[G, N, Detection_Point, DBRequest](caller, dn,called)
endproc (* end process Launch_Service_at_SCF *)
process Abbreviated_Dialing[G, N, Detection_Point, DBRequest ](caller
:network_adress,dn:dialled_number, called:network_adress) :noexit :=
Translate_SIB[G, N, Detection_Point, DBRequest ](caller, dn, called)
endproc
process Originating_Call_Screening[G, N, Detection_Point, DBRequest ](caller
:network_adress,dn:dialled_number, called:network_adress):noexit :=
Screen_SIB[G, N, Detection_Point, DBRequest ](caller, dn, called)
endproc
process Screen_SIB[G, N, Detection_Point, DBRequest ](caller :network_adress,dn:dialled_number,
called:network_adress) : noexit:=
(
[called ne adr2 (*NotIn ScreenList(caller)*)] ->
State_Analysed_Info [G, N, Detection_Point, DBRequest](caller, dn, called)
)
[]
(
[called eq adr2(*IsIn ScreenList(caller)*)] ->
(
G !caller !HangsUp;
N !caller !IdleState;
CCF_SSF[G, N, Detection_Point, DBRequest ]
)
)
endproc
process Translate_SIB[G, N, Detection_Point, DBRequest ](caller :network_adress,dn:dialled_number,
called:network_adress):noexit :=
State_Orig_Auth[G, N, Detection_Point, DBRequest]( caller,dn, get_adress(get_translated_number(dn)))
endproc
endspec (* *)