/*** IOSTS ttt ***
Data:
  Variables: vSlots vNT vLoadAmount vSlotIndex vCurrencySought vSlotsAvailable
    vLastAvailSlot vNewBalMax

  Parameters: pSlotCount pRefCurCount pLogSize pNT_Limit vIssID vCardID
    vDateExp vDeactivated vLocked

  Messages: mTP_Inquiry mCredLoadResp mInitLoadResp
Initial Condition: (((((pSlotCount > 0) and (pSlotCount <= 15)) and ((pRefCurCount >= 0) and (pRefCurCount <= 3))) and ((pLogSize > 0) and (pLogSize < 64))) and true)

  Locations: <Start,Start>:L2P <CepInit,P1>:L2P <CepIFL_LocateSlot,P2>:L2P
    <CepInit,Reject>:Inconclu <CepIFL_LoadPending,P3>:L2P
    <CepCFL_CreditForLoad,P4>:L2P
Initial Location: <Start,Start>:L2P
Alphabet:

  Input Actions: CepReply

  Output Actions: CepCommand

  Internal Actions: tau_CepIFL_InUse tau_CepIFL_NotInUse
 *** IOSTS ttt ***/
process ttt;
var
  vSlots : SlotArray;
  vNT : nat;
  vLoadAmount : nat;
  vSlotIndex : nat;
  vCurrencySought : nat;
  vSlotsAvailable : nat;
  vLastAvailSlot : nat;
  vNewBalMax : nat;
  pSlotCount : nat;
  pRefCurCount : nat;
  pLogSize : nat;
  pNT_Limit : nat;
  vIssID : nat;
  vCardID : nat;
  vDateExp : nat;
  vDeactivated : bool;
  vLocked : bool;
  mTP_Inquiry : CommandType;
  mCredLoadResp : ReplyType;
  mInitLoadResp : ReplyType;
state
<Start,Start>:L2P :init;
<CepInit,P1>:L2P;
<CepIFL_LocateSlot,P2>:L2P;
<CepInit,Reject>:Inconclu;
<CepIFL_LoadPending,P3>:L2P;
<CepCFL_CreditForLoad,P4>:L2P;
transition
from <Start,Start>:L2P
  if (((((pSlotCount > 0) and (pSlotCount <= 15)) and ((pRefCurCount >= 0) and (pRefCurCount <= 3))) and ((pLogSize > 0) and (pLogSize < 64))) and true)
  to <CepInit,P1>:L2P;
from <CepInit,P1>:L2P
  if (((((mTP_Inquiry.Command = LOADINIT) and not (vNT >= pNT_Limit)) and not vDeactivated) and not vLocked) and (((not (vNT >= pNT_Limit) and not vDeactivated) and not vLocked) and (mTP_Inquiry.Command = LOADINIT)))
  sync CepCommand !mTP_Inquiry
  do {
    vLoadAmount:=mTP_Inquiry.LoadAmt|
    vSlotIndex:=0|
    vCurrencySought:=mTP_Inquiry.Currency|
    vSlotsAvailable:=0|
    vLastAvailSlot:=pSlotCount|
    vNewBalMax:=mTP_Inquiry.NewBalMax
  }
  to <CepIFL_LocateSlot,P2>:L2P;
from <CepIFL_LocateSlot,P2>:L2P
  if (((vSlotIndex < pSlotCount) and vSlots[vSlotIndex].InUse) and (vSlots[vSlotIndex].Currency <> vCurrencySought))
  sync tau_CepIFL_InUse
  do {
    vSlotIndex:=(vSlotIndex + 1)
  }
  to <CepIFL_LocateSlot,P2>:L2P;
from <CepIFL_LocateSlot,P2>:L2P
  if ((vSlotIndex < pSlotCount) and not vSlots[vSlotIndex].InUse)
  sync tau_CepIFL_NotInUse
  do {
    vSlotIndex:=(vSlotIndex + 1)|
    vSlotsAvailable:=(vSlotsAvailable + 1)|
    vLastAvailSlot:=vSlotIndex
  }
  to <CepIFL_LocateSlot,P2>:L2P;
from <CepIFL_LoadPending,P3>:L2P
  if ((mTP_Inquiry.Command = LOADCREDIT) and (mTP_Inquiry.Command = LOADCREDIT))
  sync CepCommand !mTP_Inquiry
  to <CepCFL_CreditForLoad,P4>:L2P;
from <CepCFL_CreditForLoad,P4>:L2P
  if ((((((vSlotIndex <= pSlotCount) and not vSlots[vSlotIndex].InUse) and (mCredLoadResp.Balance = vLoadAmount)) and (mCredLoadResp.CompCode = x00)) and (mCredLoadResp.Status = x9000)) 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,P1>:L2P;
from <CepCFL_CreditForLoad,P4>:L2P
  if ((((((vSlotIndex <= pSlotCount) and vSlots[vSlotIndex].InUse) and (mCredLoadResp.Balance = vLoadAmount)) and (mCredLoadResp.CompCode = x00)) and (mCredLoadResp.Status = x9000)) and (mCredLoadResp.Status = x9000))
  sync CepReply ?mCredLoadResp
  do {
    vSlots[vSlotIndex].Balance:=vLoadAmount|
    vSlots[vSlotIndex].BalMax:=vNewBalMax
  }
  to <CepInit,P1>:L2P;
from <CepIFL_LocateSlot,P2>:L2P
  if (((vSlotIndex >= pSlotCount) and (vSlotsAvailable = 0)) and ((mInitLoadResp.Status = x9401) and not (mInitLoadResp.Status = x9000)))
  sync CepReply ?mInitLoadResp
  to <CepInit,Reject>:Inconclu;
from <CepIFL_LocateSlot,P2>:L2P
  if ((((vSlotIndex < pSlotCount) and vSlots[vSlotIndex].InUse) and (vSlots[vSlotIndex].Currency = vCurrencySought)) and ((((vSlots[vSlotIndex].Balance + vLoadAmount) > vSlots[vSlotIndex].BalMax) and (mInitLoadResp.Status = x9402)) and not (mInitLoadResp.Status = x9000)))
  sync CepReply ?mInitLoadResp
  to <CepInit,Reject>:Inconclu;
from <CepIFL_LocateSlot,P2>:L2P
  if (((vSlotIndex >= pSlotCount) and (vSlotsAvailable <> 0)) and ((((((mInitLoadResp.IssId = vIssID) and (mInitLoadResp.CardId = vCardID)) and (mInitLoadResp.DateExp = vDateExp)) and (mInitLoadResp.NT_CEP = vNT)) and (mInitLoadResp.Status = x9000)) and (mInitLoadResp.Status = x9000)))
  sync CepReply ?mInitLoadResp
  do {
    vSlotIndex:=vLastAvailSlot|
    vNT:=(vNT + 1)
  }
  to <CepIFL_LoadPending,P3>:L2P;
from <CepIFL_LocateSlot,P2>:L2P
  if (((((vSlotIndex < pSlotCount) and vSlots[vSlotIndex].InUse) and (vSlots[vSlotIndex].Currency = vCurrencySought)) and ((vSlots[vSlotIndex].Balance + vLoadAmount) <= vSlots[vSlotIndex].BalMax)) and ((((((mInitLoadResp.IssId = vIssID) and (mInitLoadResp.CardId = vCardID)) and (mInitLoadResp.DateExp = vDateExp)) and (mInitLoadResp.NT_CEP = vNT)) and (mInitLoadResp.Status = x9000)) and (mInitLoadResp.Status = x9000)))
  sync CepReply ?mInitLoadResp
  do {
    vNT:=(vNT + 1)
  }
  to <CepIFL_LoadPending,P3>:L2P;