system CEPS_card;

/* CEPS e-purse card and test purposes 
 *
 * This example is based on the Common Electronic Purse Standard (CEPS)
 * e-purse system.  CEPS itself builds on the Europay-MasterCard-VISA (EMV)
 * standard.  Copies of the original documents for both of these can be 
 * found in "~dclarke/CEPS/".  The originals are available from 
 * www.cepsco.com and www.emvco.com on the web.
 *
 * The section numbers given below refer to section numbers in the
 * "cepstechspecv2.2.pdf" document.
 *
 * ---------------------------------------------------------------------------
 *
 * The process CEPScard currently implements the following commands:
 *   Section 8.7.1 CEP Inquiry - Slot Information
 *   Section 8.7.2 CEP Inquiry - Reference Currency
 *   Section 8.7.3 CEP Inquiry - Transaction Logs
 *   Section 13.1 CEP Load - Initialize for Load
 *   Section 13.1 CEP Load - Credit for Load
 *
 * There is a minimal implementation of:
 *   Section 8.5.2 Reset
 *   Section 8.5.3 Application Selection
 */

type
  StatusType = /* the oh-so-user-friendly two-byte command status */
    enum
      x6A83, /* Record not found */

      x9000, /* Normal processing */

      x9101, /* Application is not active */
      x9102, /* Transaction Number (NT_CEP) has reached its limit */
      x9106, /* Application has been deactivated */
      x9110, /* CEP Application is locked */

      x9401, /* Currency specified not available */
      x9402, /* Load amount is too high */
      x9409, /* Currency not found; slot available */
      x940A, /* Currency not found; no slot available */

      x9580  /* Command out of sequence */
    ; /* end enum */

  CompletionCode = /* the oh-so-user-friendly one-byte completion code */
    enum
      x00  /* Normal processing */
    ; /* end enum */

  PowerType = /* Parameters for the Power action */
    enum 
      OFF,    /* The power is being interrupted */
      ON      /* Power is being applied */
    ; /* end enum */

  AidType = /* Parameters for 8.5.3 Application Selection */
    enum 
      CEP,      /* Select the CEP (e-purse) application */
      ERROR_AID /* might be useful someday */
    ; /* end enum */

  FCIType = record       /* Return value from 8.5.3 Application Selection */
    Status : StatusType;
  end;

  CommandCodeType =
    enum 
      NONE ,       /* might be useful someday */

                   /* Commands for 8.7.1 CEP Inquiry - Slot Information */
      SPECIFIC ,   /* search for a specific currency in any slot */
      ALLSLOTS00 , /* initiate a "FOR" loop returning each in-use slot */
      ALLSLOTS01 , /* the "NEXT" operator for loop initiated by ALLSLOTS00 */

                   /* Command for 8.7.2 CEP Inquiry - Reference Currency */
      REFCURR,     /* Return the reference currency/currencies */

                   /* Command for 8.7.3 CEP Inquiry - Transaction Logs */
      LOGINQ00,    /* Most recent transaction data */
      LOGINQ01,    /* Preceding transaction */

		   /* Command for 13 Load Transaction */
      LOADINIT,    /* Initialize for load */
      LOADCREDIT,  /* Credit for load */

      ERROR_INQ    /* might be useful someday */
    ; /* end enum */

  TxTypeType =
    enum
      TxLoad,
      TxUnload,
      TxExchange,
      TxPurchase,
      TxCancelLastPurchase
    ; /* end enum */

  CommandType =
    record  
      Command  : CommandCodeType;

      Currency : nat; /* what currency slot to access */

      TxType   : TxTypeType; /* for inquiries, which log data to return */

      DateTime : nat; /* date and time time-stamp for */
      AcqID    : nat; /* load acquirer ID */
      LdvID    : nat; /* load device ID */
      LoadAmt  : nat; /* load amount */

      ReturnRcep : bool; /* flag, true if R_LSAM in command, return R_CEP */
      UpdateSlot : bool; /* flag, true if slot balance is to be updated */
      UpdateOthr : bool; /* flag, true if "other data" is to be updated */
      CompCode   : CompletionCode;  /* completion code */
      MacPresent : bool; /* Is the S_2 MAC present? */
      Mac_S2     : nat;  /* The S2 MAC */
      R_LSAM     : nat;  /* The R_LSAM for unlinked loads */
      NewBalMax  : nat;  /* New BalMax for a virgin slot */
    end;

  LogEntryType =
    record
      TxType   : TxTypeType; /* Transaction type (load, purchase, etc.) */
      TxDate   : nat;        /* Transaction date/time stamp */
      TxCurr   : nat;        /* Currency ID */
      TxCurr2  : nat;        /* Target currency (exchange) */
      TxAuth   : nat;        /* Authentication method (purchase) */
      TxAcqID  : nat;        /* Acquirer ID */
      TxRID    : nat;        /* RID of PSAM creator (purchase) */
      TxPsamID : nat;        /* Identifier of PSAM creator (purchase) */
      TxLdvID  : nat;        /* Acquirer's load device ID (load/exchange) */
      TxAmt    : nat;        /* Amount */
      TxAmtStep: nat;        /* Amount of last step (purchase) */
      TxNT     : nat;        /* NT_CEP -- the card's transaction number */
      TxBal    : nat;        /* Balance of slot after completion */
      TxBalMax : nat;        /* Maximum balance after completion */
      TxBalOld : nat;        /* Old target balance before tx (exchange) */
      TxBalSrc : nat;        /* Source balance after tx (exchange) */
      TxCC     : StatusType; /* Completion code */
      TxPosLoc : nat;        /* Location data for purchase device (purchase) */
    end;

  ReplyType = 
    record
                       /* Reply data 8.7.1 CEP Inquiry - Slot Information */
      SlotIndex : nat; /* index of physical slot reported */
      Currency  : nat; /* see SlotType */
      Balance   : nat; /* see SlotType */
      BalMax    : nat; /* see SlotType */

                       /* Reply data 8.7.2 CEP Inquiry - Reference Currency */
      Count     : nat; /* number of reference currencies reported */
      RC_Curr_0 : nat; /* currency # for first reference currency */
      RC_Max_0  : nat; /* maximum balance for first reference currency */
      RC_Curr_1 : nat; /* currency # for second reference currency */
      RC_Max_1  : nat; /* maximum balance for second reference currency */
      RC_Curr_2 : nat; /* currency # for third reference currency */
      RC_Max_2  : nat; /* maximum balance for third reference currency */

                       /* Reply data 8.7.3 CEP Inquiry - Transaction Logs */
      Entry     : LogEntryType; /* requested log data */

		       /* Reply data 13.1 CEP Load - Initialize for Load */
      IssId     : nat; /* Issuer ID of CEP application */
      CardId    : nat; /* Card ID */
      DateExp   : nat; /* Expiration Date */
      NT_CEP    : nat; /* Transaction Number */
      S_1       : nat; /* Card MAC */
      H_CEP     : nat; /* SHA-1 hash */

		       /* Reply data 13.1 CEP Load - Credit for Load */
      CompCode  : CompletionCode; /* Transaction completion code */
      S_3       : nat; /* Final MAC from CEP card */
      R_CEP     : nat; /* Proof of no transaction */

      Status    : StatusType;
    end;

  SlotType = 
    record
      InUse    : bool; /* is there a currency assigned to this slot?        */
      Currency : nat;  /* what currency is it?                              */
      Fixed    : bool; /* is the currency for this slot fixed or changable? */
      Balance  : nat;  /* the balance of the slot in currency units         */
      BalMax   : nat;  /* the maximum balance allowed for this slot         */

    
    end;

 
  ReferenceCurrencyType =
    record
      Currency : nat; /* what currency is the reference? */
      BalMax   : nat; /* the maximum balance for this currency */
    end;

  LogArray = array [ 0 .. 63 ] of LogEntryType;

  TransactionLogType =
    record
      pLogSize : nat;   /* The total number of log slots available */
      InUse : nat;      /* The number of slots currently in use */
      NextInsert : nat; /* The next slot to use to log a transaction */
      Entry : LogArray; /* The array of slots */
    end;

  /* Array of slots, the basic slot array for the card.  Constant size 16
   * is hard-coded for convenience.  The actual number of physical slots
   * present in the card is determined by the pSlotCount parameter.
   * Of course it should hold that 0 < pSlotCount <= 16
   */

  SlotArray = array [ 0 .. 15 ] of SlotType;
  SlotsReported = array[0..15] of bool;
  ReportArrayType = array[0..256] of ReplyType;

   
  /* Array of reference currencies for the card.  Constant size 3
   * is hard-coded for convenience.  The actual number of reference
   * currencies supported by the card is determined by the pRefCurCount
   * parameter.  It should hold that 0 <= pRefCurCount <= 3.
   */

  ReferenceCurrencyArray = array [ 0 .. 2 ] of ReferenceCurrencyType;

signal
  DUMMY(bool); /* not used in model; makes the warnings disappear */

gate
  Perso(nat,nat,nat);
  SetRefCur(nat,nat,nat);

  Power(PowerType); /* Apply/Interrupt power action */

  Reset(bool); /* Reset action of Section 8.5.2 */
  ATR(bool);   /* Reply to reset action */

  Select(AidType);      /* Select action of Section 8.5.3 */
  SelectReply(FCIType); /* Reply to selection action */

  CepCommand(CommandType); /* Generic CEP command interface */
  CepReply(ReplyType);     /* Generic CEP reply interface   */

  /* internal actions */

  tau_CepSIS_NotFound; /* looping during specific slot info query */
  tau_CepSIS_InUse;
  tau_CepSIS_NotInUse;
  tau_CepSIS_Found;

  tau_CepSIQ_InUse;    /* looping during FOR/NEXT slot info query */
  tau_CepSIQ_NotInUse;
  tau_CepSIQ_Complete;

  tau_CepTLI_Exhausted;
  tau_CepTLI_SkipLogEntry;
  tau_CepTLI_ReportLogEntry;

  tau_CepIFL_NotFound;
  tau_CepIFL_InUse;
  tau_CepIFL_NotInUse;
  tau_CepIFL_Found;
  tau_CepIFL_LoadAmtOK;
  tau_CepIFL_LoadAmtNotChecked;
	
buffer
  dummy: queue of DUMMY; /* not used in model; makes the warnings disappear */

process CEPScard;

var
  /* "physical" paramters of the card */

  pSlotCount   : nat;     /* Number of slots in card (hardware parameter) */
  pRefCurCount : nat;     /* Number of reference currencies */
  pLogSize     : nat;     /* Number of slots in transaction log (hdwr parm) */
  pNT_Limit    : nat;     /* Limit value of vNT; tx forbidden here and above */

  /* Parameters of the card and CEP application */

  vIssID       : nat;     /* Issuer ID of CEP application */
  vCardID      : nat;     /* Card identifier */
  vDateExp     : nat;     /* Expiration date */

  /* the static storage of the card */

  vSlots       : SlotArray;              /* The array of slot data */
  slotsReported : SlotsReported;
  vRefCur      : ReferenceCurrencyArray; /* the array of refrnce currencies */

  vTxLog_pLogSize : nat;
      vTxLog_InUse : nat;
      vTxLog_NextInsert : nat;

   vTxLog_Entry : LogArray;
      /* the transaction log */
   vNT          : nat;                    /* transaction sequence number */
  vDeactivated : bool;                   /* Application is deactived */
  vLocked      : bool;                   /* Application is locked */
  vLoadAmount  : nat;                    /* Load amount from load request */

  /* Working storage -- variables */

  vSlotIndex      : nat; /* generic index for indexing slots */
  vCurrencySought : nat; /* place of recording which currency we search */
  vSlotsAvailable : nat; /* count of non-InUse slots found during search */
  vSlotsReported  : nat; /* count of slots reported in non-specific inquiry */
  vLastAvailSlot  : nat; /* pointer to an available slot */

  vLogInqActive   : bool;       /* is a log inquiry active? */
  vLogIndex       : nat;        /* index into log for inquiry sequence */
  vLastInqType    : TxTypeType; /* type of data checked by last log inquiry */
  vNewBalMax      : nat;        /* new BalMax sent with a credit-for-load */

  
 reportSize : nat;
 report : ReportArrayType;  
 
  /* Messages */

  mPowerValue   : PowerType;
  mAID          : AidType;
  mInquiry: CommandType;
  mSlotInfo     : ReplyType;
  mFCI          : FCIType;
  mTxLogInfo    : ReplyType;
  mInitLoadResp : ReplyType;
  mCredLoadResp : ReplyType;

  mIssID       : nat;
  mCardID      : nat;
  mDateExp     : nat;

  mRefCurIndex    : nat;
  mRefCurCurrency : nat;
  mRefCurBalMax   : nat;

state
  Start : init;
  PrePerso;
  PowerOff;

  Init;
  PerformReset0;
  InitAndReset;
  NoAppSelected;
  SelectCepReply;

  CepInit;
  CepCommandOutOfSequence;

  CepSlotInquirySpecific;
  CepSIS_Found;
  CepSIS_NotFound;

  CepSlotInquirySequence;
  CepSIQ_Reply;
  CepSIQ_Ready;

  CepReferenceCurrencyInquiry;

  CepTLI_SendLogEntry;
  CepTLI_ReportLogEntry;
  CepTLI_Exhausted;

  CepIFL_NTExhausted;
  CepIFL_CepDeactivated;
  CepIFL_CepLocked;
  CepIFL_NotFoundNoneAvailable;
  CepIFL_NotFoundSlotAvailable;
  CepIFL_LocateSlot;
  CepIFL_Found;
  CepIFL_InitForLoad;
  CepIFL_LoadPending;
  CepCFL_CreditForLoad;

  AllMacro;

transition
  from Start
    if ((pSlotCount > 0) and (pSlotCount <= 15)) and
       ((pRefCurCount >= 0) and (pRefCurCount <= 3)) and
       ((pLogSize > 0) and (pLogSize < 64))
  to PowerOff;

  from PowerOff
    if (mPowerValue = ON)
    sync Power?(mPowerValue)
  to Init;

  from Init
    sync Reset?(any)
  to PerformReset0;

  from PerformReset0
    sync ATR!(any)
  to InitAndReset;

  from InitAndReset
    if (mInquiry.Command = LOADINIT)
    sync CepCommand?(mInquiry)
  to NoAppSelected;

  from NoAppSelected
    if (mInitLoadResp.Status = x9101)
    sync CepReply!(mInitLoadResp)
  to InitAndReset;

  from InitAndReset
    if (mAID = CEP)
    sync Select?(mAID)
  to SelectCepReply;

  from SelectCepReply
    if (mFCI.Status = x9000)
    sync SelectReply!(mFCI)
    do
      vLogInqActive := false
  to CepInit;

  from CepInit
    if (mInquiry.Command = SPECIFIC)
    sync CepCommand?(mInquiry)
    do {
      vSlotIndex := 0 |
      vCurrencySought := mInquiry.Currency |
      vSlotsAvailable := 0
    }
  to CepSlotInquirySpecific;

  from CepSlotInquirySpecific
    if (vSlotIndex >= pSlotCount)
    sync tau_CepSIS_NotFound
  to CepSIS_NotFound;

  from CepSlotInquirySpecific
    if (vSlotIndex < pSlotCount) and
       (vSlots[vSlotIndex].InUse) and
       (vSlots[vSlotIndex].Currency <> vCurrencySought)
    sync tau_CepSIS_NotInUse
    do
      vSlotIndex := vSlotIndex + 1
  to CepSlotInquirySpecific;

  from CepSlotInquirySpecific
    if (    vSlotIndex < pSlotCount) and
       (not vSlots[vSlotIndex].InUse)
    sync tau_CepSIS_InUse
    do {
      vSlotIndex := vSlotIndex + 1 |
      vSlotsAvailable := vSlotsAvailable + 1
    }
  to CepSlotInquirySpecific;

  from CepSlotInquirySpecific
    if (vSlotIndex < pSlotCount) and
       (vSlots[vSlotIndex].InUse) and
       (vSlots[vSlotIndex].Currency = vCurrencySought)
    sync tau_CepSIS_Found
  to CepSIS_Found;

  from CepSIS_Found
    if (mSlotInfo.SlotIndex  =        vSlotIndex          ) and
       (mSlotInfo.Currency   = vSlots[vSlotIndex].Currency) and
       (mSlotInfo.Balance    = vSlots[vSlotIndex].Balance ) and
       (mSlotInfo.BalMax     = vSlots[vSlotIndex].BalMax  ) and
       (mSlotInfo.Status = x9000)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepSIS_NotFound
    if (vSlotsAvailable > 0) and (mSlotInfo.Status = x9409)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepSIS_NotFound
    if (vSlotsAvailable = 0) and (mSlotInfo.Status = x940A)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepInit
    if (mInquiry.Command = ALLSLOTS01)
    sync CepCommand?(mInquiry)
  to CepCommandOutOfSequence;

  from CepCommandOutOfSequence
    if (mSlotInfo.Status = x9580)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepInit
    if (mInquiry.Command = ALLSLOTS00)
    sync CepCommand?(mInquiry)
    do {
      vSlotIndex := 0 |
      vSlotsReported := 0 |
      reportSize := 0
    }
  to CepSlotInquirySequence;

  from CepSlotInquirySequence
    if ((vSlotIndex < pSlotCount) and
	(vSlots[vSlotIndex].InUse))
    sync tau_CepSIQ_InUse
    do {
      slotsReported[vSlotIndex] := false |
      vSlotIndex := vSlotIndex + 1
    }
  to CepSlotInquirySequence;

  from CepSlotInquirySequence
    if ((    vSlotIndex < pSlotCount) and
	(not vSlots[vSlotIndex].InUse))
    sync tau_CepSIQ_NotInUse
    do {
      slotsReported[vSlotIndex] := true |
      vSlotIndex := vSlotIndex + 1 |
      vSlotsReported := vSlotsReported + 1
    }
  to CepSlotInquirySequence;

  from CepSlotInquirySequence
    if (vSlotIndex = pSlotCount)
    sync tau_CepSIQ_Complete
  to CepSIQ_Reply;

  from CepSIQ_Reply
    if (vSlotsReported >= pSlotCount) and (mSlotInfo.Status = x6A83)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepSIQ_Reply
    if (vSlotsReported < pSlotCount) and
       ((mSlotInfo.SlotIndex >= 0) and 
        (mSlotInfo.SlotIndex <  pSlotCount)) and
       (not slotsReported[mSlotInfo.SlotIndex] ) and
       (    vSlots[mSlotInfo.SlotIndex].InUse) and
       (mSlotInfo.Currency = vSlots[mSlotInfo.SlotIndex].Currency) and
       (mSlotInfo.Balance  = vSlots[mSlotInfo.SlotIndex].Balance ) and
       (mSlotInfo.BalMax   = vSlots[mSlotInfo.SlotIndex].BalMax  ) and
       (mSlotInfo.Status = x9000) and (reportSize < 15)
    sync CepReply!(mSlotInfo)
    do {
     slotsReported[mSlotInfo.SlotIndex] := true |
     vSlotsReported := vSlotsReported + 1 |
     reportSize := reportSize+1|
     report[reportSize].Currency:= vSlots[mSlotInfo.SlotIndex].Currency|
     report[reportSize].Balance := vSlots[mSlotInfo.SlotIndex].Balance|
     report[reportSize].Status := x9000
    }
  to CepSIQ_Ready;

  from CepSIQ_Ready
    if (mInquiry.Command <> ALLSLOTS00) and
       (mInquiry.Command <> ALLSLOTS01)
    sync CepCommand?(mInquiry)
  to CepCommandOutOfSequence;

  from CepSIQ_Ready
    if (mInquiry.Command = ALLSLOTS00)
    sync CepCommand?(mInquiry)
    do {
      vSlotsReported := 0 |
      vSlotIndex := 0
    }
  to CepSlotInquirySequence;

  from CepSIQ_Ready
    if (mInquiry.Command = ALLSLOTS01)
    sync CepCommand?(mInquiry)
  to CepSIQ_Reply;

  from CepInit
    if (mInquiry.Command = REFCURR)
    sync CepCommand?(mInquiry)
  to CepReferenceCurrencyInquiry;

  from CepReferenceCurrencyInquiry
    if (pRefCurCount = 0) and (mSlotInfo.Status = x9401)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepReferenceCurrencyInquiry
    if (pRefCurCount = 1) and
       (mSlotInfo.Count = 1) and
       (mSlotInfo.RC_Curr_0 = vRefCur[0].Currency) and
       (mSlotInfo.RC_Max_0  = vRefCur[0].BalMax) and
       (mSlotInfo.Status = x9000)
    sync CepReply!(mSlotInfo)
  to CepInit;
  
  from CepReferenceCurrencyInquiry
    if (pRefCurCount = 2) and
       (mSlotInfo.Count = 2) and
       (mSlotInfo.RC_Curr_0 = vRefCur[0].Currency) and
       (mSlotInfo.RC_Max_0  = vRefCur[0].BalMax) and
       (mSlotInfo.RC_Curr_1 = vRefCur[1].Currency) and
       (mSlotInfo.RC_Max_1  = vRefCur[1].BalMax) and
       (mSlotInfo.Status = x9000)
    sync CepReply!(mSlotInfo)
  to CepInit;
  
  from CepReferenceCurrencyInquiry
    if (pRefCurCount = 3) and
       (mSlotInfo.Count = 3) and
       (mSlotInfo.RC_Curr_0 = vRefCur[0].Currency) and
       (mSlotInfo.RC_Max_0  = vRefCur[0].BalMax) and
       (mSlotInfo.RC_Curr_1 = vRefCur[1].Currency) and
       (mSlotInfo.RC_Max_1  = vRefCur[1].BalMax) and
       (mSlotInfo.RC_Curr_2 = vRefCur[2].Currency) and
       (mSlotInfo.RC_Max_2  = vRefCur[2].BalMax) and
       (mSlotInfo.Status = x9000)
    sync CepReply!(mSlotInfo)
  to CepInit;

  from CepInit
    if (mInquiry.Command = LOGINQ01) and (not vLogInqActive)
    sync CepCommand?(mInquiry)
  to CepCommandOutOfSequence;

  

  from CepInit
    if (mInquiry.Command = LOGINQ00)
    sync CepCommand?(mInquiry)
    do {
      vLogIndex := 1 |
      vLogInqActive := true |
      vLastInqType := mInquiry.TxType
    }
  to CepTLI_SendLogEntry;

  from CepInit
    if ((mInquiry.Command = LOGINQ01) and 
	(vLogInqActive) and
	(mInquiry.TxType = vLastInqType))
    sync CepCommand?(mInquiry)
    do {
      vLogIndex := 1 |
      vLogInqActive := true |
      vLastInqType := mInquiry.TxType
    }
  to CepTLI_SendLogEntry;

  from CepInit
    if ((mInquiry.Command = LOGINQ01) and 
	(vLogInqActive) and
	(mInquiry.TxType <> vLastInqType))
    sync CepCommand?(mInquiry)
    do
      vLogInqActive := false
  to CepCommandOutOfSequence;

  from CepTLI_SendLogEntry
    if (vLogIndex > vTxLog_InUse)
    sync tau_CepTLI_Exhausted
  to CepTLI_Exhausted;

  from CepTLI_SendLogEntry
    if ((vLogIndex <= vTxLog_InUse) and
	(((vLastInqType = TxLoad) and 
	  ((vTxLog_Entry[vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex) % vTxLog_pLogSize].TxType
	    <> TxLoad) and
	   (vTxLog_Entry[vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex) % vTxLog_pLogSize].TxType
	    <> TxUnload))) or
	 ((vLastInqType = TxExchange) and 
	  ((vTxLog_Entry[vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex) % vTxLog_pLogSize].TxType
	    <> TxExchange))) or
	 ((vLastInqType = TxPurchase) and 
	  ((vTxLog_Entry[vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex) % vTxLog_pLogSize].TxType
	    <> TxPurchase) and
	   (vTxLog_Entry[vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex) % vTxLog_pLogSize].TxType
	    <> TxCancelLastPurchase)))
        ))
    sync tau_CepTLI_SkipLogEntry
    do
      vLogIndex := vLogIndex + 1
  to CepTLI_SendLogEntry;

  from CepTLI_SendLogEntry
    if ((vLogIndex <= vTxLog_InUse) and
	(((vLastInqType = TxLoad) and 
	  ((vTxLog_Entry[(vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex)) % vTxLog_pLogSize].TxType
	    = TxLoad) or
	   (vTxLog_Entry[(vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex)) % vTxLog_pLogSize].TxType
	    = TxUnload))) or
	 ((vLastInqType = TxExchange) and 
	  ((vTxLog_Entry[(vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex)) % vTxLog_pLogSize].TxType
	    = TxExchange))) or
	 ((vLastInqType = TxPurchase) and 
	  ((vTxLog_Entry[(vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex)) % vTxLog_pLogSize].TxType
	    = TxPurchase) or
	   (vTxLog_Entry[(vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex)) % vTxLog_pLogSize].TxType
	    = TxCancelLastPurchase)))
        ))
    sync tau_CepTLI_ReportLogEntry
  to CepTLI_ReportLogEntry;

  from CepTLI_ReportLogEntry
    if (mTxLogInfo.Entry = 
	vTxLog_Entry[vTxLog_NextInsert+(vTxLog_pLogSize-vLogIndex)]) and
       (mTxLogInfo.Status = x9000)
    sync CepReply!(mTxLogInfo)
  to CepInit;

  from CepTLI_Exhausted
    if (mTxLogInfo.Status = x6A83)
    sync CepReply!(mTxLogInfo)
    do
      vLogInqActive := false
  to CepInit;

  from CepInit
    if (mInquiry.Command = LOADINIT) and
       (vNT >= pNT_Limit) and
       (not vDeactivated) and
       (not vLocked)
    sync CepCommand?(mInquiry)
  to CepIFL_NTExhausted;

  from CepIFL_NTExhausted
    if (mInitLoadResp.Status = x9102)
    sync CepReply!(mInitLoadResp)
  to CepInit;

  from CepInit
    if (mInquiry.Command = LOADINIT) and
       (vDeactivated)
    sync CepCommand?(mInquiry)
  to CepIFL_CepDeactivated;

  from CepIFL_CepDeactivated
    if (mInitLoadResp.Status = x9106)
    sync CepReply!(mInitLoadResp)
  to CepInit;

  from CepInit
    if (mInquiry.Command = LOADINIT) and
       (not vDeactivated) and
       (vLocked)
    sync CepCommand?(mInquiry)
  to CepIFL_CepLocked;

  from CepIFL_CepLocked
    if (mInitLoadResp.Status = x9110)
    sync CepReply!(mInitLoadResp)
  to CepInit;

  from CepInit
    if (mInquiry.Command = LOADINIT) and
       (not (vNT >= pNT_Limit)) and
       (not vDeactivated) and
       (not vLocked)
    sync CepCommand?(mInquiry)

    do {
      vLoadAmount := mInquiry.LoadAmt |

      vSlotIndex := 0 |
      vCurrencySought := mInquiry.Currency |
      vSlotsAvailable := 0 |
      vLastAvailSlot := pSlotCount |
      vNewBalMax := mInquiry.NewBalMax

   
    }
  to CepIFL_LocateSlot;

  from CepIFL_LocateSlot
    if (vSlotIndex >= pSlotCount) and (vSlotsAvailable = 0)
    sync tau_CepIFL_NotFound
  to CepIFL_NotFoundNoneAvailable;

  from CepIFL_LocateSlot
    if (vSlotIndex >= pSlotCount) and (vSlotsAvailable <> 0)
    sync tau_CepIFL_NotFound
    do
      vSlotIndex := vLastAvailSlot
  to CepIFL_NotFoundSlotAvailable;

  from CepIFL_LocateSlot
    if (vSlotIndex < pSlotCount) and
       (vSlots[vSlotIndex].InUse) and
       (vSlots[vSlotIndex].Currency <> vCurrencySought)
    sync tau_CepIFL_InUse
    do
      vSlotIndex := vSlotIndex + 1
  to CepIFL_LocateSlot;

  from CepIFL_LocateSlot
    if (    vSlotIndex < pSlotCount) and
       (not vSlots[vSlotIndex].InUse)
    sync tau_CepIFL_NotInUse
    do {
      vSlotIndex := vSlotIndex + 1 |
      vSlotsAvailable := vSlotsAvailable + 1 |
      vLastAvailSlot := vSlotIndex
    }
  to CepIFL_LocateSlot;

  from CepIFL_LocateSlot
    if (vSlotIndex < pSlotCount) and
       (vSlots[vSlotIndex].InUse) and
       (vSlots[vSlotIndex].Currency = vCurrencySought)
    sync tau_CepIFL_Found
  to CepIFL_Found;

  from CepIFL_NotFoundNoneAvailable
    if (mInitLoadResp.Status = x9401)
    sync CepReply!(mInitLoadResp)
  to CepInit;

  from CepIFL_Found
    if (vSlots[vSlotIndex].Balance + vLoadAmount > 
        vSlots[vSlotIndex].BalMax) and
       (mInitLoadResp.Status = x9402)
    sync CepReply!(mInitLoadResp)
  to CepInit;

  from CepIFL_Found
    if (vSlots[vSlotIndex].Balance + vLoadAmount <= 
        vSlots[vSlotIndex].BalMax)
    sync tau_CepIFL_LoadAmtOK
  to CepIFL_InitForLoad;

  from CepIFL_NotFoundSlotAvailable
    sync tau_CepIFL_LoadAmtNotChecked
  to CepIFL_InitForLoad;

  from CepIFL_InitForLoad
    if (mInitLoadResp.IssId = vIssID) and
       (mInitLoadResp.CardId = vCardID) and
       (mInitLoadResp.DateExp = vDateExp) and
       (mInitLoadResp.NT_CEP = vNT) and
       (mInitLoadResp.Status = x9000)
    sync CepReply!(mInitLoadResp)
    do
      vNT := vNT + 1
  to CepIFL_LoadPending;

  from CepInit
    if (mInquiry.Command = LOADCREDIT)
    sync CepCommand?(mInquiry)
  to CepCommandOutOfSequence;

  from CepIFL_LoadPending
    if (mInquiry.Command <> LOADCREDIT)
    sync CepCommand?(mInquiry)
  to CepCommandOutOfSequence;


  from CepIFL_LoadPending
    if (mInquiry.Command = LOADCREDIT)
    sync CepCommand?(mInquiry)
  to CepCFL_CreditForLoad;

  from CepCFL_CreditForLoad
    if (not vSlots[vSlotIndex].InUse) and
       (mCredLoadResp.Balance = vLoadAmount) and
       (mCredLoadResp.CompCode = x00) and
       (mCredLoadResp.Status = x9000)
    sync CepReply!(mCredLoadResp)
    do {
      vSlots[vSlotIndex].InUse    := true |
      vSlots[vSlotIndex].Currency := vCurrencySought |
      vSlots[vSlotIndex].Fixed    := false |
      vSlots[vSlotIndex].Balance  := vLoadAmount |
      vSlots[vSlotIndex].BalMax   := vNewBalMax
    }
  to CepInit;

  
  from CepCFL_CreditForLoad
    if (vSlots[vSlotIndex].InUse) and
       (mCredLoadResp.Balance = vLoadAmount) and
       (mCredLoadResp.CompCode = x00) and
       (mCredLoadResp.Status = x9000)
    sync CepReply!(mCredLoadResp)
   do{
      vSlots[vSlotIndex].Balance  := vLoadAmount |
      vSlots[vSlotIndex].BalMax   := vNewBalMax
    }
  to CepInit;


  /*from PrePerso
    sync Perso?(mIssID)?(mCardID)?(mDateExp)
    do {
      vDeactivated := false |
      vLocked := false |
      vTxLog_pLogSize := pLogSize |
      vTxLog_InUse := 0 |
      vTxLog_NextInsert := 0 |

      vIssID := mIssID |
      vCardID := mCardID |
      vDateExp := mDateExp
    }
  to PowerOff;

  from PrePerso
    if (mRefCurIndex < pRefCurCount)
    sync SetRefCur?(mRefCurIndex)?(mRefCurCurrency)?(mRefCurBalMax)
    do {
      vRefCur[mRefCurIndex].Currency := mRefCurCurrency |
      vRefCur[mRefCurIndex].BalMax   := mRefCurBalMax
    }
  to PrePerso;*/

  /*  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  -  */

  from AllMacro
    if (mPowerValue = OFF)
    sync Power?(mPowerValue)
  to PowerOff;

  /* --------------------------------------------------------------------- */
  /* End of process CEPScard                                               */
  /* --------------------------------------------------------------------- */

process TestPurpose_SIQ;


var
    vSlotsReported:nat;
    pSlotCount : nat;
    
  mTP_Inquiry1    : CommandType;
  mTP_SlotInfo   : ReplyType;
  mTP_PowerValue : PowerType;
 
state
  Start:init;
  P1;P2;
  Accept;Reject;
  AllMacro;

transition
  from Start
  to P1;

  

  from P1
       if (mTP_Inquiry1.Command = NONE) 
      sync  CepCommand?(mTP_Inquiry1)
  to Accept;

  from P1
    if (mTP_Inquiry1.Command = ALLSLOTS00)
    sync CepCommand?(mTP_Inquiry1)
  to P2;

  from P2
    if (mTP_Inquiry1.Command = ALLSLOTS01)
    sync CepCommand?(mTP_Inquiry1)
  to P2;

  from P2  
   if (vSlotsReported < pSlotCount)
     sync CepReply!(mTP_SlotInfo)
     to P2;

  from P2
    if (vSlotsReported >= pSlotCount)
    sync CepReply!(mTP_SlotInfo)
  to P1;

  

  from AllMacro
    if (mTP_PowerValue = OFF)
    sync Power?(mTP_PowerValue)
  to Reject; 

    
/* end process TestPurpose_SIQ */




process TestPurpose_LOAD;

var
vDeactivated, vLocked: bool;
vNT : nat;
pNT_Limit: nat;

/*messages */

mTP_PowerValue: PowerType;
mTP_Inquiry: CommandType;
mTP_InitLoadResp,mTP_InitCreditResp :ReplyType;
mTP_Select: AidType;
state Start: init; P0; P1; P2; P3; P4; Accept; Reject; AllMacro;


transition
  from Start
  to P1;

  
  from P1
    if(mTP_Inquiry.Command = NONE)
    sync CepCommand?(mTP_Inquiry)
  to Accept;

  from P1
    if (not (vNT >= pNT_Limit) and not (vDeactivated) and not(vLocked)
     and (mTP_Inquiry.Command = LOADINIT))
    sync CepCommand?(mTP_Inquiry)
  to P2;


  from P2  
    if(mTP_InitLoadResp.Status = x9000)
    sync CepReply!(mTP_InitLoadResp)
  to P3;
 
  from P3
    if (mTP_Inquiry.Command = LOADCREDIT)
    sync CepCommand?(mTP_Inquiry)
  to P4;

 from P4  
   if(mTP_InitCreditResp.Status = x9000)
    sync CepReply!(mTP_InitCreditResp)
  to P1;


  from AllMacro
    if (mTP_PowerValue = OFF)
    sync Power?(mTP_PowerValue)
  to Reject; 

/* end process TestPurpose_LOAD */





  /* lines that begin with "/*stg>" are fed to the STG command line parser */

/*stg> CEPScard := if2iosts(CEPScard);
/*stg> s  := if2iosts(CEPScard);

/* test of request for all currencies in sequence */


/*stg> tp := if2iosts(TestPurpose_LOAD);
/*stg> tp':= complete(tp,s);
/*stg> p  := s*tp';
-- /*stg> p' := close(p);
/*stg> p' := p;
/*stg> t := select(p');
/*stg> tt := simplify(t);
*/