/*** IOSTS ttt ***
Data:
  Variables: slotsReported vSlotIndex vSlotsReported reportSize report

  Parameters: vSlots pSlotCount pRefCurCount pLogSize

  Messages: mTP_Inquiry1 mSlotInfo
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 <CepSlotInquirySequence,P2>:L2P
    <CepSIQ_Reply,P2>:L2P <CepSIQ_Ready,P2>:L2P
Initial Location: <Start,Start>:L2P
Alphabet:

  Input Actions: CepReply

  Output Actions: CepCommand

  Internal Actions: tau_CepSIQ_InUse tau_CepSIQ_NotInUse tau_CepSIQ_Complete
 *** IOSTS ttt ***/
process ttt;
var
  slotsReported : SlotsReported;
  vSlotIndex : nat;
  vSlotsReported : nat;
  reportSize : nat;
  report : ReportArrayType;
  vSlots : SlotArray;
  pSlotCount : nat;
  pRefCurCount : nat;
  pLogSize : nat;
  mTP_Inquiry1 : CommandType;
  mSlotInfo : ReplyType;
state
<Start,Start>:L2P :init;
<CepInit,P1>:L2P;
<CepSlotInquirySequence,P2>:L2P;
<CepSIQ_Reply,P2>:L2P;
<CepSIQ_Ready,P2>: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_Inquiry1.Command = ALLSLOTS00) and (mTP_Inquiry1.Command = ALLSLOTS00))
  sync CepCommand !mTP_Inquiry1
  do {
    vSlotIndex:=0|
    vSlotsReported:=0|
    reportSize:=0
  }
  to <CepSlotInquirySequence,P2>:L2P;
from <CepSlotInquirySequence,P2>:L2P
  if ((vSlotIndex < pSlotCount) and vSlots[vSlotIndex].InUse)
  sync tau_CepSIQ_InUse
  do {
    slotsReported[vSlotIndex]:=false|
    vSlotIndex:=(vSlotIndex + 1)
  }
  to <CepSlotInquirySequence,P2>:L2P;
from <CepSlotInquirySequence,P2>:L2P
  if ((vSlotIndex < pSlotCount) and not vSlots[vSlotIndex].InUse)
  sync tau_CepSIQ_NotInUse
  do {
    slotsReported[vSlotIndex]:=true|
    vSlotIndex:=(vSlotIndex + 1)|
    vSlotsReported:=(vSlotsReported + 1)
  }
  to <CepSlotInquirySequence,P2>:L2P;
from <CepSlotInquirySequence,P2>:L2P
  if (vSlotIndex = pSlotCount)
  sync tau_CepSIQ_Complete
  to <CepSIQ_Reply,P2>:L2P;
from <CepSIQ_Reply,P2>:L2P
  if (((vSlotsReported >= pSlotCount) and (mSlotInfo.Status = x6A83)) and (vSlotsReported >= pSlotCount))
  sync CepReply ?mSlotInfo
  to <CepInit,P1>:L2P;
from <CepSIQ_Reply,P2>:L2P
  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)) and (vSlotsReported < pSlotCount))
  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,P2>:L2P;
from <CepSIQ_Ready,P2>:L2P
  if ((mTP_Inquiry1.Command = ALLSLOTS01) and (mTP_Inquiry1.Command = ALLSLOTS01))
  sync CepCommand !mTP_Inquiry1
  to <CepSIQ_Reply,P2>:L2P;