-------------------------- MODULE TraversalTimingMC --------------------------
EXTENDS SchedulerChecksMC
                                                                               
                                                                                    
TraversalTurnT11(player) == [OpenTurn5(player,2,[SideA |-> 1,SideB |-> 1]) EXCEPT !.phase="NeutralValue00001",!.formalBegun=TRUE]
TraversalLayoutT11(n) ==
 [orders |-> [SchemaAtom082 |-> IF n=0 THEN <<>> ELSE IF n=1 THEN <<"outer">> ELSE <<"inner","outer">>],
  slots |-> [p \in IF n=0 THEN {} ELSE IF n=1 THEN {"outer"} ELSE {"inner","outer"} |->
    [targetSite |-> "SchemaAtom082",barrierCard |-> IF p="outer" THEN 3 ELSE 4,reservation |-> 0,retained |-> FALSE]],used |-> {"inner","outer"}]
TraversalControlT11(r) ==
 [traversal |-> r,encounter |-> IF r.phase="Encounter" THEN r.phaseId ELSE 0,siteInspections |-> EmptyT11,itemInspections |-> EmptyT11,
  abortedEncounters |-> {},abortedInspectiones |-> {},abortedItemInspectiones |-> {},paidOpen |-> FALSE,windows |-> <<>>,
  windowCleanupDue |-> FALSE,onlyWindowCleanup |-> FALSE,phaseEndedIds |-> {},phaseStepsSkipped |-> FALSE,
  redirect |-> NoTraversalRedirect6,redirectStage |-> "NoValue",redirectCheckpointDue |-> FALSE,
  announced |-> FALSE,costsPaid |-> FALSE,badPubAdded |-> FALSE,declarationProcessed |-> FALSE,
  siteInspectionChosen |-> FALSE,siteInspectionFinished |-> FALSE,windowsDone |-> FALSE,fundReturned |-> FALSE,resultDeclared |-> FALSE,returned |-> FALSE]
TraversalInitialT11 == TraversalControlT11(OpenTraversal6(7,1000,"AuditCaller"))
TraversalWorkT11(jack,sub) == [jackChoice |-> jack,resolvedSub |-> sub]
TraversalGraphFixtureT11(step,decision) ==
 LET r==[OpenTraversal6(7,1000,"AuditCaller") EXCEPT !.step=step,!.phase=TraversalOraclePhases11[step],!.attacked="SchemaAtom082",
          !.formalBegun=step \notin {"ProcedureCode12371046a2e5","ProcedureCodeacc82dbcc545"},!.ending=TraversalOraclePhases11[step]="TraversalEnds",
          !.position=IF TraversalOraclePhases11[step] \in {"Success","TraversalEnds"} \/ step \in {"ProcedureCode7e82ab2b38b7","ProcedureCodea732fbc12ae0"} \/ decision \in {"NoBarrier","NoPosition"}
                     THEN "NoValue" ELSE IF decision="NewPosition" THEN "inner" ELSE "outer",
          !.reachedSuccess=TraversalOraclePhases11[step]="Success",!.successful=TraversalOraclePhases11[step]="Success"]
     c==[TraversalControlT11(r) EXCEPT !.announced=TRUE,!.costsPaid=TRUE,!.badPubAdded=TRUE,!.declarationProcessed=TRUE,
          !.siteInspectionChosen=TRUE,!.siteInspectionFinished=TRUE,!.windowsDone=TRUE,!.fundReturned=TRUE,!.resultDeclared=TRUE]
     e==[OpenEncounter6(1000,3,7,FALSE,"AuditTraversal",IF decision="NoBarrierInstruction" THEN <<1>> ELSE <<1,2>>) EXCEPT
          !.stage=IF step="ProcedureCodeda7bff1d9270" THEN "BeginReactions" ELSE IF step="ProcedureCode687f72772ab1" THEN "Complete" ELSE "BarrierInstructions",!.paidReached=TRUE,!.resolved={1}]
     m==[OpenMovement6(r,"Approach",3,0,TRUE) EXCEPT !.begun=TRUE,!.declined=decision#"WithdrawTraversal",!.advanced=TRUE,
          !.movedToNew=decision="NewPosition",!.approachedTargetSite=step="ProcedureCodea732fbc12ae0"]
 IN [control |-> c,encounter |-> e,movement |-> m,layout |-> TraversalLayoutT11(2),activated |-> IF decision="ItemActivated" THEN {3} ELSE {},
     work |-> TraversalWorkT11(IF decision="WithdrawTraversal" THEN "WithdrawTraversal" ELSE "Continue",IF decision="BarrierInstruction" THEN 1 ELSE 0)]
TraversalPostFrameT11(c,step,phase,pid) ==
 [c EXCEPT !.traversal.step=step,!.traversal.phase=phase,!.traversal.phaseId=pid,
    !.traversal.usedPhaseIds=IF phase#c.traversal.phase THEN @ \cup {pid} ELSE @,
    !.traversal.reachedSuccess=@ \/ phase="Success",!.traversal.ending=@ \/ phase="TraversalEnds",
    !.traversal.position=IF phase \in {"Success","TraversalEnds"} THEN "NoValue" ELSE @,
    !.encounter=IF phase="Encounter" THEN pid ELSE IF c.traversal.phase="Encounter" THEN 0 ELSE @,
    !.phaseStepsSkipped=FALSE,!.windowCleanupDue=IF phase="TraversalEnds" /\ phase#c.traversal.phase THEN TRUE ELSE IF c.traversal.step="ProcedureCode6ea937bb44ac" THEN FALSE ELSE @]
TraversalCandidateControlsT11(c) ==
 {TraversalPostFrameT11(c,step,phase,pid) : step \in TraversalOracleStepSet11 \cup {"UnauthorizedStep"},phase \in {"Initiation","Approach","Encounter","Movement","Success","TraversalEnds"},pid \in {c.traversal.phaseId,c.traversal.phaseId+1}}
TraversalDestinationT11(c) == IF c.returned THEN <<"ReturnToCaller","OutsideTraversal">> ELSE <<c.traversal.step,c.traversal.phase>>
ActualTraversalDestinationsT11(f,completed,drained) ==
 LET b==f.control ended==[b EXCEPT !.phaseEndedIds=@ \cup {b.traversal.phaseId}]
     c==IF BeginNormalTraversalPhaseEnd6(b,ended,f.layout,f.activated,f.encounter,f.movement,f.work,completed,{TraversalPhaseEndEvent6(b.traversal)}) THEN ended ELSE b
     end==[EndTraversalOutcome6(b,1001) EXCEPT !.traversal.withdrewTraversal=TRUE]
     done==[b EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds=@ \cup {b.traversal.phaseId}]
     returned==[done EXCEPT !.returned=TRUE]
 IN {TraversalDestinationT11(a) : a \in {g \in TraversalCandidateControlsT11(c) : AdvanceNormalTraversalStep6(c,g,f.layout,f.activated,f.encounter,f.movement,f.work,g.traversal.phaseId,completed,drained,{})}} \cup
    (IF f.work.jackChoice="WithdrawTraversal" /\ MovementWithdrawTraversal6(b,end,f.movement,f.layout,f.layout,1001,TRUE,completed /\ drained,TRUE,EndTraversalEffectEvents6(b)) THEN {TraversalDestinationT11(end)} ELSE {}) \cup
    (IF CompleteTraversal6(b,done,completed,{[tag |-> "TraversalEnds",traversalId |-> b.traversal.id],TraversalPhaseEndEvent6(b.traversal)},{b.traversal.id}) /\ ReturnTraversalToCaller6(done,returned,drained,"AuditCaller") THEN {TraversalDestinationT11(returned)} ELSE {})
ExpectedTraversalDestinationT11(edge) == IF edge.after="ReturnToCaller" THEN <<edge.after,"OutsideTraversal">> ELSE <<edge.after,TraversalOraclePhases11[edge.after]>>
TraversalEntryAndGraphChecksT11 ==
 /\ TraversalInitialT11.traversal.step=TraversalOracleEntry11 /\ TraversalInitialT11.traversal.phase="Initiation" /\ ~TraversalInitialT11.traversal.formalBegun /\ ~DuringTraversal6(TraversalInitialT11.traversal)
 /\ TraversalSteps6=TraversalOracleStepSet11 /\ TraversalOracleHidden11={}
 /\ \A step \in TraversalOracleStepSet11 : TraversalStepInfo6(step).kind=TraversalOracleKinds11[step] /\ TraversalStepInfo6(step).phase=TraversalOraclePhases11[step]
 /\ \A edge \in TraversalOracleEdges11 :
      LET f==TraversalGraphFixtureT11(edge.before,edge.decision) IN
      /\ ActualTraversalDestinationsT11(f,TRUE,TRUE)={ExpectedTraversalDestinationT11(edge)}
      /\ ActualTraversalDestinationsT11(f,FALSE,TRUE)={} /\ ActualTraversalDestinationsT11(f,TRUE,FALSE)={}
TraversalObjectsT11 == [id \in 1..4 |-> IF id=4 THEN TestObjectsT11[3] ELSE TestObjectsT11[id]]
TraversalSiteT11(player,c,a,l) == TraversalPrioritySite9(TraversalTurnT11(player),c.traversal,a,l,c)
TraversalOpeningT11(id,site) == [tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> "Paid",site |-> site,members |-> {},instances |-> EmptyT11,group |-> 0,beginning |-> NoTimingRef9,instruction |-> [id |-> 0],effectRevision |-> 0]
TraversalWindowT11(id,site) == NewPriorityWindow9(id,"Paid",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0)
ActualTraversalOptionT11(w,kind,actor,target) ==
 LET option==OptionT11(kind,actor,target) IN BeginPriorityOption9(<<w>>,<<StartPriorityOptionFrame9(w,option,200)>>,option,TraversalObjectsT11,LegalityT11(w,option),EmptyT11)
LegacyTraversalWindowT11(w) == [open |-> w.open,kind |-> w.kind,phaseId |-> w.site.structure.id,step |-> w.site.step,priority |-> w.priority]

TraversalActivationReceiptT11(w,option) == [windowId |-> w.id,reception |-> w.reception,site |-> w.site,option |-> option,transactionId |-> 200,view |-> LegacyTraversalWindowT11(w)]
TraversalActivationReceiptMatchesT11(w,c,a,l,receipt) ==
 /\ w.stage="Resolving" /\ w.busy.kind="Activation" /\ w.busy.controller="SideA"
 /\ receipt.windowId=w.id /\ receipt.reception=w.reception /\ receipt.site=w.site /\ receipt.option=w.busy /\ receipt.transactionId=w.busyTransaction
 /\ receipt.view.open=w.open /\ receipt.view.kind=w.kind /\ receipt.view.phaseId=w.site.structure.id /\ receipt.view.step=w.site.step /\ receipt.view.priority=w.busy.controller
 /\ w.site.traversalId=c.traversal.id /\ w.site.structure.id=c.traversal.phaseId /\ w.site.step=c.traversal.step
 /\ w.busy.target=ApproachedBarrier6(a,l)

TraversalWindowChecksT11 ==
 /\ \A step \in TraversalOracleStepSet11 :
      LET expected==IF step \in DOMAIN TraversalOracleWindowOptions11 THEN TraversalOracleWindowOptions11[step] ELSE [paid |-> FALSE,nonBarrierActivation |-> FALSE,approachedBarrierActivation |-> FALSE,score |-> FALSE] IN
      /\ TraversalWindowOptions6(step)=expected
      /\ \A player \in SetupPlayers :
           LET c==TraversalGraphFixtureT11(step,"Next").control a==[OpenApproach6(c.traversal) EXCEPT !.begun=TRUE] l==TraversalLayoutT11(2) site==TraversalSiteT11(player,c,a,l) IN
           /\ WindowSiteAllowed9("Paid",site)=expected.paid
           /\ (expected.paid =>
                LET w==TraversalWindowT11(1,site) first==PriorityReadyT11(w) SchemaAtom187==PriorityReadyT11(PassPriorityFrame9(first))
                    sideA==IF player="SideA" THEN first ELSE SchemaAtom187 sideB==IF player="SideB" THEN first ELSE SchemaAtom187 IN
                /\ w.priority=player /\ OpenPriorityWindow9(<<>>,<<w>>,1,"Paid",site,EmptyT11,TraversalOpeningT11(1,site),{})
                /\ ActualTraversalOptionT11(sideA,"RegularPaid","SideA",0) /\ ActualTraversalOptionT11(sideB,"RegularPaid","SideB",0)
                /\ ActualTraversalOptionT11(sideA,"Activation","SideA",1)=expected.nonBarrierActivation /\ ActualTraversalOptionT11(sideA,"Activation","SideA",2)=expected.nonBarrierActivation
                /\ ActualTraversalOptionT11(sideA,"Activation","SideA",3)=expected.approachedBarrierActivation /\ ~ActualTraversalOptionT11(sideA,"Activation","SideA",4)
                /\ ~ActualTraversalOptionT11(sideB,"Activation","SideB",1) /\ ~ActualTraversalOptionT11(sideA,"ObjectiveCompletion","SideA",0) /\ ~ActualTraversalOptionT11(sideB,"ObjectiveCompletion","SideB",0)
                /\ ~ActualTraversalOptionT11(first,"RegularPaid",(IF player="SideA" THEN "SideB" ELSE "SideA"),0)
                /\ CheckpointPriority9(<<w>>,<<first>>,PriorityCheckpointT11(w))
                /\ ~CheckpointPriority9(<<w>>,<<first>>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE])
                /\ ~CheckpointPriority9(<<w>>,<<first>>,[PriorityCheckpointT11(w) EXCEPT !.reception=99])
                /\ ~WindowSiteAllowed9("Paid",[site EXCEPT !.timingLive=FALSE]))
TraversalInitiationAndPositionChecksT11 ==
 LET b==TraversalInitialT11 a==[b EXCEPT !.announced=TRUE,!.costsPaid=TRUE,!.traversal.attacked="SchemaAtom082"]
     bp==[a EXCEPT !.traversal.step="ProcedureCodeacc82dbcc545"] funded==[bp EXCEPT !.badPubAdded=TRUE]
     begin==[funded EXCEPT !.traversal.step="ProcedureCode4d6bd06d2c9f"] begun==[begin EXCEPT !.traversal.formalBegun=TRUE]
     pos==[begun.traversal EXCEPT !.step="ProcedureCode347de0bdd6b4"] placed==[pos EXCEPT !.position="outer"]
     approachTraversal==[placed EXCEPT !.phase="Approach",!.step="ProcedureCode453e949a114f"] approach==OpenApproach6(approachTraversal) approached==[approach EXCEPT !.begun=TRUE]
     paidTraversal==[approachTraversal EXCEPT !.step="ProcedureCode3a6daf593ad4"] w==[open |-> TRUE,kind |-> "Paid",phaseId |-> 1000,step |-> "ProcedureCode3a6daf593ad4",priority |-> "SideA"]
     barrierCard==TraversalObjectsT11[3] up==[barrierCard EXCEPT !.face="Up",!.activated=TRUE]
 IN /\ AnnounceTraversalTargetSite6(b,a,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,TRUE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ ~AnnounceTraversalTargetSite6(b,a,"SchemaAtom082",[SchemaAtom082 |-> 1],FALSE,TRUE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ ~AnnounceTraversalTargetSite6(b,a,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,FALSE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ AddInitiationLiabilityMarker6(bp,funded,1,3,2) /\ ~AddInitiationLiabilityMarker6(bp,funded,1,2,2)
    /\ ~AddInitiationLiabilityMarker6([bp EXCEPT !.costsPaid=FALSE],[funded EXCEPT !.costsPaid=FALSE],1,3,2)
    /\ FormalTraversalBegin6(begin,begun,{TraversalBeginEvent6(begin.traversal)}) /\ DuringTraversal6(begun.traversal) /\ ~FormalTraversalBegin6(begin,begun,{})
    /\ ~FormalTraversalBegin6([begin EXCEPT !.badPubAdded=FALSE],[begun EXCEPT !.badPubAdded=FALSE],{TraversalBeginEvent6(begin.traversal)})
    /\ SetInitialSideBPosition6(pos,placed,TraversalLayoutT11(2),"ProcedureCode347de0bdd6b4") /\ SetInitialSideBPosition6(pos,[pos EXCEPT !.position="NoValue"],TraversalLayoutT11(0),"ProcedureCode347de0bdd6b4")
    /\ ~SetInitialSideBPosition6(pos,placed,TraversalLayoutT11(2),"ProcedureCode4d6bd06d2c9f")
    /\ BeginApproach6(approachTraversal,approach,approached,TraversalLayoutT11(2),{[tag |-> "ApproachBarrier",barrierCard |-> 3,phaseId |-> 1000,traversalId |-> 7]})
    /\ ApproachActivation6(paidTraversal,approached,TraversalLayoutT11(2),w,3,barrierCard,up,TRUE,TRUE)
    /\ ~ApproachActivation6(paidTraversal,approached,TraversalLayoutT11(2),w,3,barrierCard,up,FALSE,TRUE)
    /\ ~ApproachActivationPermission6(paidTraversal,approached,TraversalLayoutT11(2),w,4)
    /\ ~ApproachActivationPermission6(paidTraversal,approached,TraversalLayoutT11(2),[w EXCEPT !.phaseId=99],3)
    /\ ~ApproachActivationPermission6(paidTraversal,approached,TraversalLayoutT11(2),[w EXCEPT !.priority="SideB"],3)
    /\ InitiationDestination6([placed EXCEPT !.step="ProcedureCode7e3f7e5033c8"],[TraversalLayoutT11(2) EXCEPT !.slots["outer"].barrierCard=0])="Movement"
    /\ ApproachDestination6(approached,TraversalLayoutT11(2),{})="Movement"
    /\ ApproachDestination6(approached,[TraversalLayoutT11(2) EXCEPT !.slots["outer"].barrierCard=0],{3})="Movement"
TraversalEncounterAndMovementChecksT11 ==
 LET r==[TraversalGraphFixtureT11("ProcedureCode714dfe070fed","Next").control.traversal EXCEPT !.position="outer"] l==TraversalLayoutT11(2)
     e0==OpenEncounter6(1000,3,7,FALSE,"AuditTraversal",<<1,2>>) eb==[e0 EXCEPT !.stage="BeginReactions"]
     ep==[eb EXCEPT !.stage="Paid",!.paidReached=TRUE] es==[ep EXCEPT !.stage="BarrierInstructions"]
     one==[es EXCEPT !.resolved={1}] both==[one EXCEPT !.resolved={1,2}] done==[both EXCEPT !.stage="Complete"]
     m0==OpenMovement6(r,"Encounter",3,1000,TRUE) m1==[m0 EXCEPT !.begun=TRUE,!.passedBarrier=3]
     decisionTraversal==[r EXCEPT !.step="ProcedureCode9bca3a096549"] declined==[m1 EXCEPT !.declined=TRUE]
     advanceTraversal==[r EXCEPT !.step="ProcedureCoded4ddeafb5f2f"] inward==[advanceTraversal EXCEPT !.position="inner"]
 IN /\ BeginEncounter6(e0,eb,TRUE,{[tag |-> "EncounterBarrier",encounterId |-> 1000,barrierCard |-> 3,traversalId |-> 7]})
    /\ BeginEncounterPaid6(eb,ep,TRUE,{}) /\ ~BeginEncounterPaid6(eb,ep,FALSE,{})
    /\ CloseEncounterPaid6(ep,es,TRUE) /\ ~CloseEncounterPaid6(ep,es,FALSE)
    /\ TraversalOracleSuppressInstructionSteps11={"ProcedureCode8b3260c0010f"}
    /\ LET c==TraversalGraphFixtureT11("ProcedureCode8b3260c0010f","Next").control a==[OpenApproach6(c.traversal) EXCEPT !.begun=TRUE]
            w==PriorityReadyT11(TraversalWindowT11(1,TraversalSiteT11("SideB",c,a,l)))
            barrierInstructionSuppressed==[ep EXCEPT !.barrierInstructionSuppressed={1},!.barrierInstructionSuppressedBy[1]=700] IN
         /\ PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,LegacyTraversalWindowT11(w),{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,[LegacyTraversalWindowT11(w) EXCEPT !.step="ProcedureCode4f60245a1dde"],{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,[LegacyTraversalWindowT11(w) EXCEPT !.phaseId=99],{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,[LegacyTraversalWindowT11(w) EXCEPT !.priority="SideA"],{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,LegacyTraversalWindowT11(w),{1},700,FALSE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,LegacyTraversalWindowT11(w),{1},700,TRUE,FALSE,{})
    /\ NextEncounterSub6(es)=1 /\ ResolveEncounterSub6(es,one,1,TRUE) /\ NextEncounterSub6(one)=2
    /\ ~ResolveEncounterSub6(es,[es EXCEPT !.resolved={2}],2,TRUE) /\ ~ResolveEncounterSub6(es,one,1,FALSE)
    /\ ~ResolveEncounterSub6(one,one,1,TRUE) /\ ResolveEncounterSub6(one,both,2,TRUE) /\ NextEncounterSub6(both)=0
    /\ CompleteEncounter6(both,done,TRUE) /\ ~CompleteEncounter6(one,[one EXCEPT !.stage="Complete"],TRUE)
    /\ ~CompleteEncounter6(both,done,FALSE)
    /\ MovementPassEvents6(r,l)={[tag |-> "PassBarrier",traversalId |-> 7,phaseId |-> 1000,barrierCard |-> 3]}
    /\ MovementPassEvents6([r EXCEPT !.position="NoValue"],l)={}
    /\ MovementPassEvents6(r,[l EXCEPT !.slots["outer"].barrierCard=0])={}
    /\ MovementPassEvents6([r EXCEPT !.position="inner"],l)={[tag |-> "PassBarrier",traversalId |-> 7,phaseId |-> 1000,barrierCard |-> 4],[tag |-> "PassAllBarrier",traversalId |-> 7,phaseId |-> 1000,barrierCard |-> 4]}
    /\ BeginMovement6(r,m0,m1,l,MovementPassEvents6(r,l))
    /\ DeclineMovementWithdrawTraversal6(decisionTraversal,m1,declined,TRUE) /\ ~DeclineMovementWithdrawTraversal6(decisionTraversal,m1,declined,FALSE)
    /\ AdvanceMovement6(advanceTraversal,inward,declined,[declined EXCEPT !.advanced=TRUE,!.movedToNew=TRUE],l,l)
    /\ NextInwardPosition6(l,"SchemaAtom082","inner")="NoValue" /\ NextInwardPosition6(l,"SchemaAtom082","outer")="inner"
    /\ ~AdvanceMovement6(advanceTraversal,inward,m1,[m1 EXCEPT !.advanced=TRUE,!.movedToNew=TRUE],l,l)
TraversalSuccessAndEndChecksT11 ==
 LET c==TraversalGraphFixtureT11("ProcedureCodebbb14496b09b","Next").control s==[c EXCEPT !.declarationProcessed=FALSE,!.traversal.successful=FALSE]
     declared==[s EXCEPT !.declarationProcessed=TRUE,!.traversal.successful=TRUE]
     prevented==[s EXCEPT !.declarationProcessed=TRUE] b==[declared EXCEPT !.traversal.step="ProcedureCoded75d879e00ff"] chosen==[b EXCEPT !.siteInspectionChosen=TRUE]
     bf==[b EXCEPT !.siteInspectionChosen=FALSE,!.siteInspectionFinished=FALSE] bc==[bf EXCEPT !.siteInspectionChosen=TRUE]
     directive==[kind |-> "Inspection",choice |-> "Inspection",traversalId |-> 7,targetSite |-> "SchemaAtom082",origin |-> "RulesTraversalInspection"]
     end==[TraversalGraphFixtureT11("ProcedureCode6ea937bb44ac","Next").control EXCEPT !.windowsDone=FALSE,!.fundReturned=FALSE,!.resultDeclared=FALSE]
     wd==[end EXCEPT !.windowsDone=TRUE] fund==[wd EXCEPT !.traversal.step="ProcedureCode84dea7dc8ecc"] fr==[fund EXCEPT !.fundReturned=TRUE]
     result==[fr EXCEPT !.traversal.step="ProcedureCode5e397645e65c"] aDrawPile==[result EXCEPT !.resultDeclared=TRUE,!.traversal.unsuccessful=TRUE]
     last==[aDrawPile EXCEPT !.traversal.step="ProcedureCode9606a4cd52b4"] completed==[last EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds={1000}]
     events=={[tag |-> "TraversalEnds",traversalId |-> 7],TraversalPhaseEndEvent6(last.traversal)}
 IN /\ DeclareSuccessfulTraversal6(s,declared,TRUE,{[tag |-> "SuccessfulTraversal",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ DeclareSuccessfulTraversal6(s,prevented,FALSE,{}) /\ ~ShouldDeclareUnsuccessful6(prevented.traversal,[SchemaAtom082 |-> 1])
    /\ ChooseRulesInspection6(bf,bc,"Inspection",{"Inspection"},TRUE,directive) /\ ~ChooseRulesInspection6(bf,bc,"Inspection",{"Inspection"},FALSE,directive)
    /\ FinishRulesInspectionInstruction6(bc,[bc EXCEPT !.siteInspectionFinished=TRUE],TRUE)
    /\ ~FinishRulesInspectionInstruction6(bc,[bc EXCEPT !.siteInspectionFinished=TRUE],FALSE)
    /\ FinishTraversalEndWindows6(end,wd) /\ ReturnLiabilityMarkerFund6(fund,fr,3,0,10,13)
    /\ ~ReturnLiabilityMarkerFund6([fund EXCEPT !.windowsDone=FALSE],[fr EXCEPT !.windowsDone=FALSE],3,0,10,13)
    /\ ~ReturnLiabilityMarkerFund6(fund,fr,3,1,10,12)
    /\ DeclareUnsuccessfulTraversal6(result,aDrawPile,[SchemaAtom082 |-> 1],{[tag |-> "UnsuccessfulTraversal",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ ~ShouldDeclareUnsuccessful6(result.traversal,EmptyT11)
    /\ DuringTraversal6(last.traversal) /\ CompleteTraversal6(last,completed,TRUE,events,{7}) /\ ~DuringTraversal6(completed.traversal)
    /\ ~CompleteTraversal6(last,completed,FALSE,events,{7})
    /\ ReturnTraversalToCaller6(completed,[completed EXCEPT !.returned=TRUE],TRUE,"AuditCaller")
    /\ ~ReturnTraversalToCaller6(completed,[completed EXCEPT !.returned=TRUE],FALSE,"AuditCaller")
    /\ ~ReturnTraversalToCaller6(completed,[completed EXCEPT !.returned=TRUE],TRUE,"WrongCaller")
TraversalCleanupAndAdapterChecksT11 ==
 LET paid==[id |-> 1,kind |-> "Paid",open |-> TRUE,beginPhaseId |-> 0,pending |-> {},lostPending |-> {},priority |-> "SideB"]
     begin==[paid EXCEPT !.id=2,!.kind="Reaction",!.beginPhaseId=1000,!.pending={1,2}]
     other==[paid EXCEPT !.id=3,!.kind="Reaction",!.pending={3}]
     pc==[paid EXCEPT !.open=FALSE,!.priority="NoValue"] bc==[begin EXCEPT !.open=FALSE,!.pending={},!.lostPending={1,2},!.priority="NoValue"] oc==[other EXCEPT !.open=FALSE,!.pending={},!.priority="NoValue"]
     c==TraversalGraphFixtureT11("ProcedureCode3a6daf593ad4","Next").control a==[OpenApproach6(c.traversal) EXCEPT !.begun=TRUE] l==TraversalLayoutT11(2)
     w==PriorityReadyT11(PassPriorityFrame9(PriorityReadyT11(TraversalWindowT11(1,TraversalSiteT11("SideB",c,a,l))))) option==OptionT11("Activation","SideA",3)
     resolving==StartPriorityOptionFrame9(w,option,200) receipt==TraversalActivationReceiptT11(w,option)
     forced==[OpenEncounter6(900,3,7,TRUE,"ExactChildCaller",<<>>) EXCEPT !.stage="Complete"]
 IN /\ ProcessTraversalEndWindow6(<<paid>>,<<>>,pc,FALSE,{},{}) /\ ~ProcessTraversalEndWindow6(<<paid>>,<<>>,pc,TRUE,{1},{})
    /\ ProcessTraversalEndWindow6(<<begin>>,<<>>,bc,FALSE,{},{}) /\ ~ProcessTraversalEndWindow6(<<begin>>,<<>>,bc,TRUE,{1},{})
    /\ ProcessTraversalEndWindow6(<<other>>,<<>>,oc,TRUE,{3},{}) /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,oc,FALSE,{},{})
    /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,oc,TRUE,{3},{"NewStructure"})
    /\ BeginPriorityOption9(<<w>>,<<resolving>>,option,TraversalObjectsT11,LegalityT11(w,option),EmptyT11)
    /\ resolving.priority="NoValue" /\ receipt.view.priority="SideA"
    /\ TraversalActivationReceiptMatchesT11(resolving,c,a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.windowId=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.reception=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.site.turnId=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.option.target=4])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.transactionId=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,[c EXCEPT !.traversal.id=99],a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11(resolving,[c EXCEPT !.traversal.phaseId=99],a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11(resolving,[c EXCEPT !.traversal.step="ProcedureCode4d474d346807"],a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11([resolving EXCEPT !.busy.target=4],c,a,l,receipt)
    /\ ReturnForcedEncounter6(<<forced>>,<<>>,c.traversal,c.traversal,"ExactChildCaller",{},{900})
    /\ ~ReturnForcedEncounter6(<<forced>>,<<>>,c.traversal,c.traversal,"WrongChildCaller",{},{900})
TraversalPointwiseInitT11 == guideCaseT11 \in 1..6 /\ qT11=EmptyT11
TraversalPointwiseSpecT11 == TraversalPointwiseInitT11 /\ [][PointwiseNextT11]_<<guideCaseT11,qT11>>


                                                                             
                                                                                  
TraversalItemActivatedT11(objects) == {id \in DOMAIN objects : objects[id].deployed /\ objects[id].kind="Barrier" /\ objects[id].activated}
TraversalTraceCandidatesT11(c) ==
 {TraversalPostFrameT11(c,step,TraversalStepInfo6(step).phase,IF TraversalStepInfo6(step).phase=c.traversal.phase THEN c.traversal.phaseId ELSE c.traversal.phaseId+1) : step \in TraversalSteps6}
TraversalDecisionT11(s) ==
 CASE s.control.traversal.step="ProcedureCode7e3f7e5033c8" -> IF s.control.traversal.position \in DOMAIN s.layout.slots /\ s.layout.slots[s.control.traversal.position].barrierCard#0 THEN "Barrier" ELSE "NoBarrier"
 [] s.control.traversal.step="ProcedureCode4d474d346807" -> IF ApproachedBarrier6(s.approach,s.layout) \in TraversalItemActivatedT11(s.objects) THEN "ItemActivated" ELSE "NoEncounter"
 [] s.control.traversal.step="ProcedureCodef1914978bb8e" -> IF s.work.resolvedSub#0 THEN "BarrierInstruction" ELSE "NoBarrierInstruction"
 [] s.control.traversal.step="ProcedureCode9bca3a096549" -> s.work.jackChoice
 [] s.control.traversal.step="ProcedureCode6c5d14f545f7" -> IF s.movement.movedToNew THEN "NewPosition" ELSE "NoPosition"
 [] OTHER -> "Next"
TraversalAuditDoneT11 == qT11.control.returned
TraversalAuditInitT11 ==
 /\ guideCaseT11=8
 /\ \E n \in 0..2 : \E activationPlan \in SUBSET OccupiedBarrier6(TraversalLayoutT11(n)),order \in {<<>>,<<1,2>>},jack \in BOOLEAN,fund \in {0,1} :
      LET l==TraversalLayoutT11(n) r==TraversalInitialT11.traversal IN
      qT11=[control |-> TraversalInitialT11,layout |-> l,objects |-> [id \in 1..4 |-> IF id \in {3,4} \ OccupiedBarrier6(l) THEN [TraversalObjectsT11[id] EXCEPT !.deployed=FALSE,!.zone="SideAHand"] ELSE TraversalObjectsT11[id]],
        approach |-> OpenApproach6(r),encounter |-> OpenEncounter6(0,0,7,FALSE,"AuditTraversal",order),movement |-> OpenMovement6(r,"Initiation",0,0,TRUE),
        order |-> order,activationPlan |-> activationPlan,jack |-> jack,initialFund |-> fund,fund |-> fund,bank |-> 12,
        stack |-> <<>>,windows |-> <<>>,nextWindow |-> 1,usedWindows |-> {},optionDone |-> FALSE,activationReceipt |-> EmptyT11,pendingEvents |-> {},
        ready |-> FALSE,drained |-> FALSE,specialJump |-> FALSE,pendingStep |-> "NoValue",pendingPhase |-> 0,
        work |-> TraversalWorkT11("Continue",0),history |-> <<>>,edges |-> <<>>,events |-> <<>>,checkpoints |-> <<>>,expired |-> {}]
TraversalRecordWorkT11(before,after,events) ==
 [after EXCEPT !.ready=TRUE,!.drained=FALSE,!.pendingStep=before.control.traversal.step,!.pendingPhase=before.control.traversal.phaseId,
   !.history=Append(@,[step |-> before.control.traversal.step,kind |-> TraversalStepInfo6(before.control.traversal.step).kind,phaseId |-> before.control.traversal.phaseId,
     events |-> events,position |-> before.control.traversal.position,barrierCard |-> MovementBarrier6(before.control.traversal,before.layout),selectedSub |-> after.work.resolvedSub,reachedSuccess |-> before.control.traversal.reachedSuccess,targetSiteExists |-> before.control.traversal.attacked \in DOMAIN before.layout.orders]),
   !.events=Append(@,events)]
TraversalRecordEdgeT11(before,after,target) ==
 [after EXCEPT !.edges=Append(@,[before |-> before.control.traversal.step,after |-> target,decision |-> TraversalDecisionT11(before),phaseId |-> before.control.traversal.phaseId])]
TraversalAuditWorkT11 ==
 /\ ~TraversalAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>>
 /\ LET c==qT11.control r==c.traversal kind==TraversalStepInfo6(r.step).kind IN
    CASE kind="AnnounceAndPay" ->
      LET g==[c EXCEPT !.traversal.attacked="SchemaAtom082",!.announced=TRUE,!.costsPaid=TRUE] ev=={[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> r.id,targetSite |-> "SchemaAtom082"]} IN
      /\ AnnounceTraversalTargetSite6(c,g,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,TRUE,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="LiabilityMarker" ->
      LET g==[c EXCEPT !.badPubAdded=TRUE] IN
      /\ AddInitiationLiabilityMarker6(c,g,qT11.fund,qT11.fund+2,2)
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g,!.fund=@+2,!.bank=@-2],{})
    [] kind="TraversalBegins" ->
      LET g==[c EXCEPT !.traversal.formalBegun=TRUE] ev=={TraversalBeginEvent6(r)} IN
      /\ FormalTraversalBegin6(c,g,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="InitialPosition" ->
      LET g==[r EXCEPT !.position=OutermostOccupiedPosition6(qT11.layout,r.attacked)] IN
      /\ SetInitialSideBPosition6(r,g,qT11.layout,r.step) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control.traversal=g],{})
    [] kind="ApproachBarrier" ->
      LET a==[qT11.approach EXCEPT !.begun=TRUE] ev=={[tag |-> "ApproachBarrier",barrierCard |-> ApproachedBarrier6(a,qT11.layout),phaseId |-> r.phaseId,traversalId |-> r.id]} IN
      /\ BeginApproach6(r,qT11.approach,a,qT11.layout,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.approach=a],ev)
    [] kind="EncounterBarrier" ->
      LET e==[qT11.encounter EXCEPT !.stage="BeginReactions"] ev=={[tag |-> "EncounterBarrier",encounterId |-> e.id,barrierCard |-> e.barrierCard,traversalId |-> e.traversalId]} IN
      /\ BeginEncounter6(qT11.encounter,e,TRUE,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.encounter=e],ev)
    [] kind="NextBarrierInstruction" ->
      LET sub==NextEncounterSub6(qT11.encounter) e==IF sub=0 THEN qT11.encounter ELSE [qT11.encounter EXCEPT !.resolved=@ \cup {sub}] IN
      /\ (sub=0 \/ ResolveEncounterSub6(qT11.encounter,e,sub,TRUE))
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.encounter=e,!.work.resolvedSub=sub],{})
    [] kind="PassBarrier" ->
      LET m==[qT11.movement EXCEPT !.begun=TRUE,!.passedBarrier=MovementBarrier6(r,qT11.layout),!.passedAll=MovementBarrier6(r,qT11.layout)#0 /\ NextInwardPosition6(qT11.layout,r.attacked,r.position)="NoValue"] ev==MovementPassEvents6(r,qT11.layout) IN
      /\ BeginMovement6(r,qT11.movement,m,qT11.layout,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.movement=m],ev)
    [] kind="WithdrawTraversalDecision" ->
      IF qT11.jack THEN
        LET g==[EndTraversalOutcome6(c,r.phaseId+1) EXCEPT !.traversal.withdrewTraversal=TRUE] ev==EndTraversalEffectEvents6(c)
            before==[qT11 EXCEPT !.work.jackChoice="WithdrawTraversal"] next==[before EXCEPT !.control=g,!.specialJump=TRUE] IN
        /\ MovementWithdrawTraversal6(c,g,qT11.movement,qT11.layout,qT11.layout,r.phaseId+1,TRUE,TRUE,TRUE,ev)
        /\ qT11'=TraversalRecordEdgeT11(before,TraversalRecordWorkT11(before,next,ev),"ProcedureCode6ea937bb44ac")
      ELSE LET m==[qT11.movement EXCEPT !.declined=TRUE] IN
        /\ DeclineMovementWithdrawTraversal6(r,qT11.movement,m,TRUE)
        /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.movement=m,!.work.jackChoice="Continue"],{})
    [] kind="AdvancePosition" ->
      LET g==[r EXCEPT !.position=NextInwardPosition6(qT11.layout,r.attacked,r.position)] m==[qT11.movement EXCEPT !.advanced=TRUE,!.movedToNew=g.position#"NoValue"] IN
      /\ AdvanceMovement6(r,g,qT11.movement,m,qT11.layout,qT11.layout)
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control.traversal=g,!.movement=m],{})
    [] kind="ApproachTargetSite" ->
      LET m==[qT11.movement EXCEPT !.approachedTargetSite=TRUE] ev=={[tag |-> "ApproachTargetSite",traversalId |-> r.id,targetSite |-> r.attacked,phaseId |-> r.phaseId]} IN
      /\ ApproachTargetSite6(r,qT11.movement,m,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.movement=m],ev)
    [] kind="DeclareSuccessful" ->
      LET g==[c EXCEPT !.declarationProcessed=TRUE,!.traversal.successful=TRUE] ev=={[tag |-> "SuccessfulTraversal",traversalId |-> r.id,targetSite |-> r.attacked]} IN
      /\ DeclareSuccessfulTraversal6(c,g,TRUE,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="RulesInspection" ->
      IF ~c.siteInspectionChosen THEN
        LET g==[c EXCEPT !.siteInspectionChosen=TRUE] directive==[kind |-> "Inspection",choice |-> "Inspection",traversalId |-> r.id,targetSite |-> r.attacked,origin |-> "RulesTraversalInspection"] IN
        /\ ChooseRulesInspection6(c,g,"Inspection",{"Inspection"},TRUE,directive) /\ qT11'=[qT11 EXCEPT !.control=g]
      ELSE LET g==[c EXCEPT !.siteInspectionFinished=TRUE] IN
        /\ FinishRulesInspectionInstruction6(c,g,TRUE) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],{})
    [] kind="EndWindows" ->
      LET g==[c EXCEPT !.windowsDone=TRUE] IN
      /\ FinishTraversalEndWindows6(c,g) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],{})
    [] kind="ReturnLiabilityMarker" ->
      LET g==[c EXCEPT !.fundReturned=TRUE] IN
      /\ ReturnLiabilityMarkerFund6(c,g,qT11.fund,0,qT11.bank,qT11.bank+qT11.fund)
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g,!.bank=@+qT11.fund,!.fund=0],{})
    [] kind="DeclareUnsuccessful" ->
      LET applies==ShouldDeclareUnsuccessful6(r,[SchemaAtom082 |-> 1]) g==[c EXCEPT !.resultDeclared=TRUE,!.traversal.unsuccessful=applies]
          ev==IF applies THEN {[tag |-> "UnsuccessfulTraversal",traversalId |-> r.id,targetSite |-> r.attacked]} ELSE {} IN
      /\ DeclareUnsuccessfulTraversal6(c,g,[SchemaAtom082 |-> 1],ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="CompleteTraversal" ->
      LET g==[c EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds=@ \cup {r.phaseId}] ev=={[tag |-> "TraversalEnds",traversalId |-> r.id],TraversalPhaseEndEvent6(r)} IN
      /\ CompleteTraversal6(c,g,TRUE,ev,{r.id}) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g,!.expired={r.id}],ev)
    [] kind="CompletePhase" /\ r.phase="Encounter" ->
      LET e==[qT11.encounter EXCEPT !.stage="Complete"] IN
      /\ CompleteEncounter6(qT11.encounter,e,TRUE) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.encounter=e],{})
    [] kind \in {"CompletePhase","BarrierInstructionLoop","MovementBranch"} -> qT11'=TraversalRecordWorkT11(qT11,qT11,{})
    [] OTHER -> FALSE
TraversalAuditWindowOpenT11 ==
 /\ ~TraversalAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>> /\ TraversalStepInfo6(qT11.control.traversal.step).kind="PaidWindow"
 /\ LET c==qT11.control e==qT11.encounter
        paid==WithFullySuppressInstruction6([e EXCEPT !.stage="Paid",!.paidReached=TRUE])
        site==TraversalSiteT11("SideB",c,qT11.approach,qT11.layout) id==qT11.nextWindow w==TraversalWindowT11(id,site) IN
    /\ (c.traversal.phase#"Encounter" \/ BeginEncounterPaid6(e,paid,TRUE,NewFullySuppressInstructionEvents6(e,paid)))
    /\ OpenPriorityWindow9(<<>>,<<w>>,id,"Paid",site,EmptyT11,TraversalOpeningT11(id,site),qT11.usedWindows)
    /\ qT11'=[qT11 EXCEPT !.stack= <<w>>,!.control.paidOpen=TRUE,!.nextWindow=@+1,!.usedWindows=@ \cup {id},!.optionDone=FALSE,
         !.encounter=IF c.traversal.phase="Encounter" THEN paid ELSE @,!.pendingEvents=IF c.traversal.phase="Encounter" THEN NewFullySuppressInstructionEvents6(e,paid) ELSE {}]
TraversalPaymentT11(w) == [tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> w.busyTransaction,allTriggerCostsPaid |-> TRUE,costCheckpointAndReactionsDrained |-> TRUE]
TraversalOptionReturnT11(w,done) == [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> w.busyTransaction,triggerPayment |-> TraversalPaymentT11(w),allCostsPaid |-> TRUE,optionComplete |-> done,childrenReturned |-> TRUE,reactionsDrained |-> TRUE]
TraversalAuditWindowStepT11 ==
 /\ ~TraversalAuditDoneT11 /\ ~qT11.ready /\ Len(qT11.stack)=1
 /\ LET w==WindowTop9(qT11.stack) barrierCard==ApproachedBarrier6(qT11.approach,qT11.layout)
        wantActivation==w.site.step="ProcedureCode3a6daf593ad4" /\ w.priority="SideA" /\ barrierCard \in qT11.activationPlan /\ ~qT11.objects[barrierCard].activated IN
    \/ /\ w.stage="NeedCheckpoint" /\ CheckpointPriority9(qT11.stack,<<PriorityReadyT11(w)>>,PriorityCheckpointT11(w))
       /\ qT11'=[qT11 EXCEPT !.stack= <<PriorityReadyT11(w)>>]
    \/ /\ w.stage="Ready" /\ wantActivation
       /\ LET option==OptionT11("Activation","SideA",barrierCard) next==StartPriorityOptionFrame9(w,option,200) IN
          /\ BeginPriorityOption9(qT11.stack,<<next>>,option,qT11.objects,LegalityT11(w,option),EmptyT11)
          /\ qT11'=[qT11 EXCEPT !.stack= <<next>>,!.optionDone=FALSE,!.activationReceipt=TraversalActivationReceiptT11(w,option)]
    \/ /\ w.stage="Resolving" /\ ~qT11.optionDone
       /\ TraversalActivationReceiptMatchesT11(w,qT11.control,qT11.approach,qT11.layout,qT11.activationReceipt)
       /\ LET card==qT11.objects[w.busy.target] after==[card EXCEPT !.face="Up",!.activated=TRUE] IN
          /\ ApproachActivation6(qT11.control.traversal,qT11.approach,qT11.layout,qT11.activationReceipt.view,w.busy.target,card,after,TRUE,TRUE)
          /\ qT11'=[qT11 EXCEPT !.objects[w.busy.target]=after,!.optionDone=TRUE]
    \/ /\ w.stage="Resolving" /\ qT11.optionDone
       /\ CompletePriorityOption9(qT11.stack,<<CompletePriorityOptionFrame9(w)>>,TraversalOptionReturnT11(w,qT11.optionDone))
       /\ qT11'=[qT11 EXCEPT !.stack= <<CompletePriorityOptionFrame9(w)>>]
    \/ /\ w.stage="Ready" /\ ~wantActivation
       /\ PassPriority9(qT11.stack,<<PassPriorityFrame9(w)>>,w.priority,[id |-> 0])
       /\ qT11'=[qT11 EXCEPT !.stack= <<PassPriorityFrame9(w)>>]
    \/ /\ w.stage="Closed" /\ PopClosedPriorityWindow9(qT11.stack,<<>>)
       /\ LET e==qT11.encounter after==[e EXCEPT !.stage="BarrierInstructions"] IN
          /\ (w.site.step#"ProcedureCode8b3260c0010f" \/ CloseEncounterPaid6(e,after,TRUE))
          /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.stack= <<>>,!.control.paidOpen=FALSE,!.windows=Append(@,qT11.control.traversal.step),!.encounter=IF w.site.step="ProcedureCode8b3260c0010f" THEN after ELSE @],qT11.pendingEvents)
TraversalPhaseEndCandidateT11(c) == [c EXCEPT !.phaseEndedIds=@ \cup {c.traversal.phaseId}]
TraversalPhaseAndLastSubChecksT11 ==
 LET f==TraversalGraphFixtureT11("ProcedureCode7e3f7e5033c8","Barrier") b==f.control ended==TraversalPhaseEndCandidateT11(b)
     g==TraversalPostFrameT11(ended,"ProcedureCode453e949a114f","Approach",1001) missing==TraversalPostFrameT11(b,"ProcedureCode453e949a114f","Approach",1001)
     stale==TraversalPostFrameT11(ended,"ProcedureCode453e949a114f","Approach",1000)
     sub==[TraversalGraphFixtureT11("ProcedureCodef1914978bb8e","BarrierInstruction") EXCEPT !.encounter=[OpenEncounter6(1000,3,7,FALSE,"AuditTraversal",<<1>>) EXCEPT !.stage="BarrierInstructions",!.paidReached=TRUE,!.resolved={1}]]
 IN /\ BeginNormalTraversalPhaseEnd6(b,ended,f.layout,f.activated,f.encounter,f.movement,f.work,TRUE,{TraversalPhaseEndEvent6(b.traversal)})
    /\ ~BeginNormalTraversalPhaseEnd6(ended,ended,f.layout,f.activated,f.encounter,f.movement,f.work,TRUE,{TraversalPhaseEndEvent6(b.traversal)})
    /\ ~AdvanceNormalTraversalStep6(b,missing,f.layout,f.activated,f.encounter,f.movement,f.work,1001,TRUE,TRUE,{})
    /\ AdvanceNormalTraversalStep6(ended,g,f.layout,f.activated,f.encounter,f.movement,f.work,1001,TRUE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6(ended,stale,f.layout,f.activated,f.encounter,f.movement,f.work,1000,TRUE,TRUE,{})
    /\ ActualTraversalDestinationsT11(sub,TRUE,TRUE)={<<"ProcedureCodeaa0828fbf852","Encounter">>}
    /\ TraversalPhaseEndEvent6(b.traversal)=[tag |-> "PhaseEnds",phase |-> b.traversal.phase,phaseId |-> b.traversal.phaseId,traversalId |-> b.traversal.id]

TraversalCanEndPhaseT11(s) == BeginNormalTraversalPhaseEnd6(s.control,TraversalPhaseEndCandidateT11(s.control),s.layout,TraversalItemActivatedT11(s.objects),s.encounter,s.movement,s.work,s.ready,{TraversalPhaseEndEvent6(s.control.traversal)})
TraversalAuditPhaseEndT11 ==
 /\ qT11.ready /\ ~qT11.drained /\ TraversalCanEndPhaseT11(qT11)
 /\ qT11'=[qT11 EXCEPT !.control=TraversalPhaseEndCandidateT11(qT11.control),!.events=Append(@,{TraversalPhaseEndEvent6(qT11.control.traversal)})]
TraversalAuditDrainT11 ==
 /\ qT11.ready /\ ~qT11.drained /\ ~TraversalCanEndPhaseT11(qT11)
 /\ qT11'=[qT11 EXCEPT !.drained=TRUE,!.checkpoints=Append(@,[step |-> qT11.pendingStep,phaseId |-> qT11.pendingPhase,
     insidePhase |-> qT11.pendingPhase \notin qT11.control.phaseEndedIds,insideTraversal |-> DuringTraversal6(qT11.control.traversal)])]
TraversalViewJoinT11(c,g,a,e,m,l,activated) ==
 CASE c.traversal.step="ProcedureCode7e3f7e5033c8" -> CompleteInitiationTraversalView6(c.traversal,g.traversal,l,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCode4d474d346807" -> CompleteApproachTraversalView6(c.traversal,g.traversal,a,l,activated,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCode687f72772ab1" -> CompleteOrdinaryEncounterTraversalView6(c.traversal,g.traversal,e,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCodea732fbc12ae0" \/ (c.traversal.step="ProcedureCode6c5d14f545f7" /\ m.movedToNew) -> CompleteMovementTraversalView6(c.traversal,g.traversal,m,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCodec7b41615d673" -> CompleteSuccessTraversalView6([traversal |-> c.traversal,siteInspectionFinished |-> c.siteInspectionFinished],[traversal |-> g.traversal,siteInspectionFinished |-> g.siteInspectionFinished],g.traversal.phaseId,TRUE)
 [] OTHER -> TRUE
TraversalAuditAdvanceT11 ==
 /\ qT11.ready /\ qT11.drained /\ ~qT11.specialJump /\ ~qT11.control.traversal.complete /\ qT11.stack= <<>>
 /\ \E g \in TraversalTraceCandidatesT11(qT11.control) :
      /\ AdvanceNormalTraversalStep6(qT11.control,g,qT11.layout,TraversalItemActivatedT11(qT11.objects),qT11.encounter,qT11.movement,qT11.work,g.traversal.phaseId,qT11.ready,qT11.drained,{})
      /\ TraversalViewJoinT11(qT11.control,g,qT11.approach,qT11.encounter,qT11.movement,qT11.layout,TraversalItemActivatedT11(qT11.objects))
      /\ qT11'=TraversalRecordEdgeT11(qT11,[qT11 EXCEPT !.control=g,!.ready=FALSE,!.drained=FALSE,!.pendingEvents={},
           !.approach=IF g.traversal.phase="Approach" /\ g.traversal.phaseId#qT11.control.traversal.phaseId THEN OpenApproach6(g.traversal) ELSE @,
           !.encounter=IF g.traversal.phase="Encounter" /\ g.traversal.phaseId#qT11.control.traversal.phaseId THEN OpenEncounter6(g.traversal.phaseId,ApproachedBarrier6(qT11.approach,qT11.layout),g.traversal.id,FALSE,"AuditTraversal",qT11.order) ELSE @,
           !.movement=IF g.traversal.phase="Movement" /\ g.traversal.phaseId#qT11.control.traversal.phaseId THEN OpenMovement6(g.traversal,qT11.control.traversal.phase,IF qT11.control.traversal.phase="Encounter" THEN qT11.encounter.barrierCard ELSE IF qT11.control.traversal.phase="Approach" THEN ApproachedBarrier6(qT11.approach,qT11.layout) ELSE 0,IF qT11.control.traversal.phase="Encounter" THEN qT11.encounter.id ELSE 0,TRUE) ELSE @],g.traversal.step)
TraversalAuditAfterJackT11 ==
 /\ qT11.ready /\ qT11.drained /\ qT11.specialJump
 /\ qT11'=[qT11 EXCEPT !.ready=FALSE,!.drained=FALSE,!.specialJump=FALSE]
TraversalAuditReturnT11 ==
 /\ qT11.ready /\ qT11.drained /\ qT11.control.traversal.complete /\ ~TraversalAuditDoneT11
 /\ LET c==[qT11.control EXCEPT !.returned=TRUE] IN
      /\ ReturnTraversalToCaller6(qT11.control,c,qT11.drained,"AuditCaller")
      /\ qT11'=TraversalRecordEdgeT11(qT11,[qT11 EXCEPT !.control=c],"ReturnToCaller")
TraversalAuditNextT11 == /\ UNCHANGED guideCaseT11
 /\ (TraversalAuditWorkT11 \/ TraversalAuditWindowOpenT11 \/ TraversalAuditWindowStepT11 \/ TraversalAuditPhaseEndT11 \/ TraversalAuditDrainT11 \/ TraversalAuditAdvanceT11 \/ TraversalAuditAfterJackT11 \/ TraversalAuditReturnT11 \/ (TraversalAuditDoneT11 /\ UNCHANGED qT11))
TraversalAuditSpecT11 == TraversalAuditInitT11 /\ [][TraversalAuditNextT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(TraversalAuditNextT11)
TraversalFormalConditionsT11(events) == UNION
 {CASE e.tag="TraversalBegins" -> {"TraversalBegins"} \cup (IF e.alsoInitiates THEN {"TraversalInitiated"} ELSE {})
  [] e.tag="ApproachBarrier" -> {"ApproachBarrierBegins"} [] e.tag="EncounterBarrier" -> {"EncounterBarrierBegins"}
  [] e.tag="PassBarrier" -> {"PassBarrier"} [] e.tag="PassAllBarrier" -> {"PassAllProtectingBarrier"}
  [] e.tag="ApproachTargetSite" -> {"ApproachTargetSite"} [] e.tag="SuccessfulTraversal" -> {"SuccessfulTraversal"}
  [] e.tag="UnsuccessfulTraversal" -> {"UnsuccessfulTraversal"} [] e.tag="TraversalEnds" -> {"TraversalEnds"} [] OTHER -> {} : e \in events}
TraversalExpectedFormalT11(row,layout) ==
 IF row.step="ProcedureCode714dfe070fed" THEN IF row.barrierCard=0 THEN {} ELSE {"PassBarrier"} \cup (IF row.position=Head(layout.orders["SchemaAtom082"]) THEN {"PassAllProtectingBarrier"} ELSE {})
 ELSE IF row.step="ProcedureCode5e397645e65c" THEN IF ~row.reachedSuccess /\ row.targetSiteExists THEN {"UnsuccessfulTraversal"} ELSE {}
 ELSE IF row.step \in DOMAIN TraversalOracleFormalConditions11 THEN TraversalOracleFormalConditions11[row.step] ELSE {}
TraversalAuditInvariantT11 ==
 /\ guideCaseT11=8 /\ TraversalFrameValid6(qT11.control.traversal) /\ SideBPositionValid6(qT11.control.traversal,qT11.layout)
 /\ qT11.bank+qT11.fund=12+qT11.initialFund /\ qT11.bank \in Nat /\ qT11.fund \in Nat
 /\ Len(qT11.edges)<=Len(qT11.history)
 /\ \A i \in 1..Len(qT11.edges) :
      /\ qT11.edges[i] \in {[before |-> e.before,after |-> e.after,decision |-> e.decision,phaseId |-> qT11.edges[i].phaseId] : e \in TraversalOracleEdges11}
      /\ qT11.edges[i].before=qT11.history[i].step
      /\ (qT11.edges[i].before="ProcedureCodef1914978bb8e" => (qT11.edges[i].decision="BarrierInstruction")=(qT11.history[i].selectedSub#0))
 /\ \A i \in 1..Len(qT11.history) :
      LET row==qT11.history[i] IN
      /\ row.kind=TraversalOracleKinds11[row.step]
      /\ TraversalFormalConditionsT11(row.events)=TraversalExpectedFormalT11(row,qT11.layout)
      /\ (row.step="ProcedureCode714dfe070fed" /\ row.barrierCard=0 => row.events={})
      /\ (row.step="ProcedureCode714dfe070fed" => \A event \in row.events : event.tag#"PassAllBarrier" \/ (row.barrierCard#0 /\ row.position="inner") \/ (row.barrierCard#0 /\ Len(qT11.layout.orders["SchemaAtom082"])=1))
 /\ \A i \in 1..Len(qT11.checkpoints) :
      LET row==qT11.checkpoints[i] IN
      /\ (row.step="ProcedureCode9606a4cd52b4" => ~row.insideTraversal /\ ~row.insidePhase)
      /\ (row.step \in {"ProcedureCode7e3f7e5033c8","ProcedureCode4d474d346807","ProcedureCode687f72772ab1","ProcedureCodea732fbc12ae0","ProcedureCodec7b41615d673"} => ~row.insidePhase)
 /\ {event.phaseId : event \in {e \in UNION SetupRange(qT11.events) : e.tag="PhaseEnds"}}=qT11.control.phaseEndedIds
 /\ (qT11.control.traversal.complete => qT11.expired={7} /\ ~DuringTraversal6(qT11.control.traversal) /\ qT11.fund=0)
 /\ (TraversalAuditDoneT11 => qT11.control.traversal.complete /\ qT11.drained /\ qT11.fund=0 /\ qT11.bank=12+qT11.initialFund /\ qT11.control.traversal.successful#qT11.control.traversal.unsuccessful /\ Len(qT11.edges)=Len(qT11.history))
TraversalAuditEventuallyReturnsT11 == <>TraversalAuditDoneT11

TraversalPointwiseChecksT11 == CASE guideCaseT11=1 -> (TraversalEntryAndGraphChecksT11 /\ TraversalPhaseAndLastSubChecksT11) [] guideCaseT11=2 -> TraversalWindowChecksT11
 [] guideCaseT11=3 -> TraversalInitiationAndPositionChecksT11 [] guideCaseT11=4 -> TraversalEncounterAndMovementChecksT11 [] guideCaseT11=5 -> TraversalSuccessAndEndChecksT11 [] OTHER -> TraversalCleanupAndAdapterChecksT11
=============================================================================