(****************************************************************************) (* Feature Interactions from UCM *) (* Version: 0.14c *) (* Date : September 8, 1998 *) (* Authors: Daniel Amyot (damyot@csi.uottawa.ca) *) (* Dorin Petriu (dorin@sce.carleton.ca) *) (* SCE Department, Carleton University, Ottawa, Canada *) (* History: *) (* Sep. 8, 1998 : Added Probes for structural coverage. *) (* Aug. 19, 1998: Fixed part of INFB-TCS interaction in billing. *) (* Solved the INFB-TCS FI in ProcessCallStub. *) (* Aug. 13, 1998: Recomposed TCS as an alternative to INFB. *) (* No FI between TCS and CND, as expected. *) (* FI found between TCS and INFB in this way! *) (* Aug. 12, 1998: TCS implemented and tested. No FI with INTL. *) (* Aug. 11, 1998: New stub for Busy in Post-Dial. Conforms to the *) (* new map with 13 features. *) (* Added support for AirBegin and AirEnd (Cell). *) (* Started implementing TCS (priority over others) *) (* July 12, 1998: Added INFB and 2 tests. The feature works. *) (* Added Query gate to OS. *) (* All test cases now check the final billing Log. *) (* Checking interactions between INTL and INFB. *) (* None found, as expected. *) (* Checking interactions between CND and INFB. *) (* None found, as expected? *) (* July 10, 1998: Added a FList to users. CND now works. *) (* Restructured the test suite *) (* Checks for interactions between CND and INTL. *) (* None found, as expected. *) (* July 9, 1998 : Sets AudibleRinging and Ringing. *) (* Updated SCP. Now INTL works. *) (* Updated the switch. CND almost works. *) (* July 8, 1998 : Specified part of PostDialStub and *) (* ProcessCallStub to make POTS work. It does now. *) (* July 7, 1998 : Added lt and ge to type Time *) (* Reimplemented SCPDB and query operations *) (* Reimplemented Status and query operations *) (* Created six generic POTS state processes *) (* Created two test processes for POTS and three *) (* for INTL from the Chisel diagrams. *) (* Defined the mechanism for composing feature *) (* plugins in stubs. *) (* July 6, 1998 : Added types SPList, Status and SCPDB *) (* Added processes DisplayStub, PreDialStub *) (* Created process PostDialStub *) (* Created Default & INTL plugins for PreDialStub *) (* Worked on User and Switch for POTS/INTL *) (* Added two complex test processes for POTS. *) (* July 5, 1998 : Added process GlobalClock *) (* Added types Cadence, PIN, Message, TriggerName *) (* ResponseType, Log, LogRecord, Feature, FList *) (* SInfo, SDB, AddList *) (* July 4, 1998 : Added Boolean, adapted Address, and simplified *) (* NaturalNumbers. *) (* July 2, 1998 : Created structure and process skeletons. *) (* June 16, 1998: Modified IS8807 ADT. *) (****************************************************************************) specification FI_UCM[OffHook, (* User2Switch *) OnHook, (* User2Switch *) Dial, (* User2Switch *) Flash, (* User2Switch *) DialTone, (* Switch2User *) StartAR, (* Switch2User: Start AudibleRinging *) StartR, (* Switch2User: Start Ringing *) StartCWT, (* Switch2User: Start CallWaitingTone *) StopAR, (* Switch2User: Stop AudibleRinging *) StopR, (* Switch2User: Stop Ringing *) StopCWT, (* Switch2User: Stop CallWaitingTone *) LineBusyTone, (* Switch2User *) Announce, (* Switch2User *) Disconnect, (* Switch2User *) Display, (* Switch2User *) CreateUser, (* NEW: For creating user instances. *) Init, (* NEW: Initialize switch for testing. *) Query (* NEW: Allows to query OS' Log. *) ]:noexit (*======================================================*) (* Modified IS8807 ADT definitions *) (*======================================================*) (* Types FBoolean, Element, and Set contain corrections *) (* to the library from the International Standard 8870. *) (* Type Boolean remains the same, but NaturalNumber was *) (* simplified by removing unnecessary arithmetic and *) (* comparison operators *) type Boolean is sorts Bool opns true, false: -> Bool not: Bool -> Bool _ and _, _ or _, _ xor _, _ implies _, _ iff _, _ eq _, _ ne _: Bool, Bool -> Bool eqns forall x, y: Bool ofsort Bool not (true) = false ; not (false) = true ; x and true = x ; x and false = false ; x or true = true ; x or false = x ; x xor y = x and not (y) or (y and not (x)) ; x implies y = y or not (x) ; x iff y = x implies y and (y implies x) ; x eq y = x iff y ; x ne y = x xor y ; endtype (* Boolean *) (*********************************************) type NaturalNumber is Boolean sorts Nat opns 0: -> Nat Succ: Nat -> Nat _ + _: Nat, Nat -> Nat _ eq _, _ ne _: Nat, Nat -> Bool eqns forall m, n: Nat ofsort Nat m + 0 = m ; m + Succ (n) = Succ (m) + n ; ofsort Bool 0 eq 0 = true ; 0 eq Succ (m) = false ; Succ (m) eq 0 = false ; Succ (m) eq Succ (n) = m eq n ; m ne n = not (m eq n) ; endtype (* NaturalNumber *) (*********************************************) type FBoolean is formalsorts FBool formalopns true : -> FBool not : FBool -> FBool formaleqns forall x : FBool ofsort FBool not(not(x)) = x; endtype (* FBoolean *) (*********************************************) type Element is FBoolean formalsorts Element formalopns _ eq _, _ ne _ : Element, Element -> FBool formaleqns forall x, y, z : Element ofsort Element x eq y = true => x = y ; ofsort FBool x = y => x eq y = true ; x eq y =true , y eq z = true => x eq z = true ; x ne y = not(x eq y) ; endtype (* Element *) (*********************************************) type Set is Element, Boolean, NaturalNumber sorts Set opns {} : -> Set Insert, Remove : Element, Set -> Set _IsIn_, _NotIn_ : Element, Set -> Bool _Union_, _Ints_, _Minus_ : Set, Set -> Set _eq_, _ne_, _Includes_, _IsSubsetOf_ : Set, Set -> Bool Card : Set -> Nat eqns forall x, y : Element, s, t : Set ofsort Set x IsIn Insert(y,s) => Insert(x, Insert(y,s)) = Insert(y,s) ; Remove(x, {}) = {} ; Remove(x, Insert(x,s)) = s ; x ne y = true of FBool => Remove(x, Insert(y,s)) = Insert(y, Remove(x,s)); {} Union s = s ; Insert(x,s) Union t = Insert(x,s Union t) ; {} Ints s = {} ; x IsIn t => Insert(x,s) Ints t = Insert(x,s Ints t) ; x NotIn t => Insert(x,s) Ints t = s Ints t ; s Minus {} = s ; s Minus Insert(x, t) = Remove(x,s) Minus t ; ofsort Bool x IsIn {} = false ; x eq y = true of FBool => x IsIn Insert(y,s) = true ; x ne y = true of FBool => x IsIn Insert(y,s) = x IsIn s ; x NotIn s = not(x IsIn s) ; s Includes {} = true ; s Includes Insert(x,t) = (x IsIn s) and (s Includes t) ; s IsSubsetOf t = t Includes s ; s eq t = (s Includes t) and (t Includes s); s ne t = not(s eq t) ; ofsort Nat Card({}) = 0 ; x NotIn s => Card(Insert(x,s)) = Succ(Card(s)) ; endtype (* Set *) (*=============================================*) (* FI_UCM ADT definitions *) (*=============================================*) (* The Time type is mapped onto natural numbers. *) type Time1 is NaturalNumber renamedby sortnames Time for Nat opnnames tic for succ initTime for 0 endtype (* Time1 *) (* Additional comparison operators for time range. *) type Time is Time1 opns _ lt _, _ ge _ : Time, Time -> Bool eqns forall t1, t2 : Time ofsort Bool t1 lt initTime = false ; initTime lt tic(t1) = true ; tic(t1) lt tic(t2) = t1 lt t2 ; t1 ge t2 = not (t1 lt t2); endtype (* Time *) (*********************************************) (* The Address type contains the Address sort, *) (* which is an enumeration of user identifiers *) (* or numbers that can be dialled. *) type Address is NaturalNumber sorts Address opns userA, userB, userC, anonymous, undefined, star69 : -> Address zeroPlus : Address -> Address map : Address -> Nat dest : Address -> Address _ eq _, _ ne _ : Address, Address -> Bool eqns forall user1, user2 : Address ofsort Nat map(userA) = 0; map(userB) = succ(0); map(userC) = succ(succ(0)); map(anonymous) = succ(succ(succ(0))); map(undefined) = succ(succ(succ(succ(0)))); (* for CND *) map(star69) = succ(succ(succ(succ(succ(0))))); (* for RC *) map(zeroPlus(user1)) = succ(succ(succ(succ(succ(succ(0)))))); (* for CC *) ofsort Address dest(zeroPlus(user1)) = user1; (* for CC *) ofsort Bool user1 eq user2 = map(user1) eq map(user2); user1 ne user2 = not(user1 eq user2); endtype (* Address *) (* List of addresses, implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization *) type AddList0 is Set actualizedby Address using sortnames Address for Element Bool for FBool endtype (* AddList0 *) type AddList is AddList0 renamedby sortnames AddList for Set opnnames NoAddList for {} (* Empty list of addresses *) endtype (* AddList *) (*********************************************) (* The Cadence is either Ring or SpecialTone. *) type Cadence is Boolean sorts Cadence opns specialRing, tone : -> Cadence _ eq _, _ ne _ : Cadence, Cadence -> Bool eqns forall c1, c2 : Cadence ofsort Bool specialRing eq specialRing = true; specialRing eq tone = false; tone eq specialRing = false; tone eq tone = true; c1 ne c2 = not(c1 eq c2); endtype (* Cadence *) (*********************************************) (* The PIN is either validPIN or invalidPIN *) type PIN is Cadence renamedby sortnames PIN for Cadence opnnames validPIN for tone invalidPIN for specialRing endtype (* PIN *) (*********************************************) (* The Message type is mainly for announcements *) type Message is NaturalNumber sorts Message opns AskForPIN, displayMessage, collectedDigits, ScreenedMessage : -> Message map : Message -> Nat _ eq _, _ ne _ : Message, Message -> Bool eqns forall m1, m2 : Message ofsort Nat map(AskForPIN) = 0; map(displayMessage) = succ(0); map(collectedDigits) = succ(succ(0)); map(ScreenedMessage) = succ(succ(succ(0))); (* Add new messages when necessary *) ofsort Bool m1 eq m2 = map(m1) eq map(m2); m1 ne m2 = not(m1 eq m2); endtype (* Message *) (*********************************************) (* The TriggerName sort is an enumeration of *) (* the names of IN triggers. *) type TriggerName is NaturalNumber sorts TriggerName opns ORIGINATION_ATTEMPT, INFO_COLLECTED, INFO_ANALYZED, NETWORK_BUSY : -> TriggerName map : TriggerName -> Nat _ eq _, _ ne _ : TriggerName, TriggerName -> Bool eqns forall m1, m2 : TriggerName ofsort Nat map(ORIGINATION_ATTEMPT) = 0; map(INFO_COLLECTED) = succ(0); map(INFO_ANALYZED) = succ(succ(0)); map(NETWORK_BUSY) = succ(succ(succ(0))); ofsort Bool m1 eq m2 = map(m1) eq map(m2); m1 ne m2 = not(m1 eq m2); endtype (* TriggerName *) (*********************************************) (* The ResponseType sort is an enumeration of*) (* the SCP responses to trigger messages. *) type ResponseType is NaturalNumber sorts ResponseType opns ANALYZE_ROUTE, CONTINUE, FORWARD_CALL, SEND_TO_RESOURCE, DISCONNECT : -> ResponseType map : ResponseType -> Nat _ eq _, _ ne _ : ResponseType, ResponseType -> Bool eqns forall m1, m2 : ResponseType ofsort Nat map(ANALYZE_ROUTE) = 0; map(CONTINUE) = succ(0); map(FORWARD_CALL) = succ(succ(0)); map(SEND_TO_RESOURCE) = succ(succ(succ(0))); map(DISCONNECT) = succ(succ(succ(succ(0)))); ofsort Bool m1 eq m2 = map(m1) eq map(m2); m1 ne m2 = not(m1 eq m2); endtype (* ResponseType *) (*********************************************) (* The type of log in the OS is Begin, End, AirBegin, or AirEnd *) type LogType is NaturalNumber sorts LogType opns Begin, End, AirBegin, AirEnd : -> LogType map : LogType -> Nat _ eq _, _ ne _ : LogType, LogType -> Bool eqns forall m1, m2 : LogType ofsort Nat map(Begin) = 0; map(End) = succ(0); map(AirBegin) = succ(succ(0)); map(AirEnd) = succ(succ(succ(0))); ofsort Bool m1 eq m2 = map(m1) eq map(m2); m1 ne m2 = not(m1 eq m2); endtype (* LogType *) (* A record for the Log. *) (* Can be l(Begin,X,Y,P,T) or l(End,X,Y,undefined, T) for regular logs *) (* and l(AirBegin,X,undefined,undefined,T) or *) (* l(AirEnd,X,undefined,undefined, T) for cellular logs. *) type LogRecord is Address, Time, LogType sorts LogRecord opns l : LogType, Address, Address, Address, Time -> LogRecord _ eq _, _ ne _ : LogRecord, LogRecord -> Bool eqns forall X1, X2, Y1, Y2, P1, P2 : Address, T1, T2 : Time, LT1, LT2 : LogType ofsort Bool (LT1 eq LT2) and (X1 eq X2) and (Y1 eq Y2) and (P1 eq P2) and (T1 eq T2) => l(LT1,X1,Y1,P1,T1) eq l(LT2,X2,Y2,P2,T2) = true; not((LT1 eq LT2) and (X1 eq X2) and (Y1 eq Y2) and (P1 eq P2) and (T1 eq T2)) => l(LT1,X1,Y1,P1,T1) eq l(LT2,X2,Y2,P2,T2) = false; l(LT1,X1,Y1,P1,T1) ne l(LT2,X2,Y2,P2,T2) = not(l(LT1,X1,Y1,P1,T1) eq l(LT2,X2,Y2,P2,T2)); endtype (* LogRecord *) (* List of log records (logs), implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization *) type Log0 is Set actualizedby LogRecord using sortnames LogRecord for Element Bool for FBool endtype (* Logs0 *) type Log is Log0 renamedby sortnames Log for Set opnnames NoLog for {} (* Empty list of log records *) endtype (* Log *) (*********************************************) (* The Feature sort is an enumeration of the *) (* features to which users can subscribe, *) (* including POTS. *) type Feature is NaturalNumber sorts Feature opns POTS, (* Plain Old Telephone System *) CFBL, (* Call Forward Busy Line *) CND, (* Call Name Delivery *) INFB, (* IN Freephone Billing *) INFR, (* IN Freephone Routing *) INTL, (* IN Teen Line *) TCS, (* Terminating Call Screening *) 3WC, (* Three-way Calling *) INCF, (* IN Call Forwarding *) CW, (* Call Waiting *) CC, (* Charge Call *) (* Phase II features, plus one more. *) Cell, (* Cellular *) RC, (* Return Call *) ACB (* Automatic Call Back (Dorin's) *) : -> Feature map : Feature -> Nat _ eq _, _ ne _ : Feature, Feature -> Bool eqns forall m1, m2 : Feature ofsort Nat map(POTS) = 0; map(CFBL) = succ(0); map(CND) = succ(succ(0)); map(INFR) = succ(succ(succ(0))); map(INFB) = succ(succ(succ(succ(0)))); map(INTL) = succ(succ(succ(succ(succ(0))))); map(TCS) = succ(succ(succ(succ(succ(succ(0)))))); map(3WC) = succ(succ(succ(succ(succ(succ(succ(0))))))); map(INCF) = succ(succ(succ(succ(succ(succ(succ(succ(0)))))))); map(CW) = succ(succ(succ(succ(succ(succ(succ(succ(succ(0))))))))); map(CC) = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(0)))))))))); map(Cell) = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(0))))))))))); map(RC) = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(0)))))))))))); map(ACB) = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(0))))))))))))); ofsort Bool m1 eq m2 = map(m1) eq map(m2); m1 ne m2 = not(m1 eq m2); endtype (* Feature *) (* List of features, implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization *) type Flist0 is Set actualizedby Feature using sortnames Feature for Element Bool for FBool endtype (* Logs0 *) type Flist is Flist0 renamedby sortnames Flist for Set opnnames NoFList for {} (* Empty list of features *) endtype (* Flist *) (*********************************************) (* A record for the subscriber information. *) (* Format: sub(userID, Features, BLForward, LastIncoming, *) (* Screened, ChargePin) *) type SInfo is AddList, FList, PIN sorts SInfo opns sub : Address, (* User identifier *) FList, (* List of subscribed features *) Address, (* BLForward, for CFBL *) Address, (* LastIncoming, for CND *) AddList, (* Screened list, for TCS *) PIN (* Charge PIN, for CC *) -> SInfo _ eq _, _ ne _ : SInfo, SInfo -> Bool eqns forall s1, s2, bl1, bl2, li1, li2: Address, fl1, fl2: Flist, sl1, sl2: AddList, p1, p2: PIN ofsort Bool (s1 eq s2) and (fl1 eq fl2) and (bl1 eq bl2) and (li1 eq li2) and (sl1 eq sl2) and (p1 eq p2) => sub(s1, fl1, bl1, li1, sl1, p1) eq sub(s2, fl2, bl2, li2, sl2, p2) = true; not((s1 eq s2) and (fl1 eq fl2) and (bl1 eq bl2) and (li1 eq li2) and (sl1 eq sl2) and (p1 eq p2)) => sub(s1, fl1, bl1, li1, sl1, p1) eq sub(s2, fl2, bl2, li2, sl2, p2) = false; sub(s1, fl1, bl1, li1, sl1, p1) ne sub(s2, fl2, bl2, li2, sl2, p2) = not(sub(s1, fl1, bl1, li1, sl1, p1) eq sub(s2, fl2, bl2, li2, sl2, p2)); endtype (* SInfo *) (* Database of subscriber records (SInfo), implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization. *) type SDB0 is Set actualizedby SInfo using sortnames SInfo for Element Bool for FBool endtype (* SDB0 *) type SDB1 is SDB0 renamedby sortnames SDB for Set opnnames NoSDB for {} (* Empty list of subscribers *) endtype (* SDB1 *) (* Query operators *) type SDB is SDB1 opns (* Tells whether a subscriber has subscribed a particular feature *) has : Address, Feature, SDB -> Bool (* Sets/Gets the$LastIncoming caller *) setLastIncoming : Address, Address, SDB -> SDB getLastIncoming : Address, SDB -> Address (* Check whether the caller party is on the callee's TCS *) isOnTCS : Address, Address, SDB -> Bool (* Caller, Callee *) eqns forall s1, s2, s3, bl1, li1, li2: Address, sl1: AddList, p1: PIN, f1, f2: Feature, fl : FList, sdb : SDB ofsort Bool has(s1, f1, NoSDB) = false; s1 eq s2 => has(s1, f1, Insert(sub(s2,fl,bl1,li1,sl1,p1), sdb)) = f1 IsIn fl; s1 ne s2 => has(s1, f1, Insert(sub(s2,fl,bl1,li1,sl1,p1), sdb)) = has(s1, f1, sdb); isOnTCS(s1, s2, NoSDB) = false; s3 eq s2 => isOnTCS(s1, s2, Insert(sub(s3,fl,bl1,li1,sl1,p1), sdb)) = s1 IsIn sl1; s3 ne s2 => isOnTCS(s1, s2, Insert(sub(s3,fl,bl1,li1,sl1,p1), sdb)) = isOnTCS(s1, s2, sdb); ofsort SDB setLastIncoming(s1, li1, NoSDB) = NoSDB; s1 eq s2 => setLastIncoming(s1, li1, Insert(sub(s2,fl,bl1,li2,sl1,p1), sdb)) = Insert(sub(s2,fl,bl1,li1,sl1,p1), sdb); s1 ne s2 => setLastIncoming(s1, li1, Insert(sub(s2,fl,bl1,li2,sl1,p1), sdb)) = Insert(sub(s2,fl,bl1,li2,sl1,p1), setLastIncoming(s1, li1,sdb)); ofsort Address getLastIncoming(s1, NoSDB) = undefined; s1 eq s2 => getLastIncoming(s1, Insert(sub(s2,fl,bl1,li1,sl1,p1), sdb)) = li1; s1 ne s2 => getLastIncoming(s1, Insert(sub(s2,fl,bl1,li1,sl1,p1), sdb)) = getLastIncoming(s1, sdb); endtype (* SDB *) (*********************************************) (* The SCPit sort is an enumeration of the *) (* SCP types of information in the database. *) type SCPit is NaturalNumber sorts SCPit opns Redirect, TeenPIN, TeenTime, ForwardedTo : -> SCPit map : SCPit -> Nat _ eq _, _ ne _ : SCPit, SCPit -> Bool eqns forall s1, s2 : SCPit ofsort Nat map(Redirect) = 0; map(TeenPIN) = succ(0); map(TeenTime) = succ(succ(0)); map(ForwardedTo) = succ(succ(succ(0))); ofsort Bool s1 eq s2 = map(s1) eq map(s2); s1 ne s2 = not(s1 eq s2); endtype (* SCPit *) (* Information records about the feature parameters in the SCP *) (* These heterogeneous records share the same format to simplify *) (* the equations. *) type SCPinfo is SCPit, Address, Time, PIN sorts SCPinfo opns (* INFR: Redirect A B T1 T2 C *) (* -> scp(Redirect, A, B, T1, T2, C, validPIN) *) (* INTL: TeenPIN A PIN *) (* -> scp(TeenPIN, A, undefined, initTime, initTime, undefined, PIN) *) (* INTL: TeenTime A T1 T2 *) (* -> scp(TeenTime, A, undefined, T1, T2, undefined, validPIN) *) (* INCF: ForwardedTo B C *) (* -> scp(ForwardedTo, undefined, B, initTime, initTime, C, validPIN) *) scp : SCPit, Address, Address, Time, Time, Address, PIN -> SCPinfo _ eq _, _ ne _ : SCPinfo, SCPinfo -> Bool eqns forall s1, s2 : SCPit, a1, a2, b1, b2, c1, c2: Address, t11, t12, t21, t22 : Time, pin1, pin2 : PIN ofsort bool (s1 eq s2) and (a1 eq a2) and (b1 eq b2) and (c1 eq c2) and (t11 eq t12) and (t21 eq t22) and (pin1 eq pin2) => scp(s1, a1, b1, t11, t21, c1, pin1) eq scp(s2, a2, b2, t12, t22, c2, pin2) = true; not((s1 eq s2) and (a1 eq a2) and (b1 eq b2) and (c1 eq c2) and (t11 eq t12) and (t21 eq t22) and (pin1 eq pin2)) => scp(s1, a1, b1, t11, t21, c1, pin1) eq scp(s2, a2, b2, t12, t22, c2, pin2) = false; scp(s1, a1, b1, t11, t21, c1, pin1) ne scp(s2, a2, b2, t12, t22, c2, pin2) = not(scp(s1, a1, b1, t11, t21, c1, pin1) eq scp(s2, a2, b2, t12, t22, c2, pin2)) endtype (* SCPinfo *) (* Database of feature parameters (SCPinfo) in the SCP, implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization. *) type SCPDB0 is Set actualizedby SCPinfo using sortnames SCPinfo for Element Bool for FBool endtype (* SCPDB0 *) type SCPDB1 is SCPDB0 renamedby sortnames SCPDB for Set opnnames NoSCPDB for {} (* Empty list of feature parameters. *) endtype (* SCPDB1 *) (* Query operators *) type SCPDB is SCPDB1 opns (* Tells whether this is an INTL restricted time or not *) IsInTeenTime : Address, Time, SCPDB -> Bool IsValidTeenPIN : Address, PIN, SCPDB -> Bool eqns forall scpit : SCPit, a1, a2, b, c : Address, t, t1, t2 : Time, p, p1, p2 : PIN, scpdb : SCPDB ofsort Bool (* IsInTeenTime *) IsInTeenTime(a1, t, NoSCPDB) = false; (scpit eq TeenTime) and (a1 eq a2) and (t ge t1) and (t lt t2) => IsInTeenTime(a1, t, Insert(scp(scpit, a2, b, t1, t2, c, p), scpdb)) = true; not((scpit eq TeenTime) and (a1 eq a2) and (t ge t1) and (t lt t2)) => IsInTeenTime(a1, t, Insert(scp(scpit, a2, b, t1, t2, c, p), scpdb)) = IsInTeenTime(a1, t, scpdb); (* IsValidTeenPIN *) IsValidTeenPIN(a1, p1, NoSCPDB) = false; (scpit eq TeenPIN) and (a1 eq a2) and (p1 eq p2) => IsValidTeenPIN(a1, p1, Insert(scp(scpit, a2, b, t1, t2, c, p2), scpdb)) = true; not((scpit eq TeenPIN) and (a1 eq a2) and (p1 eq p2)) => IsValidTeenPIN(a1, p1, Insert(scp(scpit, a2, b, t1, t2, c, p2), scpdb)) = IsValidTeenPIN(a1, p1, scpdb); endtype (* SCPDB *) (*********************************************) (* The StatItem sort is an enumeration of the *) (* status items in the switch in the database. *) type StatItem is NaturalNumber sorts StatItem opns Busy, Ringing, AudibleRinging, ThreeWay, CallWaiting : -> StatItem map : StatItem -> Nat _ eq _, _ ne _ : StatItem, StatItem -> Bool eqns forall s1, s2 : StatItem ofsort Nat map(Busy) = 0; map(Ringing) = succ(0); map(AudibleRinging) = succ(succ(0)); map(ThreeWay) = succ(succ(succ(0))); map(CallWaiting) = succ(succ(succ(succ(0)))); ofsort Bool s1 eq s2 = map(s1) eq map(s2); s1 ne s2 = not(s1 eq s2); endtype (* StatItem *) (* Status records collected in the switch during calls *) type Stat is Address, StatItem sorts Stat opns (* POTS: Busy A -> stat(Busy, A, undefined) *) (* POTS: Ringing A B -> stat(Rigning, A, B) *) (* POTS: AudibleRinging A B -> stat(AudibleRinging, A, B) *) (* 3WC : ThreeWay X -> stat(ThreeWay, X, undefined) *) (* CW : CallWaiting X -> stat(CallWaiting, X, undefined) *) stat : StatItem, Address, Address -> Stat _ eq _, _ ne _ : Stat, Stat -> Bool eqns forall a1, a2, b1, b2: Address, si1, si2: StatItem ofsort Bool (a1 eq a2) and (b1 eq b2) and (si1 eq si2) => stat(si1, a1, b1) eq stat(si2, a2, b2) = true; not((a1 eq a2) and (b1 eq b2) and (si1 eq si2)) => stat(si1, a1, b1) eq stat(si2, a2, b2) = false; stat(si1, a1, b1) ne stat(si2, a2, b2) = not(stat(si1, a1, b1) eq stat(si2, a2, b2)); endtype (* Stat *) (* Database of status records in the switch, implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization. *) type Status0 is Set actualizedby Stat using sortnames Stat for Element Bool for FBool endtype (* Status0 *) type Status1 is Status0 renamedby sortnames Status for Set opnnames NoStatus for {} (* Empty list of status. *) endtype (* Status1 *) (* Query operators *) type Status is Status1 opns (* Tells whether a subscriber is Idle or Busy *) isIdle, isBusy : Address, Status -> Bool eqns forall a1, a2, b1, b2 : Address, si1, si2 : StatItem, s : Status ofsort Bool (* isIdle *) isIdle(a1, NoStatus) = true; (a1 eq a2) and (si2 eq Busy) => isIdle(a1, Insert(stat(si2, a2, b2), s)) = false; not((a1 eq a2) and (si2 eq Busy)) => isIdle(a1, Insert(stat(si2, a2, b2), s)) = isIdle(a1, s); (* isBusy *) isBusy(a1, s) = not(isIdle(a1, s)); endtype (* Status *) (*=============================================*) (* Stub Path ADT definitions *) (*=============================================*) (* Entry and exit points of each stub in the maps *) type StubPath is NaturalNumber sorts StubPath opns inPreD1, outPreD1, outPreD2, (* pre-dial stub *) inPostD1, outPostD1, outPostD2, outPostD3, outPostD4, outPostD5, (* post-dial stub *) inBill1, outBill2, (* billing stub *) inPC1, outPC1, outPC2, outPC3, outPC4, (* process-call stub *) inDisp1, outDisp1, (* display stub *) inBusy1, outBusy1, outBusy2 (* busy stub *) : -> StubPath map : StubPath -> Nat _ eq _, _ ne _ : StubPath, StubPath -> Bool eqns forall sp1, sp2 : StubPath ofsort Nat map(inPreD1) (* From OffHook *) = 0; map(outPreD1) (* To Dial *) = succ(map(inPreD1)); map(outPreD2) (* To Reject *) = succ(map(outPreD1)); map(inPostD1) (* From Dial *) = succ(map(outPreD2)); map(outPostD1) (* To Term-Connected *) = succ(map(inPostD1)); map(outPostD2) (* To Orig-Connected *) = succ(map(outPostD1)); map(outPostD3) (* To Billing *) = succ(map(outPostD2)); map(outPostD4) (* To Reject *) = succ(map(outPostD3)); map(outPostD5) (* To Busy *) = succ(map(outPostD4)); map(inBill1) (* From Post-Dial *) = succ(map(outPostD5)); map(outBill2) (* To Result-OS *) = succ(map(inBill1)); map(inPC1) (* From Call *) = succ(map(outBill2)); map(outPC1) (* To Ring (Term) *) = succ(map(inPC1)); map(outPC2) (* To Busy *) = succ(map(outPC1)); map(outPC3) (* To Reject *) = succ(map(outPC2)); map(outPC4) (* To stub itself *) = succ(map(outPC3)); map(inDisp1) (* From PC stub *) = succ(map(outPC4)); map(outDisp1) (* To OffHook *) = succ(map(inDisp1)); map(inBusy1) (* From Process-Call *) = succ(map(outDisp1)); map(outBusy1) (* To Busy *) = succ(map(inBusy1)); map(outBusy2) (* To Call_X *) = succ(map(outBusy1)); ofsort Bool sp1 eq sp2 = map(sp1) eq map(sp2); sp1 ne sp2 = not(sp1 eq sp2); endtype (* StubPath *) type SPList0 is Set actualizedby StubPath using sortnames StubPath for Element Bool for FBool endtype (* SPList0 *) type SPList is SPList0 renamedby sortnames SPList for Set opnnames NoSPList for {} (* Empty list of path identifiers. *) endtype (* SPList *) (*=============================================*) (* Behaviour Description *) (*=============================================*) behaviour (* Gates not visible to the users are set to be internal. *) (* Interfaces (e.g. Switch2User) are splitted into several*) (* gates, one per type of message. *) hide Trigger, (* Switch2SCP *) Resource, (* Switch2SCP *) Response, (* SCP2Switch *) LogBegin, (* 2OS *) LogEnd, (* 2OS *) AirBegin, (* 2OS *) AirEnd, (* 2OS *) Time (* NEW: Used by the Switch to get the time *) in (* Get the Initial state from the environment *) Init ?InitSDB:SDB ?InitStatus:Status ?InitSCPDB:SCPDB ?currentTime:Time; ( (* We create as many users as necessary. *) UserFactory [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, CreateUser] |[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display]| ( ( GlobalClock [Time](currentTime) |[Time]| Switch [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd, Time](InitSDB, InitStatus) |[Trigger, Resource, Response]| SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd](InitSCPDB) ) |[LogBegin, LogEnd, AirBegin, AirEnd]| OS [LogBegin, LogEnd, AirBegin, AirEnd, Query](NoLog) ) ) where (********************************************************************) (* Process UserFactory: To create ans initialise necessary users . *) (********************************************************************) process UserFactory [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, CreateUser]: noexit := CreateUser ?userId:Address ?userFeatures:FList; ( (* Create the user *) User [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display] (userId, userFeatures) ||| (* Prepare to accept new creation request *) UserFactory [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, CreateUser] ) endproc (* UserFactory *) (********************************************************************) (* Process User: To be instantiated by all users with a userId. *) (********************************************************************) process User [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display] (userId: Address, uf:FList): noexit := (* POTS - Origination (Root map) *) OffHook !userId; (*_PROBE_*) User [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display] (userId, uf) [] DialTone !userId; ( Dial !userId ?userTo:Address; User [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display] (userId, uf) [] OnHook !userId; (*_PROBE_*) stop ) [] LineBusyTone !userId; OnHook !userId; (*_PROBE_*) stop [] (* POTS - Origination (post-dial default map) *) StartAR !userId ?userTo:Address; ( OnHook !userId; StopAR !userId !userTo; (*_PROBE_*) stop [] StopAR !userId !userTo; (* CONNECTED state! Use Disconnect map. *) ( OnHook !userId; (*_PROBE_*) stop [] Disconnect !userId !userTo; OnHook !userId; (*_PROBE_*) stop ) ) [] (* POTS - Termination (post-dial default map) *) ( ( StartR !userId ?userFrom:Address; exit(userId, userFrom, uf, any SPList) ||| DisplayStub[Display](userId, uf, Insert(inDisp1, NoSPList)) ) >> accept userId:Address, userFrom:Address, uf:FList, outPaths:SPList in (* outDisp1 is the only possible outPath... *) [outDisp1 IsIn outPaths] -> ( OffHook !userId; StopR !userId !userFrom; (* CONNECTED state! Use Disconnect map) *) ( Disconnect !userId !UserFrom; OnHook !userId; (*_PROBE_*) stop [] OnHook !userId; (*_PROBE_*) stop ) [] (* userFrom has gon on-hook. *) StopR !userId !userFrom; (*_PROBE_*) stop ) ) [] (* INTL - Origination (pre-dial INTL map) *) Announce !userId !AskForPIN; ( Dial !userId ?p:PIN; (*_PROBE_*) User [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display] (userId, uf) [] OnHook !userId; (*_PROBE_*) stop ) [] Announce !userId !InvalidPIN; OnHook !userId; (*_PROBE_*) stop [] (* TCS reject *) Announce !userId !ScreenedMessage; OnHook !userId; (*_PROBE_*) stop (* NOT TO FORGET: Flash may be interpreted as OnHook-OffHook... *) where (********************************************************************) (* Stub Process DisplayStub: in map Post-Dial. One input path and *) (* one output path *) (********************************************************************) process DisplayStub[Display](userId:Address, uf:FList, inPaths:SPList) : exit(Address, Address, FList, SPList) := (* In this stub, CND is optional (we do not have access to SCPDB). *) [CND NotIn uf] -> (* Can’t put a probe here... Check P13!=P6+P7+P8 instead. *) (* POTS default plugin *) exit(userId, any Address, uf, Insert(outDisp1, NoSPList)) [] [CND IsIn uf] -> (* CND plugin. UserFrom provided by the switch. *) Display !userId ?userFrom:Address; (*_PROBE_*) exit(userId, any Address, uf, Insert(outDisp1, NoSPList)) endproc (* DisplayStub *) endproc (* User *) (********************************************************************) (* Process Switch: *) (********************************************************************) process Switch [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd, Time] (sdb:SDB, status:Status) : noexit := OffHook ?userFrom:Address [isIdle(userFrom, status)]; PreDialStub[OnHook, Trigger, Response, Resource, Announce, Dial, Time] (Insert(inPreD1, NoSPList), userFrom, sdb, (* Set userFrom Busy *) Insert(stat(Busy, userFrom, undefined), status)) >> accept userFrom:Address, sdb:SDB, status:Status, outPaths:SPList in (* outPreD1: Ok *) [outPreD1 IsIn outPaths] -> ( DialTone !userFrom; ( ( Dial !userFrom ?userTo:Address; PostDialStub[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time](Insert(inPostD1, NoSPList), userFrom, userTo, sdb, status) >> accept userFrom:Address, userTo:Address, userPay:Address, sdb:SDB, status:Status, outPaths:SPList in (* Output path 1 comes before 2,3, which can work as alternatives (for disconnection purposes). *) (* Paths 4, 5, and {1,2,3} are alternative paths. *) [outPostD1 IsIn outPaths] -> ( (* userFrom may have disconnected... *) [isBusy(userFrom, status)] -> Time ?t:time; LogBegin !userFrom !userTo !userPay !t; ( (* Orig-Connected, and Orig disconnects (POTS 7) *) [outPostD2 IsIn outPaths] -> ( OnHook !userFrom; ( let status:Status = Remove(stat(Busy, userFrom, undefined), status) in ( Disconnect !userTo !userFrom; exit(userFrom, userTo, sdb, status) ||| Time ?t:time; LogEnd !userFrom !userTo !t; exit(userFrom, userTo, sdb, status) ) >> accept userFrom:Address, userTo:Address, sdb:SDB, status:Status in OnHook !userTo; ( let status:Status = Remove(stat(Busy, userTo, undefined), status) in (*_PROBE_*) stop ) ) ) [] (* Term-Connected, and Term disconnects (POTS 10) *) [outPostD3 IsIn outPaths] -> ( OnHook !userTo; ( let status:Status = Remove(stat(Busy, userTo, undefined), status) in ( Disconnect !userFrom !userTo; exit(userFrom, userTo, sdb, status) ||| Time ?t:time; LogEnd !userFrom !userTo !t; exit(userFrom, userTo, sdb, status) ) >> accept userFrom:Address, userTo:Address, sdb:SDB, status:Status in OnHook !userFrom; ( let status:Status = Remove(stat(Busy, userFrom, undefined), status) in (*_PROBE_*) stop ) ) ) ) [] [IsIdle(userFrom, status)] -> ( (* UserFrom has gone on-hook. *) (*_PROBE_*) stop ) ) [] [outPostD4 IsIn outPaths] -> ( (* Reject path. *) Announce !userFrom !ScreenedMessage; OnHook !userFrom; ( let status:Status = Remove(stat(Busy, userFrom, undefined), status) in (*_PROBE_*) stop ) ) [] [outPostD5 IsIn outPaths] -> ( (* Busy. (POTS 15) *) LineBusyTone !userFrom; OnHook !userFrom; ( let status:Status = Remove(stat(Busy, userFrom, undefined), status) in (*_PROBE_*) stop ) ) ) [] OnHook !userFrom; (* From POTS 7-12? *) ( (* Set userFrom Idle *) let status:Status = Remove(stat(Busy, userFrom, undefined), status) in (*_PROBE_*) stop ) ) ) ||| (* outPreD2: reject *) [outPreD2 IsIn outPaths] -> ( OnHook !userFrom; (* From INTL 12 *) ( (* Set userFrom Idle *) let status:Status = Remove(stat(Busy, userFrom, undefined), status) in (*_PROBE_*) stop ) ) where (********************************************************************) (* Stub Process PreDialStub: *) (********************************************************************) process PreDialStub[OnHook, Trigger, Response, Resource, Announce, Dial, Time] (inPaths: SPList, userFrom: Address, sdb: SDB, status: Status):exit (Address, SDB, Status, SPList) := (* In this stub, INTL is mutually exclusive with all other features. *) (* INTL plugin *) [has(userFrom, INTL, sdb)] -> (* NEW EVENTS: we believe that the INTL information should be located in the SCP. *) (* Is the time in the subscriber's TeenTime interval? *) Time ?time:Time; (* Get the current time *) Resource !INTL !userFrom !time; Response !INTL !userFrom ?inTeenTime:Bool; ( (* Unrestricted time for INTL *) [not(inTeenTime)] -> (*_PROBE_*) exit (userFrom, sdb, status, Insert(outPreD1, NoSPList)) [] (* Restricted time for INTL *) [inTeenTime] -> Trigger !ORIGINATION_ATTEMPT !userFrom !userFrom !undefined !time ; Response !SEND_TO_RESOURCE !userFrom ?m:message; Announce !userFrom !m; ( OnHook !UserFrom; (*_PROBE_*) stop (* INTL 13 *) [] Dial !userFrom ?pin:PIN; Resource !userFrom !pin; ( Response !CONTINUE !userFrom !userFrom !undefined; (*_PROBE_*) exit (userFrom, sdb, status, Insert(outPreD1, NoSPList)) [] Response !SEND_TO_RESOURCE !userFrom !invalidPIN; Resource !userFrom !undefined; Announce !userFrom !invalidPIN; Response !DISCONNECT !userFrom !undefined; (*_PROBE_*) exit (userFrom, sdb, status, Insert(outPreD2, NoSPList)) ) ) ) [] (* Default plugin *) [not(has(userFrom, INTL, sdb))] -> (*_PROBE_*) exit (userFrom, sdb, status, Insert(outPreD1, NoSPList)) endproc (* PreDialStub *) (********************************************************************) (* Stub Process PostDialStub: *) (********************************************************************) process PostDialStub[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths: SPList, userFrom: Address, userTo:Address, sdb: SDB, status: Status):exit (Address, Address, Address, SDB, Status, SPList) := (* Use the processCallStub first *) ProcessCallStub[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (Insert(inPC1, NoSPList), userFrom, userTo, sdb, status) >> accept userFrom:Address, userTo:Address, userPay:Address, sdb:SDB, status:Status, outPaths:SPList in (* All choices are mutually exclusive here. *) (* outPC1: Idle *) [outPC1 IsIn outPaths] -> ( (* Set userTo Busy *) let status:Status = Insert(stat(Busy, userTo, undefined), status) in ( StartAR !userFrom !userTo; (*_PROBE_*) exit (userFrom, userTo, userPay, any SDB, Insert(stat(AudibleRinging, userFrom, userTo), Insert(stat(Ringing, userTo, userFrom), status))) ||| StartR !userTo !userFrom; (*_PROBE_*) exit (userFrom, userTo, userPay, any SDB, Insert(stat(AudibleRinging, userFrom, userTo), Insert(stat(Ringing, userTo, userFrom), status))) ||| (* For SetDisplayStub and CND plugin for ProcessCallStub *) ( [has(userTo, CND, sdb)] -> (* Update LastIncoming and Display it. *) Display !userTo !userFrom; (*_PROBE_*) exit (userFrom, userTo, userPay, setLastIncoming(userTo, userFrom, sdb), any Status) [] [not(has(userTo, CND, sdb))] -> (* Do nothing special *) (*_PROBE_*) exit (userFrom, userTo, userPay, sdb, any Status) ) ) >> accept userFrom:Address, userTo:Address, userPay:Address, sdb:SDB, status:Status in OffHook !userTo; (* POTS 5 *) ( StopAR !userFrom !userTo; (*_PROBE_*) exit ( userFrom, userTo, userPay, sdb, Remove(stat(AudibleRinging, userFrom, userTo), Remove(stat(Ringing, userTo, userFrom), status)), Insert(outPostD1, Insert(outPostD2, Insert(outPostD3, NoSPList))) ) ||| StopR !userTo !userFrom; (*_PROBE_*) exit ( userFrom, userTo, userPay, sdb, Remove(stat(AudibleRinging, userFrom, userTo), Remove(stat(Ringing, userTo, userFrom), status)), Insert(outPostD1, Insert(outPostD2, Insert(outPostD3, NoSPList))) ) ) [] (* Disconnection possible here... *) OnHook !userFrom; (* POTS 5 *) ( (* Set userFrom Idle *) let status:Status = Remove(stat(Busy, userFrom, undefined), status) in ( StopAR !userFrom !userTo; (* Set userTo idle after the synchronization *) (*_PROBE_*) exit (userFrom, userTo, userPay, sdb, Remove(stat(Busy, userTo, undefined), Remove(stat(AudibleRinging, userFrom, userTo), Remove(stat(Ringing, userTo, userFrom), status))), Insert(outPostD1, NoSPList)) ||| StopR !userTo !userFrom; (*_PROBE_*) exit (userFrom, userTo, userPay, sdb, Remove(stat(Busy, userTo, undefined), Remove(stat(AudibleRinging, userFrom, userTo), Remove(stat(Ringing, userTo, userFrom), status))), Insert(outPostD1, NoSPList)) ) ) ) [] (* outPC2: Busy *) [outPC2 IsIn outPaths] -> ( (* Invoke BusyStub *) BusyStub[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (Insert(inBusy1, NoSPList), userFrom, userTo, userPay, sdb, status) >> accept userFrom:Address, userTo:Address, userPay:Address, sdb:SDB, status:Status, outPaths:SPList in [outBusy1 IsIn outPaths] -> (* CC: invalid PIN *) (*_PROBE_*) exit (userFrom, userTo, userPay, sdb, status, Insert(outPostD5, NoSPList)) [] [outBusy2 IsIn outPaths] -> (* TO BE DONE *) (*_PROBE_*) stop ) [] (* outPC3: Reject *) [outPC3 IsIn outPaths] -> ( (* TCS Reject *) (*_PROBE_*) exit (userFrom, userTo, userPay, sdb, status, Insert(outPostD4, NoSPList)) ) [] (* outPC4: Back to stub *) [outPC4 IsIn outPaths] -> ( (*_PROBE_*) stop (* TO BE DONE *) ) where (************************************************************) (* Stub Process ProcessCallStub: *) (************************************************************) process ProcessCallStub [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths: SPList, userFrom: Address, userTo:Address, sdb: SDB, status: Status) : exit (Address, Address, Address, SDB, Status, SPList) := (* CND will be taken care of at outPC1, after all these plug-ins. *) (* TCS (reject path) has priority over the other features. *) [has(userTo, TCS, sdb) and isOnTCS(userFrom, userTo, SDB)] -> (*_PROBE_*) (* Caller on the list. Reject call. *) exit (userFrom, userTo, userFrom, sdb, status, Insert(outPC3, NoSPList)) [] (* Remaining features *) [not(has(userTo, TCS, sdb) and isOnTCS(userFrom, userTo, SDB))] -> ( (* INFB *) [has(userTo, INFB, sdb)] -> (*_PROBE_*) PluginINFB[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths, userFrom, userTo, sdb, status) [] (* Default *) [not(has(userTo, INFB, sdb))] -> (*_PROBE_*) PluginDefault[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths, userFrom, userTo, sdb, status) ) where process PluginINFB[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths: SPList, userFrom: Address, userTo:Address, sdb: SDB, status: Status) : exit (Address, Address, Address, SDB, Status, SPList) := (* INFB plugin for ProcessCallStub *) Time ?t:Time; Trigger !INFO_ANALYZED !userTo !userFrom !userTo !t; Response !ANALYZE_ROUTE !userTo !userFrom !userTo !userTo; ( [IsIdle(userTo, status)] -> (*_PROBE_*) (* Called party (userTo) pays. *) exit (userFrom, userTo, userTo, sdb, status, Insert(outPC1, NoSPList)) [] [IsBusy(userTo, status)] -> (*_PROBE_*) exit (userFrom, userTo, userTo, sdb, status, Insert(outPC2, NoSPList)) ) endproc (* PluginINFB *) process PluginDefault [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths: SPList, userFrom: Address, userTo:Address, sdb: SDB, status: Status) : exit (Address, Address, Address, SDB, Status, SPList) := (* Default plugin for ProcessCallStub *) [IsIdle(userTo, status)] -> (*_PROBE_*) exit (userFrom, userTo, userFrom, sdb, status, Insert(outPC1, NoSPList)) [] [IsBusy(userTo, status)] -> (*_PROBE_*) exit (userFrom, userTo, userFrom, sdb, status, Insert(outPC2, NoSPList)) endproc (* PluginDefault *) endproc (* ProcessCallStub *) (************************************************************) (* Stub Process BusyStub: *) (************************************************************) process BusyStub [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Trigger, Resource, Response, LogBegin, LogEnd, Time] (inPaths: SPList, userFrom: Address, userTo:Address, userPay:Address, sdb: SDB, status: Status) : exit (Address, Address, Address, SDB, Status, SPList) := (* POTS default plugin. *) exit (userFrom, userTo, userPay, sdb, status, Insert(outBusy1, NoSPList)) (* No probe here. Obviously covered for now. *) (* TO BE DONE: other plugins. *) endproc (* BusyStub *) endproc (* PostDialStub *) endproc (* Switch *) (********************************************************************) (* Process SCP: *) (********************************************************************) process SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd] (scpbd:SCPDB) : noexit := (* From INTL: check if time is within TeenTime limits. *) Resource !INTL ?user:Address ?time:Time; Response !INTL !user !IsInTeenTime(user, time, scpbd); (*_PROBE_*) SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd](scpbd) [] (* From INTL: Origination attempt to connect. Ask for PIN. *) Trigger !ORIGINATION_ATTEMPT ?user:Address ?user2:Address !undefined ?t:Time [user eq user2]; Response !SEND_TO_RESOURCE !user !AskForPIN; (*_PROBE_*) SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd](scpbd) [] (* From INTL: check PIN *) Resource ?user:Address ?pin:PIN; ( [IsValidTeenPIN(user, pin, scpbd)] -> Response !CONTINUE !user !user !undefined; (*_PROBE_*) SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd](scpbd) [] [not(IsValidTeenPIN(user, pin, scpbd))] -> Response !SEND_TO_RESOURCE !user !invalidPIN; Resource ?user:Address !undefined; Response !DISCONNECT !user !undefined; (*_PROBE_*) SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd](scpbd) ) [] (* From INFB: IN Analyze *) Trigger !INFO_ANALYZED ?userTo:Address ?userFrom:Address ?userTo2:Address ?t:Time [userTo eq userTo2]; Response !ANALYZE_ROUTE !userTo !userFrom !userTo !userTo; (*_PROBE_*) SCP [Trigger, Resource, Response, LogBegin, LogEnd, AirBegin, AirEnd](scpbd) endproc (* SCP *) (********************************************************************) (* Process OS: *) (********************************************************************) process OS [LogBegin, LogEnd, AirBegin, AirEnd, Query](log:Log) : noexit := LogBegin ?From:Address ?To:Address ?Paying:Address ?t:Time; (*_PROBE_*) OS[LogBegin, LogEnd, AirBegin, AirEnd, Query] (Insert(l(Begin, From, To, Paying, t),log)) [] LogEnd ?From:Address ?To:Address ?t:Time; (*_PROBE_*) OS[LogBegin, LogEnd, AirBegin, AirEnd, Query] (Insert(l(End, From, To, undefined, t),log)) [] (* For Phase II features *) AirBegin ?From:Address ?t:Time; (*_PROBE_*) OS[LogBegin, LogEnd, AirBegin, AirEnd, Query] (Insert(l(AirBegin, From, undefined, undefined, t),log)) [] AirEnd ?From:Address ?t:Time; (*_PROBE_*) OS[LogBegin, LogEnd, AirBegin, AirEnd, Query] (Insert(l(AirEnd, From, undefined, undefined, t),log)) [] (* NEW functionality which allow a test case to check the Log. *) Query !log; (*_PROBE_*) OS[LogBegin, LogEnd, AirBegin, AirEnd, Query](log) endproc (* OS *) (********************************************************************) (* Process GlobalClock: computes the relative time incrementally and*) (* provides timestamps (t) when required. *) (********************************************************************) process GlobalClock [Time](t:Time) : noexit := Time !T; GlobalClock[Time](tic(t)) (* No probe here. Obviously covered... *) endproc (* GlobalClock *) (*====================================================================*) (* *) (* POTS PROCESSES *) (* *) (*====================================================================*) (* These six processes represent common test sequences (repreenting *) (* a canonical tester) among many features (POTS states 1, 2, 4, 5, *) (* 13 and 15). 3WC and CW are not covered entirely by these. *) (* They all exit so that we can check the Log afterwards in test cases*) (* using these processes. *) process POTS_1 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom:Address, userTo:Address) : exit(Nat) := OffHook !userFrom; POTS_2 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) endproc (* POTS_1 *) process POTS_2 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom:Address, userTo:Address) : exit(Nat) := DialTone !userFrom; (* State 2 *) ( i; OnHook !userFrom; exit(succ(succ(succ(succ(0))))) (* State 17 *) [] i; Dial !userFrom !userTo; (* State 3 *) ( POTS_4 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) [] POTS_15 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) ) ) endproc (* POTS_2 *) process POTS_4 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom:Address, userTo:Address) : exit(Nat) := ( StartAR !userFrom !userTo; exit(userFrom, userTo) ||| StartR !userTo !userFrom; exit(userFrom, userTo) ) >> accept userFrom:Address, userTo:Address in ( i; POTS_5 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) [] i; POTS_13[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) ) endproc (* POTS_4 *) process POTS_5 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom:Address, userTo:Address) : exit(Nat) := OffHook !userTo; ( (* State 6 *) StopAR !userFrom !userTo; exit(userFrom, userTo) ||| StopR !userTo !userFrom; exit(userFrom, userTo) ) >> accept userFrom:Address, userTo:Address in ( i; OnHook !userFrom; (* State 7 *) Disconnect !userTo !userFrom; (* State 8 *) onHook !userTo; exit(0) (* State 9 *) [] i; OnHook !userTo; (* State 10 *) Disconnect !userFrom !userTo; (* State 11 *) OnHook !userFrom; exit(succ(0)) (* State 12 *) ) endproc (* POTS_5 *) process POTS_13[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom:Address, userTo:Address) : exit(Nat) := OnHook !userFrom; ( (* State 14 *) StopAR !userFrom !userTo; exit(succ(succ(0))) ||| StopR !userTo !userFrom; exit(succ(succ(0))) ) endproc (* POTS_13 *) process POTS_15[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom:Address, userTo:Address) : exit(Nat) := LineBusyTone !userFrom; OnHook !userFrom; exit(succ(succ(succ(0)))) (* State 16 *) endproc (* POTS_15 *) (*====================================================================*) (* *) (* TEST PROCESSES *) (* *) (*====================================================================*) (**********) (** POTS **) (**********) (* TEST CASES *) process tPOTS1 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Init, CreateUser, Query, Success] : noexit := (* Cases where userB is not busy. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, NoFList, undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !NoFList; POTS_1 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userA, userB) (* Check the Log *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(InitTime)), Insert(l(Begin, userA, userB, userA, InitTime), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) endproc (* tPOTS1 *) process tPOTS2 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Init, CreateUser, Query, Success] : noexit := (* Cases where userB is busy. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, NoFList, undefined, undefined, NoAddList, validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !NoFList; POTS_1 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userA, userB) (* Check the Log *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) endproc (* tPOTS2 *) (**********) (** INTL **) (**********) (* COMMON BEHAVIOUR *) process cINTL1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] : exit(Nat) := (* Cases where TeenTime is restricted and A provides the valid PIN. *) OffHook !userA; Announce !userA !AskForPIN; ( i; Dial !userA !validPIN; POTS_2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userA, userB) [] i; OnHook !userA; exit(succ(succ(succ(succ(succ(0)))))) ) endproc (* cINTL1 *) process cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] : exit(Nat) := (* Cases where TeenTime is restricted and A does not provide the valid PIN. *) OffHook !userA; Announce !userA !AskForPIN; ( i; Dial !userA !invalidPIN; Announce !userA !invalidPIN; OnHook !userA; exit (succ(succ(succ(succ(succ(succ(0))))))) [] i; OnHook !userA; exit(succ(succ(succ(succ(succ(0)))))) ) endproc (* cINTL2 *) (* TEST PROCESSES *) process tINTL1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where TeenTime is not restricted. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, NoFList, undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, tic(tic(initTime)), tic(tic(tic(initTime))), undefined, validPIN), NoSCPDB) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !NoFList; POTS_1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) (* Check the Log *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userA, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) endproc (* tINTL1 *) process tINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where TeenTime is restricted and A provides the valid PIN. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, NoFList, undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !NoFList; cINTL1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userA, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) endproc (* tINTL2 *) process tINTL3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where TeenTime is restricted and A does not provide the valid PIN. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, NoFList, undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !NoFList; cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* No connection *) [(exitCode eq succ(succ(succ(succ(succ(0)))))) or (exitCode eq succ(succ(succ(succ(succ(succ(0)))))))] -> Query !NoLog; Success; stop ) endproc (* tINTL3 *) (*********) (** CND **) (*********) (* COMMON BEHAVIOUR *) process cCND1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] : exit(Nat) := (* Starts at POTS state 2. *) (* Should Display the originator's number. *) DialTone !userA; Dial !userA !userB; ( StartAR !userA !userB; exit(userA, userB) ||| StartR !userB !userA; exit(userA, userB) ||| Display !userB !userA; exit(userA, userB) ) >> accept userFrom:Address, userTo:Address in ( i; POTS_5 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) [] i; POTS_13[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userFrom, userTo) ) endproc (* cCND1 *) (* TEST PROCESSES *) process tCND1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Should Display the originator's number. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(CND, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(CND, NoFList); OffHook !userA; cCND1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(InitTime)), Insert(l(Begin, userA, userB, userA, InitTime), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) endproc (* tCND1 *) process tCND2 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Init, CreateUser, Query, Success] : noexit := (* Cases where userB is busy. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(INFB, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(INFB, NoFList); POTS_1 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (userA, userB) (* Check the Log *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) endproc (* tCND2 *) (**********) (** INFB **) (**********) (* NO SPECIAL COMMON BEHAVIOUR *) (* TEST PROCESSES *) process tINFB1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where B is not Busy. Affect the billing. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(INFB, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(INFB, NoFList); POTS_1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) (* Check the Log. UserB should be charged. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userB, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) endproc (* tINFB1 *) process tINFB2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where B is Busy. Do not affect billing. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(INFB, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(INFB, NoFList); POTS_1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) (* Check the Log *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) endproc (* tINFB2 *) (*********) (** TCS **) (*********) (* COMMON BEHAVIOUR *) process cTCS1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] : exit(Nat) := OffHook !userA; DialTone !userA; (* State 2 *) ( i; OnHook !userA; exit(succ(succ(succ(succ(0))))) (* State 17 *) [] i; Dial !userA !userB; (* State 3 *) POTS_4[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) ) endproc (* cTCS1 *) process cTCS2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] : exit(Nat) := OffHook !userA; DialTone !userA; (* State 2 *) ( i; OnHook !userA; exit(succ(succ(succ(succ(0))))) (* State 17 *) [] i; Dial !userA !userB; (* State 3 *) POTS_15[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) ) endproc (* cTCS2 *) process cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] : exit(Nat) := OffHook !userA; DialTone !userA; (* State 2 *) ( i; OnHook !userA; exit(succ(succ(succ(succ(0))))) (* State 17 *) [] i; Dial !userA !userB; (* State 3 *) Announce !userA !ScreenedMessage; OnHook !userA; exit(succ(succ(succ(succ(0))))) (* TCS State 4, same as POTS State 17 *) ) endproc (* cTCS3 *) (* TEST PROCESSES *) process tTCS1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where B is not Busy and A is not screened. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, NoFList); cTCS1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. UserA should be charged. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(InitTime)), Insert(l(Begin, userA, userB, userA, InitTime), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) endproc (* tTCS1 *) process tTCS2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where B is Busy and A is not screened. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, NoFList); cTCS2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) endproc (* tTCS2 *) process tTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Cases where A is screened. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, NoFList); cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) endproc (* tTCS3 *) (*====================================================================*) (* *) (* FI TEST PROCESSES *) (* *) (*====================================================================*) (**************) (* INTL - CND *) (**************) process fiINTL_CND[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Should Display the originator's number. *) ( (* Cases where TeenTime is not restricted. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(CND, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, tic(tic(initTime)), tic(tic(tic(initTime))), undefined, validPIN), NoSCPDB) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(CND, NoFList); OffHook !userA; cCND1 [OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userA, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* tINTL2 *) (* Cases where TeenTime is restricted and A provides the valid PIN. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(CND, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(CND, NoFList); OffHook !userA; Announce !userA !AskForPIN; Dial !userA !validPIN; cCND1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userA, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* tINTL3 *) (* Cases where TeenTime is restricted and A does not provide the valid PIN. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(CND, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(CND, NoFList); cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* No connection *) [(exitCode eq succ(succ(succ(succ(succ(0)))))) or (exitCode eq succ(succ(succ(succ(succ(succ(0)))))))] -> Query !NoLog; Success; stop ) ) endproc (* fiINTL_CND *) (***************) (* INTL - INFB *) (***************) process fiINTL_INFB[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := (* Should Display the originator's number. *) ( (* Cases where TeenTime is not restricted. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(INFB, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, tic(tic(tic(initTime))), tic(tic(tic(tic(initTime)))), undefined, validPIN), NoSCPDB) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(INFB, NoFList); POTS_1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) (* Check the Log. UserB should be charged. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(tic(InitTime)))), Insert(l(Begin, userA, userB, userB, tic(tic(InitTime))), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* tINTL2 *) (* Cases where TeenTime is restricted and A provides the valid PIN. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(INFB, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(tic(initTime))), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(INFB, NoFList); cINTL1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. UserB should be charged. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(tic(InitTime)))), Insert(l(Begin, userA, userB, userB, tic(tic(InitTime))), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* tINTL3 *) (* Cases where TeenTime is restricted and A does not provide the valid PIN. *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(INFB, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(tic(initTime))), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(INFB, NoFList); cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* No connection *) [(exitCode eq succ(succ(succ(succ(succ(0)))))) or (exitCode eq succ(succ(succ(succ(succ(succ(0)))))))] -> Query !NoLog; Success; stop ) ) endproc (* fiINTL_INFB *) (****************) (** CND - INFB **) (****************) process fiCND_INFB[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := ( (* Should Display the originator's number. *) (* Cases where B is not Busy. Affect the billing. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(CND, Insert(INFB, NoFList)), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(CND, Insert(INFB, NoFList)); OffHook !userA; cCND1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. UserB should be charged. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userB, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where B is Busy. Does not affect billing. *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(CND, Insert(INFB, NoFList)), undefined, undefined, NoAddList, validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(CND, Insert(INFB, NoFList)); POTS_1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success](userA, userB) (* Check the Log *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) endproc (* fiCND_INFB *) (**************) (* INTL - TCS *) (**************) process fiINTL_TCS[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := ( (* Cases where A's TeenTime is not restricted, A is not on B's TCS list, and B is idle. *) (* tTCS1 and tINTL1 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, tic(tic(initTime)), tic(tic(tic(initTime))), undefined, validPIN), NoSCPDB) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cTCS1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userA, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is not restricted, A is not on B's TCS list, and B is Busy. *) (* tTCS2 and tINTL1 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !Insert(scp(TeenTime, userA, undefined, tic(tic(initTime)), tic(tic(tic(initTime))), undefined, validPIN), NoSCPDB) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cTCS2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is not restricted, and A is on B's TCS list. *) (* tTCS3 and tINTL1 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !Insert(scp(TeenTime, userA, undefined, tic(tic(initTime)), tic(tic(tic(initTime))), undefined, validPIN), NoSCPDB) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is restricted, A has the valid PIN, A is not on B's TCS list, and B is idle. *) (* tTCS1 and tINTL2 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cINTL1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userA, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is restricted, A has the valid PIN, A is not on B's TCS list, and B is busy. *) (* tTCS2 and tINTL2 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cINTL1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is restricted, A has the valid PIN, A is on B's TCS list. *) (* tTCS3 and tINTL2 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); OffHook !userA; Announce !userA !AskForPIN; ( i; Dial !userA !validPIN; DialTone !userA; Dial !userA !userB; Announce !userA !ScreenedMessage; OnHook !userA; exit(succ(succ(succ(succ(0))))) (* TCS State 4, same as POTS State 17 *) [] i; OnHook !userA; exit(succ(succ(succ(0)))) ) (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is restricted, A has an invalid PIN, A is not on B's TCS list, and B is idle. *) (* tTCS1 and tINTL3 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, invalidPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* No connection *) [(exitCode eq succ(succ(succ(succ(succ(0)))))) or (exitCode eq succ(succ(succ(succ(succ(succ(0)))))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is restricted, A has an invalid PIN, A is not on B's TCS list, and B is busy. *) (* tTCS1 and tINTL3 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, invalidPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, NoAddList, validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* No connection *) [(exitCode eq succ(succ(succ(succ(succ(0)))))) or (exitCode eq succ(succ(succ(succ(succ(succ(0)))))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A's TeenTime is restricted, A has an invalid PIN, A is on B's TCS list *) (* tTCS1 and tINTL3 *) Init !Insert(sub(userA, Insert(INTL, NoFList), undefined, undefined, NoAddList, invalidPIN), Insert(sub(userB, Insert(TCS, NoFList), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !NoStatus !Insert(scp(TeenTime, userA, undefined, initTime, tic(tic(initTime)), undefined, validPIN), Insert(scp(TeenPIN, userA, undefined, initTime, initTime, undefined, validPIN), NoSCPDB)) !InitTime; CreateUser !userA !Insert(INTL, NoFList); CreateUser !userB !Insert(TCS, NoFList); cINTL2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* No connection *) [(exitCode eq succ(succ(succ(succ(succ(0)))))) or (exitCode eq succ(succ(succ(succ(succ(succ(0)))))))] -> Query !NoLog; Success; stop ) ) endproc (* fiINTL_TCS *) (*************) (* CND - TCS *) (*************) process fiCND_TCS[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := ( (* Cases where A is not on B's TCS list, and B is idle. Should Display the originator's number. *) (* tTCS1 and tCND1 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(CND, NoFList)), undefined, undefined, NoAddList, validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(CND, NoFList)); OffHook !userA; cCND1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(InitTime)), Insert(l(Begin, userA, userB, userA, InitTime), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A is not on B's TCS list, and B is busy. *) (* tTCS2 and tCND2 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(CND, NoFList)), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(CND, NoFList)); cTCS2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A is on B's TCS list, and B is busy. Do not display. *) (* tTCS3 and tCND2 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(CND, NoFList)), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(CND, NoFList)); cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A is on B's TCS list, and B is idle. Do not display. *) (* tTCS3 and tCND1 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(CND, NoFList)), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(CND, NoFList)); cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) endproc (* fiCND_TCS *) (**************) (* INFB - TCS *) (**************) process fiINFB_TCS[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success, CreateUser, Query, Init] : noexit := ( (* Cases where A is not on B's TCS list, and B is idle. Affect the billing. *) (* tTCS1 and tINFB1 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(INFB, NoFList)), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(INFB, NoFList)); cTCS1[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. UserB should be charged. *) >> accept exitCode:Nat in ( (* One connection *) [(exitCode eq 0) or (exitCode eq succ(0))] -> Query !Insert(l(End, userA, userB, undefined, tic(tic(InitTime))), Insert(l(Begin, userA, userB, userB, tic(InitTime)), NoLog)); Success; stop [] (* No connection *) [not( (exitCode eq 0) or (exitCode eq succ(0)) )] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A is not on B's TCS list, and B is busy. Do not affect the billing. *) (* tTCS2 and tINFB2 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(INFB, NoFList)), undefined, undefined, Insert(userC, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(INFB, NoFList)); cTCS2[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A is on B's TCS list, and B is busy. Do not affect the billing. *) (* tTCS3 and tINFB2 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(INFB, NoFList)), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !Insert(stat(Busy, userB, undefined), NoStatus) !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(INFB, NoFList)); cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) [] ( (* Cases where A is on B's TCS list, and B is idle. Do not affect the billing. *) (* tTCS3 and tINFB1 *) Init !Insert(sub(userA, NoFList, undefined, undefined, NoAddList, validPIN), Insert(sub(userB, Insert(TCS, Insert(INFB, NoFList)), undefined, undefined, Insert(userA, NoAddList), validPIN), NoSDB)) !NoStatus !NoSCPDB !InitTime; CreateUser !userA !NoFList; CreateUser !userB !Insert(TCS, Insert(INFB, NoFList)); cTCS3[OffHook, OnHook, Dial, Flash, DialTone, StartAR, StartR, StartCWT, StopAR, StopR, StopCWT, LineBusyTone, Announce, Disconnect, Display, Success] (* Check the Log. *) >> accept exitCode:Nat in ( (* No connection only. *) [(exitCode eq succ(succ(succ(0)))) or (exitCode eq succ(succ(succ(succ(0)))))] -> Query !NoLog; Success; stop ) ) endproc (* fiINFB_TCS *) endspec (* FI_UCM *)