------------------------- MODULE TraversalProceduresMC -------------------------
EXTENDS TraversalContracts
                                                                       
                                                                            
                                                                     
                                                                         
                                                                      
                                                                                
VARIABLE q6
EmptyTraversalMapT6 == [x \in {} |-> x]
ControlT6(r) ==
 [traversal |-> r,encounter |-> 0,siteInspections |-> EmptyTraversalMapT6,itemInspections |-> EmptyTraversalMapT6,
  abortedEncounters |-> {},abortedInspectiones |-> {},abortedItemInspectiones |-> {},
  paidOpen |-> FALSE,windows |-> {},windowCleanupDue |-> FALSE,
  onlyWindowCleanup |-> FALSE,phaseEndedIds |-> {},phaseStepsSkipped |-> FALSE,
  redirect |-> NoTraversalRedirect6,redirectStage |-> "NoValue",redirectCheckpointDue |-> FALSE]
PositionT6(i) == IF i = 1 THEN "inner" ELSE "outer"
LayoutT6(n) ==
 LET ids == {PositionT6(i) : i \in 1..n}
 IN [orders |-> [SchemaAtom082 |-> [i \in 1..n |-> PositionT6(i)]],
  slots |-> [p \in ids |-> [targetSite |-> "SchemaAtom082",barrierCard |-> IF p = "inner" THEN 1 ELSE 2,reservation |-> 0,retained |-> FALSE]],
  used |-> ids]
InitViewT6(q) == [traversal |-> q.flow.traversal,announced |-> q.announced,costsPaid |-> q.costsPaid,badPubAdded |-> q.badPubAdded]
SuccessViewT6(q) ==
 [traversal |-> q.flow.traversal,declarationProcessed |-> q.declarationProcessed,
  siteInspectionChosen |-> q.siteInspectionChosen,siteInspectionFinished |-> q.siteInspectionFinished]
EndViewT6(q) ==
 [traversal |-> q.flow.traversal,phaseEndedIds |-> q.flow.phaseEndedIds,windows |-> <<>>,
  windowsDone |-> q.windowsDone,fundReturned |-> q.fundReturned,
  resultDeclared |-> q.resultDeclared,returned |-> q.returned]
DoneT6 == q6.returned
InitTraversals6 ==
 \E n \in 0..2:
 \E activation \in SUBSET (1..n), suppressesInstructions \in BOOLEAN, jack \in BOOLEAN, suppress \in BOOLEAN:
  LET r == OpenTraversal6(1,1,"action1")
  IN q6 = [flow |-> ControlT6(r),plan |-> [n |-> n,activation |-> activation,suppressesInstructions |-> suppressesInstructions,jack |-> jack,suppress |-> suppress],
    layout |-> LayoutT6(n),activated |-> {},announced |-> FALSE,costsPaid |-> FALSE,badPubAdded |-> FALSE,
    declarationProcessed |-> FALSE,siteInspectionChosen |-> FALSE,siteInspectionFinished |-> FALSE,
    windowsDone |-> FALSE,fundReturned |-> FALSE,resultDeclared |-> FALSE,returned |-> FALSE,
    fund |-> 0,bank |-> 3,ready |-> FALSE,resolvedSub |-> 0,
    approach |-> OpenApproach6(r),encounter |-> OpenEncounter6(0,0,1,FALSE,"traversal",<<>>),
    movement |-> OpenMovement6(r,"Initiation",0,0,TRUE),traversalEndEvents |-> 0,expired |-> {},
    paidWindows |-> {},windowCount |-> 0,drainedPhaseIds |-> {}]
WorkTraversals6 ==
 /\ ~DoneT6 /\ ~q6.flow.traversal.complete /\ ~q6.ready
 /\ LET r == q6.flow.traversal
        step == r.step
        i == InitViewT6(q6)
        e == q6.encounter
        m == q6.movement
        s == SuccessViewT6(q6)
        end == EndViewT6(q6)
    IN CASE step = "ProcedureCode12371046a2e5" ->
         LET g == [i EXCEPT !.traversal.attacked = "SchemaAtom082",!.announced = TRUE,!.costsPaid = TRUE]
         IN /\ AnnounceTraversalTargetSite6(i,g,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,TRUE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 1,targetSite |-> "SchemaAtom082"]})
            /\ q6' = [q6 EXCEPT !.flow.traversal = g.traversal,!.announced = TRUE,!.costsPaid = TRUE,!.ready = TRUE]
       [] step = "ProcedureCodeacc82dbcc545" ->
         /\ AddInitiationLiabilityMarker6(i,[i EXCEPT !.badPubAdded = TRUE],q6.fund,q6.fund+1,1)
         /\ q6' = [q6 EXCEPT !.badPubAdded = TRUE,!.fund = @+1,!.bank = @-1,!.ready = TRUE]
       [] step = "ProcedureCode4d6bd06d2c9f" ->
         LET g == [i EXCEPT !.traversal.formalBegun = TRUE]
         IN /\ FormalTraversalBegin6(i,g,{TraversalBeginEvent6(r)})
            /\ q6' = [q6 EXCEPT !.flow.traversal = g.traversal,!.ready = TRUE]
       [] step = "ProcedureCode347de0bdd6b4" ->
         LET g == [r EXCEPT !.position = OutermostOccupiedPosition6(q6.layout,"SchemaAtom082")]
         IN /\ SetInitialSideBPosition6(r,g,q6.layout,step)
            /\ q6' = [q6 EXCEPT !.flow.traversal = g,!.ready = TRUE]
       [] step = "ProcedureCode453e949a114f" ->
         LET a == [q6.approach EXCEPT !.begun = TRUE]
             events == IF ApproachedBarrier6(a,q6.layout) = 0 THEN {}
               ELSE {[tag |-> "ApproachBarrier",barrierCard |-> ApproachedBarrier6(a,q6.layout),phaseId |-> r.phaseId,traversalId |-> 1]}
         IN /\ BeginApproach6(r,q6.approach,a,q6.layout,events)
            /\ q6' = [q6 EXCEPT !.approach = a,!.ready = TRUE]
       [] step = "ProcedureCodeda7bff1d9270" ->
         LET g == [e EXCEPT !.stage = "BeginReactions"]
         IN /\ BeginEncounter6(e,g,TRUE,{[tag |-> "EncounterBarrier",encounterId |-> e.id,barrierCard |-> e.barrierCard,traversalId |-> 1]})
            /\ q6' = [q6 EXCEPT !.encounter = g,!.ready = TRUE]
       [] step = "ProcedureCodef1914978bb8e" ->
         LET sub == NextEncounterSub6(e)
             g == IF sub = 0 THEN e ELSE [e EXCEPT !.resolved = @ \cup {sub}]
         IN /\ IF sub # 0 THEN ResolveEncounterSub6(e,g,sub,TRUE) ELSE TRUE
            /\ q6' = [q6 EXCEPT !.encounter = g,!.resolvedSub = sub,!.ready = TRUE]
       [] step = "ProcedureCode687f72772ab1" ->
         LET g == [e EXCEPT !.stage = "Complete"]
         IN /\ CompleteEncounter6(e,g,TRUE)
            /\ q6' = [q6 EXCEPT !.encounter = g,!.ready = TRUE]
       [] step = "ProcedureCode714dfe070fed" ->
         LET g == [m EXCEPT !.begun = TRUE,!.passedBarrier = MovementBarrier6(r,q6.layout),
                   !.passedAll = MovementBarrier6(r,q6.layout) # 0 /\ NextInwardPosition6(q6.layout,"SchemaAtom082",r.position) = "NoValue"]
         IN /\ BeginMovement6(r,m,g,q6.layout,MovementPassEvents6(r,q6.layout))
            /\ q6' = [q6 EXCEPT !.movement = g,!.ready = TRUE]
       [] step = "ProcedureCode9bca3a096549" ->
         IF q6.plan.jack THEN
           LET c == [EndTraversalOutcome6(q6.flow,r.phaseId+1) EXCEPT !.traversal.withdrewTraversal = TRUE]
           IN /\ MovementWithdrawTraversal6(q6.flow,c,m,q6.layout,q6.layout,r.phaseId+1,TRUE,TRUE,TRUE,EndTraversalEffectEvents6(q6.flow))
              /\ q6' = [q6 EXCEPT !.flow = c]
         ELSE /\ DeclineMovementWithdrawTraversal6(r,m,[m EXCEPT !.declined = TRUE],TRUE)
              /\ q6' = [q6 EXCEPT !.movement.declined = TRUE,!.ready = TRUE]
       [] step = "ProcedureCoded4ddeafb5f2f" ->
         LET g == [r EXCEPT !.position = NextInwardPosition6(q6.layout,"SchemaAtom082",r.position)]
             n == [m EXCEPT !.advanced = TRUE,!.movedToNew = g.position # "NoValue"]
         IN /\ AdvanceMovement6(r,g,m,n,q6.layout,q6.layout)
            /\ q6' = [q6 EXCEPT !.flow.traversal = g,!.movement = n,!.ready = TRUE]
       [] step = "ProcedureCode7e82ab2b38b7" ->
         /\ ApproachTargetSite6(r,m,[m EXCEPT !.approachedTargetSite = TRUE],
                 {[tag |-> "ApproachTargetSite",traversalId |-> 1,targetSite |-> "SchemaAtom082",phaseId |-> r.phaseId]})
         /\ q6' = [q6 EXCEPT !.movement.approachedTargetSite = TRUE,!.ready = TRUE]
       [] step = "ProcedureCodebbb14496b09b" ->
         LET g == [s EXCEPT !.declarationProcessed = TRUE,!.traversal.successful = ~q6.plan.suppress]
         IN /\ DeclareSuccessfulTraversal6(s,g,~q6.plan.suppress,
                IF q6.plan.suppress THEN {} ELSE {[tag |-> "SuccessfulTraversal",traversalId |-> 1,targetSite |-> "SchemaAtom082"]})
            /\ q6' = [q6 EXCEPT !.declarationProcessed = TRUE,!.flow.traversal = g.traversal,!.ready = TRUE]
       [] step = "ProcedureCoded75d879e00ff" ->
         LET g == [s EXCEPT !.siteInspectionChosen = TRUE]
         IN /\ ChooseRulesInspection6(s,g,"Inspection",{"Inspection"},TRUE,
                 [kind |-> "Inspection",choice |-> "Inspection",traversalId |-> 1,targetSite |-> "SchemaAtom082",origin |-> "RulesTraversalInspection"])
            /\ FinishRulesInspectionInstruction6(g,[g EXCEPT !.siteInspectionFinished = TRUE],TRUE)
            /\ q6' = [q6 EXCEPT !.siteInspectionChosen = TRUE,!.siteInspectionFinished = TRUE,!.ready = TRUE]
       [] step = "ProcedureCode6ea937bb44ac" ->
         /\ FinishTraversalEndWindows6(end,[end EXCEPT !.windowsDone = TRUE])
         /\ q6' = [q6 EXCEPT !.windowsDone = TRUE,!.ready = TRUE,
                            !.drainedPhaseIds = @ \cup q6.flow.phaseEndedIds]
       [] step = "ProcedureCode84dea7dc8ecc" ->
         /\ ReturnLiabilityMarkerFund6(end,[end EXCEPT !.fundReturned = TRUE],q6.fund,0,q6.bank,q6.bank+q6.fund)
         /\ q6' = [q6 EXCEPT !.fundReturned = TRUE,!.fund = 0,!.bank = @+q6.fund,!.ready = TRUE]
       [] step = "ProcedureCode5e397645e65c" ->
         LET g == [end EXCEPT !.resultDeclared = TRUE,!.traversal.unsuccessful = ~r.reachedSuccess]
         IN /\ DeclareUnsuccessfulTraversal6(end,g,[SchemaAtom082 |-> 1],
                IF r.reachedSuccess THEN {} ELSE {[tag |-> "UnsuccessfulTraversal",traversalId |-> 1,targetSite |-> "SchemaAtom082"]})
            /\ q6' = [q6 EXCEPT !.resultDeclared = TRUE,!.flow.traversal = g.traversal,!.ready = TRUE]
       [] step = "ProcedureCode9606a4cd52b4" ->
         LET g == [end EXCEPT !.traversal.complete = TRUE,!.phaseEndedIds = @ \cup {r.phaseId}]
         IN /\ CompleteTraversal6(end,g,TRUE,{[tag |-> "TraversalEnds",traversalId |-> 1],TraversalPhaseEndEvent6(r)},{1})
            /\ q6' = [q6 EXCEPT !.flow.traversal = g.traversal,!.flow.phaseEndedIds = g.phaseEndedIds,
                    !.traversalEndEvents = @+1,!.expired = {1}]
       [] TraversalStepInfo6(step).kind = "PaidWindow" ->
         /\ IF step = "ProcedureCode3a6daf593ad4" /\ MovementBarrier6(r,q6.layout) \in q6.plan.activation THEN
             LET down == [form |-> "Card",kind |-> "Barrier",zone |-> "Play",deployed |-> TRUE,face |-> "Down",activated |-> FALSE]
             IN ApproachActivation6(r,q6.approach,q6.layout,
                  [open |-> TRUE,kind |-> "Paid",phaseId |-> r.phaseId,step |-> step,priority |-> "SideA"],
                  MovementBarrier6(r,q6.layout),down,[down EXCEPT !.face = "Up",!.activated = TRUE],TRUE,TRUE)
            ELSE TRUE
         /\ IF step = "ProcedureCode8b3260c0010f" THEN
             LET paid == WithFullySuppressInstruction6([e EXCEPT !.stage = "Paid",!.paidReached = TRUE])
                 barrierInstructionSuppressed == IF q6.plan.suppressesInstructions THEN WithFullySuppressInstruction6([paid EXCEPT !.barrierInstructionSuppressed = {1,2},!.barrierInstructionSuppressedBy = [x \in {1,2} |-> 9]]) ELSE paid
                 g == [barrierInstructionSuppressed EXCEPT !.stage = "BarrierInstructions"]
             IN /\ BeginEncounterPaid6(e,paid,TRUE,NewFullySuppressInstructionEvents6(e,paid))
                /\ IF q6.plan.suppressesInstructions THEN PaidSuppressInstructionEncounterSubs6(paid,barrierInstructionSuppressed,
                   [open |-> TRUE,kind |-> "Paid",step |-> step,phaseId |-> e.id,priority |-> "SideB"],
                   {1,2},9,TRUE,TRUE,NewFullySuppressInstructionEvents6(paid,barrierInstructionSuppressed)) ELSE TRUE
                /\ CloseEncounterPaid6(barrierInstructionSuppressed,g,TRUE)
                /\ q6' = [q6 EXCEPT !.encounter = g,!.ready = TRUE,
                    !.paidWindows = @ \cup {<<r.phaseId,step>>},!.windowCount = @+1]
            ELSE q6' = [q6 EXCEPT !.activated = IF step = "ProcedureCode3a6daf593ad4" /\ MovementBarrier6(r,q6.layout) \in q6.plan.activation THEN @ \cup {MovementBarrier6(r,q6.layout)} ELSE @,
                    !.ready = TRUE,!.paidWindows = @ \cup {<<r.phaseId,step>>},!.windowCount = @+1]
       [] OTHER -> q6' = [q6 EXCEPT !.ready = TRUE]
FinishPhaseTraversals6 ==
 /\ ~DoneT6 /\ ~q6.flow.traversal.complete /\ q6.ready
 /\ LET r == q6.flow.traversal
        work == [jackChoice |-> "Continue",resolvedSub |-> q6.resolvedSub]
        next == NextTraversalStep6(r.step,TraversalBranch6(r,q6.layout,q6.activated,q6.encounter,q6.movement,work))
        f == [q6.flow EXCEPT !.phaseEndedIds = @ \cup {r.phaseId}]
    IN /\ TraversalStepInfo6(next).phase # r.phase
       /\ BeginNormalTraversalPhaseEnd6(q6.flow,f,q6.layout,q6.activated,q6.encounter,q6.movement,work,TRUE,{TraversalPhaseEndEvent6(r)})
       /\ q6' = [q6 EXCEPT !.flow = f]
DrainPhaseTraversals6 ==
 /\ ~DoneT6 /\ q6.ready /\ q6.flow.traversal.phaseId \in q6.flow.phaseEndedIds
 /\ q6.flow.traversal.phaseId \notin q6.drainedPhaseIds
 /\ q6' = [q6 EXCEPT !.drainedPhaseIds = @ \cup {q6.flow.traversal.phaseId}]
AdvanceTraversals6 ==
 /\ ~DoneT6 /\ ~q6.flow.traversal.complete /\ q6.ready
 /\ LET r == q6.flow.traversal
        work == [jackChoice |-> "Continue",resolvedSub |-> q6.resolvedSub]
        next == NextTraversalStep6(r.step,TraversalBranch6(r,q6.layout,q6.activated,q6.encounter,q6.movement,work))
        phase == TraversalStepInfo6(next).phase
        changed == phase # r.phase
        id == IF changed THEN r.phaseId+1 ELSE r.phaseId
        g == [r EXCEPT !.step = next,!.phase = phase,!.phaseId = id,
              !.usedPhaseIds = @ \cup {id},!.reachedSuccess = @ \/ phase = "Success",
              !.ending = @ \/ phase = "TraversalEnds",!.position = IF phase \in {"Success","TraversalEnds"} THEN "NoValue" ELSE @]
        f == [q6.flow EXCEPT !.traversal = g,
              !.phaseEndedIds = IF changed THEN @ \cup {r.phaseId} ELSE @,
              !.encounter = IF phase = "Encounter" THEN id ELSE IF r.phase = "Encounter" THEN 0 ELSE @,
              !.phaseStepsSkipped = FALSE,
              !.windowCleanupDue = IF phase = "TraversalEnds" /\ changed THEN TRUE ELSE IF r.step = "ProcedureCode6ea937bb44ac" THEN FALSE ELSE @]
    IN /\ (~changed \/ r.phaseId \in q6.drainedPhaseIds)
       /\ AdvanceNormalTraversalStep6(q6.flow,f,q6.layout,q6.activated,q6.encounter,q6.movement,work,id,TRUE,TRUE,{})
       /\ CASE r.step = "ProcedureCode7e3f7e5033c8" -> CompleteInitiationTraversalView6(r,g,q6.layout,id,TRUE)
          [] r.step = "ProcedureCode4d474d346807" -> CompleteApproachTraversalView6(r,g,q6.approach,q6.layout,q6.activated,id,TRUE)
          [] r.step = "ProcedureCode687f72772ab1" -> CompleteOrdinaryEncounterTraversalView6(r,g,q6.encounter,id,TRUE)
          [] r.step \in {"ProcedureCode6c5d14f545f7","ProcedureCodea732fbc12ae0"} /\ changed -> CompleteMovementTraversalView6(r,g,q6.movement,id,TRUE)
          [] r.step = "ProcedureCodec7b41615d673" -> CompleteSuccessTraversalView6(SuccessViewT6(q6),[SuccessViewT6(q6) EXCEPT !.traversal = g],id,TRUE)
          [] OTHER -> TRUE
       /\ q6' = [q6 EXCEPT !.flow = f,!.ready = FALSE,!.resolvedSub = 0,
            !.approach = IF changed /\ phase = "Approach" THEN OpenApproach6(g) ELSE @,
            !.encounter = IF changed /\ phase = "Encounter" THEN OpenEncounter6(id,MovementBarrier6(g,q6.layout),1,FALSE,"traversal",<<1,2>>) ELSE @,
            !.movement = IF changed /\ phase = "Movement" THEN OpenMovement6(g,r.phase,
                IF r.phase = "Encounter" THEN q6.encounter.barrierCard ELSE MovementBarrier6(r,q6.layout),
                IF r.phase = "Encounter" THEN q6.encounter.id ELSE 0,TRUE) ELSE @]
ReturnTraversals6 ==
 /\ q6.flow.traversal.complete /\ ~q6.returned
 /\ q6.flow.traversal.phaseId \in q6.drainedPhaseIds
 /\ ReturnTraversalToCaller6(EndViewT6(q6),[EndViewT6(q6) EXCEPT !.returned = TRUE],TRUE,"action1")
 /\ q6' = [q6 EXCEPT !.returned = TRUE]
DrainTraversalEndReactions6 ==
 /\ q6.flow.traversal.complete /\ ~q6.returned /\ q6.flow.traversal.phaseId \notin q6.drainedPhaseIds
 /\ q6' = [q6 EXCEPT !.drainedPhaseIds = @ \cup {q6.flow.traversal.phaseId}]
NextTraversals6 == WorkTraversals6 \/ FinishPhaseTraversals6 \/ DrainPhaseTraversals6 \/ AdvanceTraversals6 \/
             DrainTraversalEndReactions6 \/ ReturnTraversals6 \/ (DoneT6 /\ UNCHANGED q6)
SpecTraversals6 == InitTraversals6 /\ [][NextTraversals6]_q6 /\ WF_q6(NextTraversals6)
ExpectedWindowCountT6(plan) ==
 IF plan.jack THEN 2 + (IF plan.n > 0 THEN 1 + (IF plan.n \in plan.activation THEN 1 ELSE 0) ELSE 0)
 ELSE 1 + plan.n + Cardinality(plan.activation) + 2*(IF plan.n = 0 THEN 1 ELSE plan.n)
TraversalsInvariant6 ==
 /\ TraversalFrameValid6(q6.flow.traversal)
 /\ PositionLayoutValid6(q6.layout,1..q6.plan.n) /\ SideBPositionValid6(q6.flow.traversal,q6.layout)
 /\ q6.fund \in Nat /\ q6.bank \in Nat /\ q6.fund+q6.bank = 3
 /\ q6.flow.traversal.formalBegun => q6.announced /\ q6.costsPaid /\ q6.badPubAdded
 /\ q6.flow.traversal.successful => q6.flow.traversal.reachedSuccess
 /\ q6.flow.traversal.unsuccessful => ~q6.flow.traversal.reachedSuccess
 /\ q6.windowCount = Cardinality(q6.paidWindows)
 /\ 2 \in q6.encounter.resolved => 1 \in (q6.encounter.resolved \cup q6.encounter.barrierInstructionSuppressed)
 /\ q6.flow.traversal.complete => q6.windowsDone /\ q6.fundReturned /\ q6.resultDeclared /\ q6.fund = 0
 /\ q6.returned => q6.flow.traversal.complete
 /\ q6.returned => q6.windowCount = ExpectedWindowCountT6(q6.plan)
 /\ q6.returned => q6.flow.phaseEndedIds = q6.flow.traversal.usedPhaseIds
 /\ q6.drainedPhaseIds \subseteq q6.flow.phaseEndedIds
 /\ q6.returned => q6.drainedPhaseIds = q6.flow.traversal.usedPhaseIds
 /\ q6.flow.traversal.usedPhaseIds \ {q6.flow.traversal.phaseId} \subseteq q6.flow.phaseEndedIds
 /\ q6.flow.traversal.phase # "TraversalEnds" => q6.flow.traversal.usedPhaseIds \ {q6.flow.traversal.phaseId} \subseteq q6.drainedPhaseIds
 /\ q6.returned => q6.flow.traversal.successful = (~q6.plan.jack /\ ~q6.plan.suppress)
 /\ q6.returned => q6.flow.traversal.unsuccessful = q6.plan.jack
 /\ q6.traversalEndEvents = IF q6.flow.traversal.complete THEN 1 ELSE 0
 /\ q6.expired = IF q6.flow.traversal.complete THEN {1} ELSE {}
EventuallyReturns6 == <>DoneT6
=============================================================================