r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

TraversalProceduresMC¶

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

This model/fact module also contains 42 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

AdvanceTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

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 @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceNormalTraversalStep6, CompleteApproachTraversalView6, CompleteInitiationTraversalView6, CompleteMovementTraversalView6, CompleteOrdinaryEncounterTraversalView6, CompleteSuccessTraversalView6, MovementBarrier6, NextTraversalStep6, OpenApproach6, OpenEncounter6, OpenMovement6, TraversalBranch6, TraversalStepInfo6, DoneT6, SuccessViewT6, q6

ControlT6 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoTraversalRedirect6, EmptyTraversalMapT6

DoneT6 · operator

reference-profile · input revision 2 · CC0 1.0

DoneT6 == q6.returned

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q6

DrainPhaseTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

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}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DoneT6, q6

DrainTraversalEndReactions6 · operator

reference-profile · input revision 2 · CC0 1.0

DrainTraversalEndReactions6 ==
 /\ q6.flow.traversal.complete /\ ~q6.returned /\ q6.flow.traversal.phaseId \notin q6.drainedPhaseIds
 /\ q6' = [q6 EXCEPT !.drainedPhaseIds = @ \cup {q6.flow.traversal.phaseId}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q6

EmptyTraversalMapT6 · operator

reference-profile · input revision 2 · CC0 1.0

EmptyTraversalMapT6 == [x \in {} |-> x]

Exact module download · Source bundle and reproduction instructions

EndViewT6 · operator

reference-profile · input revision 2 · CC0 1.0

EndViewT6(q) ==
 [traversal |-> q.flow.traversal,phaseEndedIds |-> q.flow.phaseEndedIds,windows |-> <<>>,
  windowsDone |-> q.windowsDone,fundReturned |-> q.fundReturned,
  resultDeclared |-> q.resultDeclared,returned |-> q.returned]

Exact module download · Source bundle and reproduction instructions

EventuallyReturns6 · operator

reference-profile · input revision 2 · CC0 1.0

EventuallyReturns6 == <>DoneT6

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DoneT6

ExpectedWindowCountT6 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

FinishPhaseTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginNormalTraversalPhaseEnd6, NextTraversalStep6, TraversalBranch6, TraversalPhaseEndEvent6, TraversalStepInfo6, DoneT6, q6

InitTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

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 |-> {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenApproach6, OpenEncounter6, OpenMovement6, OpenTraversal6, ControlT6, LayoutT6, q6

InitViewT6 · operator

reference-profile · input revision 2 · CC0 1.0

InitViewT6(q) == [traversal |-> q.flow.traversal,announced |-> q.announced,costsPaid |-> q.costsPaid,badPubAdded |-> q.badPubAdded]

Exact module download · Source bundle and reproduction instructions

LayoutT6 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionT6

NextTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

NextTraversals6 == WorkTraversals6 \/ FinishPhaseTraversals6 \/ DrainPhaseTraversals6 \/ AdvanceTraversals6 \/
             DrainTraversalEndReactions6 \/ ReturnTraversals6 \/ (DoneT6 /\ UNCHANGED q6)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceTraversals6, DoneT6, DrainPhaseTraversals6, DrainTraversalEndReactions6, FinishPhaseTraversals6, ReturnTraversals6, WorkTraversals6, q6

PositionT6 · operator

reference-profile · input revision 2 · CC0 1.0

PositionT6(i) == IF i = 1 THEN "inner" ELSE "outer"

Exact module download · Source bundle and reproduction instructions

ReturnTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReturnTraversalToCaller6, EndViewT6, q6

SpecTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

SpecTraversals6 == InitTraversals6 /\ [][NextTraversals6]_q6 /\ WF_q6(NextTraversals6)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitTraversals6, NextTraversals6, q6

SuccessViewT6 · operator

reference-profile · input revision 2 · CC0 1.0

SuccessViewT6(q) ==
 [traversal |-> q.flow.traversal,declarationProcessed |-> q.declarationProcessed,
  siteInspectionChosen |-> q.siteInspectionChosen,siteInspectionFinished |-> q.siteInspectionFinished]

Exact module download · Source bundle and reproduction instructions

TraversalsInvariant6 · operator

reference-profile · input revision 2 · CC0 1.0

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 {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionLayoutValid6, SideBPositionValid6, TraversalFrameValid6, ExpectedWindowCountT6, q6

WorkTraversals6 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AddInitiationLiabilityMarker6, AdvanceMovement6, AnnounceTraversalTargetSite6, ApproachActivation6, ApproachTargetSite6, ApproachedBarrier6, BeginApproach6, BeginEncounter6, BeginEncounterPaid6, BeginMovement6, ChooseRulesInspection6, CloseEncounterPaid6, CompleteEncounter6, CompleteTraversal6, DeclareSuccessfulTraversal6, DeclareUnsuccessfulTraversal6, DeclineMovementWithdrawTraversal6, EndTraversalEffectEvents6, EndTraversalOutcome6, FinishRulesInspectionInstruction6, FinishTraversalEndWindows6, FormalTraversalBegin6, MovementBarrier6, MovementPassEvents6, MovementWithdrawTraversal6, NewFullySuppressInstructionEvents6, NextEncounterSub6, NextInwardPosition6, OutermostOccupiedPosition6, PaidSuppressInstructionEncounterSubs6, ResolveEncounterSub6, ReturnLiabilityMarkerFund6, SetInitialSideBPosition6, TraversalBeginEvent6, TraversalPhaseEndEvent6, TraversalStepInfo6, WithFullySuppressInstruction6, DoneT6, EndViewT6, InitViewT6, SuccessViewT6, q6

q6 · variable

reference-profile · input revision 2 · CC0 1.0

q6

Exact module download · Source bundle and reproduction instructions