// ***************************************************************************
// @copyright   Copyright Notification
//   No part may be reproduced except as authorized by written permission.
//   The copyright and the foregoing restriction extend to reproduction in all media.
//   Trademark 2010, 3GPP Organizational Partners (ARIB, ATIS, CCSA, ETSI, TTA, TTC).
//   All rights reserved.
// @version: IWD_10wk37
// * $Date: 2010-09-15 12:00:17 +0200 (Wed, 15 Sep 2010) $
// * $Rev: 3889 $
// ***************************************************************************

module NAS_Attach_UG_GERAN {

  import from CommonDefs all;
  import from GERAN_Parameters all;
  import from UTRAN_Parameters all;
  import from Parameters all;
  import from GERAN_Component all;
  import from CommonIratDefs all;
  import from UTRANGERAN_CommonFunctions all;
  import from GERAN_CommonFunctions all;
  import from NAS_AuxiliaryDefsAndFunctions all;
  import from NAS_24008TypeDefs all;
  import from NAS_CommonTypeDefs all;
  import from NAS_CommonTemplates all;
  import from NAS_24008Templates all;
  import from GERAN_TypeDefs all;
  import from GERAN_Templates all;
  import from UpperTesterFunctions all;


//---------------------------------------------------------------------
/**
  * @desc Attach / rejected / EPS services and non-EPS services not allowed (multi RAT test)
*/
function f_TC_9_2_1_1_11_GERAN () runs on GERAN_PTC
{
 /*
    Test Purpose (TP)
(1)
with { UE has sent an ATTACH REQUEST message including a PDN CONNECTIVITY REQUEST message }
ensure that {
  when { UE receives an ATTACH REJECT message with the reject cause set to "EPS services and non-EPS services not allowed" }
    then { UE considers the USIM as invalid for EPS services and non-EPS services and enters state EMM-DEREGISTERED }
            }
(2)
with { UE receives an ATTACH REJECT message with the reject cause set to "EPS services and non-EPS services not allowed" }
ensure that {
  when { the UE has been switched off, then switched on }
    then { the UE sends an ATTACH REQUEST message with IMSI, including a PDN CONNECTIVITY REQUEST message }
            }
(3)
with { UE receives an ATTACH REJECT message with the reject cause set to "EPS services and non-EPS services not allowed" }
ensure that {
  when { the UE has been switched off, then switched on and a UMTS or GSM cell is found }
    then { the UE sends an ATTACH REQUEST message with IMSI and TMSI status indicated invalid TMSI }
            }

    */

    /*
    Pre-test conditions
System Simulator:
-    Cell A, Cell B (home PLMN, different TAs) and Cell G (another PLMN)
-    If pc_UTRAN Cell 5 and if (NOT pc_UTRAN AND pc_GERAN) Cell 24 are configured according to Table 4.4.4-2 in [18].
-    if pc_UTRAN, Cell 5 (only active when stated)
-    if pc_GERAN and NOT pc_UTRAN, Cell 24 (only active when stated)
-    The different cells may not be simultaneously activated.
UE:
-   the UE is configured to initiate EPS attach;
-   the UE is previously registered on E-UTRAN, and when on E-UTRAN, the UE is last authenticated and registered on cell A using default message contents according to TS 36.508 [18];
-   if pc_UTRAN (respectively if pc_GERAN and NOT pc_UTRAN), the UE is previously registered on UTRAN (respectively GERAN), and when on UTRAN (respectively GERAN), the UE is last registered on cell 5 (respectively cell 24) using default message contents according to TS 36.508 [18].
Preamble:
-    The UE is in state Switched OFF (state 1) according to clause [18].

  */

  var boolean v_TriggerRxd := false;
  var G_LLC_DATAMESSAGE_IND v_LLCDataInd;

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell(geran_Cell24);
    
    // Pre-Preamble on GERAN cell first to set PTSMI, PTSMI Sig and TMSI in USIM
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);

    //@siclog "Step 21a1" siclog@
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //  Check: Does the UE transmit an ATTACH REQUEST message in the next 30 seconds? (F)
    //@siclog "Step 21a2" siclog@
    f_GERAN_CheckNoAttachOnCell (geran_Cell24, 30.0, "Step 21a2");

    //@siclog "Step 21a3" siclog@
    // The operator initiates an attach by MMI or by AT command.
    f_UT_TriggerAttach(UT);

    //  Check: Does the UE transmit an ATTACH REQUEST message in the next 30 seconds? (F)
    //@siclog "Step 21a4" siclog@
    f_GERAN_CheckNoAttachOnCell (geran_Cell24, 30.0, "Step 21a4");

    //@siclog "Step 21a5" siclog@
    f_UT_SwitchOffUE (UT, false);

    //@siclog "Step 21a6" siclog@
    f_UT_SwitchOnUE (UT, false );

    //  Check: Does the UE transmit an ATTACH REQUEST message with IMSI-1and TMSI status indicated invalid TMSI?
    //@siclog "Step 21a8" siclog@
    f_UplinkTBFOnePhase (geran_Cell24);
    alt { // Receive GPRS Attach Request Message
      [] G_LLC.receive(car_G_LLC_UnitData_IND(cr_G_AttachReqWithIMSI(cr_AttachType(?, tsc_I_AttachTypeCombined),
                                                                     f_Imsi2MobileIdentity(px_IMSI_Def),
                                                                     cr_RAI_Any(omit),
                                                                     '111'B)))  -> value v_LLCDataInd
        {
          f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 21a8");
        }
    }
    f_GERAN_TestBody_Set( false );
    
    f_DownlinkTBFEstablishment(geran_Cell24, 1);
    G_LLC.send(cas_G_LLC_UnitData_Req (f_GERAN_TLLI_Get(geran_Cell24), tsc_LLCSapi_GMM, tsc_LLC_PM, px_GSM_CipheringOnOff,
                          cs_G_AttachReject('16'O))); // cause 'congestion'

    // Test case now finished on GERAN side
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);
    f_GERAN_SS_CellRelease ( geran_Cell24 );
  } // doesn't support GERAN

} // f_TC_9_2_1_1_11_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_1_12_GERAN () runs on GERAN_PTC
{
    /*
    Test Purpose (TP)
 (1) with { UE has sent an ATTACH REQUEST message including a PDN CONNECTIVITY REQUEST message }
ensure that {
  when { UE receives an ATTACH REJECT message with the reject cause set to "EPS services not allowed" }
then { UE deletes the GUTI and the last visited registered TAI and KSI and considers the USIM as invalid
  for EPS services until switching off or the UICC containing the USIM is removed and deletes the list of
  equivalent PLMNS and UE enters state EMM-DEREGISTERED }
  }

    SS: Cell A, Cell B and Cell G:
        Cell A and Cell B (HPLMN, different TAs),
        Cell G (another PLMN)
        if pc_UTRA, Cell 5 (HPLMN, UTRAN NMO 2)
        if NOT pc_UTRA and pc_GERAN, Cell 24 (HPLMN, GERAN, NMO 2)
     UE: The test USIM contains IMSI-1, GUTI-1 and TAI-1 and EPS update status is "EU1: UPDATED"
         if pc_GERAN or pc_UTRA, the test USIM contains P-TMSI, P-TMSI signature1 and RAI-1 and
         GPRS update status is "GU1: UPDATED" */

  var boolean v_TriggerRxd := false;
  var G_L2_DATAMESSAGE_IND v_LocUpd;
  var template (value) MobileIdentity v_MobileIdIMSI := f_Imsi2MobileIdentity(px_IMSI_Def);
  var O3_Type v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  //var O1_Type v_RAC := f_GERAN_RAC_Get(geran_Cell24);
  var O2_Type v_LAC := f_GERAN_LAC_Get(geran_Cell24);
  var G_LogicChType v_ChannelType;
  var SubChannelNumber v_SubChannel;
  timer t_Wait := f_UG_SetTimerToleranceMin (120.0);
  timer t_Wait1 := f_UG_SetTimerToleranceMin (30.0);

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell(geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    // Second Trigger
    //@siclog "Step 10a1" siclog@
    // Set Cell 5 to "Serving Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 10a3" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message in the next 2 minutes?
    t_Wait.start;
    f_UplinkTBFOnePhase (geran_Cell24);
    alt {
    []    G_LLC.receive(car_G_LLC_UnitData_IND ( cr_G_AttachReq(?, ?, ?, ?)))
       {
         t_Wait.stop;
         f_GERAN_SetVerdictFailOrInconc (__FILE__, __LINE__, "Step 10a4");
       }
    [pc_CS] G_L2.receive(car_G_L2_Estab_IND(geran_Cell24, tsc_PhyCh0, ?, ?, cr_G_LocationUpdatingRequest))
                        -> value v_LocUpd
        {
         v_ChannelType := v_LocUpd.sabm.g_LogicChType;
         v_SubChannel := v_LocUpd.sabm.subChannel;

         G_L2.send (cas_G_L2_DATA_REQ (geran_Cell24, 0, tsc_PhyCh0, v_ChannelType, v_SubChannel, cs_G_RFN_Omit, cs_G_LocUpdAcpIMSI (v_PLMN, v_LAC, v_MobileIdIMSI)));
         repeat;
        }

    [] t_Wait.timeout {}
    }

    //@siclog "Step 10a4" siclog@
    f_UT_TriggerAttach (UT);

    //@siclog "Step 10a5" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message in the next 30 seconds?
    t_Wait1.start;
    f_UplinkTBFOnePhase (geran_Cell24);
    alt {
    []    G_LLC.receive(car_G_LLC_UnitData_IND ( cr_G_AttachReq(?, ?, ?, ?)))
       {
         t_Wait1.stop;
         f_GERAN_SetVerdictFailOrInconc (__FILE__, __LINE__, "Step 10a5");
       }

    [] t_Wait1.timeout {}
    }

    // Finished here for now
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);

    // Third Trigger
    //@siclog "Step 10a6" siclog@
    // Set Cell 5 to "Suitable Neighbour Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_SuitableNeighbourCell);

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );

    f_GERAN_SS_CellRelease ( geran_Cell24 );

   } // UE doesn't support GERAN, so do nothing
 } // f_TC_9_2_1_1_12_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_5_GERAN () runs on GERAN_PTC
{

    /* TC_9_2_1_2_5
    Test Purpose (TP)
     (1)
    with { UE has sent an ATTACH REQUEST message }
    ensure that {
      when { UE receives an ATTACH REJECT message with the EMM cause set to 'EPS services and non-EPS services not allowed' }
        then { UE deletes the GUTI, last visited registered TAI and KSI and considers the USIM as invalid
              for EPS services and non-EPS services and enters state EMM-DEREGISTERED }
     (2)
    with { UE has sent an ATTACH REQUEST message }
    ensure that {
      when { UE receives an ATTACH REJECT message with the EMM cause set to 'EPS services and non-EPS services not allowed' }
        then { UE deletes the P-TMSI, P-TMSI signature, RAI, GPRS ciphering key sequence number, TMSI, LAI and ciphering key sequence number }
   
    Preconditions:
    System Simulator:
    -   Cell A and B
     -  if pc_UTRA supported by UE, Cell 5
                    Cell5 belongs to LAI-1 and RAI-1 (home PLMN)
     -  if NOT pc_UTRA and pc_GERAN, Cell 24
                    Cell24 belongs to LAI-1 and RAI-1 (home PLMN)
    UE:
    -   The test USIM contains IMSI-1, GUTI-1 and TAI-1, and EPS update status is "EU1: UPDATED".
    -   The test USIM contains P-TMSI-1 (belonging RAI-1) and the GPRS update status is "GU1:UPDATED"
    -   The test USIM containts TMSI-1 (belonging to LAI-1) and the update status is "U1:UPDATED"
    
    Preamble:
    -   UE is in state Switched OFF (state 1) according to clause [18]

    */

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    fl_TC_9_2_1_2_5and7_Body_GERAN ();

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );

    f_GERAN_Postamble (geran_Cell24, G1_IDLE);

  } // UE doesn't support GERAN, or supports UTRAN too, so do nothing

} // fl_TC_9_2_1_2_5_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_7_GERAN () runs on GERAN_PTC
{

    /* TC_9_2_1_2_7
    Test Purpose (TP)
     (1)
    with { UE has sent an ATTACH REQUEST message }
    ensure that {
      when { UE receives an ATTACH REJECT message with the EMM cause set to "Illegal ME" }
        then { UE deletes the GUTI, last visited registered TAI and KSI and considers the USIM as invalid
              for EPS services and non-EPS services and enters state EMM-DEREGISTERED }
     (2)
    with { UE has sent an ATTACH REQUEST message }
    ensure that {
      when { UE receives an ATTACH REJECT message with the EMM cause set to "Illegal ME" }
        then { UE deletes the P-TMSI, P-TMSI signature, RAI, GPRS ciphering key sequence number, TMSI, LAI and ciphering key sequence number }
    
    
    Preconditions
    System Simulator:
    -   Cell A and B
     -  if pc_UTRA supported by UE, Cell 5
                    Cell5 belongs to LAI-1 and RAI-1 (home PLMN)
     -  if NOT pc_UTRA and pc_GERAN, Cell 24
                    Cell24 belongs to LAI-1 and RAI-1 (home PLMN)
    UE:
    -   The test USIM contains IMSI-1, GUTI-1 and TAI-1, and EPS update status is "EU1: UPDATED".
    -   The test USIM contains P-TMSI-1 (belonging RAI-1) and the GPRS update status is "GU1:UPDATED"
    -   The test USIM containts TMSI-1 (belonging to LAI-1) and the update status is "U1:UPDATED"
    
    Preamble:
    -   UE is in state Switched OFF (state 1) according to clause [18]

    */

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    fl_TC_9_2_1_2_5and7_Body_GERAN ();

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );

    f_GERAN_Postamble (geran_Cell24, G1_IDLE);

  } // UE doesn't support GERAN, or supports UTRAN too, so do nothing

} // f_TC_9_2_1_2_7_GERAN

//---------------------------------------------------------------------
function fl_TC_9_2_1_2_5and7_Body_GERAN () runs on GERAN_PTC
{

  var boolean v_TriggerRxd := false;
  var G_LLC_DATAMESSAGE_IND v_LLCDataInd;
  var B3_Type v_AttachType;
  var octetstring v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  var O1_Type v_RAC := f_GERAN_RAC_Get(geran_Cell24);
  var O2_Type v_LAC := f_GERAN_LAC_Get(geran_Cell24);
  
    // First Trigger
    //@siclog "Step 1" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
  
    // Second Trigger
    //@siclog "Step 8a1" siclog@
    // Set Cell 24 to "Serving Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 8a3" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message in the next 30 seconds?
    f_GERAN_CheckNoAttachOnCell (geran_Cell24, 30.0, "Step 10a3");
  
    // Third Trigger
    //@siclog "Step 10" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);

    // Fourth Trigger
    //@siclog "Step 15a1" siclog@
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_UT_SwitchOffUE (UT, false);

    // Set Cell 24 to "Serving Cell"
    //@siclog "Step 15a2" siclog@
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 15a3" siclog@
    f_UT_SwitchOnUE (UT, false );

    //@siclog "Step 15a5" siclog@
    // Check: Does the UE send an ATTACH REQUEST?
    f_UplinkTBFOnePhase (geran_Cell24);
    alt { // Receive GPRS Attach Request Message
    [] G_LLC.receive(car_G_LLC_UnitData_IND ( cr_G_AttachReqWithIMSI (cr_AttachType(?, tsc_I_AttachTypeCombined),
                                                                      f_Imsi2MobileIdentity(px_IMSI_Def),
                                                                      cr_RAI (omit, cr_LAI(omit, v_PLMN, 'FFFE'O), ?),
                                                                      '111'B)))  -> value v_LLCDataInd
      {
        f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 15a5");
        v_AttachType := v_LLCDataInd.unit.msg.attReq.attachType.attachType;
        f_GERAN_SplitPGCycle_Set(geran_Cell24, v_LLCDataInd.unit.msg.attReq.drxParameter);
      }
    }

    //@siclog "Step 15a6 - 15a7" siclog@
    f_GERAN_GPRS_Authentication (geran_Cell24);

    // Send GPRS Attach Accept
    //@siclog "Step 15a8" siclog@
    f_DownlinkTBFEstablishment(geran_Cell24, 1);
    G_LLC.send(cas_G_LLC_UnitData_Req (f_GERAN_TLLI_Get(geran_Cell24), tsc_LLCSapi_GMM, tsc_LLC_PM, px_GSM_CipheringOnOff,
                  cs_G_AttachAccept (cs_GMM_AttachResult(v_AttachType), cs_RAI(omit, cs_LAI(omit, v_PLMN, v_LAC), v_RAC),
                                cs_PTMSI_Signature (px_PTMSI_SigDef), cs_MobileIdTMSIorPTMSI ('18'O, px_PTMSI_Def))));

    //Receive GPRS Attach Complete Message
    //@siclog "Step 15a9" siclog@
    f_UplinkTBFOnePhase (geran_Cell24);
    G_LLC.receive(car_G_LLC_UnitData_IND (cr_G_AttachComplete));

} // // end function fl_TC_9_2_1_2_5and7_Body_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_6_GERAN () runs on GERAN_PTC
{
    /*
    Test Purpose (TP)
     (1)
    with { UE has sent an ATTACH REQUEST message }
    ensure that {
      when { UE receives an ATTACH REJECT message with the EMM cause set to "Illegal ME" }
        then { UE deletes the GUTI, last visited registered TAI and KSI and considers the USIM as invalid
              for EPS services and non-EPS services and enters state EMM-DEREGISTERED }
     (2)
    with { UE has sent an ATTACH REQUEST message }
    ensure that {
      when { UE receives an ATTACH REJECT message with the EMM cause set to "Illegal ME" }
        then { UE deletes the P-TMSI, P-TMSI signature, RAI, GPRS ciphering key sequence number, TMSI, LAI and ciphering key sequence number }
    */

    /*
    Pre-test conditions

    System Simulator:
    -   Cell A and B
     -  If pc_UTRAN is supported by UE, Cell 5 belongs to LAI-1 and RAI-1 (home PLMN)
     -  If pc_GERAN and NOT pc_UTRAN is supported by UE, Cell 24 belongs to LAI-1 and RAI-1 (home PLMN)
    UE:
    None.
    Preamble:
    -   USIM contains IMSI-1, GUTI-1 and TAI-1 and EPS update status is "EU1: UPDATED".
    -   USIM contains P-TMSI-1 (belonging to RAI-1) and the GPRS update status is "GU1: UPDATED"
    -   USIM contains TMSI-1 (belonging to LAI-1) and the update status is "U1: UPDATED"
    -   UE is switched OFF.

    */
  var boolean v_TriggerRxd := false;
  var G_LLC_DATAMESSAGE_IND v_LLCDataInd;
  var B3_Type v_AttachType;
  var octetstring v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  var O1_Type v_RAC := f_GERAN_RAC_Get(geran_Cell24);
  var O2_Type v_LAC := f_GERAN_LAC_Get(geran_Cell24);

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    // First Trigger
    //@siclog "Step 1" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);

    // Second Trigger
    //@siclog "Step 10a1" siclog@
    // Set Cell 24 to "Serving Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 10a3" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message in the next 30 seconds?
    f_GERAN_CheckNoAttachOnCell (geran_Cell24, 30.0, "Step 10a3");

    // Finished here for now
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);

    // Third Trigger
    //@siclog "Step 12" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);

    // Fourth Trigger
    //@siclog "Step 17a1" siclog@
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_UT_SwitchOffUE (UT, false);

    //  Set Cell 24 to "Serving Cell"
    //@siclog "Step 17a2" siclog@
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 17a5" siclog@
    // Check: Does the UE send an ATTACH REQUEST?
    f_UplinkTBFOnePhase (geran_Cell24);
    alt { // Receive GPRS Attach Request Message
    []    G_LLC.receive(car_G_LLC_UnitData_IND ( cr_G_AttachReqWithIMSI (cr_AttachType(?, tsc_I_AttachTypeCombined),
                                                                         f_Imsi2MobileIdentity(px_IMSI_Def),
                                                                         cr_RAI (omit, cr_LAI(omit, v_PLMN, 'FFFE'O), ?),
                                                                         '111'B))) -> value v_LLCDataInd
      {
        f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 17a5");
        v_AttachType := v_LLCDataInd.unit.msg.attReq.attachType.attachType;
        f_GERAN_SplitPGCycle_Set(geran_Cell24, v_LLCDataInd.unit.msg.attReq.drxParameter);
      }
    }

    //@siclog "Step 17a6 - 17a7" siclog@
    f_GERAN_GPRS_Authentication (geran_Cell24);

    //  Send GPRS Attach Accept
    //@siclog "Step 17a8" siclog@
    f_DownlinkTBFEstablishment(geran_Cell24, 1);
    G_LLC.send(cas_G_LLC_UnitData_Req (f_GERAN_TLLI_Get(geran_Cell24), tsc_LLCSapi_GMM, tsc_LLC_PM, px_GSM_CipheringOnOff,
                  cs_G_AttachAccept (cs_GMM_AttachResult(v_AttachType), cs_RAI(omit, cs_LAI(omit, v_PLMN, v_LAC), v_RAC),
                                cs_PTMSI_Signature (px_PTMSI_SigDef), cs_MobileIdTMSIorPTMSI ('18'O, px_PTMSI_Def))));

    //Receive GPRS Attach Complete Message
    //@siclog "Step 17a9" siclog@
    f_UplinkTBFOnePhase (geran_Cell24);
    G_LLC.receive(car_G_LLC_UnitData_IND (cr_G_AttachComplete));

  // Test case now finished on GERAN side
  f_GERAN_TestBody_Set( false );

  f_GERAN_Postamble (geran_Cell24, G1_IDLE);

    } // UE doesn't support GERAN, or supports UTRAN too, so do nothing
} // f_TC_9_2_1_2_6_GERAN

//---------------------------------------------------------------------
/**
  * @desc Combined attach / rejected / EPS services not allowed (multi RAT test)
*/
function f_TC_9_2_1_2_8_GERAN () runs on GERAN_PTC
{

 /*
  * Test Purpose (TP)
  * (1)
  * with { UE has sent an ATTACH REQUEST message including a PDN CONNECTIVITY REQUEST message }
  * ensure that {
  *   when { UE receives an ATTACH REJECT message with the reject cause set to "EPS services not allowed" }
  *     then { UE considers the USIM as invalid for EPS services and enters state EMM-DEREGISTERED and UE does not attempt to attach on any other cell }
  *   }
  */

  /*
   * System Simulator:
   * -   Cell A and Cell B
   * -   If pc_UTRAN supported by UE, Cell 5.
   * -   Cell 5 belongs to LAI-1 and RAI-1(home PLMN)
   * -   If pc_GERAN and NOT pc_UTRAN supported by UE, Cell 24.
   * -   Cell 24 belongs to LAI-1 and RAI-1(home PLMN)
   * UE:
   * -   The test USIM contains IMSI1, GUTI1 and TAI1, and EPS update status is "EU1: UPDATED".
   * -   The test USIM contains P-TMSI-1 (belonging to RAI-1) and the GPRS update status is "GU1: UPDATED".
   * -   The test USIM contains TMSI-1 (belonging to LAI-1) and the update status is "U1: UPDATED".
   * Preamble:
   * -   The UE is in state Switched OFF (state 1) according to clause [18].
   */

  var boolean v_TriggerRxd := false;
  var G_L2_DATAMESSAGE_IND v_LocUpd;
  var octetstring v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  var O2_Type v_LAC := f_GERAN_LAC_Get(geran_Cell24);

  var G_LogicChType v_ChannelType;
  var SubChannelNumber v_SubChannel;

  var template (value) MobileIdentity v_MobileIdIMSI := f_Imsi2MobileIdentity(px_IMSI_Def);
  v_MobileIdIMSI.iei := '13'O; // Need to include iei in LUAccept, but function returns without iei
  

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN);
     
    f_GERAN_CreateCell (geran_Cell24);
 
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    //@siclog "Step 1" siclog@
    //The SS configures: Cell 5 as a "Suitable neighbour cell".
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_SuitableNeighbourCell);
    
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    
    // IF pc_GERAN THEN the following messages are sent and shall be received on cell 24.
    //  Check: Does the UE transmit a LOCATION UPDATING REQUEST message on Cell 24? (1, P)
    //@siclog "Step 6a1 - 6a2" siclog@
    alt {
      []    G_L2.receive (car_G_L2_Estab_IND (geran_Cell24, ?, ?, ?, cr_G_LocationUpdatingRequest))
        -> value v_LocUpd
        {
          f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 6a2");
          v_ChannelType := v_LocUpd.sabm.g_LogicChType;
          v_SubChannel := v_LocUpd.sabm.subChannel;
        }
    }
       
    //  The SS transmits a LOCATION UPDATING ACCEPT message with Location updating type = "IMSI attach" as specified in 3GPP TS 24.008.
    //@siclog "Step 6a3" siclog@
    G_L2.send (cas_G_L2_DATA_REQ (geran_Cell24, 0, tsc_PhyCh0, v_ChannelType, v_SubChannel, cs_G_RFN_Omit, cs_G_LocUpdAcpIMSI ( v_PLMN, v_LAC, v_MobileIdIMSI )));
       
    // Test case now finished on GERAN side
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger); // Send trigger to EUTRA side
    f_GERAN_TestBody_Set( false );
    
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    
    f_GERAN_Postamble (geran_Cell24, G1_IDLE);
   
  } // GERAN not supported so do nothing
} // f_TC_9_2_1_2_8_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_9_GERAN () runs on GERAN_PTC
{
    // @desc Combined attach / rejected / PLMN not allowed

  /*
    System Simulator:
     -  Cell I and Cell G
     -  If pc_GERAN supported by UE, Cell 24

    UE:
    -   The test USIM contains IMSI1, GUTI1 and TAI1, and EPS update status is "EU1: UPDATED".
    -   The "forbidden PLMN list" is empty.

    Preamble:
    -   The UE is in state Switched OFF (state 1) according to [18].M contains P-TMSI-1 (belonging to RAI-1) and the update status is "U1: UPDATED"
    */

  var boolean v_TriggerRxd := false;
  var octetstring v_PLMN := '001201'O;

  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_PLMN_Set (geran_Cell24, v_PLMN);

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );
  
    // First Trigger
    //@siclog "Step 1" siclog@
    // +   Set Cell 24 as the "Non-Suitable cell".
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
  
    // Second Trigger
    //@siclog "Step 9a1" siclog@
    // +   Set Cell 24 as the "Serving cell".
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //+   The following messages are sent and shall be received on cell 24.
    //+   Check: Does the UE transmit an ATTACH REQUEST message in the next 30 seconds?
    //@siclog "Step 9a2 - 9a3" siclog@
    f_GERAN_CheckNoAttachOnCell (geran_Cell24, 30.0, "Step 9a3");

    //@siclog "Step 10" siclog@
    // +   Set Cell 24 as the "Non-Suitable cell".
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );
    // So just wait for trigger to take down the cell
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SS_CellRelease ( geran_Cell24 );
    }
} // f_TC_9_2_1_2_9_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_11_GERAN () runs on GERAN_PTC
{

    /* Test Purpose (TP)
     
        (1)
        with { UE has sent an ATTACH REQUEST message }
        ensure that {
          when { UE receives an ATTACH REJECT message with the EMM cause set to "Roaming not allowed in this tracking area" }
            then { UE sets the EPS update status to EU3 ROAMING NOT ALLOWED and UE deletes the GUTI, the last visited registered TAI and KSI and UE enters the state EMM-DEREGISTERED.LIMITED-SERVICE or optionally EMM-DEREGISTERED.PLMN-SEARCH and UE stores the current TAI in the list of "forbidden tracking areas for roaming" and deletes the TMSI, the LAI and the ciphering key sequence number }
                    }
        (2)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE or EMM-DEREGISTERED.PLMN-SEARCH state and the current TAI is in the list of "forbidden tracking areas for roaming" }
        ensure that {
          when { UE re-selects a new cell in the same TA where it was rejected }
            then { UE does not attempt to attach }
                    }
                    
        (3)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE or EMM-DEREGISTERED.PLMN-SEARCH state and the TAI of the current cell belongs to the list of "forbidden tracking areas for roaming" }
        ensure that {
          when { UE enters a cell belonging to a tracking area not in the list of "forbidden tracking areas for roaming" }
            then { UE attempts to attach with IMSI }
                    }
    
        (4)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE or EMM-DEREGISTERED.PLMN-SEARCH state and the list of "forbidden tracking areas for roaming" contains more than one TAI }
        ensure that {
          when { UE selects a cell belonging to one of the TAIs in the list of "forbidden tracking areas for roaming" }
            then { UE does not attempt to attach }
                    }
   
        (5)
        with { UE has sent an ATTACH REQUEST message }
        ensure that {
          when { UE receives an ATTACH REJECT message with the EMM cause set to "Roaming not allowed in this tracking area" }
            then { UE deletes RAI, P-TMSI, P-TMSI signature and GPRS ciphering key sequence number and sets the GPRS update status to GU3 ROAMING NOT ALLOWED }
                    }
   
        (6)
        with { UE is switched off or the UICC containing the USIM is removed }
        ensure that {
          when { UE is powered on in the cell belonging to the TAI which was in the list of "forbidden tracking areas for roaming" before UE was switched off or the USIM is inserted again on that cell }
            then { UE performs registration on that cell }
                    }
    
        (7)
        with { a cell of the HPLMN is available }
        ensure that {
          when { UE performs a PLMN selection }
            then { UE returns to a cell of the HPLMN }
                    }
   
   
        System Simulator:
        -     Cell C, Cell I, Cell K, Cell L and if pc_UTRAN Cell 5 and if (NOT pc_UTRAN AND pc_GERAN)
              Cell 24 are configured according to Table 6.3.2.2-1 in [18],
              but at most two cells are simultaneously activated:
        -     Cell I and Cell K (visited PLMN, same TA),
        -     Cell L (same visited PLMN, another TA),
        -     Cell C (home PLMN),
        -     if pc_UTRAN, Cell 5 (only active when stated),
        -     same PLMN like visited PLMN above
        -     RAI-1 (RAC & LAC values chosen by SS)
        -     System information indicate that NMO 1 is used
        -     if pc_GERAN and NOT pc_UTRAN, Cell 24 (only active when stated).
        -     same PLMN like visited PLMN above
        -     RAC-1 (RAC & LAC values chosen by SS)
        -     System information indicate that NMO 1 is used
        NOTE 1:   Cell K is present to confirm that UE does not attempt attach to the cell in same TAI after reject
                  from the SS.
        NOTE 2:   Cell C is present to confirm that UE does attempt attach to the cell in HPLMN after reject
                  from the SS.
        NOTE 3:   The requirement in 3GPP TS 24.301 to store at least 40 entries in the list of "forbidden tracking
                  areas for roaming" is not fully tested.
        NOTE 4:   Different types of UE may use different methods to periodically clear the list of forbidden areas
                  (e.g. every day at 12 am) for roaming. If the list is cleared while the test is being run,
                  it may be necessary to re-run the test.
        UE:
        -     The test USIM contains IMSI-1, GUTI-1 and TAI-1, and EPS update status is "EU1: UPDATED".
        -     The test USIM contains P-TMSI-1 (belonging to RAI-1) and the GPRS update status is "GU1: UPDATED".
        -     The test USIM contains TMSI-1 (belonging to LAI-1) and the update status is "U1: UPDATED".

        Preamble:
        -     The UE is in state Switched OFF (state 1) according to [18]
    */


  var boolean v_TriggerRxd := false;
  var G_LLC_DATAMESSAGE_IND v_LLCDataInd;
  var octetstring v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  
  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    // First Trigger
    //@siclog "Step 1" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
  
    // Second Trigger
    //@siclog "Step 16a1" siclog@
    // Set Cell 24 to "Serving Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 16a2" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message without P-TMSI, P-TMSI signature, RAI, TMSI
    f_UplinkTBFOnePhase (geran_Cell24);
    alt { // Receive GPRS Attach Request Message
      []    G_LLC.receive(car_G_LLC_UnitData_IND ( cr_G_AttachReqWithIMSI (cr_AttachType(?, tsc_I_AttachTypeCombined),
                                                                           f_Imsi2MobileIdentity(px_IMSI_Def),
                                                                           cr_RAI (omit, cr_LAI(omit, v_PLMN, 'FFFE'O), ?),
                                                                           '111'B))) -> value v_LLCDataInd
        {
          f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 16a2");
        }
    }

    //@siclog "Step 16a3" siclog@
    // Send an ATTACH REJECT message with GMM Cause "Roaming not allowed in this location area"
     G_LLC.send(cas_G_LLC_UnitData_Req (f_GERAN_TLLI_Get(geran_Cell24), tsc_LLCSapi_GMM, tsc_LLC_PM, px_GSM_CipheringOnOff,
                           cs_G_AttachReject('0D'O))); // cause 'Roaming not allowed in this location area'

    // Finished here for now
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );

    f_GERAN_SS_CellRelease ( geran_Cell24 );

  } // UE doesn't support GERAN, or supports UTRAN too, so do nothing

} // f_TC_9_2_1_2_11_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_13_GERAN () runs on GERAN_PTC
{

    /* Test Purpose (TP)
        (1)
        with { UE has sent an ATTACH REQUEST message }
        ensure that {
          when { UE receives an ATTACH REJECT message with the EMM cause set to 'No Suitable Cells In tracking area' }
            then { UE sets the EPS update status to EU3 ROAMING NOT ALLOWED, deletes any GUTI, last visited registered TAI and KSI, resets the attach attempt counter, enters the state EMM-DEREGISTERED.LIMITED-SERVICE and stores the current TAI in the list of "forbidden tracking areas for roaming" }
                    }
                    
        (2)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE state and the current TAI is in the list of "forbidden tracking areas for roaming" }
        ensure that {
          when { UE re-selects a cell that belongs to the TAI where UE was rejected }
            then { UE does not attempt to attach }
                    }

        (3)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE state and the current TAI is in the list of "forbidden tracking areas for roaming" and KSI was deleted }
        ensure that {
          when { in the same PLMN, UE enters a cell which provides normal service and belongs to the tracking area not in the list of "forbidden tracking areas for roaming" }
            then { UE attempts to attach with IMSI indicated that no key is available }
                    }

        (4)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE state and the current TAI is in the list of "forbidden tracking areas for roaming" }
        ensure that {
          when { there are cells in the same PLMN and other PLMN that provide normal service and belong to the tracking area not in the list of "forbidden tracking areas for roaming" }
            then { UE attempts to attach to the cell in the same PLMN }
                    }

        (5)
        with { UE is in EMM-DEREGISTERED.LIMITED-SERVICE state and the list of "forbidden tracking areas for roaming" contains more than one TAI }
        ensure that {
          when { UE re-selects a cell that belongs to one of the TAIs in the list of "forbidden tracking areas for roaming" }
            then { UE does not attempt to attach }
                    }

        (6)
        with { UE has sent an ATTACH REQUEST message }
        ensure that {
          when { UE receives an ATTACH REJECT message with the EMM cause set to 'No Suitable Cells In tracking area' }
            then { UE deletes RAI, P-TMSI, P-TMSI signature, GPRS ciphering key sequence number, TMSI, LAI and ciphering key sequence number }
                    }

        (7)
        with { UE is swithched off }
        ensure that {
          when { UE is powered on in the cell belonging to the TAI which was in the list of "forbidden tracking areas for roaming" before UE was switched off }
            then { UE attempts to attach }
                    }


        System Simulator:
            -   Cell I, Cell J, Cell K and Cell L are configured according to Table 6.3.2.2-1 in [18] (maximum 3 cells are simultaneously active):
            -   Cell I and Cell K (visited PLMN, same TA),
            -   Cell L (same visited PLMN, another TA),
            -   Cell J (another VPLMN),
            -   if pc_UTRAN, Cell 5 (only active when stated),
            -   same PLMN like visited PLMN above
            -   RAI-1 (RAC & LAC values chosen by SS)
            -   System information indicate that NMO 1 is used
            -   if pc_GERAN and NOT pc_UTRAN, Cell 24 (only active when stated).
            -   same PLMN like visited PLMN above
            -   RAC-1 (RAC & LAC values chosen by SS)
            -   System information indicate that NMO 1 is used
            NOTE 1: Cell L is present to confirm that UE searches in the same PLMN after reject from the SS.
            NOTE 2: Cell K is present to confirm that UE shall not attempt attach to the cell in same TAI it was once rejected from.
            NOTE 3: The requirement in 3GPP TS 24.301 to store at least 40 entries in the list of "forbidden tracking areas for roaming" is not fully tested.
            NOTE 4: Different types of UE may use different methods to periodically clear the list of forbidden areas (e.g. every day at 12 am) for roaming. If the list is cleared while the test is being run, it may be necessary to re-run the test.
            UE:
            -   The test USIM contains IMSI-1, GUTI-1 and TAI-1, and EPS update status is "EU1: UPDATED".
            -   The test USIM contains P-TMSI-1 (belonging to RAI-1) and the GPRS update status is "GU1: UPDATED".
            -   The test USIM contains TMSI-1 (belonging to LAI-1) and the update status is "U1: UPDATED".
            Preamble:
            -   The UE is in state Switched OFF (state 1) according to clause [18].
    */

  var boolean v_TriggerRxd := false;
  var G_LLC_DATAMESSAGE_IND v_LLCDataInd;
  var octetstring v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  
  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    // First Trigger
    //@siclog "Step 1" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
  
    // Second Trigger
    //@siclog "Step 14a1" siclog@
    // Set Cell 24 to "Serving Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 14a2" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message without P-TMSI, P-TMSI signature, RAI, TMSI
    f_UplinkTBFOnePhase (geran_Cell24);
    alt { // Receive GPRS Attach Request Message
      [] G_LLC.receive(car_G_LLC_UnitData_IND (cr_G_AttachReqWithIMSI(cr_AttachType(?, tsc_I_AttachTypeCombined),
                                                                      f_Imsi2MobileIdentity(px_IMSI_Def),
                                                                      cr_RAI (omit, cr_LAI(omit, v_PLMN, 'FFFE'O), ?),
                                                                      '111'B))) -> value v_LLCDataInd
        {
          f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 14a2");
        }
    }

    //@siclog "Step 14a3" siclog@
    // Send an ATTACH REJECT message with GMM Cause "Roaming not allowed in this location area"
     G_LLC.send(cas_G_LLC_UnitData_Req (f_GERAN_TLLI_Get(geran_Cell24), tsc_LLCSapi_GMM, tsc_LLC_PM, px_GSM_CipheringOnOff,
                           cs_G_AttachReject('0D'O))); // cause 'Roaming not allowed in this location area'

    //@siclog "Step 15" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);

    // Finished here for now
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );

    f_GERAN_SS_CellRelease ( geran_Cell24 );

  } // UE doesn't support GERAN, or supports UTRAN too, so do nothing

} // f_TC_9_2_1_2_13_GERAN

//---------------------------------------------------------------------
function f_TC_9_2_1_2_15_GERAN () runs on GERAN_PTC
{

    /*Test Purpose (TP)
        (1)
        with { UE has detected T3410 expiry after sending an ATTACH REQUEST message and has the attach attempt counter set to the value less than four }
        ensure that {
          when { UE detects T3411 expiry }
            then { UE restarts the attach procedure }
                    }

        (2)
        with { UE has sent an ATTACH REQUEST message and has the attach attempt counter set to four }
        ensure that {
          when { UE detects T3410 expiry }
            then { UE deletes GUTI, TAI list, last visited registered TAI and KSI }
                    }

        (3)
        with { UE has sent an ATTACH REQUEST message and has the attach attempt counter set to four }
        ensure that {
          when { UE detects T3410 expiry }
            then { UE deletes LAI, TMSI, ciphering key sequence number, RAI, P-TMSI, P-TMSI signature, and GPRS ciphering key sequence number }
                    }

        (4)
        with { UE has started T3402 }
        ensure that {
          when { UE detects T3402 expiry }
            then { UE restarts the attach procedure }
                    }

        System Simulator:
        -   Cell A, if pc_UTRAN Cell 5 and if (NOT pc_UTRAN AND pc_GERAN) Cell 24 are configured.
        -   Cell A,
        -   if pc_UTRAN, Cell 5 (only active when stated),
            -   same PLMN like visited PLMN above
            -   RAI-1 (RAC & LAC values chosen by SS)
            -   System information indicate that NMO 1 is used
        -   if pc_GERAN and NOT pc_UTRAN, Cell 24 (only active when stated).
            -   same PLMN like visited PLMN above
            -   RAC-1 (RAC & LAC values chosen by SS)
            -   System information indicate that NMO 1 is used
        UE:
        -   The test USIM contains IMSI-1, GUTI-1 and TAI-1, and EPS update status is "EU1: UPDATED".
        -   The test USIM contains P-TMSI-1 (belonging to RAI-1) and the GPRS update status is "GU1: UPDATED".
        -   The test USIM contains TMSI-1 (belonging to LAI-1) and the update status is "U1: UPDATED".
        Preamble:
        -   The UE is in state Switched OFF (state 1) according to [18]
    */

  var boolean v_TriggerRxd := false;
  var G_LLC_DATAMESSAGE_IND v_LLCDataInd;
  var octetstring v_PLMN := f_GERAN_PLMN_Get(geran_Cell24);
  
  if (pc_GERAN and not pc_UTRA) { // UE supports GERAN but not UTRAN
    f_GERAN_Init(EUTRA_GERAN); // This is still only a 2 PTC test

    f_GERAN_CreateCell (geran_Cell24);
    f_GERAN_Pre_Preamble (geran_Cell24);
    f_GERAN_InterRAT_InitialiseAuthParams();  // The UE starts in EUTRA, so wait for it to send the Auth Params
    f_GERAN_TestBody_Set( true );

    // First Trigger
    //@siclog "Step 1" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);
  
    // Second Trigger
    //@siclog "Step 13a1" siclog@
    // Set Cell 24 to "Serving Cell"
    v_TriggerRxd := f_WaitForIRATCoOrd_Trigger (EUTRA);
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_ServingCell);

    //@siclog "Step 13a2" siclog@
    // Check: Does the UE transmit an ATTACH REQUEST message without P-TMSI, P-TMSI signature, RAI, TMSI
    f_UplinkTBFOnePhase (geran_Cell24);
    alt { // Receive GPRS Attach Request Message
    [] G_LLC.receive(car_G_LLC_UnitData_IND(cr_G_AttachReqWithIMSI(cr_AttachType(?, tsc_I_AttachTypeCombined),
                                                                   f_Imsi2MobileIdentity(px_IMSI_Def),
                                                                   cr_RAI (omit, cr_LAI(omit, v_PLMN, 'FFFE'O), ?),
                                                                   '111'B)))  -> value v_LLCDataInd
      {
        f_GERAN_PreliminaryPass (__FILE__, __LINE__, "Step 13a2");
      }
    }

    //@siclog "Step 14" siclog@
    // Set Cell 24 to "Non Suitable Cell"
    f_GERAN_SetCellPowerLevel (geran_Cell24, tsc_GERAN_NonSuitableCell);

    // Finished here for now
    f_SendIRATCoOrd (EUTRA, cms_IRAT_Trigger);

    // Test case now finished on GERAN side
    f_GERAN_TestBody_Set( false );

    f_GERAN_SS_CellRelease ( geran_Cell24 );

  } // UE doesn't support GERAN, or supports UTRAN too, so do nothing

} // f_TC_9_2_1_2_15_GERAN

} // module NAS_Attach_UG_GERAN
