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

TraversalChecksMC

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 145 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.

ApproachChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

ApproachChecks6 ==
 LET r == [OpenTraversal6(1,10,"action1") EXCEPT !.formalBegun = TRUE,!.phase = "Approach",!.step = "ProcedureCode453e949a114f",!.position = "outer",!.attacked = "SchemaAtom082"]
     a == OpenApproach6(r)
     begun == [a EXCEPT !.begun = TRUE]
     l == PositionFixture6
     barrierCard == ApproachedBarrier6(a,l)
     paidTraversal == [r EXCEPT !.step = "ProcedureCode3a6daf593ad4"]
     ev == {[tag |-> "ApproachBarrier",barrierCard |-> barrierCard,phaseId |-> 10,traversalId |-> 1]}
     w == [open |-> TRUE,kind |-> "Paid",phaseId |-> 10,step |-> "ProcedureCode3a6daf593ad4",priority |-> "SideA"]
     reaction == [kind |-> "Reaction",open |-> TRUE,beginPhaseId |-> 10,pending |-> {"mandatory","optional"},lostPending |-> {},priority |-> "SideA"]
     closed == [reaction EXCEPT !.open = FALSE,!.pending = {},!.lostPending = {"mandatory","optional"},!.priority = "NoValue"]
     last == [r EXCEPT !.step = "ProcedureCode4d474d346807"]
     dest == [last EXCEPT !.phase = "Encounter",!.step = "ProcedureCodeda7bff1d9270",!.phaseId = 11,!.usedPhaseIds = {10,11}]
     down == [form |-> "Card",kind |-> "Barrier",zone |-> "Play",deployed |-> TRUE,face |-> "Down",activated |-> FALSE]
 IN /\ BeginApproach6(r,a,begun,l,ev)
    /\ ~BeginApproach6(r,begun,begun,l,ev)
    /\ ApproachActivation6(paidTraversal,begun,l,w,barrierCard,down,[down EXCEPT !.face = "Up",!.activated = TRUE],TRUE,TRUE)
    /\ ~ApproachActivation6(paidTraversal,begun,l,w,barrierCard,down,[down EXCEPT !.face = "Up",!.activated = TRUE],FALSE,TRUE)
    /\ ~ApproachActivationPermission6(r,begun,l,w,barrierCard)
    /\ ~ApproachActivationPermission6([r EXCEPT !.step = "ProcedureCode4d474d346807"],begun,l,w,barrierCard)
    /\ ~ApproachActivationPermission6(paidTraversal,begun,l,w,1)
    /\ ~ApproachActivationPermission6(paidTraversal,begun,l,[w EXCEPT !.phaseId = 99],barrierCard)
    /\ ~ApproachActivationPermission6(paidTraversal,begun,l,[w EXCEPT !.step = "ProcedureCode2cd618a9e624"],barrierCard)
    /\ ~ApproachActivationPermission6(paidTraversal,begun,l,[w EXCEPT !.priority = "SideB"],barrierCard)
    /\ ApproachedBarrier6(begun,[l EXCEPT !.slots["outer"].barrierCard = 3]) = 3
    /\ ~BeginApproach6(r,begun,begun,[l EXCEPT !.slots["outer"].barrierCard = 3],ev)
    /\ CloseEndedBeginReaction6(reaction,closed,{10})
    /\ ~CloseEndedBeginReaction6(reaction,closed,{11})
    /\ ~CloseEndedBeginReaction6([reaction EXCEPT !.beginPhaseId = 0],[closed EXCEPT !.beginPhaseId = 0],{10})
    /\ CompleteApproachTraversalView6(last,dest,begun,l,{barrierCard},11,TRUE)
    /\ ~CompleteApproachTraversalView6(last,dest,begun,l,{barrierCard},11,FALSE)
    /\ ApproachDestination6(begun,l,{}) = "Movement"
    /\ ApproachDestination6(begun,[l EXCEPT !.slots["outer"].barrierCard = 0],{barrierCard}) = "Movement"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionFixture6, ApproachActivation6, ApproachActivationPermission6, ApproachDestination6, ApproachedBarrier6, BeginApproach6, CloseEndedBeginReaction6, CompleteApproachTraversalView6, OpenApproach6, OpenTraversal6

Block6Assertions · operator

reference-profile · input revision 2 · CC0 1.0

Block6Assertions ==
 CASE block6 = 0 -> TRUE
 [] block6 = 1 -> GeneralTraversalChecks6
 [] block6 = 2 -> PositionChecks6
 [] block6 = 3 -> InitiationChecks6
 [] block6 = 4 -> ApproachChecks6
 [] block6 = 5 -> EncounterChecks6
 [] block6 = 6 -> MovementChecks6
 [] block6 = 7 -> SuccessChecks6
 [] block6 = 8 -> TraversalEndsChecks6
 [] block6 = 9 -> ProcedureChecks6

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ApproachChecks6, EncounterChecks6, GeneralTraversalChecks6, InitiationChecks6, MovementChecks6, PositionChecks6, ProcedureChecks6, SuccessChecks6, TraversalEndsChecks6, block6

EmptyFrames6 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

EncounterChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

EncounterChecks6 ==
 LET e == OpenEncounter6(50,2,1,FALSE,"traversal",<<1,2>>)
     begin == [e EXCEPT !.stage = "BeginReactions"]
     paid == [begin EXCEPT !.stage = "Paid",!.paidReached = TRUE]
     barrierInstructionSuppressed == WithFullySuppressInstruction6([paid EXCEPT !.barrierInstructionSuppressed = {1,2},!.barrierInstructionSuppressedBy = [s \in {1,2} |-> 9]])
     gained == [barrierInstructionSuppressed EXCEPT !.order = <<1,2,3>>,!.usedSubIds = {1,2,3},!.barrierInstructionSuppressedBy = [s \in {1,2,3} |-> IF s=3 THEN 0 ELSE 9]]
     rebroke == [gained EXCEPT !.barrierInstructionSuppressed = {1,2,3},!.barrierInstructionSuppressedBy[3] = 9]
     multi == WithFullySuppressInstruction6([paid EXCEPT !.barrierInstructionSuppressed = {1,2},!.barrierInstructionSuppressedBy = [s \in {1,2} |-> s]])
     w == [open |-> TRUE,kind |-> "Paid",step |-> "ProcedureCode8b3260c0010f",phaseId |-> 50,priority |-> "SideB"]
     zero == [OpenEncounter6(51,3,1,FALSE,"traversal",<<>>) EXCEPT !.stage = "BeginReactions"]
     zeroPaid == WithFullySuppressInstruction6([zero EXCEPT !.stage = "Paid",!.paidReached = TRUE])
     bypassed == [zero EXCEPT !.stage = "Complete",!.bypassed = TRUE,!.aborted = TRUE]
     resolving == [paid EXCEPT !.stage = "BarrierInstructions"]
     r == [OpenTraversal6(1,10,"action1") EXCEPT !.formalBegun = TRUE,!.phase = "Movement",!.step = "ProcedureCode714dfe070fed"]
     f == OpenEncounter6(52,3,1,TRUE,"pass reaction",<<1>>)
     done == [f EXCEPT !.stage = "Complete"]
     control == [TraversalControlFixture6(r) EXCEPT !.encounter = 52]
     ended == EndTraversalOutcome6(control,11)
     outer == OpenEncounter6(52,3,0,TRUE,"outer itemInspection",<<1>>)
     inner == OpenEncounter6(53,2,0,TRUE,"outer encounter",<<1>>)
     scopes == [id \in {1,2,3} |-> [encounterAncestors |-> CASE id=1 -> {} [] id=2 -> {52} [] OTHER -> {52,53}]]
     noTraversalControl == [TraversalControlFixture6(NoTraversal6) EXCEPT !.encounter = 53,!.siteInspections = scopes,!.itemInspections = scopes]
     chain == <<outer,inner>>
     chainEnd == ForcedEndOutcome6(noTraversalControl,chain,0)
     deadChain == [i \in 1..2 |-> [chain[i] EXCEPT !.stage = "Complete",!.aborted = TRUE]]
     bypassControl == TraversalControlFixture6([r EXCEPT !.phase = "Encounter",!.phaseId = 50,!.usedPhaseIds = {10,50},!.step = "ProcedureCode8b3260c0010f",!.position = "outer",!.attacked = "SchemaAtom082"])
     bypassTarget == [phase |-> "Movement",phaseId |-> 51,step |-> "ProcedureCode714dfe070fed",attacked |-> "SchemaAtom082",position |-> "outer"]
     bypassRequest == [bypassControl EXCEPT !.redirect = bypassTarget,!.redirectStage = "PaidWindow",!.phaseStepsSkipped = TRUE,!.traversal.usedPhaseIds = {10,50,51}]
     bypassNormal == [paid EXCEPT !.stage = "Complete",!.bypassed = TRUE,!.aborted = TRUE]
 IN /\ BeginEncounter6(e,begin,TRUE,{[tag |-> "EncounterBarrier",encounterId |-> 50,barrierCard |-> 2,traversalId |-> 1]})
    /\ BeginEncounterPaid6(begin,paid,TRUE,{})
    /\ ~BeginEncounterPaid6(begin,paid,FALSE,{})
    /\ PaidSuppressInstructionEncounterSubs6(paid,barrierInstructionSuppressed,w,{1,2},9,TRUE,TRUE,NewFullySuppressInstructionEvents6(paid,barrierInstructionSuppressed))
    /\ ~PaidSuppressInstructionEncounterSubs6(paid,barrierInstructionSuppressed,[w EXCEPT !.priority = "SideA"],{1,2},9,TRUE,TRUE,NewFullySuppressInstructionEvents6(paid,barrierInstructionSuppressed))
    /\ ~PaidSuppressInstructionEncounterSubs6(paid,barrierInstructionSuppressed,w,{1,2},9,TRUE,FALSE,NewFullySuppressInstructionEvents6(paid,barrierInstructionSuppressed))
    /\ barrierInstructionSuppressed.fullyBy = {9} /\ multi.fullyBy = {}
    /\ UpdateEncounterSubs6(barrierInstructionSuppressed,gained,<<1,2,3>>,TRUE,{})
    /\ gained.fullyBarrierInstructionSuppressed /\ 3 \notin gained.barrierInstructionSuppressed
    /\ SuppressInstructionEncounterSubs6(gained,rebroke,{3},9,TRUE,TRUE,{})
    /\ ~SuppressInstructionEncounterSubs6(barrierInstructionSuppressed,barrierInstructionSuppressed,{1},9,TRUE,TRUE,{})
    /\ ~AllCurrentSubsBarrierInstructionSuppressed6(zero) /\ AllCurrentSubsBarrierInstructionSuppressed6(zeroPaid)
    /\ BeginEncounterPaid6(zero,zeroPaid,TRUE,NewFullySuppressInstructionEvents6(zero,zeroPaid))
    /\ zeroPaid.fullyBy = {}
    /\ BypassEncounter6(zero,bypassed,TRUE,{[tag |-> "Bypass",encounterId |-> 51,barrierCard |-> 3,traversalId |-> 1]})
    /\ ~bypassed.fullyBarrierInstructionSuppressed
    /\ BypassEncounter6(zeroPaid,[zeroPaid EXCEPT !.stage = "Complete",!.bypassed = TRUE,!.aborted = TRUE],TRUE,{[tag |-> "Bypass",encounterId |-> 51,barrierCard |-> 3,traversalId |-> 1]})
    /\ BypassTraversalRedirect6(bypassControl,bypassRequest,bypassNormal,51,{})
    /\ ~BypassTraversalRedirect6(bypassControl,bypassRequest,[bypassNormal EXCEPT !.forced = TRUE],51,{})
    /\ ~ResolveEncounterSub6(paid,[paid EXCEPT !.resolved = {1}],1,TRUE)
    /\ ~ResolveEncounterSub6(bypassed,[bypassed EXCEPT !.resolved = {1}],1,TRUE)
    /\ NextEncounterSub6(resolving) = 1
    /\ ~ResolveEncounterSub6(resolving,[resolving EXCEPT !.resolved = {2}],2,TRUE)
    /\ ResolveEncounterSub6(resolving,[resolving EXCEPT !.resolved = {1}],1,TRUE)
    /\ ~ResolveEncounterSub6(resolving,[resolving EXCEPT !.resolved = {1}],1,FALSE)
    /\ NextEncounterSub6([resolving EXCEPT !.barrierInstructionSuppressed = {1}]) = 2
    /\ ~CompleteEncounter6(resolving,[resolving EXCEPT !.stage = "Complete"],TRUE)
    /\ CompleteEncounter6([barrierInstructionSuppressed EXCEPT !.stage = "BarrierInstructions"],[barrierInstructionSuppressed EXCEPT !.stage = "Complete"],TRUE)
    /\ PushForcedEncounter6(<<>>,<<f>>,r,r,f,{},TRUE)
    /\ ~PushForcedEncounter6(<<>>,<<f>>,r,r,f,{52},TRUE)
    /\ ~ForcedInstructionFinished6(52,{})
    /\ ReturnForcedEncounter6(<<done>>,<<>>,r,r,"pass reaction",{},{52})
    /\ ~ReturnForcedEncounter6(<<f>>,<<>>,r,r,"pass reaction",{},{52})
    /\ ReturnForcedEncounter6(<<done>>,<<>>,[r EXCEPT !.attacked = "SchemaAtom082"],[r EXCEPT !.attacked = "SchemaAtom082"],"pass reaction",{},{52})
    /\ MoveTraversalDuringForcedEncounter6(<<f>>,<<f>>,r,[r EXCEPT !.attacked = "SchemaAtom082"],TRUE)
    /\ EndTraversalDuringForced6(control,ended,<<f>>,<<[f EXCEPT !.stage = "Complete",!.aborted = TRUE]>>,{},{52},11,EndTraversalEffectEvents6(control))
    /\ EndTraversalDuringForced6(noTraversalControl,chainEnd,chain,deadChain,{},{52,53},0,ForcedEndEvents6(noTraversalControl,chain))
    /\ DOMAIN chainEnd.siteInspections = {1} /\ DOMAIN chainEnd.itemInspections = {1}
    /\ chainEnd.abortedInspectiones = {2,3} /\ chainEnd.abortedItemInspectiones = {2,3}
    /\ chainEnd.phaseEndedIds = {52,53} /\ chainEnd.abortedEncounters = {52,53}
    /\ chainEnd.traversal = NoTraversal6
    /\ Cardinality(ForcedEndEvents6(noTraversalControl,chain)) = 2
    /\ Cardinality(ForcedEndEvents6([noTraversalControl EXCEPT !.phaseEndedIds = {52}],chain)) = 1
    /\ ~EndTraversalDuringForced6(noTraversalControl,EndTraversalOutcome6(noTraversalControl,0),chain,deadChain,{},{52,53},0,ForcedEndEvents6(noTraversalControl,chain))
    /\ ~WithFullySuppressInstruction6(OpenEncounter6(53,2,1,FALSE,"traversal",<<1,2>>)).fullyBarrierInstructionSuppressed

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalControlFixture6, AllCurrentSubsBarrierInstructionSuppressed6, BeginEncounter6, BeginEncounterPaid6, BypassEncounter6, BypassTraversalRedirect6, CompleteEncounter6, EndTraversalDuringForced6, EndTraversalEffectEvents6, EndTraversalOutcome6, ForcedEndEvents6, ForcedEndOutcome6, ForcedInstructionFinished6, MoveTraversalDuringForcedEncounter6, NewFullySuppressInstructionEvents6, NextEncounterSub6, NoTraversal6, OpenEncounter6, OpenTraversal6, PaidSuppressInstructionEncounterSubs6, PushForcedEncounter6, ResolveEncounterSub6, ReturnForcedEncounter6, SuppressInstructionEncounterSubs6, UpdateEncounterSubs6, WithFullySuppressInstruction6

GeneralTraversalChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

GeneralTraversalChecks6 ==
 LET r == [OpenTraversal6(1,10,"action1") EXCEPT !.formalBegun = TRUE,!.phase = "Movement",
                                               !.step = "ProcedureCode4f60245a1dde",!.attacked = "SchemaAtom018",!.position = "pos1"]
     b == TraversalControlFixture6(r)
     target == [phase |-> "Approach",phaseId |-> 11,step |-> "ProcedureCode453e949a114f",attacked |-> "SchemaAtom018",position |-> "pos1"]
     req == [b EXCEPT !.redirect = target,!.phaseStepsSkipped = TRUE,!.traversal.usedPhaseIds = {10,11},!.redirectStage = "PaidWindow"]
     win == [req EXCEPT !.paidOpen = FALSE,!.redirectStage = "Checkpoint",!.redirectCheckpointDue = TRUE,!.phaseEndedIds = {10}]
     checked == [win EXCEPT !.redirectStage = "Ready",!.redirectCheckpointDue = FALSE]
     committed == [checked EXCEPT !.traversal.phase = "Approach",!.traversal.step = "ProcedureCode453e949a114f",!.traversal.phaseId = 11,
          !.traversal.usedPhaseIds = {10,11},!.redirect = NoTraversalRedirect6,!.redirectStage = "NoValue",!.phaseStepsSkipped = FALSE]
     edge == [traversalId |-> 1,standard |-> TRUE,from |-> "Encounter",to |-> "Pass",
              fromBarrier |-> "barrierObj",toBarrier |-> "barrierObj",encounterId |-> 50]
     scoped == [b EXCEPT !.traversal = NoTraversal6,!.encounter = 50,
          !.itemInspections = [outer |-> [encounterAncestors |-> {}],inner |-> [encounterAncestors |-> {50}]],
          !.siteInspections = [inner |-> [encounterAncestors |-> {50}]]]
     noTraversalEnd == EndTraversalOutcome6(scoped,0)
     end == EndTraversalOutcome6(b,12)
     noPaid == [b EXCEPT !.paidOpen = FALSE]
     noPaidReq == [noPaid EXCEPT !.redirect = target,!.phaseStepsSkipped = TRUE,!.traversal.usedPhaseIds = {10,11},
                                !.redirectStage = "Checkpoint",!.redirectCheckpointDue = TRUE,!.phaseEndedIds = {10}]
     inTraversalScopes == [scoped EXCEPT !.traversal = r]
     lateScopes == [inTraversalScopes EXCEPT !.traversal = end.traversal]
     lateEnd == EndTraversalOutcome6(lateScopes,0)
     target2 == [target EXCEPT !.phaseId = 13,!.attacked = "SchemaAtom082",!.position = "pos2"]
     retargeted == [req EXCEPT !.redirect = target2,!.traversal.attacked = "SchemaAtom082",
                    !.traversal.position = "pos2",!.traversal.usedPhaseIds = {10,11,13}]
 IN /\ Cardinality(TraversalPhases6) = 6 /\ OpenTraversal6(1,10,"action1").phase = "Initiation"
    /\ TraversalFrameValid6(r) /\ TraversalFrameValid6(NoTraversal6)
    /\ ~DuringTraversal6(OpenTraversal6(1,10,"action1")) /\ DuringTraversal6(r) /\ DuringTraversal6(end.traversal)
    /\ DirectAttackedTargetSiteChange6(r,[r EXCEPT !.attacked = "SchemaAtom082"],"SchemaAtom082",TRUE)
    /\ ~DirectAttackedTargetSiteChange6(r,[r EXCEPT !.attacked = "SchemaAtom082",!.phase = "Approach"],"SchemaAtom082",TRUE)
    /\ IndependentEncounterTraversalView6(r,r,TRUE)
    /\ RequestTraversalRedirect6(b,req,target,TRUE,{})
    /\ ~RequestTraversalRedirect6(b,req,target,FALSE,{})
    /\ RequestTraversalRedirect6(noPaid,noPaidReq,target,TRUE,{TraversalPhaseEndEvent6(r)})
    /\ RetargetTraversalRedirect6(req,retargeted,target2,TRUE,{})
    /\ retargeted.paidOpen /\ retargeted.traversal.phase = "Movement"
    /\ ~RetargetTraversalRedirect6(req,retargeted,target2,FALSE,{})
    /\ ~CommitTraversalRedirect6(req,committed) /\ ~FinishRedirectPaidWindow6(req,win,FALSE,{TraversalPhaseEndEvent6(r)})
    /\ FinishRedirectPaidWindow6(req,win,TRUE,{TraversalPhaseEndEvent6(r)})
    /\ ~CommitTraversalRedirect6(win,committed)
    /\ EndTraversalEffectEvents6(win) = {}
    /\ EndTraversalEffectEvents6(checked) = {}
    /\ EndTraversalEffectEvents6(end) = {}
    /\ lateEnd.traversal = end.traversal /\ lateEnd.encounter = 0
    /\ DOMAIN lateEnd.itemInspections = {} /\ DOMAIN lateEnd.siteInspections = {}
    /\ EndTraversalEffectEvents6(lateScopes) =
          {[tag |-> "PhaseEnds",phase |-> "Encounter",phaseId |-> 50,traversalId |-> 1]}
    /\ FinishRedirectCheckpoint6(win,checked,TRUE) /\ ~FinishRedirectCheckpoint6(win,checked,FALSE)
    /\ CommitTraversalRedirect6(checked,committed)
    /\ CommitTraversalRedirect6([checked EXCEPT !.traversal.attacked = "SchemaAtom082"],
                          [committed EXCEPT !.traversal.attacked = "SchemaAtom082"])
    /\ ~RequestTraversalRedirect6(b,req,[target EXCEPT !.phaseId = 10],TRUE,{})
    /\ EncounterAfterApproach6([edge EXCEPT !.from = "Approach",!.to = "Encounter"])
    /\ PassAfterEncounter6(edge) /\ ~PassAfterEncounter6([edge EXCEPT !.standard = FALSE])
    /\ PassAfterFullySuppressInstruction6(edge,{[traversalId |-> 1,encounterId |-> 50,barrierCard |-> "barrierObj"]})
    /\ ~PassAfterFullySuppressInstruction6(edge,{[traversalId |-> 1,encounterId |-> 49,barrierCard |-> "barrierObj"]})
    /\ EndTheTraversal6(b,end,12,TRUE,{TraversalPhaseEndEvent6(r)})
    /\ ~EndTheTraversal6(b,end,12,FALSE,{TraversalPhaseEndEvent6(r)})
    /\ EndTraversalOutcome6(inTraversalScopes,12).itemInspections = EmptyFrames6
    /\ EndTraversalOutcome6(inTraversalScopes,12).siteInspections = EmptyFrames6
    /\ EndTraversalOutcome6(inTraversalScopes,12).encounter = 0
    /\ end.paidOpen /\ end.windows = b.windows /\ end.windowCleanupDue /\ ~end.traversal.complete
    /\ end.traversal.step = "ProcedureCode6ea937bb44ac" /\ ~end.traversal.withdrewTraversal
    /\ EndTheTraversal6(scoped,noTraversalEnd,0,TRUE,EndTraversalEffectEvents6(scoped))
    /\ DOMAIN noTraversalEnd.itemInspections = {"outer"} /\ DOMAIN noTraversalEnd.siteInspections = {}
    /\ noTraversalEnd.traversal = NoTraversal6 /\ noTraversalEnd.onlyWindowCleanup
    /\ EndTheTraversal6(TraversalControlFixture6(NoTraversal6),TraversalControlFixture6(NoTraversal6),0,TRUE,{})
    /\ WithdrawTraversal6(b,[end EXCEPT !.traversal.withdrewTraversal = TRUE],12,TRUE,TRUE,TRUE,{TraversalPhaseEndEvent6(r)})
    /\ ~WithdrawTraversal6(b,end,12,TRUE,FALSE,TRUE,{TraversalPhaseEndEvent6(r)})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyFrames6, TraversalControlFixture6, CommitTraversalRedirect6, DirectAttackedTargetSiteChange6, DuringTraversal6, EncounterAfterApproach6, EndTheTraversal6, EndTraversalEffectEvents6, EndTraversalOutcome6, FinishRedirectCheckpoint6, FinishRedirectPaidWindow6, IndependentEncounterTraversalView6, NoTraversal6, NoTraversalRedirect6, OpenTraversal6, PassAfterEncounter6, PassAfterFullySuppressInstruction6, RequestTraversalRedirect6, RetargetTraversalRedirect6, TraversalFrameValid6, TraversalPhaseEndEvent6, TraversalPhases6, WithdrawTraversal6

Init6 · operator

reference-profile · input revision 2 · CC0 1.0

Init6 == block6 \in 1..9

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block6

InitiationChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

InitiationChecks6 ==
 LET i == OpenInitiation6(OpenTraversal6(1,10,"action1"))
     announced == [i EXCEPT !.traversal.attacked = "SchemaAtom082",!.announced = TRUE,!.costsPaid = TRUE]
     bp == [announced EXCEPT !.traversal.step = "ProcedureCodeacc82dbcc545"]
     funded == [bp EXCEPT !.badPubAdded = TRUE]
     beginning == [funded EXCEPT !.traversal.step = "ProcedureCode4d6bd06d2c9f"]
     begun == [beginning EXCEPT !.traversal.formalBegun = TRUE]
     last == [begun.traversal EXCEPT !.step = "ProcedureCode7e3f7e5033c8",!.position = "outer"]
     next == [last EXCEPT !.phase = "Approach",!.step = "ProcedureCode453e949a114f",!.phaseId = 11,!.usedPhaseIds = {10,11}]
     ev == {[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 1,targetSite |-> "SchemaAtom082"]}
     targetSites == [SchemaAtom082 |-> 1,blocked |-> 1]
 IN /\ AnnounceTraversalTargetSite6(i,announced,"SchemaAtom082",targetSites,TRUE,TRUE,ev)
    /\ ~AnnounceTraversalTargetSite6(i,announced,"SchemaAtom082",targetSites,FALSE,TRUE,ev)
    /\ ~AnnounceTraversalTargetSite6(i,announced,"SchemaAtom082",targetSites,TRUE,FALSE,ev)
    /\ ~AnnounceTraversalTargetSite6(i,[announced EXCEPT !.traversal.attacked = "missing"],"missing",targetSites,TRUE,TRUE,
          {[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 1,targetSite |-> "missing"]})
    /\ ~DuringTraversal6(announced.traversal)
    /\ AddInitiationLiabilityMarker6(bp,funded,0,2,2)
    /\ AddInitiationLiabilityMarker6(bp,funded,1,3,2)
    /\ ~AddInitiationLiabilityMarker6(bp,funded,0,3,2)
    /\ ~AddInitiationLiabilityMarker6(bp,funded,0,2,-1)
    /\ ~AddInitiationLiabilityMarker6(i,[i EXCEPT !.badPubAdded = TRUE],0,2,2)
    /\ FormalTraversalBegin6(beginning,begun,{TraversalBeginEvent6(beginning.traversal)})
    /\ ~FormalTraversalBegin6([beginning EXCEPT !.costsPaid = FALSE],[begun EXCEPT !.costsPaid = FALSE],{TraversalBeginEvent6(beginning.traversal)})
    /\ ~FormalTraversalBegin6([beginning EXCEPT !.badPubAdded = FALSE],[begun EXCEPT !.badPubAdded = FALSE],{TraversalBeginEvent6(beginning.traversal)})
    /\ ~FormalTraversalBegin6([beginning EXCEPT !.announced = FALSE],[begun EXCEPT !.announced = FALSE],{TraversalBeginEvent6(beginning.traversal)})
    /\ ~FormalTraversalBegin6([beginning EXCEPT !.traversal.step = "ProcedureCodeacc82dbcc545"],[begun EXCEPT !.traversal.step = "ProcedureCodeacc82dbcc545"],{TraversalBeginEvent6(beginning.traversal)})
    /\ ~AddInitiationLiabilityMarker6([bp EXCEPT !.traversal.step = "ProcedureCode4d6bd06d2c9f"],[funded EXCEPT !.traversal.step = "ProcedureCode4d6bd06d2c9f"],0,2,2)
    /\ ~AddInitiationLiabilityMarker6(bp,funded,0,-1,-1)
    /\ DuringTraversal6(begun.traversal) /\ TraversalBeginEvent6(beginning.traversal).alsoInitiates
    /\ DirectAttackedTargetSiteChange6(begun.traversal,[begun.traversal EXCEPT !.attacked = "blocked"],"blocked",TRUE)
    /\ CompleteInitiationTraversalView6(last,next,PositionFixture6,11,TRUE)
    /\ ~CompleteInitiationTraversalView6(last,next,PositionFixture6,11,FALSE)
    /\ InitiationDestination6(last,[PositionFixture6 EXCEPT !.slots["outer"].barrierCard = 0]) = "Movement"
    /\ InitiationDestination6([last EXCEPT !.position = "NoValue"],PositionFixture6) = "Movement"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionFixture6, AddInitiationLiabilityMarker6, AnnounceTraversalTargetSite6, CompleteInitiationTraversalView6, DirectAttackedTargetSiteChange6, DuringTraversal6, FormalTraversalBegin6, InitiationDestination6, OpenInitiation6, OpenTraversal6, TraversalBeginEvent6

MovementChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

MovementChecks6 ==
 LET r == [OpenTraversal6(1,10,"action1") EXCEPT !.formalBegun = TRUE,!.phase = "Movement",!.step = "ProcedureCode714dfe070fed",!.position = "outer",!.attacked = "SchemaAtom082"]
     m == OpenMovement6(r,"Encounter",2,50,TRUE)
     begun == [m EXCEPT !.begun = TRUE,!.passedBarrier = 2]
     decision == [r EXCEPT !.step = "ProcedureCode9bca3a096549"]
     declined == [begun EXCEPT !.declined = TRUE]
     advanceTraversal == [r EXCEPT !.step = "ProcedureCoded4ddeafb5f2f"]
     inward == [advanceTraversal EXCEPT !.position = "inner"]
     advanced == [declined EXCEPT !.advanced = TRUE,!.movedToNew = TRUE]
     innerTraversal == [r EXCEPT !.position = "inner"]
     emptyTraversal == [r EXCEPT !.position = "NoValue"]
     ctl == TraversalControlFixture6(decision)
     ended == [EndTraversalOutcome6(ctl,11) EXCEPT !.traversal.withdrewTraversal = TRUE]
     last == [r EXCEPT !.step = "ProcedureCodea732fbc12ae0",!.position = "NoValue"]
     doneM == [declined EXCEPT !.advanced = TRUE,!.approachedTargetSite = TRUE]
     success == [last EXCEPT !.phase = "Success",!.step = "ProcedureCodebbb14496b09b",!.phaseId = 11,!.usedPhaseIds = {10,11},!.reachedSuccess = TRUE]
     hole == [PositionFixture6 EXCEPT !.slots["outer"].barrierCard = 0,!.slots["outer"].retained = TRUE]
     released == [hole EXCEPT !.orders["SchemaAtom082"] = <<"inner">>,!.slots = [p \in DOMAIN hole.slots \ {"outer"} |-> hole.slots[p]]]
 IN /\ BeginMovement6(r,m,begun,PositionFixture6,MovementPassEvents6(r,PositionFixture6))
    /\ Cardinality(MovementPassEvents6(innerTraversal,PositionFixture6)) = 2
    /\ MovementPassEvents6(emptyTraversal,PositionFixture6) = {}
    /\ MovementPassEvents6(r,[PositionFixture6 EXCEPT !.slots["outer"].barrierCard = 0]) = {}
    /\ ~BeginMovement6(r,begun,begun,PositionFixture6,MovementPassEvents6(r,PositionFixture6))
    /\ PassAfterEncounter6(MovementPassEdge6(begun))
    /\ ~PassAfterEncounter6(MovementPassEdge6([begun EXCEPT !.fromBarrier = 3]))
    /\ ~PassAfterFullySuppressInstruction6(MovementPassEdge6([begun EXCEPT !.fromBarrier = 3]),
          {[traversalId |-> 1,encounterId |-> 50,barrierCard |-> 2]})
    /\ ~PassAfterEncounter6(MovementPassEdge6(m))
    /\ ~PassAfterEncounter6(MovementPassEdge6([begun EXCEPT !.passedBarrier = 0]))
    /\ ~PassAfterEncounter6(MovementPassEdge6([begun EXCEPT !.standard = FALSE]))
    /\ ~PassAfterEncounter6(MovementPassEdge6([begun EXCEPT !.from = "Initiation"]))
    /\ MovementWithdrawTraversal6(ctl,ended,begun,PositionFixture6,PositionFixture6,11,TRUE,TRUE,TRUE,EndTraversalEffectEvents6(ctl))
    /\ ~MovementWithdrawTraversal6(ctl,ended,begun,PositionFixture6,PositionFixture6,11,TRUE,TRUE,FALSE,EndTraversalEffectEvents6(ctl))
    /\ ~MovementWithdrawTraversal6([ctl EXCEPT !.traversal.step = "ProcedureCode4f60245a1dde"],[ended EXCEPT !.traversal.step = "ProcedureCode6ea937bb44ac"],begun,PositionFixture6,PositionFixture6,11,TRUE,TRUE,TRUE,EndTraversalEffectEvents6(ctl))
    /\ DeclineMovementWithdrawTraversal6(decision,begun,declined,TRUE)
    /\ ~DeclineMovementWithdrawTraversal6(decision,begun,declined,FALSE)
    /\ AdvanceMovement6(advanceTraversal,inward,declined,advanced,PositionFixture6,PositionFixture6)
    /\ AdvanceMovement6(advanceTraversal,inward,declined,advanced,hole,released)
    /\ ~AdvanceMovement6(advanceTraversal,inward,declined,advanced,hole,hole)
    /\ ~AdvanceMovement6(advanceTraversal,inward,begun,[begun EXCEPT !.advanced = TRUE,!.movedToNew = TRUE],PositionFixture6,PositionFixture6)
    /\ ~ApproachTargetSite6([r EXCEPT !.step = "ProcedureCode7e82ab2b38b7"],advanced,[advanced EXCEPT !.approachedTargetSite = TRUE],
           {[tag |-> "ApproachTargetSite",traversalId |-> 1,targetSite |-> "SchemaAtom082",phaseId |-> 10]})
    /\ ApproachTargetSite6([last EXCEPT !.step = "ProcedureCode7e82ab2b38b7"],[doneM EXCEPT !.approachedTargetSite = FALSE],doneM,
           {[tag |-> "ApproachTargetSite",traversalId |-> 1,targetSite |-> "SchemaAtom082",phaseId |-> 10]})
    /\ CompleteMovementTraversalView6(last,success,doneM,11,TRUE)
    /\ ~CompleteMovementTraversalView6(last,success,doneM,11,FALSE)
    /\ CompleteMovementTraversalView6([inward EXCEPT !.step = "ProcedureCode6c5d14f545f7"],
           [inward EXCEPT !.step = "ProcedureCode453e949a114f",!.phase = "Approach",!.phaseId = 11,!.usedPhaseIds = {10,11}],advanced,11,TRUE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionFixture6, TraversalControlFixture6, AdvanceMovement6, ApproachTargetSite6, BeginMovement6, CompleteMovementTraversalView6, DeclineMovementWithdrawTraversal6, EndTraversalEffectEvents6, EndTraversalOutcome6, MovementPassEdge6, MovementPassEvents6, MovementWithdrawTraversal6, OpenMovement6, OpenTraversal6, PassAfterEncounter6, PassAfterFullySuppressInstruction6

Next6 · operator

reference-profile · input revision 2 · CC0 1.0

Next6 == UNCHANGED block6

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block6

PositionChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

PositionChecks6 ==
 LET b == PositionFixture6
     declared == [b EXCEPT !.orders["SchemaAtom082"] = <<"inner","new","outer">>,
                !.slots = [p \in {"inner","new","outer","other"} |-> IF p = "new"
                            THEN [targetSite |-> "SchemaAtom082",barrierCard |-> 0,reservation |-> 9,retained |-> FALSE] ELSE b.slots[p]],
                !.used = @ \cup {"new"}]
     deployed == [declared EXCEPT !.slots["new"].barrierCard = 4,!.slots["new"].reservation = 0]
     empty == [b EXCEPT !.slots["inner"].barrierCard = 0]
     retained == [empty EXCEPT !.slots["inner"].retained = TRUE]
     cleaned == [empty EXCEPT !.orders["SchemaAtom082"] = <<"outer">>,
              !.slots = [p \in {"outer","other"} |-> empty.slots[p]]]
     r == [OpenTraversal6(1,10,"action") EXCEPT !.attacked = "SchemaAtom082",!.position = "outer",!.phase = "Encounter",!.step = "ProcedureCode8b3260c0010f"]
     historic == [targetSite |-> "SchemaAtom082",gap |-> 1]
     swapped == [b EXCEPT !.slots["outer"].barrierCard = 3,!.slots["other"].barrierCard = 2]
     moved == [b EXCEPT !.orders["SchemaAtom018"] = <<"other","moved">>,!.slots["outer"].barrierCard = 0,
          !.slots = [p \in {"inner","outer","other","moved"} |-> IF p = "moved"
                     THEN [targetSite |-> "SchemaAtom018",barrierCard |-> 2,reservation |-> 0,retained |-> FALSE]
                     ELSE IF p = "outer" THEN [b.slots[p] EXCEPT !.barrierCard = 0] ELSE b.slots[p]],
          !.used = @ \cup {"moved"}]
     ctl == TraversalControlFixture6(r)
     pending == [ctl EXCEPT !.traversal.position = "other",!.traversal.attacked = "SchemaAtom018",
          !.traversal.usedPhaseIds = {10,11},!.phaseStepsSkipped = TRUE,!.redirectStage = "PaidWindow",
          !.redirect = SideBMoveToBarrierTarget6(r,b,"other","Approach",11)]
     retargeted == [pending EXCEPT !.traversal.position = "inner",!.traversal.attacked = "SchemaAtom082",
          !.traversal.usedPhaseIds = {10,11,13},!.redirect = SideBMoveToBarrierTarget6(r,b,"inner","Approach",13)]
     outerTarget == [pending EXCEPT !.traversal.position = "outer",!.traversal.attacked = "SchemaAtom082",
          !.traversal.usedPhaseIds = {10,11,14},!.redirect = SideBMoveToOutermostTarget6(r,b,"SchemaAtom082",14)]
     innerTraversal == [r EXCEPT !.phase = "Movement",!.position = "inner"]
 IN /\ PositionLayoutValid6(b,{1,2,3})
    /\ SamePosition6(b,"inner","other") /\ ~SamePosition6(b,"outer","other")
    /\ PositionGapAllowed6(b.orders["SchemaAtom082"],"Outermost","NoValue",2,0)
    /\ PositionGapAllowed6(b.orders["SchemaAtom082"],"Innermost","NoValue",0,2)
    /\ DeclareBarrierPosition6(b,declared,"new","SchemaAtom082",1,"DirectlyInward","outer",historic,9,"ProcedureCode6eba7e0bfa75")
    /\ ~DeclareBarrierPosition6([b EXCEPT !.used = @ \cup {"new"}],declared,"new","SchemaAtom082",1,"DirectlyInward","outer",historic,9,"ProcedureCode6eba7e0bfa75")
    /\ ~DeclareBarrierPosition6(b,declared,"new","SchemaAtom082",1,"Outermost","outer",historic,9,"ProcedureCode6eba7e0bfa75")
    /\ ~DeclareBarrierPosition6(b,declared,"new","SchemaAtom082",1,"HistoricalPlace","NoValue",[historic EXCEPT !.targetSite = "SchemaAtom018"],9,"ProcedureCode6eba7e0bfa75")
    /\ OccupyDeclaredPosition6(declared,deployed,"new",9,4,"ProcedureCode0f76bcc2eb00",TRUE)
    /\ ~OccupyDeclaredPosition6(declared,deployed,"new",8,4,"ProcedureCode0f76bcc2eb00",TRUE)
    /\ ~OccupyDeclaredPosition6(declared,deployed,"new",9,4,"ProcedureCode6eba7e0bfa75",TRUE)
    /\ PositionCleanup6(declared,declared,"NoValue","ProcedureCode2d6279f9d639")
    /\ CancelPositionReservation6(declared,[declared EXCEPT !.slots["new"].reservation = 0],"new",9,TRUE)
    /\ VacatePosition6(b,empty,"inner",TRUE)
    /\ PositionCleanup6(empty,retained,"inner","ProcedureCode2d6279f9d639")
    /\ ReleaseDepartedSideBPosition6(retained,cleaned,"inner","outer")
    /\ ReleaseDepartedSideBPosition6(empty,empty,"inner","outer")
    /\ RetainedPositionValid6(retained,innerTraversal)
    /\ ~RetainedPositionValid6(retained,[innerTraversal EXCEPT !.position = "NoValue"])
    /\ SideBAdvanceWithPositionCleanup6(innerTraversal,[innerTraversal EXCEPT !.position = "NoValue"],retained,cleaned,"ProcedureCoded4ddeafb5f2f")
    /\ SideBAdvanceWithPositionCleanup6(innerTraversal,[innerTraversal EXCEPT !.position = "NoValue"],empty,empty,"ProcedureCoded4ddeafb5f2f")
    /\ PositionCleanup6(empty,cleaned,"NoValue","ProcedureCode2d6279f9d639")
    /\ ~PositionCleanup6(empty,cleaned,"inner","ProcedureCode2d6279f9d639")
    /\ ~PositionCleanup6(empty,cleaned,"NoValue","ProcedureCode2d73b20aa788")
    /\ cleaned.used = b.used
    /\ SwapIntoPosition6(b,swapped,"outer",3,"other",TRUE)
    /\ MoveBarrierPosition6(b,moved,"outer","moved","SchemaAtom018",1,TRUE)
    /\ ~MoveBarrierPosition6(b,moved,"outer","moved","SchemaAtom018",1,FALSE)
    /\ PositionLayoutValid6(moved,{1,2,3})
    /\ swapped.orders = b.orders
    /\ SideBPositionValid6(r,declared)
    /\ NextInwardPosition6(declared,"SchemaAtom082","outer") = "new"
    /\ NextInwardPosition6(b,"SchemaAtom082","inner") = "NoValue"
    /\ SetInitialSideBPosition6([r EXCEPT !.phase = "Initiation"],[r EXCEPT !.phase = "Initiation"],b,"ProcedureCode347de0bdd6b4")
    /\ BarrierChangeTraversalPlan6(r,"Move","other","SchemaAtom018").traversal.position = "other"
    /\ BarrierChangeTraversalPlan6(r,"Move","other","SchemaAtom018").traversal.attacked = "SchemaAtom018"
    /\ BarrierChangeTraversalPlan6([r EXCEPT !.phase = "Approach"],"Swap","other","SchemaAtom018").traversal = [r EXCEPT !.phase = "Approach"]
    /\ BarrierChangeTraversalPlan6([r EXCEPT !.phase = "Approach"],"Move","other","SchemaAtom018").needsRedirect
    /\ BarrierChangeTraversalPlan6(r,"Deactivation","NoValue","NoValue").needsRedirect
    /\ BarrierChangeTraversalPlan6([r EXCEPT !.phase = "Movement"],"Swap","other","SchemaAtom018").traversal = [r EXCEPT !.phase = "Movement"]
    /\ SideBMoveNoOp6([r EXCEPT !.phase = "Success"],"other","Encounter")
    /\ SideBMoveNoOp6([r EXCEPT !.phase = "Approach"],"outer","Approach")
    /\ SideBMoveInstructionClass6(r,"outer","Encounter") = "ForcedEncounter"
    /\ SideBMoveInstructionClass6(r,"other","Encounter") = "Redirect"
    /\ SideBPositionMoveRequest6(ctl,pending,b,b,"other","Approach",11,TRUE,{})
    /\ SideBPositionMoveRequest6(pending,retargeted,b,b,"inner","Approach",13,TRUE,{})
    /\ SideBOutermostMoveRequest6(pending,outerTarget,b,b,"SchemaAtom082",14,TRUE,{})
    /\ SamePosition6(empty,"outer","outer") /\ ~SamePosition6(empty,"outer","other")
    /\ SideBMoveToBarrierTarget6(r,b,"other","Encounter",11).step = "ProcedureCodeda7bff1d9270"
    /\ SideBMoveToOutermostTarget6(r,b,"SchemaAtom018",11).position = "other"
    /\ ~SideBPositionValid6([r EXCEPT !.phase = "TraversalEnds"],b)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionFixture6, TraversalControlFixture6, BarrierChangeTraversalPlan6, CancelPositionReservation6, DeclareBarrierPosition6, MoveBarrierPosition6, NextInwardPosition6, OccupyDeclaredPosition6, OpenTraversal6, PositionCleanup6, PositionGapAllowed6, PositionLayoutValid6, ReleaseDepartedSideBPosition6, RetainedPositionValid6, SamePosition6, SetInitialSideBPosition6, SideBAdvanceWithPositionCleanup6, SideBMoveInstructionClass6, SideBMoveNoOp6, SideBMoveToBarrierTarget6, SideBMoveToOutermostTarget6, SideBOutermostMoveRequest6, SideBPositionMoveRequest6, SideBPositionValid6, SwapIntoPosition6, VacatePosition6

PositionFixture6 · operator

reference-profile · input revision 2 · CC0 1.0

PositionFixture6 ==
 [orders |-> [SchemaAtom082 |-> <<"inner","outer">>,SchemaAtom018 |-> <<"other">>],
  slots |-> [inner |-> [targetSite |-> "SchemaAtom082",barrierCard |-> 1,reservation |-> 0,retained |-> FALSE],
             outer |-> [targetSite |-> "SchemaAtom082",barrierCard |-> 2,reservation |-> 0,retained |-> FALSE],
             other |-> [targetSite |-> "SchemaAtom018",barrierCard |-> 3,reservation |-> 0,retained |-> FALSE]],
  used |-> {"inner","outer","other"}]

Exact module download · Source bundle and reproduction instructions

ProcedureChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

ProcedureChecks6 ==
 LET r == [OpenTraversal6(1,10,"action1") EXCEPT !.formalBegun = TRUE,!.step = "ProcedureCode7e3f7e5033c8",!.position = "outer",!.attacked = "SchemaAtom082"]
     ctl == [TraversalControlFixture6(r) EXCEPT !.paidOpen = FALSE,!.windows = {}]
     dummyE == OpenEncounter6(0,0,1,FALSE,"traversal",<<>>)
     dummyM == OpenMovement6(r,"Initiation",0,0,TRUE)
     next == [ctl EXCEPT !.traversal.phase = "Approach",!.traversal.step = "ProcedureCode453e949a114f",!.traversal.phaseId = 11,!.traversal.usedPhaseIds = {10,11},!.phaseEndedIds = {10}]
     endedCtl == [ctl EXCEPT !.phaseEndedIds = {10}]
     forced == [OpenEncounter6(50,2,0,TRUE,"itemInspection",<<>>) EXCEPT !.stage = "Complete"]
     encR == [r EXCEPT !.phase = "Encounter",!.phaseId = 50,!.usedPhaseIds = {10,50},!.step = "ProcedureCodef1914978bb8e"]
     encCtl == [TraversalControlFixture6(encR) EXCEPT !.paidOpen = FALSE,!.windows = {},!.encounter = 50]
     resolvedE == [OpenEncounter6(50,2,1,FALSE,"traversal",<<1>>) EXCEPT !.stage = "BarrierInstructions",!.resolved = {1}]
 IN /\ Cardinality(TraversalSteps6) = 29
    /\ \A step \in TraversalSteps6 : TraversalStepInfo6(step).kind # "Invalid" /\ TraversalStepInfo6(step).phase \in TraversalPhases6
    /\ \A step \in TraversalSteps6 : ~TraversalWindowOptions6(step).score
    /\ {s \in TraversalSteps6 : TraversalWindowOptions6(s).paid} = {"ProcedureCode71e36c9e8e04","ProcedureCode3a6daf593ad4","ProcedureCode8b3260c0010f","ProcedureCode4f60245a1dde","ProcedureCode2cd618a9e624"}
    /\ {s \in TraversalSteps6 : TraversalWindowOptions6(s).nonBarrierActivation} = {"ProcedureCode71e36c9e8e04","ProcedureCode3a6daf593ad4","ProcedureCode2cd618a9e624"}
    /\ {s \in TraversalSteps6 : TraversalWindowOptions6(s).approachedBarrierActivation} = {"ProcedureCode3a6daf593ad4"}
    /\ NextTraversalStep6("ProcedureCodef1914978bb8e","BarrierInstruction") = "ProcedureCodeaa0828fbf852" /\ NextTraversalStep6("ProcedureCodeaa0828fbf852","Next") = "ProcedureCodef1914978bb8e"
    /\ NextTraversalStep6("ProcedureCode9bca3a096549","WithdrawTraversal") = "ProcedureCode6ea937bb44ac"
    /\ BeginNormalTraversalPhaseEnd6(ctl,endedCtl,PositionFixture6,{},dummyE,dummyM,
          [jackChoice |-> "Continue",resolvedSub |-> 0],TRUE,{TraversalPhaseEndEvent6(r)})
    /\ ~BeginNormalTraversalPhaseEnd6(endedCtl,endedCtl,PositionFixture6,{},dummyE,dummyM,
          [jackChoice |-> "Continue",resolvedSub |-> 0],TRUE,{TraversalPhaseEndEvent6(r)})
    /\ ~AdvanceNormalTraversalStep6(ctl,next,PositionFixture6,{},dummyE,dummyM,
          [jackChoice |-> "Continue",resolvedSub |-> 0],11,TRUE,TRUE,{})
    /\ AdvanceNormalTraversalStep6(endedCtl,next,PositionFixture6,{},dummyE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 0],11,TRUE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6(endedCtl,next,PositionFixture6,{},dummyE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 0],11,FALSE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6(endedCtl,[next EXCEPT !.traversal.phaseId = 10,!.traversal.usedPhaseIds = {10}],
          PositionFixture6,{},dummyE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 0],10,TRUE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6(endedCtl,next,PositionFixture6,{},dummyE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 0],11,TRUE,FALSE,{})
    /\ ~AdvanceNormalTraversalStep6([endedCtl EXCEPT !.redirectCheckpointDue = TRUE],[next EXCEPT !.redirectCheckpointDue = TRUE],PositionFixture6,{},dummyE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 0],11,TRUE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6([endedCtl EXCEPT !.phaseStepsSkipped = TRUE],next,PositionFixture6,{},dummyE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 0],11,TRUE,TRUE,{})
    /\ ForcedEncounterStep6("ProcedureCode687f72772ab1","ReturnCaller",forced,forced,0,TRUE,TRUE)
    /\ ~ForcedEncounterStep6("ProcedureCode687f72772ab1","ReturnCaller",[forced EXCEPT !.stage = "BarrierInstructions"],[forced EXCEPT !.stage = "BarrierInstructions"],0,TRUE,TRUE)
    /\ TraversalBranch6([r EXCEPT !.step = "ProcedureCodef1914978bb8e"],PositionFixture6,{},
          [OpenEncounter6(50,2,1,FALSE,"traversal",<<1,2>>) EXCEPT !.resolved = {1,2}],dummyM,
          [jackChoice |-> "Continue",resolvedSub |-> 2]) = "BarrierInstruction"
    /\ ForcedEncounterStep6("ProcedureCodef1914978bb8e","ProcedureCodeaa0828fbf852",
          [forced EXCEPT !.stage = "BarrierInstructions",!.order = <<1>>,!.resolved = {1}],
          [forced EXCEPT !.stage = "BarrierInstructions",!.order = <<1>>,!.resolved = {1}],1,TRUE,TRUE)
    /\ ~ForcedEncounterStep6("ProcedureCodef1914978bb8e","ProcedureCodeaa0828fbf852",
          [forced EXCEPT !.order = <<1>>,!.resolved = {1}],
          [forced EXCEPT !.order = <<1>>,!.resolved = {1}],1,TRUE,TRUE)
    /\ AdvanceNormalTraversalStep6(encCtl,[encCtl EXCEPT !.traversal.step = "ProcedureCodeaa0828fbf852"],PositionFixture6,{2},
          resolvedE,dummyM,[jackChoice |-> "Continue",resolvedSub |-> 1],50,TRUE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6(encCtl,[encCtl EXCEPT !.traversal.step = "ProcedureCodeaa0828fbf852"],PositionFixture6,{2},
          [resolvedE EXCEPT !.stage = "Complete"],dummyM,[jackChoice |-> "Continue",resolvedSub |-> 1],50,TRUE,TRUE,{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PositionFixture6, TraversalControlFixture6, AdvanceNormalTraversalStep6, BeginNormalTraversalPhaseEnd6, ForcedEncounterStep6, NextTraversalStep6, OpenEncounter6, OpenMovement6, OpenTraversal6, TraversalBranch6, TraversalPhaseEndEvent6, TraversalPhases6, TraversalStepInfo6, TraversalSteps6, TraversalWindowOptions6

Spec6 · operator

reference-profile · input revision 2 · CC0 1.0

Spec6 == Init6 /\ [][Next6]_block6

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Init6, Next6, block6

SuccessChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

SuccessChecks6 ==
 LET r == [OpenTraversal6(1,10,"action1") EXCEPT !.formalBegun = TRUE,!.phase = "Success",!.step = "ProcedureCodebbb14496b09b",!.attacked = "auxiliarySite1",!.reachedSuccess = TRUE]
     s == OpenSuccess6(r)
     declared == [s EXCEPT !.declarationProcessed = TRUE,!.traversal.successful = TRUE]
     suppressed == [s EXCEPT !.declarationProcessed = TRUE]
     b == [declared EXCEPT !.traversal.step = "ProcedureCoded75d879e00ff"]
     chosen == [b EXCEPT !.siteInspectionChosen = TRUE]
     finished == [chosen EXCEPT !.siteInspectionFinished = TRUE]
     last == [finished EXCEPT !.traversal.step = "ProcedureCodec7b41615d673"]
     ended == [last EXCEPT !.traversal.phase = "TraversalEnds",!.traversal.step = "ProcedureCode6ea937bb44ac",!.traversal.ending = TRUE,!.traversal.phaseId = 11,!.traversal.usedPhaseIds = {10,11}]
     origin == [traversalId |-> 1,targetSiteRestricted |-> TRUE]
     binding == [traversalId |-> 1]
     siteInspection == [traversalId |-> 1,origin |-> "RulesTraversalInspection"]
     reaction == SuccessfulTraversalReaction6(7,{"Ash"})
     closed == [reaction EXCEPT !.open = FALSE,!.pending = {},!.lostPending = {"Ash"}]
     directive == [kind |-> "Replacement",choice |-> "Specimen0004",traversalId |-> 1,targetSite |-> "auxiliarySite1",origin |-> "RulesTraversalInspection"]
 IN /\ DeclareSuccessfulTraversal6(s,declared,TRUE,{[tag |-> "SuccessfulTraversal",traversalId |-> 1,targetSite |-> "auxiliarySite1"]})
    /\ DeclareSuccessfulTraversal6(s,suppressed,FALSE,{})
    /\ suppressed.traversal.reachedSuccess /\ ~suppressed.traversal.successful
    /\ ~DeclareSuccessfulTraversal6(declared,declared,TRUE,{[tag |-> "SuccessfulTraversal",traversalId |-> 1,targetSite |-> "auxiliarySite1"]})
    /\ IfSuccessfulCondition6(origin,declared.traversal,{"auxiliarySite1","auxiliarySite2"})
    /\ IfSuccessfulCondition6(origin,[declared.traversal EXCEPT !.attacked = "auxiliarySite2"],{"auxiliarySite1","auxiliarySite2"})
    /\ ~IfSuccessfulCondition6(origin,[declared.traversal EXCEPT !.attacked = "SchemaAtom082"],{"auxiliarySite1","auxiliarySite2"})
    /\ ~IfSuccessfulCondition6([origin EXCEPT !.traversalId = 2],declared.traversal,{"auxiliarySite1","auxiliarySite2"})
    /\ ~IfSuccessfulCondition6(origin,suppressed.traversal,{"auxiliarySite1","auxiliarySite2"})
    /\ ~CloseEndedBeginReaction6(reaction,closed,{10})
    /\ TraversalInspectionModifierApplies6(binding,declared.traversal,siteInspection)
    /\ ~TraversalInspectionModifierApplies6(binding,declared.traversal,[siteInspection EXCEPT !.origin = "CardEffectInspection"])
    /\ ~TraversalInspectionModifierApplies6(binding,[declared.traversal EXCEPT !.complete = TRUE],siteInspection)
    /\ ~TraversalInspectionModifierApplies6(binding,declared.traversal,[siteInspection EXCEPT !.traversalId = 2])
    /\ ChooseRulesInspection6(b,chosen,"Specimen0004",{"Inspection","Specimen0004"},TRUE,directive)
    /\ ChooseRulesInspection6([b EXCEPT !.traversal.successful = FALSE],[chosen EXCEPT !.traversal.successful = FALSE],
          "Inspection",{"Inspection"},TRUE,
          [kind |-> "Inspection",choice |-> "Inspection",traversalId |-> 1,targetSite |-> "auxiliarySite1",origin |-> "RulesTraversalInspection"])
    /\ ~ChooseRulesInspection6(b,chosen,"Specimen0004",{"Inspection","Specimen0004"},FALSE,directive)
    /\ ~ChooseRulesInspection6(b,chosen,"Specimen0004",{"Inspection"},TRUE,directive)
    /\ ~ChooseRulesInspection6([b EXCEPT !.traversal.step = "ProcedureCodebbb14496b09b"],[chosen EXCEPT !.traversal.step = "ProcedureCodebbb14496b09b"],"Specimen0004",{"Inspection","Specimen0004"},TRUE,directive)
    /\ FinishRulesInspectionInstruction6(chosen,finished,TRUE)
    /\ ~FinishRulesInspectionInstruction6(chosen,finished,FALSE)
    /\ CompleteSuccessTraversalView6(last,ended,11,TRUE)
    /\ ~CompleteSuccessTraversalView6([last EXCEPT !.siteInspectionFinished = FALSE],[ended EXCEPT !.siteInspectionFinished = FALSE],11,TRUE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ChooseRulesInspection6, CloseEndedBeginReaction6, CompleteSuccessTraversalView6, DeclareSuccessfulTraversal6, FinishRulesInspectionInstruction6, IfSuccessfulCondition6, OpenSuccess6, OpenTraversal6, SuccessfulTraversalReaction6, TraversalInspectionModifierApplies6

TraversalControlFixture6 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalControlFixture6(r) ==
 [traversal |-> r,encounter |-> 0,siteInspections |-> EmptyFrames6,itemInspections |-> EmptyFrames6,
  abortedEncounters |-> {},abortedInspectiones |-> {},abortedItemInspectiones |-> {},
  paidOpen |-> TRUE,windows |-> {"paid","reaction"},windowCleanupDue |-> FALSE,
  onlyWindowCleanup |-> FALSE,phaseEndedIds |-> {},phaseStepsSkipped |-> FALSE,redirect |-> NoTraversalRedirect6,
  redirectStage |-> "NoValue",redirectCheckpointDue |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyFrames6, NoTraversalRedirect6

TraversalEndsChecks6 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalEndsChecks6 ==
 LET r == [OpenTraversal6(1,11,"action1") EXCEPT !.formalBegun = TRUE,!.phase = "TraversalEnds",!.step = "ProcedureCode6ea937bb44ac",!.ending = TRUE,!.attacked = "SchemaAtom082"]
     ctl == TraversalControlFixture6(r)
     paid == [id |-> 1,kind |-> "Paid",open |-> TRUE,beginPhaseId |-> 0,pending |-> {},lostPending |-> {},priority |-> "SideB"]
     begin == [paid EXCEPT !.id = 2,!.kind = "Reaction",!.beginPhaseId = 10,!.pending = {"Specimen0248","mandatory"}]
     other == [paid EXCEPT !.id = 3,!.kind = "Reaction",!.pending = {"Formicary"}]
     closedPaid == [paid EXCEPT !.open = FALSE,!.priority = "NoValue"]
     closedBegin == [begin EXCEPT !.open = FALSE,!.priority = "NoValue",!.pending = {},!.lostPending = {"Specimen0248","mandatory"}]
     closedOther == [other EXCEPT !.open = FALSE,!.priority = "NoValue",!.pending = {}]
     e == OpenTraversalEnd6(ctl,<<paid,begin,other>>)
     popped == [e EXCEPT !.windows = <<paid,begin>>]
     empty == [e EXCEPT !.windows = <<>>]
     drained == [empty EXCEPT !.windowsDone = TRUE]
     fund == [drained EXCEPT !.traversal.step = "ProcedureCode84dea7dc8ecc"]
     returnedFund == [fund EXCEPT !.fundReturned = TRUE]
     result == [returnedFund EXCEPT !.traversal.step = "ProcedureCode5e397645e65c"]
     declared == [result EXCEPT !.resultDeclared = TRUE,!.traversal.unsuccessful = TRUE]
     last == [declared EXCEPT !.traversal.step = "ProcedureCode9606a4cd52b4"]
     complete == [last EXCEPT !.traversal.complete = TRUE,!.phaseEndedIds = {11}]
     ev == {[tag |-> "TraversalEnds",traversalId |-> 1],TraversalPhaseEndEvent6(last.traversal)}
 IN /\ ProcessTraversalEndWindow6(<<paid>>,<<>>,closedPaid,FALSE,{},{})
    /\ ~ProcessTraversalEndWindow6(<<paid>>,<<>>,closedPaid,TRUE,{"SelfModifyingCode"},{})
    /\ ProcessTraversalEndWindow6(<<begin>>,<<>>,closedBegin,FALSE,{},{})
    /\ ~ProcessTraversalEndWindow6(<<begin>>,<<>>,closedBegin,TRUE,{"Specimen0248"},{})
    /\ ProcessTraversalEndWindow6(<<other>>,<<>>,closedOther,TRUE,{"ResolveFormicaryActivationAndMoveBarrier"},{})
    /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,closedOther,TRUE,{"ResolveFormicary"},{"Encounter"})
    /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,closedOther,TRUE,{},{"DelayedInspection"})
    /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,closedOther,FALSE,{},{})
    /\ TraversalEndWindowStep6(e,popped,closedOther,TRUE,{"ResolveFormicaryActivationAndMoveBarrier"},{})
    /\ ~TraversalEndWindowStep6(e,[e EXCEPT !.windows = <<paid,other>>],closedBegin,TRUE,{},{})
    /\ FinishTraversalEndWindows6(empty,drained)
    /\ ~FinishTraversalEndWindows6(e,[e EXCEPT !.windowsDone = TRUE])
    /\ ReturnLiabilityMarkerFund6(fund,returnedFund,2,0,5,7)
    /\ ~ReturnLiabilityMarkerFund6(fund,returnedFund,2,1,5,7)
    /\ ~ReturnLiabilityMarkerFund6(fund,returnedFund,2,0,5,5)
    /\ ~ReturnLiabilityMarkerFund6([fund EXCEPT !.windowsDone = FALSE],[returnedFund EXCEPT !.windowsDone = FALSE],2,0,5,7)
    /\ DeclareUnsuccessfulTraversal6(result,declared,[SchemaAtom082 |-> 1],{[tag |-> "UnsuccessfulTraversal",traversalId |-> 1,targetSite |-> "SchemaAtom082"]})
    /\ ~ShouldDeclareUnsuccessful6([r EXCEPT !.reachedSuccess = TRUE,!.successful = FALSE],[SchemaAtom082 |-> 1])
    /\ ~ShouldDeclareUnsuccessful6(r,[id \in {} |-> id])
    /\ DeclareUnsuccessfulTraversal6([result EXCEPT !.traversal.reachedSuccess = TRUE],
          [result EXCEPT !.traversal.reachedSuccess = TRUE,!.resultDeclared = TRUE],[SchemaAtom082 |-> 1],{})
    /\ DuringTraversal6(last.traversal) /\ StrengthScopeAlive([scope |-> "SchemaAtom138",token |-> 1],{last.traversal.id},{},0)
    /\ CompleteTraversal6(last,complete,TRUE,ev,{1})
    /\ ~CompleteTraversal6(last,complete,FALSE,ev,{1})
    /\ ~CompleteTraversal6([last EXCEPT !.resultDeclared = FALSE],[complete EXCEPT !.resultDeclared = FALSE],TRUE,ev,{1})
    /\ ~DuringTraversal6(complete.traversal) /\ ~StrengthScopeAlive([scope |-> "SchemaAtom138",token |-> 1],{},{},0)
    /\ ReturnTraversalToCaller6(complete,[complete EXCEPT !.returned = TRUE],TRUE,"action1")
    /\ ~ReturnTraversalToCaller6(last,[last EXCEPT !.returned = TRUE],TRUE,"action1")
    /\ ~ReturnTraversalToCaller6(complete,[complete EXCEPT !.returned = TRUE],FALSE,"action1")
    /\ ~CompleteTraversal6(complete,complete,TRUE,ev,{1})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalControlFixture6, CompleteTraversal6, DeclareUnsuccessfulTraversal6, DuringTraversal6, FinishTraversalEndWindows6, OpenTraversal6, OpenTraversalEnd6, ProcessTraversalEndWindow6, ReturnLiabilityMarkerFund6, ReturnTraversalToCaller6, ShouldDeclareUnsuccessful6, TraversalEndWindowStep6, TraversalPhaseEndEvent6, StrengthScopeAlive

block6 · variable

reference-profile · input revision 2 · CC0 1.0

block6

Exact module download · Source bundle and reproduction instructions