------------------------SDT2:Proxy----------------------------------------------------ObjectName----------------------------------------ObjectType----------------------------------------!%&()LinkEndpoints--------------------------------!%()HeadingText----------------------------------- Proxy----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------5--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------()[8(! process Proxy)]}---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------%()[w(!GSDL)]}-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------()[(! l! 22!(d)[h(! l)[k(! 6)[n(! 6d! )]][ q(! 6)][2(! 6d! d!S)[8(! )!%()HeadingText-----------------------------------!%()PageOrder-------------------------------------1------------------------------------------------3------------------------------------------------- !%&()LinkEndpoints--------------------------------1------------------------------------------------------------------------------------------------------------------------------------------------------- ------------------------][(!,!",)[(! 6,!Z)][3(! 6,! d!S)[8(! Idle)]]]][(! 6d!! !S)[ 8(! Signals from MS)]][9t(! 6~d! !S)[8(! newtype BTS_PIDs_t ARRAY( BTS_ID_t, PID); endnewtype; newtype MS_PIDs_t ARRAY( Mobile_ID_t, PID); endnewtype; dcl MID1, MID2 Mobile_ID_t /* rep laces context parameters.*/, IMEI IMEI_t /* replaces context parameters.*/, called_state called_state_t, encryptedNr NATURAL, rand NATURAL, billingReport billing_report_t, reason reason_t, BTS_ID BTS_ID_t, BTS_PIDs BTS_PIDs_t, MS_PIDs MS_ PIDs_t;)]][3(! 6X! d!S)[8(! Idle)][(!,, !", ,)[(! 6 ! d!S!)[8(!- call_resp(called _state, MID1, MID2, BTS_ID))][(!,,!",,)[(! 6! d!S!)[8(!C call_resp(called_state, MID1, MID2, BTS_ID) to BTS_PIDs(BTS_ID) )][ (!,L,!",,L)[(! 6,!Z)][3(! 6! d!S)[8(! Idle)]]]]]]]][3z(! 6! d!S)[8(! Idle)][(!~!"~)[(! 6! d!S!)[8(! call_req(MID1, MID2, BTS_ID))][(!F!"F)[(! 6! d!S!)[8(!3 call_req(MID1, MID2, BTS_ID) to BTS_PIDs(BTS_ID) )][(!r!"r)[(! 6r!Z)][3(! 6r! d!S)[8(! Idle)]]]]]]]][3(! 6! d!S)[8(! Idle)][(!,@,!",,@)[(! 6! d!S!)[8(! com_start(MID1, BTS_ID))][(!,,l!",l,)[(! 6l! d!S!)[8(!. com_start(MID1, BTS_ID) to BTS_PIDs(BTS_ID) )][(!,,4!",4,)[(! 6,4!Z)][3(! 64! d!S)[8(! Idle)]]]]]]]]]]}3(! 64()[(! l! 22!(d)[(! l)[(! 6)[(! 6d! )]][ (! 6)][-(! 6d!! !S)[82(!f!"f3)[(! 6f!Z4)][3(! 62f! d!S)[8(! Idle)]]]]]]]][3(! $S (! Signals from MS)]][3(! 6d^! d!S)[8(! Idle)][ (!&!"&)[(! 6d&! d!S!)[8(!! com_finish(MID1, MID2, BTS_ID) )][(!!")[(! 6d! d!S!)[8(!4 com_finish(MID1, MID2, BTS_ID) to BTS_PIDs(BTS_ID))][!(!R!"R)[(! 6!Z)][3(! 6d! d!S)[8(! Idle)]]]]]]]][3(! 6^! d!S)[8(! Idle)][ (!LL&!"L&L)[(! 6&! d!S!)[8(! getReport(MID1, BTS_ID))][(!LL!"LL)[(! 6! d!S!)[8(!- getReport(MID1, BTS_ID) to BTS_PIDs(BTS_ID))][$(!LRL!"LLR)[(! 6L!Z)][3(! )(!4!5!7)[!(! 1!!3)[!(! 2!!3)[!(! 3!!3)[!(! 4!!3)]]]]}--------------------------------------------()[(! l! 22!(d)[(! l)["(! 6)[%(! 6d! )]][ ((! 6)][.(! 6F!! !S)[8(! Signals from BTSes)]][3B(! 6! d!S)[8(! Idle)][`(!&!"&)[1(! 6&! d!S!)[8(! call_conf(called_state, MID1))][j(!!")[U(! 6! d!S!)[8(!0 call_conf(called_state, MID1) to MS_PIDs(MID1))][o(!R!"R)[(! 6!Z)][3Q(! 6! d!S)[8(! Idle)]]]]]]]][3E(! 6! d!S)[8(! Idle)][c(!&!"&)[4(! 6&! d!S!)[8(! call_ind(MID1, MID2))][m(!!")[X (! 6! d!S!)[8(!' call_ind(MID1, MID2) to MS_PIDs(MID2))][r(!R!"R)[(! 6!Z)][3T(! 6!! d!S)[8(! Idle)]]]]]]]][3+(! 6 ! d!S)[8(! Idle)][I(!x!"x)[7(! 6 ! d!S!")[8(! call_reject(reason, MID1))][p(!r!"r)[[(! 6 r! d!S!)[8(!, call_reject(reason, MID1) to MS_PIDs(MID1))][#(!:!":)[(! 6:!Z)][3g(! 6 :! d!S)[8(! Idle)]]]]]]]]]]}]}(! giveReport)][(!"Rk()[(! l! 22!(d)[6(! l)[9(! 6)[<(! 6d! )]][ ?(! 6)][(! 6L!! !S)[8%(! Signals from BTSes)]][3(! 62! d!S)[8(! Idle)][(!^!"^)[(! 62! d!S!)[8(!!& giveReport(billingReport, MID1))][(!X!"X)[(! 62X! d!S!)[8(!2 giveReport(billingReport, MID1) to MS_PIDs(MID1))][(!' !" )[(! 6 !Z)][3(! 62 ! d!S)[8(! Idle)]]]]]]]][3(! 6! d!S)[8(! Idl(e)][(!LL&!"L&L)[(! 6&! d!S!)[8(! initMS(BTS_ID, MID1, IMEI))][(!LL!"LL06! d!S)[8(! Idle)]]]]]]]][3(! 6d! d!S)[8(! Idle)][(!x!"x)[(! 6d! d*!S!)[8(! logOn(MID1, BTS_ID, IMEI))][(!@r!"r@)[60(! 62r! ,d!S)[8(! MS_PIDs(MID1) := sender)][3(!+!")[(! 6d! d!S!)[8(!0 logOn(MID1, BTS_ID, IMEI) to BTS_PIDs(BTS_ID))]['(!l!"l,)[(! 6!Z)][3(! 6d! d!S)[8(! Idle)]]]]]]]]]][3(! 6! d!S)[8(! Idle)][(!LxL!"L-Lx)[(! 6! d!S!)[8(!" encryptedNr(encryptedNr, BTS_ID))][(!L@L!"LL@)[(! 6! d!.S!)[8(!7 encryptedNr(encryptedNr, BTS_ID) to BTS_PIDs(BTS_ID))][*(!LLl!"LlL)[(! 6Ll!Z)][3(! 6l! d!S)[8/(! Idle)]]]]]]]]]]}]]]]}--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------!)[6(! 6! d!S)[8(! BTS_PIDs(BTS_ID) := sender)][(!LRL!"LLR)[ (! 6! d!S)[8(! MID1)][1(!!")[8(! 6}! Marie)][(! 62! d!S!)[8(!$ initMS(BTS_ID, MID1, IMEI) via MS1)][(!2Fx!"xF)[(! 6x!Z)][3(! 62x! d!S)[8(! Idle)]]]]][(!XX!"X3)[8(! 6?! John)][(! 6! d!S!)[8(!$ initMS(BTS_ID, MID1, IMEI) via MS2)][(!XFXx!"XxXF)[(! 6Xx4!Z)][3(! 6x! d!S)[8(! Idle)]]]]][(!LL!"LL)[8(! 6e! parispizza)][(! 6! d5!S!)[8(!; initMS(BTS_ID, MID1, IMEI) via MS3 /* to MS_PIDs(MID1) */)][(!LFLx!"LxLF)[(! 6Lx!Z)][3(! 6x! d6!S)[8(! Idle)]]]]][(!@@!"@)[8(! 6Y! lyonpizza)][(! 6! d!S!)[8(!$ initMS(BTS_7ID, MID1, IMEI) via MS4)][(!@F@x!"@x@F)[(! 6@x!Z)][3(! 6x! d!S)[8(! Idle)]]]]]]]]]]]][3(! 62@! 8 d!S)[8(! Idle)][(!!")[(! 62! d!S!)[8(! randomNr(rand, MID2))][(!:9!":)[(! 62! d!S!)[8(!' randomNr(rand, MID2) to MS_PIDs(MID2))][(!f!"f)[(! 6:f!Z)][3~(! 62f! d!S)[8(! Idle)]]]]]]]]]]}--------------------------------------------------------------------------------------------------------------------------------------------------------h