------------------------ MODULE ConnectedTimingMC ------------------------
EXTENDS ItemTimingMC,CompositionOracle
                                                                           
                                                                              
IntegrationActionPointsT11 == INSTANCE ObjectRuntime WITH s <- qT11.actionPointWorld,CardData <- EmptyT11,InitialState <- EmptyT11,
 Commands <- NoItemInspectionCostCommandsT11,CardOverride <- NoItemInspectionCostOverrideT11,CheckpointOverrideAllowed <- NoItemInspectionCheckpointOverrideT11
ITraversalCallerT11(action) == <<"BasicTraversalAction",action.id>>
IInspectionCallerT11(traversal) == <<"TraversalInspectionInstruction",traversal.id,"ProcedureCoded75d879e00ff">>
IBT11(q) == q.control.siteInspections[20]
IAT11(q) == q.control.itemInspections[77]
IWithInspectionT11(q,b) == [q EXCEPT !.control.siteInspections=[id \in {20} |-> b]]
IWithItemInspectionT11(q,a) == [q EXCEPT !.control.itemInspections=[id \in {77} |-> a]]
IFlowT11 == [OpenSideBProcedure5(TraversalTurnT11("SideB")) EXCEPT !.step="ProcedureCode989abc27e0c6"]
ILayoutT11 == TraversalLayoutT11(0)
IActionPointWorldT11 == [turn |-> "SideB",actionPoints |-> [SideA |-> 0,SideB |-> IntegrationOracleStartActionPoints11],spent |-> ZeroCountsT11,checkpointDue |-> FALSE,event |-> "NoValue"]
IActionPointCommandT11 == [player |-> "SideB",amount |-> BasicAction5("SideB","SchemaAtom138").actionPoints,mode |-> "Spend",announced |-> TRUE]
IActionPointAfterT11(w) == [w EXCEPT !.actionPoints["SideB"]=@-1,!.spent["SideB"]=@+1,!.checkpointDue=TRUE,!.event="SpendActionPoints"]
IInitialT11 ==
 [flow |-> IFlowT11,actionPointWorld |-> IActionPointWorldT11,action |-> SideBIdleActionT11,waitTraversal |-> EmptyT11,control |-> TraversalControlT11(NoTraversal6),objects |-> ItemInspectionObjectsT11("SideAHand","Plan"),
  layout |-> ILayoutT11,movement |-> EmptyT11,encounter |-> EmptyT11,capacity |-> EmptyT11,itemInspectionHistory |-> EmptyT11,stack |-> <<>>,usedWindows |-> {},nextWindow |-> 1,
  stage |-> "LatchStart",resume |-> "NoValue",windowRole |-> "NoValue",windowResume |-> "NoValue",NeutralValue00003 |-> EmptyT11,payment |-> EmptyT11,costDrained |-> FALSE,
  fund |-> 0,bank |-> 0,siteInspectionDecision |-> "NoValue",trace |-> <<>>,rawEvents |-> <<>>,drains |-> <<>>,lastWork |-> "NoValue",revision |-> 0,
  receipts |-> EmptyT11,consumed |-> {},returnOrder |-> <<>>,windowHistory |-> <<>>,done |-> FALSE]
IObserveEventT11(e) ==
 CASE e.tag="ApproachTargetSite" -> "ApproachesTargetSiteCentralA" [] e.tag="SuccessfulTraversal" -> "TraversalSuccessful" [] e.tag="InspectionTargetSite" -> "InspectionBeginsCentralA"
   [] e.tag="ItemInspectionCard" -> "CardItemInspectioned" [] e.tag="PassBarrier" -> "BarrierPassed" [] e.tag="PassAllBarrier" -> "AllBarrierPassed"
   [] e.tag="UnsuccessfulTraversal" -> "TraversalUnsuccessful" [] OTHER -> e.tag
IRecordT11(q,label,events,resume) == [q EXCEPT !.trace=Append(@,label),!.rawEvents=Append(@,events),!.lastWork=label,!.stage="Drain",!.resume=resume,!.revision=@+1]
IOpeningT11(id,kind,site) == [tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> kind,site |-> site,members |-> {},instances |-> EmptyT11,group |-> 0,beginning |-> NoTimingRef9,instruction |-> [id |-> 0],effectRevision |-> 0]
ITurnSiteT11(q) == TurnPrioritySite9(q.flow.turn,q.flow.step,4000,q.actionPointWorld.actionPoints["SideB"],q.flow)
ITraversalSiteT11(q) == TraversalPrioritySite9(q.flow.turn,q.control.traversal,EmptyT11,q.layout,q.control)
IActionOptionT11 == PriorityOption9(30,"NeutralValue00001","SideB",0,0,RuleAbilitySource9("BasicTraversal"),0,{TimingRef9("SchemaAtom138",7)})
IActionReservationT11(q) ==
 /\ Len(q.stack)=1 /\ q.NeutralValue00003.ready=PriorityReadyT11(q.NeutralValue00003.opened)
 /\ q.NeutralValue00003.ready.site=[ITurnSiteT11(q) EXCEPT !.actionPoints=q.NeutralValue00003.opened.site.actionPoints] /\ q.NeutralValue00003.ready.kind="NeutralValue00001"
 /\ WindowTop9(q.stack)=StartPriorityOptionFrame9(q.NeutralValue00003.ready,IActionOptionT11,200)
 /\ q.NeutralValue00003.option=IActionOptionT11
IActionPaidT11(q) ==
 /\ IActionReservationT11(q) /\ q.payment.before=IActionPointWorldT11 /\ q.payment.after=IActionPointAfterT11(q.payment.before)
 /\ q.payment.window=WindowTop9(q.stack).id /\ q.payment.option=WindowTop9(q.stack).busy /\ q.payment.transaction=200
 /\ q.actionPointWorld=[q.payment.after EXCEPT !.checkpointDue=FALSE] /\ q.costDrained
IActionOptionReturnT11(q) ==
 LET w==WindowTop9(q.stack)
     trigger==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
       allTriggerCostsPaid |-> IActionPaidT11(q),costCheckpointAndReactionsDrained |-> q.costDrained]
 IN [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,triggerPayment |-> trigger,
      allCostsPaid |-> IActionPaidT11(q),optionComplete |-> ActionReadyToContinue5(q.action),
      childrenReturned |-> "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete,
                                                                                 
      reactionsDrained |-> q.costDrained /\ "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete]
IReturnReceiptT11(q,kind,frame,parent) == [kind |-> kind,frame |-> frame,parent |-> parent,objects |-> q.objects,revision |-> q.revision+1]
IItemInspectionReturnReadyT11(q) ==
 /\ "ItemInspection" \in DOMAIN q.receipts /\ "ItemInspection" \notin q.consumed
 /\ q.receipts["ItemInspection"].frame=IAT11(q) /\ q.receipts["ItemInspection"].objects=q.objects /\ q.receipts["ItemInspection"].revision=q.revision
 /\ q.receipts["ItemInspection"].parent=IBT11(q).id /\ InspectionChildReturnedT11(IBT11(q),IAT11(q))
IInspectionReturnReadyT11(q) ==
 /\ "Inspection" \in DOMAIN q.receipts /\ "Inspection" \notin q.consumed
 /\ q.receipts["Inspection"].frame=IBT11(q) /\ q.receipts["Inspection"].objects=q.objects /\ q.receipts["Inspection"].revision=q.revision
 /\ q.receipts["Inspection"].parent=q.control.traversal.id /\ IBT11(q).id=20 /\ IBT11(q).returned /\ IBT11(q).complete /\ ~IBT11(q).active
 /\ IBT11(q).traversalId=q.control.traversal.id /\ IBT11(q).targetSite=q.control.traversal.attacked /\ IBT11(q).origin="RulesTraversalInspection" /\ IBT11(q).caller=IInspectionCallerT11(q.control.traversal)
ITraversalReturnReadyT11(q) ==
 /\ "SchemaAtom138" \in DOMAIN q.receipts /\ "SchemaAtom138" \notin q.consumed
 /\ q.receipts["SchemaAtom138"].frame=q.control /\ q.receipts["SchemaAtom138"].objects=q.objects /\ q.receipts["SchemaAtom138"].revision=q.revision
 /\ q.receipts["SchemaAtom138"].parent=q.action.id /\ q.control.returned /\ q.control.traversal.complete
 /\ q.control.traversal.id=q.waitTraversal.id /\ q.action.nested=q.waitTraversal.handle /\ q.control.traversal.caller=ITraversalCallerT11(q.action)
IRecordReturnT11(q,kind,frame,parent,resume) ==
 [q EXCEPT !.receipts=[id \in DOMAIN @ \cup {kind} |-> IF id=kind THEN IReturnReceiptT11(q,kind,frame,parent) ELSE @[id]],
  !.returnOrder=Append(@,kind),!.revision=@+1,!.stage=resume]
IEventNamesT11(q) == UNION {{IObserveEventT11(e) : e \in q.rawEvents[i]} : i \in 1..Len(q.rawEvents)}
IEventCountT11(q,name) == Cardinality({i \in 1..Len(q.rawEvents) : name \in {IObserveEventT11(e) : e \in q.rawEvents[i]}})
IntegrationInitT11 == guideCaseT11=0 /\ qT11=IInitialT11
IOpenWindowT11(kind,site,role,resume) ==
 LET q==qT11 w==NewPriorityWindow9(q.nextWindow,kind,site,EmptyT11,0,NoTimingRef9,[id |-> 0],0)
     label==CASE role="StartAction" -> "5.7.1f:start" [] role="NewAction" -> "5.7.1f:new" [] role="TurnPR" -> "5.7.1e:continuation" [] OTHER -> site.step
 IN /\ OpenPriorityWindow9(q.stack,Append(q.stack,w),w.id,kind,site,EmptyT11,IOpeningT11(w.id,kind,site),q.usedWindows)
    /\ qT11'=[q EXCEPT !.stack=Append(@,w),!.usedWindows=@ \cup {w.id},!.nextWindow=@+1,!.stage="Window",!.windowRole=role,!.windowResume=resume,
         !.NeutralValue00003=IF role="StartAction" THEN [opened |-> w] ELSE @,
         !.windowHistory=Append(@,[id |-> w.id,at |-> label,kind |-> kind,site |-> site])]
IWindowStepT11 ==
 LET q==qT11 w==WindowTop9(q.stack) IN
 CASE w.stage="NeedCheckpoint" ->
        /\ CheckpointPriority9(q.stack,ReplaceWindowTop9(q.stack,PriorityReadyT11(w)),PriorityCheckpointT11(w))
        /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,PriorityReadyT11(w))]
   [] w.stage="Ready" /\ w.kind="NeutralValue00001" ->
        IF q.windowRole="NewAction" THEN qT11'=[q EXCEPT !.trace=Append(@,"5.7.1f:new"),!.done=TRUE,!.stage="Done"]
        ELSE LET busy==StartPriorityOptionFrame9(w,IActionOptionT11,200) IN
          /\ BeginPriorityOption9(q.stack,ReplaceWindowTop9(q.stack,busy),IActionOptionT11,q.objects,LegalityT11(w,IActionOptionT11),EmptyT11)
          /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,busy),!.NeutralValue00003=[opened |-> q.NeutralValue00003.opened,ready |-> w,option |-> IActionOptionT11],!.stage="ActionPay"]
   [] w.stage="Ready" /\ w.kind="Paid" ->
        /\ PassPriority9(q.stack,ReplaceWindowTop9(q.stack,PassPriorityFrame9(w)),w.priority,EmptyT11)
        /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,PassPriorityFrame9(w))]
   [] w.stage="Ready" /\ w.kind="MidItemInspection" ->
        LET a==IAT11(q) after==[a EXCEPT !.midDone=TRUE] options==ItemInspectionMidOptions7(q.objects[1],{},[exists |-> FALSE,amount |-> 0],FALSE,TRUE) IN
        /\ PassMidItemInspection9(q.stack,ReplaceWindowTop9(q.stack,ClosePriorityWindow9(w)),a,after,q.objects,options,FALSE,FALSE)
        /\ qT11'=[IWithItemInspectionT11(q,after) EXCEPT !.stack=ReplaceWindowTop9(@,ClosePriorityWindow9(w))]
   [] w.stage="Closed" ->
        LET rest==SubSeq(q.stack,1,Len(q.stack)-1) next==[q EXCEPT !.stack=rest] IN
        /\ PopClosedPriorityWindow9(q.stack,rest)
        /\ qT11'=IF q.windowRole="SchemaAtom138" THEN IRecordT11(next,q.control.traversal.step,{},"TraversalAdvance")
                  ELSE IF q.windowRole="Mid" THEN IRecordT11(next,"ProcedureCode1dd0e8f05be2",{},"ItemInspectionAdvance")
                  ELSE IRecordT11(next,"ProcedureCode484be3e50aa9",{},"TurnContinue")
ITraversalAdvanceT11 ==
 LET q==qT11 c==q.control work==TraversalWorkT11("Continue",0)
     next==NextTraversalStep6(c.traversal.step,TraversalBranch6(c.traversal,q.layout,{},q.encounter,q.movement,work)) phase==TraversalStepInfo6(next).phase
     pid==IF phase=c.traversal.phase THEN c.traversal.phaseId ELSE c.traversal.phaseId+1 after==TraversalPostFrameT11(c,next,phase,pid) IN
 /\ AdvanceNormalTraversalStep6(c,after,q.layout,{},q.encounter,q.movement,work,pid,TRUE,TRUE,{})
 /\ qT11'=[q EXCEPT !.control=after,!.stage="TraversalWork",!.movement=IF phase="Movement" /\ phase#c.traversal.phase THEN OpenMovement6(after.traversal,c.traversal.phase,0,0,TRUE) ELSE @]
ITraversalWorkT11 ==
 LET q==qT11 c==q.control r==c.traversal m==q.movement IN
 CASE r.step="ProcedureCode12371046a2e5" ->
        LET after==[c EXCEPT !.traversal.attacked="SchemaAtom082",!.announced=TRUE,!.costsPaid=TRUE] events=={[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> r.id,targetSite |-> "SchemaAtom082"]} IN
        /\ AnnounceTraversalTargetSite6(c,after,"SchemaAtom082",[SchemaAtom082 |-> [kind |-> "SchemaAtom033"]],TRUE,TRUE,events)
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,events,"TraversalAdvance")
   [] r.step="ProcedureCodeacc82dbcc545" ->
        LET after==[c EXCEPT !.badPubAdded=TRUE] IN
        /\ AddInitiationLiabilityMarker6(c,after,q.fund,q.fund,0)
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode4d6bd06d2c9f" ->
        LET after==[c EXCEPT !.traversal.formalBegun=TRUE] IN
        /\ FormalTraversalBegin6(c,after,{TraversalBeginEvent6(r)})
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,{TraversalBeginEvent6(r)},"TraversalAdvance")
   [] r.step="ProcedureCode347de0bdd6b4" ->
        LET after==[r EXCEPT !.position="NoValue"] IN
        /\ SetInitialSideBPosition6(r,after,q.layout,r.step)
        /\ qT11'=IRecordT11([q EXCEPT !.control.traversal=after],r.step,{},"TraversalAdvance")
   [] r.step \in {"ProcedureCode71e36c9e8e04","ProcedureCode4f60245a1dde","ProcedureCode2cd618a9e624"} -> IOpenWindowT11("Paid",ITraversalSiteT11(q),"SchemaAtom138","TraversalAdvance")
   [] r.step \in {"ProcedureCode7e3f7e5033c8","ProcedureCodea732fbc12ae0","ProcedureCodec7b41615d673"} ->
        LET after==[c EXCEPT !.phaseEndedIds=@ \cup {r.phaseId}] IN
        /\ BeginNormalTraversalPhaseEnd6(c,after,q.layout,{},q.encounter,m,TraversalWorkT11("Continue",0),TRUE,{TraversalPhaseEndEvent6(r)})
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,{TraversalPhaseEndEvent6(r)},"TraversalAdvance")
   [] r.step="ProcedureCode714dfe070fed" ->
        LET after==[m EXCEPT !.begun=TRUE,!.passedBarrier=0,!.passedAll=FALSE] IN
        /\ BeginMovement6(r,m,after,q.layout,{})
        /\ qT11'=IRecordT11([q EXCEPT !.movement=after],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode9bca3a096549" ->
        LET after==[m EXCEPT !.declined=TRUE] IN
        /\ DeclineMovementWithdrawTraversal6(r,m,after,TRUE)
        /\ qT11'=IRecordT11([q EXCEPT !.movement=after],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCoded4ddeafb5f2f" ->
        LET afterTraversal==[r EXCEPT !.position="NoValue"] after==[m EXCEPT !.advanced=TRUE,!.movedToNew=FALSE] IN
        /\ AdvanceMovement6(r,afterTraversal,m,after,q.layout,q.layout)
        /\ qT11'=IRecordT11([q EXCEPT !.control.traversal=afterTraversal,!.movement=after],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode6c5d14f545f7" -> qT11'=IRecordT11(q,r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode7e82ab2b38b7" ->
        LET after==[m EXCEPT !.approachedTargetSite=TRUE] events=={[tag |-> "ApproachTargetSite",traversalId |-> r.id,targetSite |-> r.attacked,phaseId |-> r.phaseId]} IN
        /\ ApproachTargetSite6(r,m,after,events)
        /\ qT11'=IRecordT11([q EXCEPT !.movement=after],r.step,events,"TraversalAdvance")
   [] r.step="ProcedureCodebbb14496b09b" ->
        LET after==[c EXCEPT !.declarationProcessed=TRUE,!.traversal.successful=TRUE] events=={[tag |-> "SuccessfulTraversal",traversalId |-> r.id,targetSite |-> "SchemaAtom082"]} IN
        /\ DeclareSuccessfulTraversal6(c,after,TRUE,events)
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,events,"TraversalAdvance")
   [] r.step="ProcedureCoded75d879e00ff" ->
        LET after==[c EXCEPT !.siteInspectionChosen=TRUE] directive==[kind |-> "Inspection",choice |-> "Inspection",traversalId |-> r.id,targetSite |-> r.attacked,origin |-> "RulesTraversalInspection"]
            b==OpenInspection7(20,directive.targetSite,"SchemaAtom082",directive.traversalId,directive.origin,IInspectionCallerT11(r),{},InspectionPolicy7("Normal",0)) IN
        /\ ChooseRulesInspection6(c,after,"Inspection",{"Inspection"},TRUE,directive)
        /\ qT11'=[IWithInspectionT11([q EXCEPT !.control=after],b) EXCEPT !.stage="InspectionWork",!.trace=Append(@,r.step),!.revision=@+1]
   [] r.step="ProcedureCode6ea937bb44ac" ->
        LET after==[c EXCEPT !.windowsDone=TRUE] IN
        /\ \A i \in 1..Len(q.stack) : q.stack[i].site.traversalId#r.id
        /\ FinishTraversalEndWindows6(c,after)
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode84dea7dc8ecc" ->
        LET after==[c EXCEPT !.fundReturned=TRUE] IN
        /\ ReturnLiabilityMarkerFund6(c,after,q.fund,0,q.bank,q.bank)
        /\ qT11'=IRecordT11([q EXCEPT !.control=after,!.fund=0],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode5e397645e65c" ->
        LET after==[c EXCEPT !.resultDeclared=TRUE,!.traversal.unsuccessful=FALSE] IN
        /\ DeclareUnsuccessfulTraversal6(c,after,[SchemaAtom082 |-> [kind |-> "SchemaAtom033"]],{})
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,{},"TraversalAdvance")
   [] r.step="ProcedureCode9606a4cd52b4" ->
        LET after==[c EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds=@ \cup {r.phaseId}] events=={[tag |-> "TraversalEnds",traversalId |-> r.id],TraversalPhaseEndEvent6(r)} IN
        /\ CompleteTraversal6(c,after,TRUE,events,{r.id})
        /\ qT11'=IRecordT11([q EXCEPT !.control=after],r.step,events,"TraversalReturn")
IInspectionWorkT11 ==
 LET q==qT11 b==IBT11(q) IN
 CASE b.step="ProcedureCode839b301bad95" ->
        LET after==[b EXCEPT !.active=TRUE,!.beginMet=TRUE] capacity==OpenCandidateCapacity7(b,q.objects) IN
        /\ BeginInspectionWithCandidates7(b,after,capacity,q.objects,0,{"SchemaAtom082"},TRUE,TRUE,{InspectionBeginEvent7(b)})
        /\ qT11'=IRecordT11([IWithInspectionT11(q,after) EXCEPT !.capacity=capacity],b.step,{InspectionBeginEvent7(b)},"InspectionAdvance")
   [] b.step="ProcedureCodeb6067693902e" -> qT11'=IRecordT11(q,b.step,{},"InspectionAdvance")
   [] b.step="ProcedureCode91f3ee0da236" ->
        LET after==[b EXCEPT !.limitSet=TRUE] IN
        /\ FreezeInspectionLimit7(b,after,TRUE)
        /\ qT11'=IRecordT11(IWithInspectionT11(q,after),b.step,{},"InspectionAdvance")
   [] b.step="ProcedureCode1404a82ab3ee" ->
        LET view==InspectionCandidates7(b,q.capacity,q.objects,<<>>,{}) IN
        /\ DeriveCandidateView7(b,q.capacity,q.objects,<<>>,{},FALSE,view)
        /\ IF view.central={} THEN qT11'=IRecordT11([q EXCEPT !.siteInspectionDecision="End"],b.step,{},"InspectionAdvance")
           ELSE LET after==InspectionSelectT11(b,1,"SchemaAtom033") IN
             /\ InspectionPresentation7(b,view).randomCentralAOffered /\ view.central={1}
             /\ ChooseCentralAInspectionCard7(b,after,view,1,0,FALSE,view.central={1})
             /\ qT11'=IRecordT11([IWithInspectionT11(q,after) EXCEPT !.siteInspectionDecision="Choose"],b.step,{},"InspectionAdvance")
   [] b.step="ProcedureCodee35e7c8fc57b" ->
        LET a==OpenItemInspection7(77,b.selectedObject,q.objects[b.selectedObject],b.traversalId,b.id,InspectionItemInspectionCaller7(b),{}) IN
        /\ qT11'=[IWithItemInspectionT11(q,a) EXCEPT !.stage="ItemInspectionWork",!.trace=Append(@,b.step),!.revision=@+1]
   [] b.step="ProcedureCodeb1fbc90c4ab0" -> qT11'=IRecordT11(q,b.step,{},"InspectionAdvance")
   [] b.step="ProcedureCode8c612115d469" ->
        LET after==[b EXCEPT !.active=FALSE,!.complete=TRUE,!.step="Complete",!.completionReason="Normal"] IN
        /\ CompleteNormalInspection7(b,after,TRUE,{InspectionEndEvent7(b)})
        /\ qT11'=IRecordT11(IWithInspectionT11(q,after),b.step,{InspectionEndEvent7(b)},"InspectionReturn")
IInspectionAdvanceT11 ==
 LET q==qT11 b==IBT11(q) IN
 IF b.step="ProcedureCode1404a82ab3ee" THEN
   IF q.siteInspectionDecision="Choose" THEN LET after==[b EXCEPT !.step="ProcedureCodee35e7c8fc57b"] IN
     /\ AdvanceInspectionSelection7(b,after,TRUE) /\ qT11'=[IWithInspectionT11(q,after) EXCEPT !.stage="InspectionWork"]
   ELSE LET after==[b EXCEPT !.step="ProcedureCode8c612115d469"] IN
     /\ SkipInspectionSelection7(b,after,q.capacity,q.objects,<<>>,{},FALSE,TRUE) /\ qT11'=[IWithInspectionT11(q,after) EXCEPT !.stage="InspectionWork"]
 ELSE LET after==[b EXCEPT !.step=NextInspectionStep7(b.step)] IN
   /\ AdvanceInspectionStep7(b,after,TRUE,TRUE) /\ qT11'=[IWithInspectionT11(q,after) EXCEPT !.stage="InspectionWork"]
IItemInspectionWorkT11 ==
 LET q==qT11 a==IAT11(q) b==IBT11(q) IN
 CASE a.step="ProcedureCodefd91bef8bbd3" ->
        LET after==[a EXCEPT !.active=TRUE,!.beginMet=TRUE] attached==[b EXCEPT !.currentItemInspectionId=a.id,!.usedItemInspectionIds=@ \cup {a.id}]
            history==[id \in {a.id} |-> [object |-> a.object,traversalId |-> a.traversalId,siteInspectionId |-> a.siteInspectionId,turnId |-> q.flow.turn.id,hadRetireCost |-> FALSE]] IN
        /\ BeginItemInspection7(a,after,q.objects,TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(a)})
        /\ AttachChosenItemInspection7(b,attached,after,ItemInspectionBeginEvent7(a))
        /\ RecordActualItemInspection7(q.itemInspectionHistory,history,after,q.flow.turn.id,FALSE,ItemInspectionBeginEvent7(a))
        /\ qT11'=IRecordT11([IWithInspectionT11(IWithItemInspectionT11(q,after),attached) EXCEPT !.itemInspectionHistory=history],a.step,{ItemInspectionBeginEvent7(a)},"ItemInspectionAdvance")
   [] a.step="ProcedureCode1dd0e8f05be2" -> IOpenWindowT11("MidItemInspection",ItemInspectionPrioritySite9(q.flow.turn,a,q.objects),"Mid","ItemInspectionAdvance")
   [] a.step="ProcedureCode546db7cc4546" ->
        LET after==[a EXCEPT !.claimObjectiveDone=TRUE] IN
        /\ ResolveItemInspectionClaimObjective7(a,after,q.objects,FALSE,FALSE,FALSE,TRUE,FALSE,FALSE)
        /\ qT11'=IRecordT11(IWithItemInspectionT11(q,after),a.step,{},"ItemInspectionAdvance")
   [] a.step="ProcedureCode662478499367" ->
        LET after==ItemInspectionEndedT11(a,"Normal") IN
        /\ CompleteNormalItemInspection7(a,after,q.objects,TRUE,{ItemInspectionEndEvent7(a)})
        /\ qT11'=IRecordT11(IWithItemInspectionT11(q,after),a.step,{ItemInspectionEndEvent7(a)},"ItemInspectionReturn")
IItemInspectionAdvanceT11 ==
 LET q==qT11 a==IAT11(q) after==[a EXCEPT !.step=NextItemInspectionStep7(a.step)] IN
 /\ AdvanceItemInspectionStep7(a,after,q.objects,TRUE,TRUE)
 /\ qT11'=[IWithItemInspectionT11(q,after) EXCEPT !.stage="ItemInspectionWork"]
IInsideItemInspectionT11(q) == IF 77 \in DOMAIN q.control.itemInspections THEN StillItemInspectioning7(IAT11(q),q.objects) ELSE FALSE
IInsideInspectionT11(q) == IF 20 \in DOMAIN q.control.siteInspections THEN IBT11(q).active /\ ~IBT11(q).complete ELSE FALSE
IConnectedStepT11 ==
 LET q==qT11 c==q.control IN
 /\ UNCHANGED guideCaseT11
 /\ CASE q.stage="LatchStart" ->
        LET after==[q.flow EXCEPT !.decision="NeutralValue00001"] IN
        /\ SideBLatchDecision5(q.flow,after,q.actionPointWorld.actionPoints["SideB"],TRUE)
        /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenAction"]
   [] q.stage="OpenAction" -> IOpenWindowT11("NeutralValue00001",ITurnSiteT11(q),"StartAction","ActionPay")
   [] q.stage="Window" -> IWindowStepT11
   [] q.stage="ActionPay" ->
        LET after==IActionPointAfterT11(q.actionPointWorld) a==NewAction5(30,"SideB",BasicActionKey5("SideB","SchemaAtom138"))
            payment==[before |-> q.actionPointWorld,after |-> after,window |-> WindowTop9(q.stack).id,option |-> IActionOptionT11,transaction |-> 200] IN
        /\ IActionReservationT11(q) /\ BasicActionLocalGate5("SideB","SchemaAtom138",FALSE)
        /\ BasicAction5("SideB","SchemaAtom138").effect="SchemaAtom138" /\ BasicAction5("SideB","SchemaAtom138").actionPoints=1 /\ BasicAction5("SideB","SchemaAtom138").resourceUnits=0
        /\ qT11'=[q EXCEPT !.actionPointWorld=after,!.payment=payment,!.action=a,!.stage="ActionCostDrain"]
        /\ IntegrationActionPointsT11!DoActionPoints(IActionPointCommandT11)
        /\ ActionStart5(q.flow.turn,"SideB",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,IActionReservationT11(q),TRUE,q.action.status="Idle",a.id,a.key,a)
   [] q.stage="ActionCostDrain" ->
        /\ q.actionPointWorld=q.payment.after /\ q.actionPointWorld.checkpointDue
        /\ qT11'=[q EXCEPT !.actionPointWorld.checkpointDue=FALSE,!.costDrained=TRUE,!.stage="ActionEffects"]
   [] q.stage="ActionEffects" ->
        LET after==[q.action EXCEPT !.status="Effects"] IN
        /\ IActionPaidT11(q) /\ ActionEffectsBegin5(q.action,after,IActionPaidT11(q))
        /\ qT11'=[q EXCEPT !.action=after,!.trace=Append(@,"ProcedureCode989abc27e0c6"),!.revision=@+1,!.stage="TraversalStart"]
   [] q.stage="TraversalStart" ->
        LET after==[q.action EXCEPT !.status="Nested",!.nested="Traversal7"] traversal==OpenTraversal6(7,1000,ITraversalCallerT11(q.action)) IN
        /\ ActionNestedBegin5(q.action,after,"Traversal7")
        /\ qT11'=[q EXCEPT !.action=after,!.waitTraversal=[id |-> traversal.id,handle |-> "Traversal7",action |-> q.action.id],!.control=TraversalControlT11(traversal),!.stage="TraversalWork"]
   [] q.stage="TraversalWork" -> ITraversalWorkT11
   [] q.stage="TraversalAdvance" -> ITraversalAdvanceT11
   [] q.stage="InspectionWork" -> IInspectionWorkT11
   [] q.stage="InspectionAdvance" -> IInspectionAdvanceT11
   [] q.stage="ItemInspectionWork" -> IItemInspectionWorkT11
   [] q.stage="ItemInspectionAdvance" -> IItemInspectionAdvanceT11
   [] q.stage="Drain" ->
        qT11'=[q EXCEPT !.drains=Append(@,[step |-> q.lastWork,insideItemInspection |-> IInsideItemInspectionT11(q),insideInspection |-> IInsideInspectionT11(q),duringTraversal |-> DuringTraversal6(c.traversal)]),!.revision=@+1,!.stage=q.resume]
   [] q.stage="ItemInspectionReturn" ->
        LET a==IAT11(q) after==[a EXCEPT !.returned=TRUE] next==IWithItemInspectionT11(q,after) IN
        /\ ReturnItemInspectionToCaller7(a,after,TRUE,InspectionItemInspectionCaller7(IBT11(q)))
        /\ qT11'=IRecordReturnT11(next,"ItemInspection",after,IBT11(q).id,"InspectionResume")
   [] q.stage="InspectionResume" ->
        LET b==IBT11(q) after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
        /\ IItemInspectionReturnReadyT11(q) /\ FinishInspectionItemInspectionInstruction7(b,after,IItemInspectionReturnReadyT11(q))
        /\ qT11'=IRecordT11([IWithInspectionT11(q,after) EXCEPT !.consumed=@ \cup {"ItemInspection"}],"7.5.5:return",{},"InspectionAdvance")
   [] q.stage="InspectionReturn" ->
        LET b==IBT11(q) after==[b EXCEPT !.returned=TRUE] next==IWithInspectionT11(q,after) IN
        /\ ReturnInspectionToCaller7(b,after,TRUE,IInspectionCallerT11(c.traversal))
        /\ qT11'=IRecordReturnT11(next,"Inspection",after,c.traversal.id,"TraversalResume")
   [] q.stage="TraversalResume" ->
        LET after==[c EXCEPT !.siteInspectionFinished=TRUE] IN
        /\ IInspectionReturnReadyT11(q) /\ FinishRulesInspectionInstruction6(c,after,IInspectionReturnReadyT11(q))
        /\ qT11'=IRecordT11([q EXCEPT !.control=after,!.consumed=@ \cup {"Inspection"}],"6.9.5b:return",{},"TraversalAdvance")
   [] q.stage="TraversalReturn" ->
        LET after==[c EXCEPT !.returned=TRUE] next==[q EXCEPT !.control=after] IN
        /\ ReturnTraversalToCaller6(c,after,TRUE,ITraversalCallerT11(q.action))
        /\ qT11'=IRecordReturnT11(next,"SchemaAtom138",after,q.action.id,"ActionResume")
   [] q.stage="ActionResume" ->
        LET after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"] IN
        /\ ITraversalReturnReadyT11(q) /\ ActionNestedReturn5(q.action,after,q.waitTraversal.handle,ITraversalReturnReadyT11(q))
        /\ qT11'=[q EXCEPT !.action=after,!.consumed=@ \cup {"SchemaAtom138"},!.stage="ActionComplete"]
   [] q.stage="ActionComplete" ->
        LET after==[q.action EXCEPT !.status="Complete"] IN
        /\ ActionComplete5(q.action,after,"SchemaAtom138" \in q.consumed /\ c.returned /\ c.traversal.complete)
        /\ qT11'=[IRecordT11([q EXCEPT !.action=after],"5.7.1f:return",{[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]},"TurnAdvance") EXCEPT !.stage="ActionWindowReturn"]
   [] q.stage="ActionWindowReturn" ->
        LET w==WindowTop9(q.stack) IN
        /\ CompletePriorityOption9(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(w)),IActionOptionReturnT11(q))
        /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.returnOrder=Append(@,"NeutralValue00001"),!.stage="PopAction"]
   [] q.stage="PopAction" ->
        /\ PopClosedPriorityWindow9(q.stack,<<>>)
        /\ qT11'=[q EXCEPT !.stack= <<>>,!.stage="Drain"]
   [] q.stage="TurnAdvance" ->
        LET after==[q.flow EXCEPT !.step="ProcedureCodea439ce381bba",!.decision="NoValue"] IN
        /\ SideBStepAdvance5(q.flow,after,ActionReadyToContinue5(q.action))
        /\ qT11'=IRecordT11([q EXCEPT !.flow=after],"ProcedureCodea439ce381bba",{},"TurnLoop")
   [] q.stage="TurnLoop" ->
        LET after==[q.flow EXCEPT !.step="ProcedureCode484be3e50aa9",!.decision="NoValue"] IN
        /\ SideBStepAdvance5(q.flow,after,TRUE) /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenPR"]
   [] q.stage="OpenPR" -> IOpenWindowT11("Paid",ITurnSiteT11(q),"TurnPR","TurnContinue")
   [] q.stage="TurnContinue" ->
        LET after==[q.flow EXCEPT !.step="ProcedureCode989abc27e0c6",!.decision="NoValue"] IN
        /\ SideBStepAdvance5(q.flow,after,TRUE) /\ qT11'=[q EXCEPT !.flow=after,!.stage="LatchNew"]
   [] q.stage="LatchNew" ->
        LET after==[q.flow EXCEPT !.decision="NeutralValue00001"] IN
        /\ SideBLatchDecision5(q.flow,after,q.actionPointWorld.actionPoints["SideB"],TRUE) /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenNewAction"]
   [] q.stage="OpenNewAction" ->
        /\ q.stack= <<>> /\ ActionReadyToContinue5(q.action) /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"}
        /\ IOpenWindowT11("NeutralValue00001",ITurnSiteT11(q),"NewAction","Done")
   [] q.stage="Done" -> UNCHANGED qT11
IntegrationSpecT11 == IntegrationInitT11 /\ [][IConnectedStepT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(IConnectedStepT11)
IWindowClassT11(row) == IF row.kind="NeutralValue00001" THEN "NeutralValue00001" ELSE IF row.kind="MidItemInspection" THEN "MidItemInspection" ELSE IF PaidWindowOptions9(row.site).nonBarrierActivation THEN "PR" ELSE "P"
IReturnGuardChecksT11(q) ==
 /\ (q.stage="ItemInspectionReturn" =>
       LET a==IAT11(q) after==[a EXCEPT !.returned=TRUE] IN
       /\ ReturnItemInspectionToCaller7(a,after,TRUE,InspectionItemInspectionCaller7(IBT11(q)))
       /\ ~ReturnItemInspectionToCaller7(a,after,FALSE,InspectionItemInspectionCaller7(IBT11(q)))
       /\ ~ReturnItemInspectionToCaller7(a,after,TRUE, <<"InspectionItemInspection",21>>))
 /\ (q.stage="InspectionResume" =>
       LET a==IAT11(q) b==IBT11(q) after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
       /\ IItemInspectionReturnReadyT11(q)
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].parent=21])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].revision=q.revision-1])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].frame=[a EXCEPT !.returned=FALSE]])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.consumed=@ \cup {"ItemInspection"}])
       /\ ItemInspectionProcedureValid7([a EXCEPT !.id=78],q.objects) /\ ~InspectionChildReturnedT11(b,[a EXCEPT !.id=78])
       /\ ~InspectionChildReturnedT11(b,[a EXCEPT !.caller= <<"InspectionItemInspection",21>>])
       /\ ~FinishInspectionItemInspectionInstruction7(b,after,FALSE)
       /\ ~ReturnItemInspectionToCaller7(a,a,TRUE,InspectionItemInspectionCaller7(b)))
 /\ (q.stage="InspectionReturn" =>
       LET b==IBT11(q) after==[b EXCEPT !.returned=TRUE] IN
       /\ ~ReturnInspectionToCaller7(b,after,FALSE,IInspectionCallerT11(q.control.traversal))
       /\ ~ReturnInspectionToCaller7(b,after,TRUE, <<"TraversalInspectionInstruction",8,"ProcedureCoded75d879e00ff">>))
 /\ (q.stage="TraversalResume" =>
       /\ IInspectionReturnReadyT11(q)
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].revision=q.revision-1])
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].frame.choices= <<>>])
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.consumed=@ \cup {"Inspection"}])
       /\ ~ReturnInspectionToCaller7(IBT11(q),IBT11(q),TRUE,IInspectionCallerT11(q.control.traversal)))
 /\ (q.stage="TraversalReturn" =>
       LET c==q.control after==[c EXCEPT !.returned=TRUE] IN
       /\ ~ReturnTraversalToCaller6(c,after,FALSE,ITraversalCallerT11(q.action))
       /\ ~ReturnTraversalToCaller6(c,after,TRUE, <<"BasicTraversalAction",31>>)
       /\ ~CompletePriorityOption9(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))),IActionOptionReturnT11(q)))
 /\ (q.stage="ActionResume" =>
       LET after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"] IN
       /\ ITraversalReturnReadyT11(q)
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].revision=q.revision-1])
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].frame.itemInspections[77].returned=FALSE])
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.consumed=@ \cup {"SchemaAtom138"}])
       /\ ~ActionNestedReturn5(q.action,after,"SiblingTraversal",TRUE)
       /\ ~ActionNestedReturn5(q.action,after,q.waitTraversal.handle,FALSE)
       /\ ~ReturnTraversalToCaller6(q.control,q.control,TRUE,ITraversalCallerT11(q.action)))
 /\ (q.stage="ItemInspectionWork" /\ "ItemInspection" \notin DOMAIN q.receipts =>
       /\ ~IItemInspectionReturnReadyT11(q)
       /\ ~ReturnInspectionToCaller7(IBT11(q),[IBT11(q) EXCEPT !.returned=TRUE],TRUE,IInspectionCallerT11(q.control.traversal))
       /\ ~ReturnTraversalToCaller6(q.control,[q.control EXCEPT !.returned=TRUE],TRUE,ITraversalCallerT11(q.action))
       /\ ~ReturnItemInspectionToCaller7(IAT11(q),[IAT11(q) EXCEPT !.returned=TRUE],TRUE,InspectionItemInspectionCaller7(IBT11(q))))
 /\ (q.stage="OpenNewAction" =>
       LET site==ITurnSiteT11(q) oldId==q.NeutralValue00003.opened.id w==NewPriorityWindow9(oldId,"NeutralValue00001",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0) IN
       /\ ~OpenPriorityWindow9(q.stack,Append(q.stack,w),oldId,"NeutralValue00001",site,EmptyT11,IOpeningT11(oldId,"NeutralValue00001",site),q.usedWindows)
       /\ q.action.status="Complete" /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"})
 /\ (q.stage \in {"ActionComplete","ActionWindowReturn"} =>
       LET after==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
       /\ (CompletePriorityOption9(q.stack,after,IActionOptionReturnT11(q)) = (q.stage="ActionWindowReturn"))
       /\ ~CompletePriorityOption9(q.stack,after,IActionOptionReturnT11([q EXCEPT !.action.status="Effects"]))
       /\ ~CompletePriorityOption9(q.stack,after,IActionOptionReturnT11([q EXCEPT !.control.returned=FALSE]))
       /\ ~CompletePriorityOption9(q.stack,after,IActionOptionReturnT11([q EXCEPT !.consumed=@ \ {"SchemaAtom138"}]))
       /\ ~CompletePriorityOption9(q.stack,after,IActionOptionReturnT11([q EXCEPT !.costDrained=FALSE])))
IActionWindowOrderT11(q) ==
 /\ (q.stage="Drain" /\ q.lastWork="5.7.1f:return" =>
       q.stack= <<>> /\ q.action.status="Complete" /\ q.returnOrder=IntegrationOracleReturnOrder11)
 /\ (q.stage \in {"ActionWindowReturn","PopAction"} =>
       /\ q.action.status="Complete" /\ Len(q.stack)=1 /\ WindowTop9(q.stack).kind="NeutralValue00001"
       /\ (WindowTop9(q.stack).open = (q.stage="ActionWindowReturn"))
       /\ \A i \in 1..Len(q.drains) : q.drains[i].step#"5.7.1f:return")
 /\ (q.stage="TurnAdvance" =>
       q.stack= <<>> /\ Len(q.drains)>0 /\ q.drains[Len(q.drains)].step="5.7.1f:return")
IntegrationSafetyT11 ==
 LET q==qT11 IN
 /\ SideBProcedureValid5(q.flow) /\ TraversalFrameValid6(q.control.traversal)
 /\ IReturnGuardChecksT11(q)
 /\ IActionWindowOrderT11(q)
 /\ \A i \in 1..Len(q.windowHistory) : IWindowClassT11(q.windowHistory[i])=IntegrationOracleWindowClasses11[q.windowHistory[i].at] /\ ~PaidWindowOptions9(q.windowHistory[i].site).score
 /\ (q.action.status#"Complete" => \A i \in 1..Len(q.windowHistory) : q.windowHistory[i].at#"5.7.1f:new")
 /\ q.objects=IInitialT11.objects /\ q.fund=0 /\ q.bank=0
 /\ q.actionPointWorld.actionPoints["SideB"] \in {IntegrationOracleStartActionPoints11,IntegrationOracleEndActionPoints11}
 /\ q.trace=SubSeq(IntegrationOracleTrace11,1,Len(q.trace))
 /\ IEventNamesT11(q) \cap IntegrationOracleAbsent11={}
 /\ \A i \in 1..Len(q.stack) : PriorityWindowValid9(q.stack[i])
 /\ \A id \in DOMAIN q.control.itemInspections : ItemInspectionProcedureValid7(q.control.itemInspections[id],q.objects)
 /\ \A id \in DOMAIN q.control.siteInspections : InspectionProcedureValid7(q.control.siteInspections[id])
 /\ (q.action.status="Nested" => q.waitTraversal.handle=q.action.nested /\ q.waitTraversal.id=q.control.traversal.id)
 /\ (q.action.status="Nested" => Len(q.stack)>0 /\ q.stack[1].kind="NeutralValue00001" /\ q.stack[1].open
       /\ q.stack[1].stage="Resolving" /\ q.stack[1].busy=IActionOptionT11)
 /\ ("ItemInspection" \in q.consumed => IAT11(q).returned)
 /\ ("Inspection" \in q.consumed => IBT11(q).returned)
 /\ ("SchemaAtom138" \in q.consumed => q.control.returned)
 /\ (q.done =>
       /\ q.trace=IntegrationOracleTrace11 /\ q.returnOrder=IntegrationOracleReturnOrder11
       /\ q.actionPointWorld.actionPoints["SideB"]=IntegrationOracleEndActionPoints11 /\ q.actionPointWorld.spent["SideB"]=1
       /\ q.action.status="Complete" /\ q.control.returned /\ q.control.traversal.complete /\ q.control.traversal.successful /\ ~q.control.traversal.unsuccessful
       /\ InspectionCentralChoices7(IBT11(q))=IntegrationOracleCentralChoices11
       /\ Cardinality(ActualItemInspectionesInInspection7(q.itemInspectionHistory,20))=IntegrationOracleActualItemInspectiones11
       /\ \A name \in IntegrationOracleEvents11 : IEventCountT11(q,name)=1
       /\ Len(q.stack)=1 /\ WindowTop9(q.stack).kind="NeutralValue00001" /\ WindowTop9(q.stack).stage="Ready" /\ WindowTop9(q.stack).priority="SideB"
       /\ WindowTop9(q.stack).id#q.NeutralValue00003.opened.id /\ WindowTop9(q.stack).busy=NoPriorityOption9
       /\ ~CanPassPriority9(WindowTop9(q.stack),EmptyT11))
IntegrationTerminatesT11 == <>qT11.done
=============================================================================