package GSM

/*
   SDL MODEL OVERVIEW
   -----------------
  
   This model represents a simplified GSM network.
  
    WHAT HAS BEEN MODELED
   ---------------------
  
   - user PIN code verification,
   - mobile IMEI checking in the EIR database (prevents using a stolen mobile),
   - user authentication: the AUC sends a random number to the mobile, who encrypts it
      and sends it back to the AUC who checks the result.
   - when a mobile moves from one cell to another, the HLR and VLR databases are
      updated.
   - when a mobile is called, the routing information is given by the HLR and VLR databases.
   - during simulation, any mobile can move to any cell.
  
   Remark: 'init' signals have been used because for the moment the SDL context parameters
   are not supported in the SDL simulator. 
  
   WHAT HAS NOT BEEN MODELED
   ------------------------
  
   - low-level protocols (physical, link, network etc. layers),
   - connection to the switched or ISDN telephone network,
   - the numerous logical channels used between a mobile phone and the base stations:
      Traffic CHannel, Synchronization CHannel, Broadcast Control CHannel,
      Standalone Dedicated Control CHannel, Access Grant CHannel, Random Access
      CHannel, Pagina CHannel,
   - supplementary services,
   - power management on the mobile phone,
   - speech and data encryption,
   - SIM card creation and unlocking,
   - called ringer heared in the caller phone.
  
  */

/*
  
   GLOSSARY
   --------
  
   - AuthentCenter (AUC): AUthentication Center.
  
   - BaseStationCtlr (BSC): Base Station Controller.ter.
  
   - BaseTxStation (BTS): Base Transceiver Station.
  
   - EquipIdRegister (EIR): Equipment Identity Register.
  
   - GSM: Global System for Mobile communications.
  
   - HomeLocRegister (HLR): Home Location Register.
  
   - IMEI: International Mobile Equipment Identity.
  
   - MobileSwitchCtr (MSC): Mobile Switching Center.
  
   - PIN: Personnal Identification Number.
  
   - VisitLocRegister (VLR): Visitor Location Register.
  
  
   BIBLIOGRAPHY
   ------------
  
   Le radiotelephone cellulaire GSM, J.Tisal, Masson, Paris, 1995.
  
  */;
newtype PIN_t
  literals unknown, pin_a, pin_b, pin_c, pin_d;
endnewtype;

/* Mobile Switch ID: */
newtype MSC_ID_t
  literals Paris, Lyon;
endnewtype;

/* Base Station Controller ID: */
newtype BSC_ID_t
  literals Paris1, Lyon1;
endnewtype;

/* Base Transceiver Station ID: */
newtype BTS_ID_t
  literals Paris11, Paris12, Lyon11, Lyon12;
endnewtype;

/* Mobile users ID: */
newtype Mobile_ID_t
  literals Nobody, Marie, John, pizza, parispizza, lyonpizza;
endnewtype;

/* Mobile phone identity: */
newtype IMEI_t
  literals IMEI1, IMEI2, IMEI3, IMEI4;
endnewtype;

/* Call rejection reason: */
newtype reason_t
  literals ok, not_allowed, invalid_ph_nr, abnormal;
endnewtype;

/*	call failure reason	*/
newtype called_state_t
  literals called_ok, called_busy, called_unreachable;
endnewtype;
newtype billing_storage struct
    called Mobile_ID_t;
    duration NATURAL;
    price REAL;
endnewtype;
syntype indice = NATURAL
  default 0
  constants 0 : 15
endsyntype;
newtype billing_report_elt
  ARRAY( indice, billing_storage);
endnewtype;
newtype billing_report_t struct
    nb_com indice;
    bil billing_report_elt;
endnewtype;
signal
  initMSC(MSC_ID_t),
  initBSC(BSC_ID_t),
  initBTS(BTS_ID_t),
  initMS(BTS_ID_t, Mobile_ID_t, IMEI_t);
/* init signals to replace by context parameters when
    available in the tool: */
signal
  answer_call,
  askReport,
  authentResp(BOOLEAN),
  badPIN,
  BTSchanging(BTS_ID_t),
  BTSresp(BOOLEAN, BTS_ID_t),
  BTSreply(BOOLEAN, BTS_ID_t),
  busy,
  call_conf(called_state_t /* status */, Mobile_ID_t /* called */, 
    BTS_ID_t) /* to a mobile */,
  call_confirm(called_state_t /* status */, Mobile_ID_t /* called */, 
    BTS_ID_t) /* to a mobile */,
  call_ind(Mobile_ID_t, Mobile_ID_t /* called */, BTS_ID_t) /* to a mobile */,
  call_inquire(Mobile_ID_t, Mobile_ID_t /* called */, 
    BTS_ID_t) /* to a mobile */,
  call_reject(reason_t, Mobile_ID_t, BTS_ID_T) /* to a mobile */,
  call_req(Mobile_ID_t /* calling */, 
    Mobile_ID_t /* called *//* from a mobile */, BTS_ID_t) /* Proxy addition */,
  call_resp(called_state_t /* status */, Mobile_ID_t /* calling */, 
    Mobile_ID_t /* called *//* from a mobile */, BTS_ID_t) /* Proxy addition */,
  checkIMEI(IMEI_t),
  com_start(Mobile_ID_t, BTS_ID_t) /* Proxy addition */,
  com_finish(Mobile_ID_t, Mobile_id_t, BTS_ID_t) /* Proxy addition */,
  convers,
  dialing(Mobile_ID_t),
  disable,
  encryptedNr(NATURAL, BTS_ID_t) /* Proxy addition */,
  endUpdHLR,
  endUpdVLR,
  getBTS(Mobile_ID_t),
  fetchBTS(Mobile_ID_t),
  getPhoneNumber(Mobile_ID_t),
  getMSC(Mobile_ID_t),
  getReport(Mobile_ID_t, BTS_ID_t) /* Proxy addition */,
  giveReport(billing_report_t, Mobile_ID_t, BTS_ID_t),
  returnReport(billing_report_t, Mobile_ID_t, BTS_ID_t),
  DBgiveReport(billing_report_t, Mobile_ID_t),
  IMEI_OK(BOOLEAN),
  initGUI(Mobile_ID_t),
  initSCM(BSC_ID_t),
  initSM(MSC_ID_t),
  logOn(Mobile_ID_t, BTS_ID_t, IMEI_t),
  mobileLocation(MSC_ID_t, BTS_ID_t, reason_t, PID),
  MSCresp(BOOLEAN, MSC_ID_t),
  offKey,
  on_hook,
  onKey,
  PIN(PIN_t),
  randomNr(NATURAL, Mobile_ID_t) /* Proxy addition */,
  rejected,
  report(Mobile_ID_t /* caller */, NATURAL) /* time */,
  ring,
  searchMobile(Mobile_ID_t),
  sendShortcut(Mobile_ID_t),
  startAuthent,
  unlock,
  unreachable,
  updateHLR(Mobile_ID_t, MSC_ID_t, BOOLEAN),
  updateVLR(Mobile_ID_t, BTS_ID_t);
signallist keys =
  answer_call, askReport, BTSchanging, dialing, offKey, on_hook, onKey, PIN;
signallist MSCtoAUC = encryptedNr, startAuthent;
signallist MSCtoBilling = com_start, com_finish, getReport;
signallist MSCtoBC =
  call_conf, call_ind, call_reject, giveReport, initBSC, randomNr;
signallist MSCtoDB =
  checkIMEI, com_start, com_finish, encryptedNr, getMSC, getReport, 
  startAuthent, updateHLR;
signallist MSCtoEIR = checkIMEI;
signallist MSCtoHLR = getMSC, updateHLR;
signallist MSCtoVLR = fetchBTS, updateVLR;
/* signallist MSCtoVLR = getBTS, updateVLR; */
/* signallist MStoMS = BTSresp, call_conf, call_ind, getBTS, giveReport; */
signallist MStoMS = BTSresp, call_confirm, call_inquire, getBTS, returnReport;
signallist MtoB =
  encryptedNr, call_req, call_resp, com_start, com_finish, getReport, logOn;
signallist VLRtoMSC = BTSreply, endUpdVLR;
/* signallist VLRtoMSC = BTSresp, endUpdVLR, getBTS; */
signallist AUCtoMSC = authentResp, randomNr;
signallist BCtoBTS =
  call_conf, call_ind, call_reject, giveReport, initBTS, randomNr;
signallist BCtoMSC =
  encryptedNr, call_req, call_resp, com_start, com_finish, getReport, logOn;
signallist BtoM =
  call_conf, call_ind, call_reject, giveReport, initMS, randomNr;
signallist BTStoBC =
  encryptedNr, call_req, call_resp, com_start, com_finish, getReport, logOn, 
  randomNr;
signallist DBtoMSC =
  authentResp, initMSC, IMEI_OK, endUpdHLR, DBgiveReport, MSCresp, randomNr;
signallist DBtoMSCtrl =
  authentResp, initMSC, IMEI_OK, endUpdHLR, DBgiveReport, randomNr;
signallist displ =
  badPIN, disable, initGUI, rejected, ring, unlock, convers, busy, unreachable, 
  giveReport;
signallist EIRtoMSC = initMSC, IMEI_OK;
signallist HLRtoMSC = endUpdHLR, MSCresp;
block type DataBases referenced;
block type MobileSwitchCtr referenced;
block type BaseStationCtlr referenced;
block type BaseTxStation referenced;
block type MobileStation referenced;
block type MSBTSProxy referenced;
endpackage GSM;



block type DataBases;

/* CIF CurrentPage 1 */

/* CIF GATE (849, 150),  (849, 50) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode TextMode 6 Siglist1 */
/* CIF Keep Specific Geode TextMode 6 Siglist2 */
/* CIF Keep Specific Geode Modified */
/* CIF TextPosition (757, 86) */
/* CIF TextPosition (869, 103) SignalList1 */
/* CIF TextPosition (869, 48) SignalList2 */
gate MSC1 out with (DBtoMSC); in with (MSCtoDB);
gate MSC2 out with (DBtoMSC); in with (MSCtoDB);
signalroute MSC2HLR
  from env via MSC2 to HomeLocRegister with (MSCtoHLR);
  from HomeLocRegister to env via MSC2 with (HLRtoMSC);
signalroute MSC1HLR
  from env via MSC1 to HomeLocRegister with (MSCtoHLR);
  from HomeLocRegister to env via MSC1 with (HLRtoMSC);
signalroute MSC1AUC
  from env via MSC1 to AuthentCenter with (MSCtoAUC);
  from AuthentCenter to env via MSC1 with (AUCtoMSC);
signalroute MSC2AUC
  from AuthentCenter to env via MSC2 with (AUCtoMSC);
  from env via MSC2 to AuthentCenter with (MSCtoAUC);
signalroute MSC2EIR
  from EquipIdRegister to env via MSC2 with (EIRtoMSC);
  from env via MSC2 to EquipIdRegister with (MSCtoEIR);
signalroute MSC1EIR
  from env via MSC1 to EquipIdRegister with (MSCtoEIR);
  from EquipIdRegister to env via MSC1 with (EIRtoMSC);
signalroute MSC2Billing
  from env via MSC2 to BillingManager with (MSCtoBilling);
  from BillingManager to env via MSC2 with DBgiveReport;
signalroute MSC1Billing
  from env via MSC1 to BillingManager with (MSCtoBilling);
  from BillingManager to env via MSC1 with DBgiveReport;
signalroute BillingLine
  from BillingManager to Billing with com_start, com_finish;
  from Billing to BillingManager with report;
process HomeLocRegister (1, 1) referenced;
process AuthentCenter (1, 1) referenced;
process EquipIdRegister (1, 1) referenced;
process BillingManager (1, 1) referenced;
process Billing (0, 4) referenced;
endblock type DataBases;



process HomeLocRegister (1, 1);

/* CIF CurrentPage 1 */

/* CIF TEXT (114, 900), (1273, 496) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
newtype HR_element_t struct
    empty BOOLEAN;
    MSC_id MSC_ID_t; /* last mobile switch where the mobile was. */
    IMEI_OK BOOLEAN; /* if FALSE, mobile not allowed (stolen ...). */
endnewtype;
newtype HomeRegister_t
  ARRAY( mobile_ID_t, HR_element_t);
endnewtype;
dcl
  MSC_id MSC_ID_t,
  mobile_id mobile_ID_t,
  IMEIstatus BOOLEAN,
  HomeRegister HomeRegister_t;
/* CIF End Text */

/* CIF TEXT (89, 120), (447, 50) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Home Location Register  */
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (264, 200), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate ready;

state ready;
  input updateHLR(mobile_id, MSC_id, IMEIstatus
/* CIF TASK (655, 420), (555, 58) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task HomeRegister(mobile_id)!empty := FALSE
/* CIF TASK (620, 508), (624, 56) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task HomeRegister(mobile_id)!MSC_id := MSC_id
/* CIF TASK (620, 594), (624, 56) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task HomeRegister(mobile_id)!IMEI_OK := IMEIstatus
/* CIF OUTPUT (828, 680), (207, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output endUpdHLR to sender
/* CIF NEXTSTATE (853, 790), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input getMSC(mobile_id
/* CIF COMMENT (1801, 277), (162, 109) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */)
    comment 'Get the home
        switch of
        the mobile.'

/* CIF DECISION (1409, 403), (545, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    decision HomeRegister(mobile_id)!empty;
    (FALSE
/* CIF OUTPUT (1264, 617), (475, 101) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output MSCresp(TRUE, HomeRegister(mobile_id)!MSC_id) to sender
/* CIF ANSWER (1810, 537), (106, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    (TRUE
/* CIF OUTPUT (1775, 617), (176, 90) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output MSCresp(FALSE) to sender
/* CIF COMMENT (1971, 623), (101, 80) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */ comment 'MSC not
              found.';
    enddecision;
    nextstate -;
endstate;
endprocess HomeLocRegister;



process AuthentCenter (1, 1);

/* CIF CurrentPage 1 */

/* CIF TEXT (70, 120), (423, 50) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Authentication Center  */
/* CIF End Text */

/* CIF TEXT (70, 914), (1495, 517) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
newtype A3_encryption_t
  operators
    A3_encrypt : NATURAL, NATURAL -> NATURAL;
  operator A3_encrypt;
  fpar
    n NATURAL,
    key NATURAL;
  returns NATURAL; referenced;
endnewtype;
dcl
  rand NATURAL := 7,
  Kp NATURAL := 
    3 /* Secret key associated to a user, normally commes from the HLR. */,
  resp NATURAL,
  expected NATURAL;
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (70, 200), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate ready;

state ready;
  input startAuthent
/* CIF OUTPUT (267, 
409), (
250, 
74) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output randomNr(rand) to sender
/* CIF TASK (171, 513), (443, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task expected := A3_encrypt(rand, Kp
/* CIF NEXTSTATE (280, 623), (224, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate waitMobileResp;
endstate;

state waitMobileResp;
  input encryptedNr(resp
/* CIF COMMENT (1069, 273), (245, 165) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */)
    comment 
  'resp was computed
        by the mobile, using
        Kp and A3_encrypt
        also present in the
        SIM smart card.'

/* CIF DECISION (818, 422), (246, 100) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    decision resp = expected;
    (FALSE
/* CIF OUTPUT (953, 634), (234, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output authentResp(FALSE) to sender;
    (TRUE
/* CIF OUTPUT (720, 632), (213, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output authentResp(TRUE) to sender
/* CIF ANSWER (1003, 552), (132, 52) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    enddecision;
    nextstate ready;
endstate;
endprocess AuthentCenter;



operator A3_encrypt;
fpar
  n NATURAL,
  key NATURAL;
returns NATURAL;

start;
    return (n * key) + 7;
endoperator A3_encrypt;



process EquipIdRegister (1, 1);

/* CIF CurrentPage 1 */

/* CIF TEXT (70, 1007), (551, 199) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
dcl
  IMEI IMEI_t;
/* CIF End Text */

/* CIF TEXT (70, 120), (480, 50) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Equipment Identity  Register  */
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (99, 200), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    output initMSC(Paris) via MSC1EIR
/* CIF OUTPUT (72, 420), (213, 80) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
    output initMSC(Lyon) via MSC2EIR
/* CIF NEXTSTATE (99, 530), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate ready;

state ready;
  input checkIMEI(IMEI
/* CIF OUTPUT (565, 420), (176, 97) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */);
    output IMEI_OK(TRUE) to sender
/* CIF NEXTSTATE (573, 547), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;
endprocess EquipIdRegister;



process BillingManager (1, 1);
newtype billing_register_t
  ARRAY( Mobile_ID_t, billing_report_t);
endnewtype;
newtype billing_PID_t
  ARRAY( Mobile_ID_t, PID);
endnewtype;
dcl
  billing_PIDs billing_PID_t,
  mobile_id,
  correspondant,
  tmp mobile_ID_t,
  bil_register billing_register_t,
  time NATURAL;
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (202, 120), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    task bil_register(Marie)!nb_com := 0;
    task bil_register(John)!nb_com := 0;
    task bil_register(parispizza)!nb_com := 0;
    task bil_register(lyonpizza)!nb_com := 0;
    nextstate ready;

state ready;
  input com_finish(mobile_id, correspondant);
    decision billing_PIDs(mobile_id) = NULL;
    (TRUE) :
      decision billing_PIDs(correspondant) = NULL;
      (FALSE) :
        task tmp := mobile_id;
        task Mobile_id := correspondant;
        task correspondant := tmp;
        output com_finish to billing_PIDs(mobile_id);
        nextstate waitReport;
      (TRUE) :
        nextstate ready;
      enddecision;
    (FALSE) :
      output com_finish to billing_PIDs(mobile_id);
      nextstate waitReport;
    enddecision;
endstate;

state waitReport;
  save *;
  input report(mobile_id, time);
    task bil_register(mobile_id)!bil(bil_register(mobile_id)!nb_com)!called := 
        correspondant;
    task bil_register(mobile_id)!bil(bil_register(mobile_id)!nb_com)!duration := 
        time;
    task bil_register(mobile_id)!bil(bil_register(mobile_id)!nb_com)!price := 
        Float(time) * 0.017;
    task bil_register(mobile_id)!nb_com := bil_register(mobile_id)!nb_com + 1;
    task billing_PIDs(mobile_id) := NULL;
    nextstate ready;
endstate;

state ready;
  input com_start(mobile_id);
    create Billing;
    task billing_PIDs(mobile_id) := offspring;
    output com_start(mobile_id) to Billing_PIDs(mobile_id);
    nextstate -;
endstate;

state ready;
  input getReport(mobile_id);
    output DBgiveReport(bil_register(mobile_id), mobile_id) to sender;
    nextstate ready;
endstate;
endprocess BillingManager;



process Billing (0, 4);

/* CIF CurrentPage 1 */

/* CIF TEXT (75, 921), (427, 207) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
dcl
  mobile_id Mobile_ID_t,
  i INTEGER;
timer
  count;
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (72, 120), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    task i := 0
/* CIF NEXTSTATE (70, 420), (205, 88) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate wait_start;

state wait_start;
  input com_start(mobile_id
/* CIF SET (441, 365), (278, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    set(now + 1, count
/* CIF NEXTSTATE (470, 498), (222, 94) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate waitTimer;
endstate;

state waitTimer;
  input count
/* CIF TASK (1265, 
388), (
200, 
120) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task i := i + 1
/* CIF SET (1226, 538), (278, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    set(now + 1, count
/* CIF NEXTSTATE (1265, 671), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate waitTimer;
endstate;

state waitTimer;
  input com_finish
/* CIF OUTPUT (888, 
388), (
341, 
88) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output report(mobile_id, i
/* CIF RESET (959, 506), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    reset(count
/* CIF STOP (959, 656), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    stop;
endstate;
endprocess Billing;



block type MobileSwitchCtr;
gate MSx out with (MStoMS); in with (MStoMS);
gate DBx out with (MSCtoDB); in with (DBtoMSC);
gate BCx out with (MSCtoBC); in with (BCtoMSC);
signalroute BC
  from MSCtrl to env via BCx with (MSCtoBC);
  from env via BCx to MSCtrl with (BCtoMSC);
signalroute SVLR
  from MSCtrl to VisitLocRegister with (MSCtoVLR);
  from VisitLocRegister to MSCtrl with (VLRtoMSC);
signalroute MS
  from env via MSx to MSCtrl with (MStoMS);
  from MSCtrl to env via MSx with (MStoMS);
signalroute DB
  from env via DBx to MSCtrl with (DBtoMSCtrl);
  from MSCtrl to env via DBx with (MSCtoDB);
signalroute SMMSC
  from search_Mobile to MSCtrl with MobileLocation;
  from MSCtrl to search_Mobile with initSM, searchMobile;
signalroute SMVLR
  from search_Mobile to VisitLocRegister with fetchBTS;
  from VisitLocRegister to search_Mobile with BTSreply;
signalroute SMDB
  from search_Mobile to env via DBx with getMSC;
  from env via DBx to search_Mobile with MSCresp;
signalroute SMMS
  from env via MSx to search_Mobile with BTSresp;
  from search_Mobile to env via MSx with getBTS;
process MSCtrl (1, 1) referenced;
process VisitLocRegister (1, 1) referenced;
process search_Mobile (1, 1) referenced;
endblock type MobileSwitchCtr;



process MSCtrl (1, 1);
dcl
  called_status called_state_t,
  me MSC_ID_t,
  bil_report billing_report_t,
  mobile_id,
  caller,
  called,
  c mobile_ID_t,
  BTS_id,
  calledBTS BTS_ID_t,
  IMEI IMEI_t,
  IMEIstatus BOOLEAN,
  rand NATURAL,
  resp NATURAL,
  authentOK BOOLEAN,
  calledMSC MSC_ID_t,
  BTSfound BOOLEAN,
  reason reason_t,
  prpid PID,
  MSC_PId PID;

start;
    nextstate waitInit;

state ready;
  input logOn(mobile_id, BTS_id, IMEI);
    output checkIMEI(IMEI);
    nextstate waitCheck;
endstate;

state waitUpdHLR;
  save *;
  input endUpdHLR;
    decision IMEIstatus;
    (TRUE) :
      output updateVLR(mobile_id, BTS_id);
      nextstate waitUpdVLR;
    (FALSE) :
      nextstate ready;
    enddecision;
endstate;

state ready;
  input call_resp(called_status, caller, called);
    output searchMobile(called);
    nextstate waitsm1;
endstate;

state waitEncryptedNr;
  save *;
  input encryptedNr(resp);
    output encryptedNr(resp) via DB;
    nextstate waitAuthent;
endstate;

state ready;
  input getBTS(c
/*  comment 
'Another switch
        looks for the
        BTS containing
        the mobile c.' */);
    task prpid := sender;
    output fetchBTS(c);
    nextstate waitBTSotherMSC;
endstate;

state ready;
  input call_confirm(called_status, called, calledBTS
/*  comment 'From
        other
        switch.' */);
    output call_conf(called_status, called, calledBTS) via BC;
    nextstate -;
endstate;

state ready;
  input DBgiveReport(bil_report, caller);
    output searchMobile(caller);
    nextstate waitsm3;
endstate;

state waitInit;
  input initMSC(me);
    output initSM(me) via SMMSC;
    decision me;
    (Lyon) :
      output initBSC(Lyon1);
    (Paris) :
      output initBSC(Paris1);
    enddecision;
    nextstate ready;
endstate;

state waitCheck;
  save *;
  input IMEI_OK(IMEIstatus);
    output updateHLR(mobile_id, me, IMEIstatus);
    nextstate waitUpdHLR;
endstate;

state waitUpdVLR;
  save *;
  input endUpdVLR;
    nextstate ready;
endstate;

state waitRandom;
  save *;
  input randomNr(rand);
    output randomNr(rand) via BC
/* comment 'To the
          mobile.' */;
    nextstate waitEncryptedNr;
endstate;

state waitsm1;
  save *;
endstate;

state waitAuthent;
  save *;
  input authentResp(authentOK);
    decision authentOK;
    (TRUE) :
      output searchMobile(called);
      nextstate waitsm2;
    (FALSE) :
      output call_reject(not_allowed) via BC;
      nextstate ready;
    enddecision;
endstate;

state waitBTSotherMSC;
  save *;
  input BTSreply(BTSfound, calledBTS
/* comment 'Response
        from my
        VLR.' */);
    output BTSresp(BTSfound, calledBTS) to prpid
/* comment 'Transmit
          response to
          the other
          switch.' */;
    nextstate ready;
endstate;

state waitsm3;
  save *;
endstate;

state waitsm2;
  save *;
endstate;

state ready;
  input call_req(caller, called);
    task 'Here begins
          the authentication
          of the mobile';
    output startAuthent;
    nextstate waitRandom;
endstate;

state ready;
  input com_finish(caller, called);
    output com_finish(caller, called) via DB;
    nextstate -;
endstate;

state ready;
  input getReport(caller);
    output getReport(caller) via DB;
    nextstate ready;
endstate;

state waitsm1;
  input mobileLocation(calledMSC, calledBTS, reason, MSC_PId);
    decision reason;
    (ok) :
      decision calledMSC = me;
      (FALSE) :
        output call_confirm(called_status, called, calledBTS) to MSC_PId
/* via MS */;
      (TRUE) :
        output call_conf(called_status, called, calledBTS) via BC;
      enddecision;
      nextstate ready;
    else :
      output call_reject(reason) via BC;
      nextstate ready;
    enddecision;
endstate;

state waitsm3;
  input mobileLocation(calledMSC, calledBTS, reason, MSC_PId);
    decision reason;
    (ok) :
      decision calledMSC = me;
      (FALSE) :
        output returnReport(bil_report, caller, calledBTS) to MSC_PId
/* via MS */;
      (TRUE) :
        output giveReport(bil_report, caller, calledBTS) via BC;
      enddecision;
      nextstate ready;
    else :
      output call_reject(reason) via BC;
      nextstate ready;
    enddecision;
endstate;

state waitsm2;
  input mobileLocation(calledMSC, calledBTS, reason, MSC_PId);
    decision reason;
    (ok) :
      decision calledMSC = me;
      (FALSE) :
        output call_inquire(caller, called, calledBTS) to MSC_PId
/* via MS */;
      (TRUE) :
        output call_ind(caller, called, calledBTS) via BC;
      enddecision;
      nextstate ready;
    else :
      output call_reject(reason) via BC;
      nextstate ready;
    enddecision;
endstate;

state ready;
  input call_inquire(caller, called, calledBTS
/* comment 'From
        other
        switch.' */);
    output call_ind(caller, called, calledBTS
/* via BC */
/* comment 'To my
          BSC.' */);
    nextstate -;
endstate;

state ready;
  input returnReport(bil_report, called, calledBTS);
    output giveReport(bil_report, called, calledBTS) via BC;
    nextstate -;
endstate;

state ready;
  input com_start(caller);
    output com_start(caller) via DB;
    nextstate -;
endstate;
endprocess MSCtrl;



process VisitLocRegister (1, 1);
newtype VR_element_t struct
    empty BOOLEAN;
    BTS_id BTS_ID_t; /* last BTS (cell) where the mobile was. */
endnewtype;
newtype VisitorRegister_t
  ARRAY( mobile_ID_t, VR_element_t);
  default (. (. TRUE, Paris11 .) .); /* no effect if put in the STRUCT. */
endnewtype;
dcl
  mobile_id mobile_ID_t,
  BTS_id BTS_ID_t,
  VisitRegister VisitorRegister_t;

start;
    nextstate ready;

state ready;
  input updateVLR(mobile_id, BTS_id);
    task VisitRegister(mobile_id)!empty := FALSE;
    task VisitRegister(mobile_id)!BTS_id := BTS_id;
    output endUpdVLR;
    nextstate -;
endstate;

state ready;
  input fetchBTS(mobile_id
/* comment 'Get the cell
         containing
        the mobile.' */);
    decision VisitRegister(mobile_id)!empty;
    (FALSE) :
      output BTSreply(TRUE, VisitRegister(mobile_id)!BTS_id) to sender;
    (TRUE) :
      output BTSreply(FALSE) to sender
/* comment 'BTS not
               found.' */;
    enddecision;
    nextstate -;
endstate;
endprocess VisitLocRegister;



process search_Mobile (1, 1);
dcl
  myMSC MSC_ID_t,
  mobile_id Mobile_ID_t,
  called_MSC MSC_ID_t,
  called_BTS BTS_ID_t,
  MSCfd,
  BTSfd BOOLEAN;

start;
    nextstate waitInit;

state ready;
  input searchMobile(mobile_id);
    output getMSC(mobile_id) via SMDB;
    nextstate waitMSC;
endstate;

state waitMSC;
  input MSCresp(MSCfd, called_MSC);
    decision MSCfd;
    (FALSE) :
      join waitMSC_3;
    (TRUE) :
      decision called_MSC = myMSC;
      (FALSE) :
        output getBTS(mobile_id) via SMMS
/* comment 'Ask to the
                  VLR in the
                  other switch.' */;
      (TRUE) :
        output fetchBTS(mobile_id) via SMVLR;
      enddecision;
      nextstate waitBTS;
    enddecision;
endstate;

connection
  waitMSC_3 :
  output mobileLocation(called_MSC, called_BTS, invalid_ph_nr) via SMMSC;
  nextstate ready;
endconnection waitMSC_3;

state waitBTS;
  input BTSresp(BTSfd, called_BTS), BTSreply(BTSfd, called_BTS
/* comment 'From my
        VLR or from
        other switch.' */);
    decision BTSfd;
    (FALSE) :
      output mobileLocation(called_MSC, called_BTS, abnormal, sender) via SMMSC;
      nextstate ready;
    (TRUE) :
      output mobileLocation(called_MSC, called_BTS, ok, sender) via SMMSC;
      nextstate ready;
    enddecision;
endstate;

state waitInit;
  input initSM(myMSC);
    nextstate ready;
endstate;
endprocess search_Mobile;



block type BaseStationCtlr;

/* CIF CurrentPage 1 */

/* CIF GATE (1167, 116),  (1167, 16) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode TextMode 6 Siglist1 */
/* CIF Keep Specific Geode TextMode 6 Siglist2 */
/* CIF Keep Specific Geode Modified */
/* CIF TextPosition (1089, 66) */
/* CIF TextPosition (1185, 76) SignalList1 */
/* CIF TextPosition (1187, 24) SignalList2 */
gate BTS1x out with (BCtoBTS); in with (BTStoBC);
gate MSx out with (BCtoMSC); in with (MSCtoBC);
gate BTS2x out with (BCtoBTS); in with (BTStoBC);
signalroute BTS2
  from env via BTS2x to BSC with (BTStoBC);
  from BSC to env via BTS2x with (BCtoBTS);
signalroute BTS1
  from env via BTS1x to BSC with (BTStoBC);
  from BSC to env via BTS1x with (BCtoBTS);
signalroute MS
  from env via MSx to BSC with (MSCtoBC);
  from BSC to env via MSx with (BCtoMSC);
signalroute BSCSCM
  from BSC to ShortcutsManager with sendShortCut, initSCM;
  from ShortcutsManager to BSC with getPhoneNumber;
process BSC referenced;
process ShortcutsManager referenced;
endblock type BaseStationCtlr;



process BSC;
newtype BTS_PIDs_t
  ARRAY( BTS_ID_t, PID);
endnewtype;
dcl
  BSC_id BSC_ID_t,
  BTS_id BTS_ID_t,
  IMEI IMEI_t,
  mobile_id,
  caller,
  called mobile_ID_t,
  rand NATURAL,
  resp NATURAL,
  BTS_PID PID,
  BTS_PIDs BTS_PIDs_t,
  calledBTS BTS_ID_t,
  called_status called_state_t,
  reason reason_t,
  bil_report billing_report_t;
/* CIF End Text */

/* CIF TEXT (505, 120), (447, 50) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Base Station Controller */
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (242, 120), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate waitInit;

state ready;
  input logOn(mobile_id, BTS_id, IMEI
/* CIF TASK (585, 409), (314, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task BTS_PIDs(BTS_id) := sender
/* CIF OUTPUT (590, 519), (303, 76) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
    output logOn(mobile_id, BTS_id, IMEI) via MS
/* CIF NEXTSTATE (663, 625), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_req(caller, called
/* CIF TASK (1086, 329), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task BTS_PID := sender
/* CIF COMMENT (1260, 329), (178, 80) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */ comment 
    'To respond to
          the sender BTS.'
/* CIF OUTPUT (983, 439), (363, 97) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output sendShortcut(called) via BSCSCM
/* CIF NEXTSTATE (1021, 567), (288, 79) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitPhoneNumber;
endstate;

state waitRandom;
  save *;
  input randomNr(rand
/* CIF OUTPUT (2154, 336), (239, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output randomNr(rand) to BTS_PID
/* CIF NEXTSTATE (2159, 446), (229, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitEncryptedNr;
endstate;

state ready;
  input call_conf(called_status, called, calledBTS
/* CIF OUTPUT (1593, 1440), (468, 97) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_conf(called_status, called) to BTS_PIDs(calledBTS
/* CIF NEXTSTATE (1747, 1567), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state ready;
  input giveReport(bil_report, called, calledBTS
/* CIF OUTPUT (3097, 887), (448, 97) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output giveReport(bil_report, called) to BTS_PIDs(calledBTS
/* CIF NEXTSTATE (3250, 1015), (143, 72) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state waitPhoneNumber;
  save *;
  input getPhoneNumber(called
/* CIF OUTPUT (1547, 380), (298, 76) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_req(caller, called) via MS
/* CIF NEXTSTATE (1608, 486), (176, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitRandom;
endstate;

state waitInit;
  input initBSC(BSC_id

/* CIF DECISION (212, 450), (220, 66) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    decision BSC_id;
    (Lyon1
/* CIF OUTPUT (324, 626), (234, 72) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */) :
      output initBTS(Lyon11) via BTS1
/* CIF OUTPUT (324, 728), (234, 72) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
      output initBTS(Lyon12) via BTS2;
    (Paris1
/* CIF OUTPUT (70, 626), (234, 72) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */) :
      output initBTS(Paris11) via BTS1
/* CIF OUTPUT (70, 728), (234, 72) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
      output initBTS(Paris12) via BTS2
/* CIF ANSWER (391, 546), (101, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    enddecision;
    output initSCM(BSC_id) via BSCSCM
/* CIF NEXTSTATE (242, 966), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate ready;
endstate;

state waitEncryptedNr;
  save *;
  input encryptedNr(resp
/* CIF OUTPUT (2039, 675), (291, 63) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output encryptedNr(resp) via MS
/* CIF NEXTSTATE (2090, 768), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate ready;
endstate;

state ready;
  input com_start(caller
/* CIF OUTPUT (2619, 1438), (324, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output com_start(caller) via MS
/* CIF NEXTSTATE (2703, 1551), (154, 74) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input getReport(caller
/* CIF OUTPUT (2658, 882), (318, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output getReport(caller) via MS
/* CIF NEXTSTATE (2737, 995), (160, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_reject(reason
/* CIF OUTPUT (3307, 1442), (284, 85) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_reject(reason) to BTS_PID
/* CIF NEXTSTATE (3353, 1557), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_resp(called_status, caller, called
/* CIF OUTPUT (2084, 1448), (515, 73) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_status, caller, called) via MS
/* CIF NEXTSTATE (2261, 1551), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_ind(caller, called, calledBTS
/* CIF OUTPUT (1184, 1440), (389, 87) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_ind(caller, called) to BTS_PIDs(calledBTS
/* CIF NEXTSTATE (1299, 1557), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state ready;
  input com_finish(caller, called
/* CIF OUTPUT (2963, 1438), (324, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output com_finish(caller, called) via MS
/* CIF NEXTSTATE (3047, 1551), (154, 74) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;
endprocess BSC;



process ShortcutsManager;
newtype shortcuts_t
  ARRAY( indice, Mobile_ID_t);
endnewtype;
newtype shortcut_corres_t
  ARRAY( Mobile_ID_t, Mobile_ID_t);
endnewtype;
dcl
  me BSC_ID_t,
  mobile_id Mobile_ID_t,
  shortcuts shortcuts_t,
  nb_shortcuts,
  i integer,
  shortcut_corres shortcut_corres_t;
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (120, 120), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate waitInit;

state ready;
  input sendShortcut(mobile_id
/* CIF TASK (1339, 400), (194, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task i := 1
/* CIF NEXTSTATE (1335, 513), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate findShortcut;
endstate;

state findShortcut;
  provided TRUE

/* CIF DECISION (2427, 403), (434, 147) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    decision mobile_id = shortcuts(i);
    (FALSE

/* CIF DECISION (2755, 670), (293, 144) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      decision i = nb_shortcuts;
      (FALSE
/* CIF TASK (2993, 934), (154, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
        task i := i + 1
/* CIF NEXTSTATE (2971, 1042), (200, 100) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
        nextstate findShortcut;
      (TRUE
/* CIF OUTPUT (2514, 934), (436, 94) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
        output getPhoneNumber(mobile_id
/* CIF NEXTSTATE (2632, 1059), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
        nextstate ready;
      enddecision;
    (TRUE
/* CIF OUTPUT (1733, 670), (696, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output getPhoneNumber(shortcut_corres(mobile_id
/* CIF NEXTSTATE (1982, 803), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */));
      nextstate ready;
    enddecision;
endstate;

state waitInit;
  input initSCM(me
/* CIF TASK (463, 394), (262, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task nb_shortcuts := 1
/* CIF TASK (443, 502), (301, 74) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task shortcuts(1) := pizza

/* CIF DECISION (521, 607), (146, 116) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    decision me;
    (paris1
/* CIF TASK (594, 848), (555, 100) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      task shortcut_corres(pizza) := parispizza;
    (lyon1
/* CIF TASK (70, 846), (493, 100) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      task shortcut_corres(pizza) := lyonpizza
/* CIF ANSWER (797, 758), (150, 60) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    enddecision;
    nextstate ready;
endstate;
endprocess ShortcutsManager;



block type BaseTxStation;

/* CIF CurrentPage 1 */

/* CIF GATE (185, 489),  (85, 489) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode TextMode 2 Siglist1 */
/* CIF Keep Specific Geode TextMode 2 Siglist2 */
/* CIF Keep Specific Geode Modified */
/* CIF TextPosition (115, 448) */
/* CIF TextPosition (91, 412) SignalList1 */
/* CIF TextPosition (20, 512) SignalList2 */
gate BCx out with (BTStoBC); in with (BCtoBTS);
gate MSx out with (BtoM); in with (MtoB);
signalroute MS
  from BTS to env via MSx with (BtoM);
  from env via MSx to BTS with (MtoB);
signalroute BC
  from env via BCx to BTS with (BCtoBTS);
  from BTS to env via BCx with (BTStoBC);
process BTS referenced;
endblock type BaseTxStation;



process BTS;
newtype MS_PIDs_t
  ARRAY( Mobile_ID_t, PID);
endnewtype;
dcl
  BTS_id BTS_ID_t /* replaces context parameters. */,
  mobile_id Mobile_ID_t,
  x BTS_ID_t /* not used */,
  IMEI IMEI_t,
  caller,
  called Mobile_ID_t
/* MS_PID PID, */,
  MS1 Mobile_ID_t,
  BTS1 BTS_ID_t
/* MS_PIDs MS_PIDs_t, */,
  reason reason_t,
  called_status called_state_t,
  resp,
  rand natural,
  bil_report billing_report_t;
/* CIF End Text */

/* CIF TEXT (70, 120), (447, 50) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Base Transceiver Station */
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (103, 200), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate waitInit;

state ready;
  input logOn(mobile_id, x, IMEI
/* CIF COMMENT (832, 195), (207, 136) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */)
    comment 
  'Note that the
        second parameter
        is not stored in
        BTS_id.'
/* CIF TASK (523, 329), (314, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task ''
/* MS_PIDs(mobile_id) :=
sender */
/* CIF OUTPUT (531, 439), (298, 79) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
    output logOn(mobile_id, BTS_id, IMEI) via BC
/* CIF NEXTSTATE (601, 548), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_req(caller, called, BTS1
/* CIF TASK (1137, 329), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task MS1 := caller
/* CIF COMMENT (1319, 318), (160, 135) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */

/* MS_PID := sender */ comment 
    'To respond
          to this mobile
          during
          authentication.'
/* CIF OUTPUT (1051, 484), (330, 76) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output call_req(caller, called, ) via BC
/* CIF NEXTSTATE (1128, 590), (176, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitRandom
/* CIF COMMENT (1319, 579), (218, 106) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
endstate;

state waitRandom;
  input randomNr(rand
/* CIF OUTPUT (1866, 337), (250, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output randomNr(rand, MS1) via MS /* to MS_PID */
/* CIF NEXTSTATE (1876, 447), (229, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitEncryptedNr;
endstate;

state ready;
  input call_conf(called_status, called
/* CIF OUTPUT (1575, 1150), (466, 87) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_conf(called_status, called) via MS /* to MS_PIDs(called) */
/* CIF NEXTSTATE (1729, 1268), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input giveReport(bil_report, called
/* CIF OUTPUT (3054, 354), (380, 97) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output giveReport(bil_report, called) via MS /* to MS_PIDs(called) */
/* CIF NEXTSTATE (3166, 481), (154, 72) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state waitInit;
  input initBTS(BTS_id
/* CIF OUTPUT (75, 530), (215, 95) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */);
    output initMS(BTS_id, Marie, IMEI1
/* via MS1 */
/* CIF OUTPUT (70, 730), (227, 97) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */);
    output initMS(BTS_id, John, IMEI2
/* via MS2 */
/* CIF OUTPUT (70, 857), (227, 97) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */);
    output initMS(BTS_id, parispizza, IMEI3
/* via MS3 */
/* CIF OUTPUT (70, 984), (227, 97) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */);
    output initMS(BTS_id, lyonpizza, IMEI4
/* via MS4 */
/* CIF NEXTSTATE (103, 1111), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate ready;
endstate;

state waitEncryptedNr;
  save *;
  input encryptedNr(resp, BTS1
/* CIF OUTPUT (1692, 672), (314, 66) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output encryptedNr(resp) via BC
/* CIF NEXTSTATE (1753, 769), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate ready;
endstate;

state ready;
  input com_start(caller, BTS1
/* CIF OUTPUT (2621, 1152), (324, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output com_start(caller) via BC
/* CIF NEXTSTATE (2706, 1265), (154, 74) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input getReport(caller, BTS1
/* CIF OUTPUT (2651, 349), (312, 91) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output getReport(caller) via BC
/* CIF NEXTSTATE (2735, 471), (143, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_reject(reason
/* CIF OUTPUT (3329, 1143), (284, 82) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_reject(reason, MS1) via MS /* to MS_PID */
/* CIF NEXTSTATE (3375, 1256), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_resp(called_status, caller, called, BTS1
/* CIF OUTPUT (2061, 1151), (521, 78) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_status, caller, called) via BC
/* CIF NEXTSTATE (2241, 1259), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input call_ind(caller, called
/* CIF OUTPUT (1252, 1150), (303, 87) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_ind(caller, called) via MS /* to MS_PIDs(called) */
/* CIF NEXTSTATE (1323, 1267), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state ready;
  input com_finish(caller, called, BTS1
/* CIF OUTPUT (2985, 1149), (324, 83) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output com_finish(caller, called) via BC
/* CIF NEXTSTATE (3070, 1262), (154, 74) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;
endprocess BTS;



block type MobileStation;

/* CIF CurrentPage 1 */

/* CIF GATE (206, 266),  (106, 266) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode TextMode 2 Siglist1 */
/* CIF Keep Specific Geode TextMode 2 Siglist2 */
/* CIF Keep Specific Geode Modified */
/* CIF TextPosition (213, 222) */
/* CIF TextPosition (100, 212) SignalList1 */
/* CIF TextPosition (53, 291) SignalList2 */
gate BTSx out with (MtoB); in with (BtoM);
gate KBDx out with (displ); in with (keys);
signal
  initSIM(PIN_t),
  checkPIN(PIN_t),
  PIN_OK(BOOLEAN);
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF SIGNALROUTE (206, 266) , (426, 266) , (426, 436) , (679, 436) */
/* CIF TextPosition (444, 440) */
/* CIF TextPosition (550, 451) SignalList1 */
/* CIF TextPosition (226, 286) SignalList2 */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode TextMode 2 Siglist1 */
/* CIF Keep Specific Geode TextMode 0 Siglist2 */
/* CIF Keep Specific Geode Modified */
signalroute KBD
  from env via KBDx to MobileSt with (keys);
  from MobileSt to env via KBDx with (displ);
signalroute BTS
  from env via BTSx to MobileSt with (BtoM);
  from MobileSt to env via BTSx with (MtoB);
signalroute ctrlSim
  from MobileSt to SIM with initSIM, checkPIN, randomNr;
  from SIM to MobileSt with PIN_OK, encryptedNr;
process MobileSt (1, 1) referenced;
process SIM (1, 1) referenced;
endblock type MobileStation;



process MobileSt (1, 1);

/* CIF CurrentPage 1 */

/* CIF TEXT (886, 1316), (984, 440) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* To store the SDL PID of the Base Tx Stations. Necessary
         to send a signal to a given BTS. */
newtype BTS_PIDs_t
  ARRAY( BTS_ID_t, PID);
endnewtype;
dcl
  me Mobile_ID_t /* replaces context parameters.*/,
  IMEI IMEI_t /* replaces context parameters.*/,
  p PIN_T,
  status BOOLEAN,
  BTSreceived,
  BTS_ID BTS_ID_t
/* BTS_PIDs BTS_PIDs_t, */,
  false_pin natural,
  enabled BOOLEAN;
/* CIF End Text */

/* CIF TEXT (70, 120), (303, 50) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Mobile Station */
/* CIF End Text */

/* CIF CurrentPage 2 */

/* CIF TEXT (98, 1063), (1449, 319) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
dcl
  caller,
  called,
  correspondant Mobile_ID_t,
  rand NATURAL,
  resp NATURAL,
  called_status called_state_t,
  reason reason_t,
  bil_report billing_report_t;
/* CIF End Text */

/* CIF TEXT (1681, 1018), (854, 370) */
/* CIF Keep Specific Geode Font 
      'fixed'
      'fixed'
      'fixed'*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Nominal scenario:
      
                     Mobile  Mobile
                       A       B
                       |       |
        call_req   --->|       |
        (dialing)      |       |---> call_ind (ring)
                       |       |
                       |       |<--- call_resp (off hook)
        call_conf  <---|       |
                       |       |
      
      */
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (527, 270), (170, 50) */
/* CIF Keep Specific Geode Color  #000000 */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate waitInit1;

state powerOff
/* CIF COMMENT (2400, 185), (200, 120) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
  input call_ind(caller, called
/* CIF OUTPUT (2353, 454), (665, 81) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_unreachable, me, caller, BTSReceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (2591, 565), (188, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state waitCheckPIN;
  input PIN_OK(status

/* CIF DECISION (3234, 471), (220, 69) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    decision status;
    (TRUE
/* CIF OUTPUT (3507, 658), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output unlock
/* CIF NEXTSTATE (3519, 
808), (
176, 
80) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      nextstate listening;
    (FALSE
/* CIF OUTPUT (3089, 651), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output badPIN
/* CIF TASK (3019, 
801), (
341, 
111) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      task false_pin := false_pin + 1

/* CIF DECISION (3080, 942), (220, 150) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      decision false_pin < 3;
      (false
/* CIF OUTPUT (3190, 1212), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
        output disable
/* CIF TASK (3165, 
1362), (
250, 
77) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
        task enabled := false
/* CIF NEXTSTATE (3173, 1469), (233, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
        nextstate disabled;
      (true
/* CIF NEXTSTATE (3010, 1212), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
        nextstate askPIN;
      enddecision;
    enddecision;
endstate;

state askPIN, conversation, listening, powerOff, ringing, waitCallConf, 
  waitCheckPIN;
  priority input BTSchanging(BTSreceived
/* CIF TASK (3825, 394), (282, 138) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task 
    'Now, this mobile
          receives from
          BTSreceived, until the
          next change of cell'
/* CIF TASK (3825, 562), (282, 103) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task 
    'Display level of the
           radio signal received
          from the BTS'
/* CIF OUTPUT (3793, 695), (345, 152) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output logOn(me, BTSreceived, IMEI
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF COMMENT (4147, 674), (213, 199) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */) comment 
    'Tells where I am to
          ''BTSreceived''.
          Missing in the
          Tisal GSM book,
          but my phone 
          does it.'
/* CIF NEXTSTATE (3866, 903), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state waitInit4;
  input initMS(BTS_ID
/* CIF TASK (1077, 370), (373, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task ''
/* BTS_PIDs(BTS_ID) := sender */
/* CIF OUTPUT (1141, 450), (245, 91) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output initGUI(me
/* CIF OUTPUT (1091, 571), (345, 152) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output logOn(me, Paris11, IMEI
/* to 
BTS_PIDs(
Paris11) */
/* CIF TASK (1127, 753), (273, 91) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task enabled := true
/* CIF NEXTSTATE (1181, 874), (166, 65) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate powerOff;
endstate;

state disabled;
  input call_ind(caller
/* CIF OUTPUT (3924, 1381), (614, 92) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_unreachable, me, caller, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (4137, 1503), (188, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state waitInit1;
  input initMS(BTS_ID, me, IMEI
/* CIF TASK (427, 528), (373, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task ''
/* BTS_PIDs(BTS_ID) := sender */

/* CIF DECISION (527, 608), (171, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    decision me;
    (parispizza
/* CIF TASK (580, 768), (143, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      join waitInit1_2;
    (lyonpizza
/* CIF TASK (763, 768), (143, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      join waitInit1_3;
    (John
/* CIF TASK (417, 768), (143, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      join waitInit1_1;
    (Marie
/* CIF TASK (254, 768), (143, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      task p := pin_a
/* CIF ANSWER (432, 688), (113, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    enddecision;
    waitInit1_4 :
    output initSIM(p
/* CIF NEXTSTATE (530, 943), (166, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate waitInit2;
endstate;

state askPIN;
  input offKey
/* CIF NEXTSTATE (2012, 
1083), (
154, 
80) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate powerOff;
endstate;

state waitInit2;
  input initMS(BTS_ID
/* CIF TASK (427, 1103), (373, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task ''
/* BTS_PIDs(BTS_ID) := sender */
/* CIF NEXTSTATE (530, 1183), (166, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitInit3;
endstate;

state waitInit3;
  input initMS(BTS_ID
/* CIF TASK (427, 1343), (373, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    task ''
/* BTS_PIDs(BTS_ID) := sender */
/* CIF NEXTSTATE (530, 1423), (166, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitInit4;
endstate;

state listening;
  input call_ind(caller
/* CIF OUTPUT (844, 342), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output ring
/* CIF TASK (739, 
452), (
369, 
97) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    task correspondant := caller
/* CIF NEXTSTATE (844, 579), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate ringing;
endstate;

state waitRandom;
  save *;
  input randomNr(rand
/* CIF OUTPUT (2283, 372), (272, 82) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output randomNr(rand) via ctrlSIM
/* CIF NEXTSTATE (2323, 485), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitSIMresult;
endstate;

state waitSIMresult;
  save *;
  input encryptedNr(resp
/* CIF OUTPUT (3051, 337), (352, 85) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output encryptedNr(resp, BTSreceived) via BTS /* to BTS_PIDs(BTSreceived) */
/* CIF NEXTSTATE (3131, 452), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate waitCallConf;
endstate;

state ringing;
  input call_ind(caller
/* CIF OUTPUT (4181, 342), (547, 81) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_busy, me, caller, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (4360, 453), (188, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state waitCallConf;
  input call_ind(caller
/* CIF OUTPUT (5332, 381), (547, 81) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_busy, me, caller, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (5511, 492), (188, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state conversation;
  input call_ind(caller
/* CIF OUTPUT (6677, 403), (547, 81) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_busy, me, caller, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (6856, 514), (188, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state powerOff
/* CIF COMMENT (2400, 185), (200, 120) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
  input onKey
/* CIF DECISION (1796, 
424), (
220, 
150) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    decision enabled;
    (true
/* CIF TASK (2084, 710), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      task false_pin := 0
/* CIF NEXTSTATE (2104, 860), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      nextstate askPIN;
    (false
/* CIF OUTPUT (1486, 696), (200, 120) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output disable
/* CIF NEXTSTATE (1470, 
846), (
233, 
80) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      nextstate disabled;
    enddecision;
endstate;

state disabled;
  input offKey
/* CIF NEXTSTATE (3750, 
1387), (
154, 
80) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate powerOff;
endstate;

state askPIN;
  input PIN(p
/* CIF OUTPUT (1785, 1080), (168, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output checkPIN(p
/* CIF NEXTSTATE (1769, 1190), (200, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate waitCheckPIN;
endstate;

state listening;
  input askReport
/* CIF OUTPUT (1348, 
334), (
470, 
86) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output getReport(me, BTSreceived /* to BTS_PIDs(BTSreceived) */
/* CIF NEXTSTATE (1510, 450), (143, 74) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state ringing;
  input answer_call
/* CIF OUTPUT (3614, 
340), (
547, 
81) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output call_resp(called_ok, me, caller, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF OUTPUT (3801, 451), (170, 88) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output convers
/* CIF NEXTSTATE (3788, 
569), (
200, 
96) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate conversation;
endstate;

state waitCallConf;
  input call_conf(called_status

/* CIF DECISION (4945, 384), (220, 150) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    decision called_status;
    (called_ok
/* CIF OUTPUT (4628, 662), (244, 91) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output convers
/* CIF OUTPUT (4523, 
784), (
453, 
111) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      output com_start(me, BTSreceived /* to BTS_PIDs(BTSreceived) */
/* CIF NEXTSTATE (4653, 925), (197, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
      nextstate conversation;
    (called_busy
/* CIF OUTPUT (4997, 654), (200, 88) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      join waitCallConf_1;
    (called_unreachable
/* CIF OUTPUT (5258, 651), (200, 91) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      join waitCallConf_2;
    enddecision;
endstate;

state conversation;
  input on_hook
/* CIF OUTPUT (6204, 
399), (
453, 
83) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output com_finish(me, correspondant, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (6351, 512), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate listening;
endstate;

state askPIN;
  input call_ind(caller
/* CIF OUTPUT (2186, 1082), (614, 92) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output call_resp(called_unreachable, me, caller, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF NEXTSTATE (2399, 1204), (188, 77) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state listening;
  input dialing(called

/* CIF DECISION (263, 345), (220, 58) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    decision called = me;
    (FALSE
/* CIF OUTPUT (360, 524), (346, 84) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output call_req(me, called, BTSreceived
/* to 
BTS_PIDs(
BTSreceived) */
/* CIF TASK (349, 638), (369, 97) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
      task correspondant := called
/* CIF NEXTSTATE (449, 765), (170, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      nextstate waitRandom
/* CIF COMMENT (639, 765), (160, 80) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */;
    (TRUE
/* CIF OUTPUT (121, 514), (160, 71) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */) :
      output rejected
/* CIF NEXTSTATE (125, 
616), (
154, 
80) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
      nextstate -;
    enddecision;
endstate;

state waitCallConf;
  input call_reject(reason
/* CIF OUTPUT (5931, 375), (253, 82) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output rejected
/* CIF NEXTSTATE (5962, 
487), (
192, 
80) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate listening;
endstate;

state listening;
  input giveReport(bil_report
/* CIF OUTPUT (1866, 340), (369, 97) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    output giveReport(bil_report) via KBD
/* CIF NEXTSTATE (1979, 467), (143, 72) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state listening;
  input offKey
/* CIF NEXTSTATE (1128, 
346), (
200, 
88) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate powerOff;
endstate;

connection
  waitInit1_1 :
  task p := pin_b
/* CIF ANSWER (566, 688), (169, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
  join waitInit1_4;
endconnection waitInit1_1;

connection
  waitInit1_2 :
  task p := pin_c
/* CIF ANSWER (756, 688), (158, 50) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
  join waitInit1_4;
endconnection waitInit1_2;

connection
  waitInit1_3 :
  task p := pin_d;
  join waitInit1_4;
endconnection waitInit1_3;

connection
  waitCallConf_1 :
  output busy
/* CIF NEXTSTATE (4997, 
772), (
200, 
120) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
  nextstate listening;
endconnection waitCallConf_1;

connection
  waitCallConf_2 :
  output unreachable
/* CIF NEXTSTATE (5258, 
772), (
200, 
120) 
*/
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
  nextstate listening;
endconnection waitCallConf_2;
endprocess MobileSt;



process SIM (1, 1);

/* CIF CurrentPage 1 */

/* CIF TEXT (70, 872), (1558, 463) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */
/* Encryption algorithm also stored in the network (never transmitted): */
newtype A3_encryption_t
  operators
    A3_encrypt1 : NATURAL, NATURAL -> NATURAL;
  operator A3_encrypt1;
  fpar
    n NATURAL,
    key NATURAL;
  returns NATURAL; referenced;
endnewtype;
dcl
  PIN PIN_t /* replaces context parameters. */,
  Kp NATURAL := 
    3 /* Secret key associated to the SIM owner, also stored in the network. */,
  p PIN_t,
  rand NATURAL;
/* CIF End Text */

/* CIF CurrentPage 1 */

/* CIF START (87, 120), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */

start;
    nextstate waitInit;

state ready;
  input checkPIN(p
/* CIF OUTPUT (285, 340), (226, 77) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */);
    output PIN_OK(p = PIN
/* CIF NEXTSTATE (318, 447), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate -;
endstate;

state ready;
  input randomNr(rand
/* CIF COMMENT (873, 228), (160, 80) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */) comment 'Comes from
        the AUC.'
/* CIF OUTPUT (576, 370), (352, 82) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    output encryptedNr(A3_encrypt1(rand, Kp
/* CIF COMMENT (940, 325), (160, 173) */
/* CIF Keep Specific Geode TextMode 3 */
/* CIF Keep Specific Geode Modified */)) comment 
    'Back to the
          AUC, which
          will compare it
          to its own
          computation.'
/* CIF NEXTSTATE (656, 529), (192, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */;
    nextstate -;
endstate;

state waitInit;
  input initSIM(PIN
/* CIF NEXTSTATE (87, 450), (160, 80) */
/* CIF Keep Specific Geode TextMode 4 */
/* CIF Keep Specific Geode Modified */);
    nextstate ready;
endstate;
endprocess SIM;



operator A3_encrypt1;
fpar
  n NATURAL,
  key NATURAL;
returns NATURAL;

start;
    return (n * key) + 7;
endoperator A3_encrypt1;



block type MSBTSProxy;
gate BTS1x out with (MtoB); in with (BtoM);
gate Ms1x out with (BtoM); in with (MtoB);
gate BTS2x out with (MtoB); in with (BtoM);
gate MS2x out with (BtoM); in with (MtoB);
gate BTS3x out with (MtoB); in with (BtoM);
gate MS3x out with (BtoM); in with (MtoB);
gate BTS4x out with (MtoB); in with (BtoM);
gate MS4x out with (BtoM); in with (MtoB);
signalroute MS1
  from Proxy to env via MS1x with (BtoM);
  from env via MS1x to Proxy with (MtoB);
signalroute BTS1
  from Proxy to env via BTS1x with (MtoB);
  from env via BTS1x to Proxy with (BtoM);
signalroute MS2
  from Proxy to env via MS2x with (BtoM);
  from env via MS2x to Proxy with (MtoB);
signalroute BTS2
  from Proxy to env via BTS2x with (MtoB);
  from env via BTS2x to Proxy with (BtoM);
signalroute MS3
  from Proxy to env via MS3x with (BtoM);
  from env via MS3x to Proxy with (MtoB);
signalroute BTS3
  from Proxy to env via BTS3x with (MtoB);
  from env via BTS3x to Proxy with (BtoM);
signalroute MS4
  from Proxy to env via MS4x with (BtoM);
  from env via MS4x to Proxy with (MtoB);
signalroute BTS4
  from Proxy to env via BTS4x with (MtoB);
  from env via BTS4x to Proxy with (BtoM);
process Proxy (1, 1) referenced;
endblock type MSBTSProxy;



process Proxy;
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 /* replaces 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;

start;
    nextstate Idle;
/* Signals from MS */

state Idle;
  input call_resp(called_state, MID1, MID2, BTS_ID);
    output call_resp(called_state, MID1, MID2, BTS_ID) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input call_req(MID1, MID2, BTS_ID);
    output call_req(MID1, MID2, BTS_ID) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input com_start(MID1, BTS_ID);
    output com_start(MID1, BTS_ID) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input com_finish(MID1, MID2, BTS_ID
/* Signals from MS */);
    output com_finish(MID1, MID2, BTS_ID) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input getReport(MID1, BTS_ID);
    output getReport(MID1, BTS_ID) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input logOn(MID1, BTS_ID, IMEI);
    task MS_PIDs(MID1) := sender;
    output logOn(MID1, BTS_ID, IMEI) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input encryptedNr(encryptedNr, BTS_ID);
    output encryptedNr(encryptedNr, BTS_ID) to BTS_PIDs(BTS_ID);
    nextstate Idle;
endstate;

state Idle;
  input call_conf(called_state, MID1);
    output call_conf(called_state, MID1) to MS_PIDs(MID1);
    nextstate Idle;
endstate;

state Idle;
  input call_ind(MID1, MID2
/* Signals from BTSes */);
    output call_ind(MID1, MID2) to MS_PIDs(MID2);
    nextstate Idle;
endstate;

state Idle;
  input call_reject(reason, MID1);
    output call_reject(reason, MID1) to MS_PIDs(MID1);
    nextstate Idle;
endstate;

state Idle;
  input giveReport(billingReport, MID1);
    output giveReport(billingReport, MID1) to MS_PIDs(MID1);
    nextstate Idle;
endstate;

state Idle;
  input initMS(BTS_ID, MID1, IMEI
/* Signals from BTSes */);
    task BTS_PIDs(BTS_ID) := sender;
    output initMS(BTS_ID, MID1, IMEI) to MS_PIDs(MID1);
    nextstate Idle;
endstate;

state Idle;
  input randomNr(rand, MID2);
    output randomNr(rand, MID2) to MS_PIDs(MID2);
    nextstate Idle;
endstate;
endprocess Proxy;