---------------------------- MODULE TraversalChecksMC ---------------------------- EXTENDS TraversalContracts VARIABLE block6 Init6 == block6 \in 1..9 Next6 == UNCHANGED block6 Spec6 == Init6 /\ [][Next6]_block6 EmptyFrames6 == [x \in {} |-> x] 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] 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)}) 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"}] 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) 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" 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" 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 == <> 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(<<>>,<>,r,r,f,{},TRUE) /\ ~PushForcedEncounter6(<<>>,<>,r,r,f,{52},TRUE) /\ ~ForcedInstructionFinished6(52,{}) /\ ReturnForcedEncounter6(<>,<<>>,r,r,"pass reaction",{},{52}) /\ ~ReturnForcedEncounter6(<>,<<>>,r,r,"pass reaction",{},{52}) /\ ReturnForcedEncounter6(<>,<<>>,[r EXCEPT !.attacked = "SchemaAtom082"],[r EXCEPT !.attacked = "SchemaAtom082"],"pass reaction",{},{52}) /\ MoveTraversalDuringForcedEncounter6(<>,<>,r,[r EXCEPT !.attacked = "SchemaAtom082"],TRUE) /\ EndTraversalDuringForced6(control,ended,<>,<<[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 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) 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) 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,<>) popped == [e EXCEPT !.windows = <>] 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(<>,<<>>,closedPaid,FALSE,{},{}) /\ ~ProcessTraversalEndWindow6(<>,<<>>,closedPaid,TRUE,{"SelfModifyingCode"},{}) /\ ProcessTraversalEndWindow6(<>,<<>>,closedBegin,FALSE,{},{}) /\ ~ProcessTraversalEndWindow6(<>,<<>>,closedBegin,TRUE,{"Specimen0248"},{}) /\ ProcessTraversalEndWindow6(<>,<<>>,closedOther,TRUE,{"ResolveFormicaryActivationAndMoveBarrier"},{}) /\ ~ProcessTraversalEndWindow6(<>,<<>>,closedOther,TRUE,{"ResolveFormicary"},{"Encounter"}) /\ ~ProcessTraversalEndWindow6(<>,<<>>,closedOther,TRUE,{},{"DelayedInspection"}) /\ ~ProcessTraversalEndWindow6(<>,<<>>,closedOther,FALSE,{},{}) /\ TraversalEndWindowStep6(e,popped,closedOther,TRUE,{"ResolveFormicaryActivationAndMoveBarrier"},{}) /\ ~TraversalEndWindowStep6(e,[e EXCEPT !.windows = <>],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}) 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,{}) 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 =============================================================================