----------------------------- MODULE TraversalContracts ----------------------------- EXTENDS TurnContracts NoTraversalRedirect6 == [phase |-> "NoValue",phaseId |-> 0,step |-> "NoValue",attacked |-> "NoValue",position |-> "NoValue"] TraversalPhases6 == {"Initiation","Approach","Encounter","Movement","Success","TraversalEnds"} OpenTraversal6(traversalId,phaseId,callerId) == [id |-> traversalId,phaseId |-> phaseId,usedPhaseIds |-> {phaseId},caller |-> callerId, phase |-> "Initiation",step |-> "ProcedureCode12371046a2e5",attacked |-> "NoValue",position |-> "NoValue", formalBegun |-> FALSE,complete |-> FALSE,ending |-> FALSE, reachedSuccess |-> FALSE,successful |-> FALSE,unsuccessful |-> FALSE,withdrewTraversal |-> FALSE] NoTraversal6 == [OpenTraversal6(0,0,"NoValue") EXCEPT !.phase = "NoValue",!.step = "NoValue",!.complete = TRUE,!.usedPhaseIds = {}] TraversalTimingPresent6(r) == r.id # 0 /\ ~r.complete DuringTraversal6(r) == TraversalTimingPresent6(r) /\ r.formalBegun TraversalFrameValid6(r) == IF r.id = 0 THEN r.complete /\ r.phase = "NoValue" ELSE r.id \in Nat \ {0} /\ r.phase \in TraversalPhases6 /\ r.phaseId \in r.usedPhaseIds /\ r.usedPhaseIds \subseteq Nat \ {0} /\ r.formalBegun \in BOOLEAN /\ r.complete \in BOOLEAN /\ r.ending \in BOOLEAN DirectAttackedTargetSiteChange6(before,after,newTargetSite,actualAuthorizedTrait) == /\ TraversalTimingPresent6(before) /\ actualAuthorizedTrait /\ newTargetSite # "NoValue" /\ after = [before EXCEPT !.attacked = newTargetSite] IndependentEncounterTraversalView6(before,after,actualEncounterWithoutPositionMove) == actualEncounterWithoutPositionMove /\ after = before TraversalPhaseEndEvent6(r) == [tag |-> "PhaseEnds",phase |-> r.phase,phaseId |-> r.phaseId,traversalId |-> r.id] TraversalPhaseEndEventsOnce6(control) == IF control.traversal.phaseId \in control.phaseEndedIds THEN {} ELSE {TraversalPhaseEndEvent6(control.traversal)} RequestTraversalRedirect6(before,after,target,actualAuthorizedTrait,events) == /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending /\ actualAuthorizedTrait /\ before.redirect = NoTraversalRedirect6 /\ target.phase \in TraversalPhases6 \ {"TraversalEnds"} /\ target.phaseId \in Nat \ {0} /\ target.phaseId \notin before.traversal.usedPhaseIds /\ after = [before EXCEPT !.redirect = target,!.phaseStepsSkipped = TRUE, !.traversal.position = target.position,!.traversal.attacked = target.attacked, !.traversal.usedPhaseIds = @ \cup {target.phaseId}, !.phaseEndedIds = IF before.paidOpen THEN @ ELSE @ \cup {before.traversal.phaseId}, !.redirectStage = IF before.paidOpen THEN "PaidWindow" ELSE "Checkpoint", !.redirectCheckpointDue = ~before.paidOpen] /\ events = IF before.paidOpen THEN {} ELSE TraversalPhaseEndEventsOnce6(before) RetargetTraversalRedirect6(before,after,target,actualAuthorizedTrait,events) == /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending /\ actualAuthorizedTrait /\ before.redirect # NoTraversalRedirect6 /\ before.redirectStage \in {"PaidWindow","Checkpoint"} /\ target.phase \in TraversalPhases6 \ {"TraversalEnds"} /\ target.phaseId \in Nat \ {0} /\ target.phaseId \notin before.traversal.usedPhaseIds /\ after = [before EXCEPT !.redirect = target,!.traversal.position = target.position, !.traversal.attacked = target.attacked,!.traversal.usedPhaseIds = @ \cup {target.phaseId}] /\ events = {} FinishRedirectPaidWindow6(before,after,actualWindowIncludingReactionsComplete,events) == /\ before.redirect # NoTraversalRedirect6 /\ before.redirectStage = "PaidWindow" /\ before.paidOpen /\ actualWindowIncludingReactionsComplete /\ after = [before EXCEPT !.paidOpen = FALSE,!.redirectStage = "Checkpoint",!.redirectCheckpointDue = TRUE, !.phaseEndedIds = @ \cup {before.traversal.phaseId}] /\ events = TraversalPhaseEndEventsOnce6(before) FinishRedirectCheckpoint6(before,after,actualNormalCheckpointAndReactionsComplete) == /\ before.redirect # NoTraversalRedirect6 /\ before.redirectStage = "Checkpoint" /\ before.redirectCheckpointDue /\ actualNormalCheckpointAndReactionsComplete /\ after = [before EXCEPT !.redirectStage = "Ready",!.redirectCheckpointDue = FALSE] CommitTraversalRedirect6(before,after) == /\ before.redirect # NoTraversalRedirect6 /\ before.redirectStage = "Ready" /\ ~before.redirectCheckpointDue /\ LET t == before.redirect IN after = [before EXCEPT !.traversal.phase = t.phase,!.traversal.step = t.step,!.traversal.phaseId = t.phaseId, !.traversal.usedPhaseIds = @ \cup {t.phaseId}, !.redirect = NoTraversalRedirect6,!.redirectStage = "NoValue",!.phaseStepsSkipped = FALSE] TraversalDirectEdge6(edge,from,to) == edge.traversalId # 0 /\ edge.standard /\ edge.from = from /\ edge.to = to /\ edge.fromBarrier = edge.toBarrier EncounterAfterApproach6(edge) == TraversalDirectEdge6(edge,"Approach","Encounter") PassAfterEncounter6(edge) == TraversalDirectEdge6(edge,"Encounter","Pass") PassAfterFullySuppressInstruction6(edge,fullyBarrierInstructionSuppressedEncounters) == PassAfterEncounter6(edge) /\ [traversalId |-> edge.traversalId,encounterId |-> edge.encounterId,barrierCard |-> edge.fromBarrier] \in fullyBarrierInstructionSuppressedEncounters OutsideEncounterScope6(frames,encounterId) == [id \in {x \in DOMAIN frames: encounterId \notin frames[x].encounterAncestors} |-> frames[id]] EndTraversalOutcome6(before,newTraversalEndsPhaseId) == IF TraversalTimingPresent6(before.traversal) THEN IF before.traversal.ending /\ before.encounter = 0 /\ DOMAIN before.siteInspections = {} /\ DOMAIN before.itemInspections = {} THEN before ELSE [before EXCEPT !.traversal = IF before.traversal.ending THEN @ ELSE [@ EXCEPT !.phase = "TraversalEnds",!.step = "ProcedureCode6ea937bb44ac",!.phaseId = newTraversalEndsPhaseId, !.usedPhaseIds = @ \cup {newTraversalEndsPhaseId},!.ending = TRUE,!.position = "NoValue"], !.phaseEndedIds = @ \cup (IF before.traversal.ending THEN {} ELSE {before.traversal.phaseId}) \cup (IF before.encounter = 0 THEN {} ELSE {before.encounter}), !.encounter = 0,!.siteInspections = [x \in {} |-> x],!.itemInspections = [x \in {} |-> x], !.abortedEncounters = IF before.encounter = 0 THEN @ ELSE @ \cup {before.encounter}, !.abortedInspectiones = @ \cup DOMAIN before.siteInspections,!.abortedItemInspectiones = @ \cup DOMAIN before.itemInspections, !.windowCleanupDue = TRUE,!.onlyWindowCleanup = FALSE,!.phaseStepsSkipped = TRUE, !.redirect = NoTraversalRedirect6,!.redirectStage = "NoValue",!.redirectCheckpointDue = FALSE] ELSE IF before.encounter # 0 THEN [before EXCEPT !.encounter = 0,!.phaseEndedIds = @ \cup {before.encounter}, !.siteInspections = OutsideEncounterScope6(@,before.encounter), !.itemInspections = OutsideEncounterScope6(@,before.encounter), !.abortedEncounters = @ \cup {before.encounter}, !.abortedInspectiones = @ \cup (DOMAIN before.siteInspections \ DOMAIN OutsideEncounterScope6(before.siteInspections,before.encounter)), !.abortedItemInspectiones = @ \cup (DOMAIN before.itemInspections \ DOMAIN OutsideEncounterScope6(before.itemInspections,before.encounter)), !.windowCleanupDue = TRUE,!.onlyWindowCleanup = TRUE,!.phaseStepsSkipped = TRUE] ELSE before EndTraversalEffectEvents6(before) == (IF TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending THEN TraversalPhaseEndEventsOnce6(before) ELSE {}) \cup (IF before.encounter # 0 /\ before.encounter \notin before.phaseEndedIds THEN {[tag |-> "PhaseEnds",phase |-> "Encounter",phaseId |-> before.encounter, traversalId |-> IF TraversalTimingPresent6(before.traversal) THEN before.traversal.id ELSE 0]} ELSE {}) EndTheTraversal6(before,after,newTraversalEndsPhaseId,actualAuthorizedInstruction,events) == /\ actualAuthorizedInstruction /\ ((TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending) => newTraversalEndsPhaseId \in Nat \ {0} /\ newTraversalEndsPhaseId \notin before.traversal.usedPhaseIds) /\ after = EndTraversalOutcome6(before,newTraversalEndsPhaseId) /\ events = EndTraversalEffectEvents6(before) WithdrawTraversal6(before,after,newTraversalEndsPhaseId,sideBChooses,actualOpportunity,legallyCanWithdrawTraversal,events) == /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending /\ sideBChooses /\ actualOpportunity /\ legallyCanWithdrawTraversal /\ newTraversalEndsPhaseId \in Nat \ {0} /\ newTraversalEndsPhaseId \notin before.traversal.usedPhaseIds /\ after = [EndTraversalOutcome6(before,newTraversalEndsPhaseId) EXCEPT !.traversal.withdrewTraversal = TRUE] /\ events = EndTraversalEffectEvents6(before) PositionIds6(l) == UNION {SetupRange(l.orders[s]): s \in DOMAIN l.orders} OccupiedBarrier6(l) == {l.slots[p].barrierCard: p \in {q \in DOMAIN l.slots: l.slots[q].barrierCard # 0}} PositionLayoutValid6(l,actualProtectingBarrier) == /\ DOMAIN l.slots = PositionIds6(l) /\ PositionIds6(l) \subseteq l.used /\ \A s \in DOMAIN l.orders: DeckSequenceValid4(l.orders[s]) /\ \A p \in SetupRange(l.orders[s]): l.slots[p].targetSite = s /\ \A s,t \in DOMAIN l.orders: s # t => SetupRange(l.orders[s]) \intersect SetupRange(l.orders[t]) = {} /\ OccupiedBarrier6(l) = actualProtectingBarrier /\ \A p \in DOMAIN l.slots: l.slots[p].barrierCard # 0 => l.slots[p].reservation = 0 /\ ~l.slots[p].retained /\ \A p,q \in DOMAIN l.slots: p # q /\ l.slots[p].barrierCard # 0 => l.slots[p].barrierCard # l.slots[q].barrierCard ProtectingBarrierForPositions6(objects) == {id \in DOMAIN objects: objects[id].form = "Card" /\ objects[id].kind = "Barrier" /\ objects[id].deployed /\ objects[id].host = 0 /\ objects[id].zone = "Play" /\ objects[id].area = "Protecting"} PositionIndex6(order,p) == CHOOSE i \in 1..Len(order): order[i] = p SamePosition6(l,p,q) == /\ p \in DOMAIN l.slots /\ q \in DOMAIN l.slots /\ PositionIndex6(l.orders[l.slots[p].targetSite],p) = PositionIndex6(l.orders[l.slots[q].targetSite],q) InsertPositionSequence6(order,p,gap) == SubSeq(order,1,gap) \o <

> \o SubSeq(order,gap+1,Len(order)) PositionGapAllowed6(order,mode,anchor,gap,rememberedGap) == /\ gap \in 0..Len(order) /\ CASE mode = "Outermost" -> gap = Len(order) [] mode = "Innermost" -> gap = 0 [] mode = "DirectlyInward" -> anchor \in SetupRange(order) /\ gap = PositionIndex6(order,anchor)-1 [] mode = "SchemaAtom016" -> TRUE [] mode = "HistoricalPlace" -> gap = rememberedGap [] OTHER -> FALSE CreatePosition6(before,after,p,targetSite,gap,barrierCard,reservation,actualCreationAuthorized) == /\ actualCreationAuthorized /\ targetSite \in DOMAIN before.orders /\ p \notin before.used \cup {"NoValue"} /\ gap \in 0..Len(before.orders[targetSite]) /\ (barrierCard # 0 => barrierCard \notin OccupiedBarrier6(before)) /\ after = [before EXCEPT !.orders[targetSite] = InsertPositionSequence6(@,p,gap), !.slots = [q \in DOMAIN @ \cup {p} |-> IF q = p THEN [targetSite |-> targetSite,barrierCard |-> barrierCard,reservation |-> reservation,retained |-> FALSE] ELSE before.slots[q]], !.used = @ \cup {p}] DeclareBarrierPosition6(before,after,p,targetSite,gap,mode,anchor,rememberedLocation,deployId,actualStep) == /\ actualStep = "ProcedureCode6eba7e0bfa75" /\ deployId # 0 /\ PositionGapAllowed6(before.orders[targetSite],mode,anchor,gap,rememberedLocation.gap) /\ (mode = "HistoricalPlace" => targetSite = rememberedLocation.targetSite) /\ CreatePosition6(before,after,p,targetSite,gap,0,deployId,TRUE) OccupyDeclaredPosition6(before,after,p,deployId,newDeployedObject,actualStep,actualDeployAuthorized) == /\ actualStep = "ProcedureCode0f76bcc2eb00" /\ actualDeployAuthorized /\ p \in DOMAIN before.slots /\ before.slots[p].reservation = deployId /\ deployId # 0 /\ before.slots[p].barrierCard = 0 /\ newDeployedObject # 0 /\ newDeployedObject \notin OccupiedBarrier6(before) /\ after = [before EXCEPT !.slots[p].barrierCard = newDeployedObject,!.slots[p].reservation = 0,!.slots[p].retained = FALSE] VacatePosition6(before,after,p,actualDeparture) == actualDeparture /\ p \in DOMAIN before.slots /\ after = [before EXCEPT !.slots[p].barrierCard = 0,!.slots[p].reservation = 0,!.slots[p].retained = FALSE] CancelPositionReservation6(before,after,p,deployId,actualDeployCancelled) == /\ actualDeployCancelled /\ p \in DOMAIN before.slots /\ before.slots[p].barrierCard = 0 /\ before.slots[p].reservation = deployId /\ deployId # 0 /\ after = [before EXCEPT !.slots[p].reservation = 0] MoveBarrierPosition6(before,after,oldPos,newPos,targetSite,gap,actualMovementAuthorized) == /\ oldPos \in DOMAIN before.slots /\ before.slots[oldPos].barrierCard # 0 /\ LET empty == [before EXCEPT !.slots[oldPos].barrierCard = 0] IN CreatePosition6(empty,after,newPos,targetSite,gap,before.slots[oldPos].barrierCard,0,actualMovementAuthorized) SwapIntoPosition6(before,after,p,incomingObject,otherPosition,actualSwapAuthorized) == /\ actualSwapAuthorized /\ p \in DOMAIN before.slots /\ before.slots[p].barrierCard # 0 /\ incomingObject # 0 /\ IF otherPosition = "NoValue" THEN /\ incomingObject \notin OccupiedBarrier6(before) /\ after = [before EXCEPT !.slots[p].barrierCard = incomingObject] ELSE /\ otherPosition \in DOMAIN before.slots /\ otherPosition # p /\ before.slots[otherPosition].barrierCard = incomingObject /\ after = [before EXCEPT !.slots[p].barrierCard = incomingObject,!.slots[otherPosition].barrierCard = before.slots[p].barrierCard] PositionCleanup6(before,after,currentSideBPosition,actualCheckpointStage) == /\ actualCheckpointStage = "ProcedureCode2d6279f9d639" /\ LET remove == {p \in DOMAIN before.slots: before.slots[p].barrierCard = 0 /\ before.slots[p].reservation = 0 /\ p # currentSideBPosition} IN after = [before EXCEPT !.slots = [p \in DOMAIN @ \ remove |-> IF p = currentSideBPosition /\ before.slots[p].barrierCard = 0 /\ before.slots[p].reservation = 0 THEN [before.slots[p] EXCEPT !.retained = TRUE] ELSE before.slots[p]], !.orders = [s \in DOMAIN @ |-> SelectSeq(before.orders[s],LAMBDA p: p \notin remove)]] ReleaseDepartedSideBPosition6(before,after,oldPosition,newPosition) == LET release == oldPosition # newPosition /\ oldPosition \in DOMAIN before.slots /\ before.slots[oldPosition].barrierCard = 0 /\ before.slots[oldPosition].reservation = 0 /\ before.slots[oldPosition].retained remove == IF release THEN {oldPosition} ELSE {} IN after = [before EXCEPT !.slots = [p \in DOMAIN @ \ remove |-> before.slots[p]], !.orders = [s \in DOMAIN @ |-> SelectSeq(before.orders[s],LAMBDA p: p \notin remove)]] RequestOrRetargetTraversal6(before,after,target,actualAuthority,events) == IF before.redirect = NoTraversalRedirect6 THEN RequestTraversalRedirect6(before,after,target,actualAuthority,events) ELSE RetargetTraversalRedirect6(before,after,target,actualAuthority,events) SideBMayHavePosition6(r) == TraversalTimingPresent6(r) /\ r.phase \notin {"Success","TraversalEnds"} SideBPositionValid6(r,l) == /\ (~SideBMayHavePosition6(r) => r.position = "NoValue") /\ (r.position # "NoValue" => r.position \in DOMAIN l.slots /\ l.slots[r.position].targetSite = r.attacked) RetainedPositionValid6(l,r) == \A p \in DOMAIN l.slots: l.slots[p].retained => l.slots[p].barrierCard = 0 /\ l.slots[p].reservation = 0 /\ SideBMayHavePosition6(r) /\ r.position = p EndTraversalWithPositionCleanup6(before,after,beforeLayout,afterLayout,newPhaseId,actualAuthority,events) == EndTheTraversal6(before,after,newPhaseId,actualAuthority,events) /\ ReleaseDepartedSideBPosition6(beforeLayout,afterLayout,before.traversal.position,after.traversal.position) OutermostOccupiedPosition6(l,targetSite) == LET occupied == SelectSeq(l.orders[targetSite],LAMBDA p: l.slots[p].barrierCard # 0) IN IF Len(occupied) = 0 THEN "NoValue" ELSE occupied[Len(occupied)] NextInwardPosition6(l,targetSite,p) == IF p = "NoValue" THEN "NoValue" ELSE LET i == PositionIndex6(l.orders[targetSite],p) IN IF i = 1 THEN "NoValue" ELSE l.orders[targetSite][i-1] SetInitialSideBPosition6(before,after,l,actualStep) == /\ actualStep = "ProcedureCode347de0bdd6b4" /\ before.phase = "Initiation" /\ TraversalTimingPresent6(before) /\ after = [before EXCEPT !.position = OutermostOccupiedPosition6(l,before.attacked)] SideBAdvancePosition6(before,after,l,actualStep) == /\ actualStep = "ProcedureCoded4ddeafb5f2f" /\ before.phase = "Movement" /\ TraversalTimingPresent6(before) /\ after = [before EXCEPT !.position = NextInwardPosition6(l,before.attacked,before.position)] SideBAdvanceWithPositionCleanup6(beforeTraversal,afterTraversal,beforeLayout,afterLayout,actualStep) == SideBAdvancePosition6(beforeTraversal,afterTraversal,beforeLayout,actualStep) /\ ReleaseDepartedSideBPosition6(beforeLayout,afterLayout,beforeTraversal.position,afterTraversal.position) BarrierChangeTraversalPlan6(r,change,newPosition,newTargetSite) == IF r.phase \in {"Initiation","Movement"} THEN [traversal |-> r,needsRedirect |-> FALSE,approachCondition |-> FALSE] ELSE IF r.phase = "Approach" /\ change \in {"Uninstall","Move"} THEN [traversal |-> r,needsRedirect |-> TRUE,approachCondition |-> FALSE] ELSE IF r.phase = "Approach" /\ change = "Swap" THEN [traversal |-> r,needsRedirect |-> FALSE,approachCondition |-> FALSE] ELSE IF r.phase = "Encounter" /\ change \in {"Uninstall","Deactivation"} THEN [traversal |-> r,needsRedirect |-> TRUE,approachCondition |-> FALSE] ELSE IF r.phase = "Encounter" /\ change \in {"Move","Swap"} THEN [traversal |-> [r EXCEPT !.position = newPosition,!.attacked = newTargetSite], needsRedirect |-> FALSE,approachCondition |-> FALSE] ELSE [traversal |-> r,needsRedirect |-> FALSE,approachCondition |-> FALSE] BarrierChangeRedirectTarget6(plan,newPhaseId) == [phase |-> "Movement",phaseId |-> newPhaseId,step |-> "ProcedureCode714dfe070fed", position |-> plan.traversal.position,attacked |-> plan.traversal.attacked] SideBMoveToBarrierTarget6(r,l,p,directive,newPhaseId) == [phase |-> directive,phaseId |-> newPhaseId, step |-> IF directive = "Approach" THEN "ProcedureCode453e949a114f" ELSE "ProcedureCodeda7bff1d9270", position |-> p,attacked |-> l.slots[p].targetSite] SideBMoveToOutermostTarget6(r,l,targetSite,newPhaseId) == LET p == OutermostOccupiedPosition6(l,targetSite) IN [phase |-> IF p = "NoValue" THEN "Movement" ELSE "Approach",phaseId |-> newPhaseId, step |-> IF p = "NoValue" THEN "ProcedureCode714dfe070fed" ELSE "ProcedureCode453e949a114f",position |-> p,attacked |-> targetSite] SideBMoveNoOp6(r,targetPosition,directive) == ~SideBMayHavePosition6(r) \/ (r.phase = "Approach" /\ r.position = targetPosition /\ directive = "Approach") SideBMoveInstructionClass6(r,p,directive) == IF SideBMoveNoOp6(r,p,directive) THEN "NoOp" ELSE IF directive = "Encounter" /\ p = r.position THEN "ForcedEncounter" ELSE "Redirect" SideBPositionMoveRequest6(before,after,l,afterLayout,p,directive,newPhaseId,actualMovementAuthorized,events) == /\ actualMovementAuthorized /\ directive \in {"Approach","Encounter"} /\ p \in DOMAIN l.slots /\ l.slots[p].barrierCard # 0 /\ IF SideBMoveNoOp6(before.traversal,p,directive) THEN after = before /\ events = {} ELSE /\ SideBMoveInstructionClass6(before.traversal,p,directive) = "Redirect" /\ RequestOrRetargetTraversal6(before,after,SideBMoveToBarrierTarget6(before.traversal,l,p,directive,newPhaseId),TRUE,events) /\ ReleaseDepartedSideBPosition6(l,afterLayout,before.traversal.position,after.traversal.position) SideBOutermostMoveRequest6(before,after,l,afterLayout,targetSite,newPhaseId,actualMovementAuthorized,events) == /\ actualMovementAuthorized /\ targetSite \in DOMAIN l.orders /\ LET t == SideBMoveToOutermostTarget6(before.traversal,l,targetSite,newPhaseId) IN IF SideBMoveNoOp6(before.traversal,t.position,t.phase) THEN after = before /\ events = {} ELSE RequestOrRetargetTraversal6(before,after,t,TRUE,events) /\ ReleaseDepartedSideBPosition6(l,afterLayout,before.traversal.position,after.traversal.position) OpenInitiation6(traversal) == [traversal |-> traversal,announced |-> FALSE,costsPaid |-> FALSE,badPubAdded |-> FALSE] TraversalBeginEvent6(r) == [tag |-> "TraversalBegins",alsoInitiates |-> TRUE,traversalId |-> r.id,targetSite |-> r.attacked] AnnounceTraversalTargetSite6(before,after,targetSite,targetSites,actualInitiationRestrictionsAllow,allTraversalCostsPaid,events) == /\ TraversalTimingPresent6(before.traversal) /\ before.traversal.phase = "Initiation" /\ before.traversal.step = "ProcedureCode12371046a2e5" /\ ~before.announced /\ ~before.traversal.formalBegun /\ ~before.traversal.ending /\ targetSite \in DOMAIN targetSites /\ actualInitiationRestrictionsAllow /\ allTraversalCostsPaid /\ after = [before EXCEPT !.traversal.attacked = targetSite,!.announced = TRUE,!.costsPaid = TRUE] /\ events = {[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> before.traversal.id,targetSite |-> targetSite]} AddInitiationLiabilityMarker6(before,after,fundBefore,fundAfter,effectiveSideALiabilityMarker) == /\ before.traversal.phase = "Initiation" /\ before.traversal.step = "ProcedureCodeacc82dbcc545" /\ ~before.traversal.ending /\ before.announced /\ before.costsPaid /\ ~before.badPubAdded /\ effectiveSideALiabilityMarker \in Nat /\ fundBefore \in Nat /\ fundAfter = fundBefore+effectiveSideALiabilityMarker /\ after = [before EXCEPT !.badPubAdded = TRUE] FormalTraversalBegin6(before,after,events) == /\ TraversalTimingPresent6(before.traversal) /\ before.traversal.phase = "Initiation" /\ before.traversal.step = "ProcedureCode4d6bd06d2c9f" /\ before.announced /\ before.costsPaid /\ before.badPubAdded /\ ~before.traversal.formalBegun /\ ~before.traversal.ending /\ after = [before EXCEPT !.traversal.formalBegun = TRUE] /\ events = {TraversalBeginEvent6(before.traversal)} InitiationDestination6(r,l) == IF r.position = "NoValue" THEN "Movement" ELSE IF r.position \notin DOMAIN l.slots THEN "Movement" ELSE IF l.slots[r.position].barrierCard = 0 THEN "Movement" ELSE "Approach" CompleteInitiationTraversalView6(before,after,l,newPhaseId,actualPhaseIncludingReactionsComplete) == /\ TraversalTimingPresent6(before) /\ before.phase = "Initiation" /\ before.step = "ProcedureCode7e3f7e5033c8" /\ ~before.ending /\ actualPhaseIncludingReactionsComplete /\ newPhaseId \in Nat \ {0} /\ newPhaseId \notin before.usedPhaseIds /\ after = [before EXCEPT !.phase = InitiationDestination6(before,l), !.step = IF InitiationDestination6(before,l) = "Approach" THEN "ProcedureCode453e949a114f" ELSE "ProcedureCode714dfe070fed", !.phaseId = newPhaseId,!.usedPhaseIds = @ \cup {newPhaseId}] OpenApproach6(r) == [id |-> r.phaseId,traversalId |-> r.id,position |-> r.position,begun |-> FALSE] ApproachedBarrier6(a,l) == IF a.position \in DOMAIN l.slots THEN l.slots[a.position].barrierCard ELSE 0 BeginApproach6(r,before,after,l,events) == /\ TraversalTimingPresent6(r) /\ ~r.ending /\ r.phase = "Approach" /\ r.step = "ProcedureCode453e949a114f" /\ before.id = r.phaseId /\ before.traversalId = r.id /\ before.position = r.position /\ ~before.begun /\ after = [before EXCEPT !.begun = TRUE] /\ events = IF ApproachedBarrier6(before,l) = 0 THEN {} ELSE {[tag |-> "ApproachBarrier",barrierCard |-> ApproachedBarrier6(before,l),phaseId |-> before.id,traversalId |-> r.id]} ApproachActivationPermission6(r,a,l,w,barrierCard) == /\ TraversalTimingPresent6(r) /\ ~r.ending /\ r.phase = "Approach" /\ r.step = "ProcedureCode3a6daf593ad4" /\ a.id = r.phaseId /\ a.traversalId = r.id /\ a.begun /\ w.open /\ w.kind = "Paid" /\ w.phaseId = a.id /\ w.step = "ProcedureCode3a6daf593ad4" /\ w.priority = "SideA" /\ barrierCard # 0 /\ barrierCard = ApproachedBarrier6(a,l) ApproachActivation6(r,a,l,w,barrierCard,beforeCard,afterCard,allCostsPaid,actualActivationAllowed) == /\ ApproachActivationPermission6(r,a,l,w,barrierCard) /\ StandardBarrierActivationStep(beforeCard,afterCard,barrierCard,"SideA", [inTraversal |-> TRUE,window |-> "ProcedureCode3a6daf593ad4",approachedObject |-> barrierCard],allCostsPaid,actualActivationAllowed) CloseEndedBeginReaction6(before,after,endedPhaseIds) == /\ before.kind = "Reaction" /\ before.open /\ before.beginPhaseId # 0 /\ before.beginPhaseId \in endedPhaseIds /\ after = [before EXCEPT !.open = FALSE,!.pending = {},!.priority = "NoValue", !.lostPending = @ \cup before.pending] ApproachDestination6(a,l,activationzedDeployedBarrier) == IF ApproachedBarrier6(a,l) # 0 /\ ApproachedBarrier6(a,l) \in activationzedDeployedBarrier THEN "Encounter" ELSE "Movement" CompleteApproachTraversalView6(before,after,a,l,activationzedDeployedBarrier,newPhaseId,actualPhaseIncludingReactionsComplete) == /\ TraversalTimingPresent6(before) /\ ~before.ending /\ before.phase = "Approach" /\ before.step = "ProcedureCode4d474d346807" /\ a.id = before.phaseId /\ a.traversalId = before.id /\ a.begun /\ actualPhaseIncludingReactionsComplete /\ newPhaseId \in Nat \ {0} /\ newPhaseId \notin before.usedPhaseIds /\ after = [before EXCEPT !.phase = ApproachDestination6(a,l,activationzedDeployedBarrier), !.step = IF ApproachDestination6(a,l,activationzedDeployedBarrier) = "Encounter" THEN "ProcedureCodeda7bff1d9270" ELSE "ProcedureCode714dfe070fed", !.phaseId = newPhaseId,!.usedPhaseIds = @ \cup {newPhaseId}] SubIds6(order) == {order[i] : i \in 1..Len(order)} OpenEncounter6(id,barrierCard,traversalId,forced,caller,order) == [id |-> id,barrierCard |-> barrierCard,traversalId |-> traversalId,forced |-> forced,caller |-> caller, stage |-> "Begin",order |-> order,usedSubIds |-> SubIds6(order), barrierInstructionSuppressedBy |-> [s \in SubIds6(order) |-> 0],barrierInstructionSuppressed |-> {},resolved |-> {}, paidReached |-> FALSE,fullyBarrierInstructionSuppressed |-> FALSE,fullyBy |-> {},bypassed |-> FALSE,aborted |-> FALSE] AllCurrentSubsBarrierInstructionSuppressed6(e) == SubIds6(e.order) \subseteq e.barrierInstructionSuppressed /\ (Len(e.order) > 0 \/ e.paidReached) WithFullySuppressInstruction6(e) == IF ~e.fullyBarrierInstructionSuppressed /\ AllCurrentSubsBarrierInstructionSuppressed6(e) THEN [e EXCEPT !.fullyBarrierInstructionSuppressed = TRUE, !.fullyBy = IF Len(e.order) = 0 THEN {} ELSE LET sources == {e.barrierInstructionSuppressedBy[s] : s \in SubIds6(e.order)} IN IF Cardinality(sources) = 1 /\ 0 \notin sources THEN sources ELSE {}] ELSE e NewFullySuppressInstructionEvents6(before,after) == IF ~before.fullyBarrierInstructionSuppressed /\ after.fullyBarrierInstructionSuppressed THEN {[tag |-> "FullySuppressInstruction",encounterId |-> before.id,barrierCard |-> before.barrierCard, traversalId |-> before.traversalId,objects |-> after.fullyBy]} ELSE {} BeginEncounter6(before,after,actualEncounterAuthorized,events) == /\ actualEncounterAuthorized /\ before.id \in Nat \ {0} /\ before.barrierCard # 0 /\ before.stage = "Begin" /\ ~before.aborted /\ after = [before EXCEPT !.stage = "BeginReactions"] /\ events = {[tag |-> "EncounterBarrier",encounterId |-> before.id,barrierCard |-> before.barrierCard,traversalId |-> before.traversalId]} BeginEncounterPaid6(before,after,beginReactionsAndCheckpointDrained,events) == /\ before.stage = "BeginReactions" /\ ~before.aborted /\ beginReactionsAndCheckpointDrained /\ after = WithFullySuppressInstruction6([before EXCEPT !.stage = "Paid",!.paidReached = TRUE]) /\ events = NewFullySuppressInstructionEvents6(before,after) SuppressInstructionEncounterSubs6(before,after,subs,sourceObject,actualAbilityTimingAndLegality,allCostsPaid,events) == /\ before.stage \in {"BeginReactions","Paid","BarrierInstructions"} /\ ~before.aborted /\ actualAbilityTimingAndLegality /\ allCostsPaid /\ subs # {} /\ subs \subseteq (SubIds6(before.order) \ before.barrierInstructionSuppressed) /\ after = WithFullySuppressInstruction6([before EXCEPT !.barrierInstructionSuppressed = @ \cup subs, !.barrierInstructionSuppressedBy = [s \in DOMAIN before.barrierInstructionSuppressedBy |-> IF s \in subs THEN sourceObject ELSE before.barrierInstructionSuppressedBy[s]]]) /\ events = NewFullySuppressInstructionEvents6(before,after) PaidSuppressInstructionEncounterSubs6(before,after,w,subs,sourceObject,actualAbilityLegal,allCostsPaid,events) == /\ before.stage = "Paid" /\ w.open /\ w.kind = "Paid" /\ w.step = "ProcedureCode8b3260c0010f" /\ w.phaseId = before.id /\ w.priority = "SideB" /\ SuppressInstructionEncounterSubs6(before,after,subs,sourceObject,actualAbilityLegal,allCostsPaid,events) UpdateEncounterSubs6(before,after,newOrder,actualBarrierInstructionChange,events) == LET ids == SubIds6(newOrder) gained == ids \ SubIds6(before.order) fresh == gained \ before.usedSubIds b == [s \in before.usedSubIds \cup fresh |-> IF s \in fresh THEN 0 ELSE before.barrierInstructionSuppressedBy[s]] IN /\ actualBarrierInstructionChange /\ before.stage \notin {"Begin","Complete"} /\ ~before.aborted /\ Cardinality(ids) = Len(newOrder) /\ gained = fresh /\ after = WithFullySuppressInstruction6([before EXCEPT !.order = newOrder, !.usedSubIds = @ \cup fresh,!.barrierInstructionSuppressedBy = b]) /\ events = NewFullySuppressInstructionEvents6(before,after) CloseEncounterPaid6(before,after,actualPaidWindowAndReactionsComplete) == /\ before.stage = "Paid" /\ ~before.aborted /\ actualPaidWindowAndReactionsComplete /\ after = [before EXCEPT !.stage = "BarrierInstructions"] NextEncounterSub6(e) == LET available == {i \in 1..Len(e.order) : e.order[i] \notin (e.barrierInstructionSuppressed \cup e.resolved)} IN IF available = {} THEN 0 ELSE e.order[CHOOSE i \in available : \A j \in available : i <= j] ResolveEncounterSub6(before,after,sub,actualEntireBarrierInstructionCompleted) == /\ before.stage = "BarrierInstructions" /\ ~before.aborted /\ sub # 0 /\ sub = NextEncounterSub6(before) /\ actualEntireBarrierInstructionCompleted /\ after = [before EXCEPT !.resolved = @ \cup {sub}] CompleteEncounter6(before,after,allEffectsAndReactionsDrained) == /\ before.stage = "BarrierInstructions" /\ ~before.aborted /\ NextEncounterSub6(before) = 0 /\ allEffectsAndReactionsDrained /\ after = [before EXCEPT !.stage = "Complete"] BypassEncounter6(before,after,actualAuthorizedBypass,events) == /\ actualAuthorizedBypass /\ before.stage \in {"BeginReactions","Paid","BarrierInstructions"} /\ ~before.aborted /\ after = [before EXCEPT !.stage = "Complete",!.bypassed = TRUE,!.aborted = TRUE] /\ events = {[tag |-> "Bypass",encounterId |-> before.id,barrierCard |-> before.barrierCard,traversalId |-> before.traversalId]} CompleteOrdinaryEncounterTraversalView6(before,after,e,newPhaseId,actualPhaseIncludingReactionsComplete) == /\ TraversalTimingPresent6(before) /\ ~before.ending /\ before.phase = "Encounter" /\ before.step = "ProcedureCode687f72772ab1" /\ ~e.forced /\ e.id = before.phaseId /\ e.traversalId = before.id /\ e.stage = "Complete" /\ actualPhaseIncludingReactionsComplete /\ newPhaseId \in Nat \ {0} /\ newPhaseId \notin before.usedPhaseIds /\ after = [before EXCEPT !.phase = "Movement",!.step = "ProcedureCode714dfe070fed", !.phaseId = newPhaseId,!.usedPhaseIds = @ \cup {newPhaseId}] BypassTraversalRedirect6(before,after,e,newPhaseId,events) == /\ ~e.forced /\ e.bypassed /\ e.stage = "Complete" /\ before.traversal.phase = "Encounter" /\ before.traversal.phaseId = e.id /\ before.traversal.id = e.traversalId /\ RequestOrRetargetTraversal6(before,after, [phase |-> "Movement",phaseId |-> newPhaseId,step |-> "ProcedureCode714dfe070fed", attacked |-> before.traversal.attacked,position |-> before.traversal.position],TRUE,events) PushForcedEncounter6(before,after,r,afterTraversal,e,usedEncounterIds,actualTraitWithoutPositionChange) == /\ actualTraitWithoutPositionChange /\ ~r.ending /\ e.forced /\ e.stage = "Begin" /\ e.id \in Nat \ {0} /\ e.id \notin usedEncounterIds /\ e.traversalId = r.id /\ after = Append(before,e) /\ afterTraversal = r ReturnForcedEncounter6(before,after,r,afterTraversal,caller,completedIds,afterCompletedIds) == /\ Len(before) > 0 /\ before[Len(before)].forced /\ before[Len(before)].stage = "Complete" /\ caller = before[Len(before)].caller /\ after = SubSeq(before,1,Len(before)-1) /\ afterTraversal = r /\ afterCompletedIds = completedIds \cup {before[Len(before)].id} ForcedInstructionFinished6(waitingEncounter,completedEncounterIds) == waitingEncounter \in completedEncounterIds MoveTraversalDuringForcedEncounter6(before,after,traversalBefore,traversalAfter,actualUnderlyingTraversalMovement) == /\ Len(before) > 0 /\ before[Len(before)].forced /\ before[Len(before)].stage # "Complete" /\ actualUnderlyingTraversalMovement /\ after = before EndForcedChain6(before,after,abortedIds,afterAbortedIds,actualEndTraversalInstruction) == /\ actualEndTraversalInstruction /\ after = [i \in 1..Len(before) |-> [before[i] EXCEPT !.stage = "Complete",!.aborted = TRUE]] /\ afterAbortedIds = abortedIds \cup {before[i].id : i \in 1..Len(before)} EncounterChainIds6(stack) == {stack[i].id : i \in 1..Len(stack)} OutsideEncounterChain6(frames,ids) == [id \in {x \in DOMAIN frames : frames[x].encounterAncestors \cap ids = {}} |-> frames[id]] ForcedEndOutcome6(control,stack,newTraversalEndsPhaseId) == LET base == EndTraversalOutcome6(control,newTraversalEndsPhaseId) ids == EncounterChainIds6(stack) siteInspections == IF TraversalTimingPresent6(control.traversal) THEN base.siteInspections ELSE OutsideEncounterChain6(control.siteInspections,ids) itemInspections == IF TraversalTimingPresent6(control.traversal) THEN base.itemInspections ELSE OutsideEncounterChain6(control.itemInspections,ids) IN [base EXCEPT !.siteInspections = siteInspections,!.itemInspections = itemInspections, !.abortedInspectiones = @ \cup (DOMAIN control.siteInspections \ DOMAIN siteInspections), !.abortedItemInspectiones = @ \cup (DOMAIN control.itemInspections \ DOMAIN itemInspections), !.abortedEncounters = @ \cup ids,!.phaseEndedIds = @ \cup ids] ForcedEndEvents6(control,stack) == EndTraversalEffectEvents6(control) \cup {[tag |-> "PhaseEnds",phase |-> "Encounter",phaseId |-> id,traversalId |-> control.traversal.id] : id \in EncounterChainIds6(stack) \ control.phaseEndedIds} EndTraversalDuringForced6(control,afterControl,stack,afterStack,abortedIds,afterAbortedIds,newTraversalEndsPhaseId,events) == /\ Len(stack) > 0 /\ stack[Len(stack)].forced /\ control.encounter = stack[Len(stack)].id /\ EndTheTraversal6(control,EndTraversalOutcome6(control,newTraversalEndsPhaseId),newTraversalEndsPhaseId,TRUE,EndTraversalEffectEvents6(control)) /\ afterControl = ForcedEndOutcome6(control,stack,newTraversalEndsPhaseId) /\ events = ForcedEndEvents6(control,stack) /\ EndForcedChain6(stack,afterStack,abortedIds,afterAbortedIds,TRUE) OpenMovement6(r,fromPhase,fromBarrier,fromEncounterId,standard) == [id |-> r.phaseId,traversalId |-> r.id,from |-> fromPhase,fromBarrier |-> fromBarrier,fromEncounterId |-> fromEncounterId, standard |-> standard,begun |-> FALSE,passedBarrier |-> 0,passedAll |-> FALSE, declined |-> FALSE,advanced |-> FALSE,movedToNew |-> FALSE,approachedTargetSite |-> FALSE] MovementContext6(r,m,step) == TraversalTimingPresent6(r) /\ ~r.ending /\ r.phase = "Movement" /\ r.step = step /\ m.id = r.phaseId /\ m.traversalId = r.id MovementBarrier6(r,l) == IF r.position \in DOMAIN l.slots THEN l.slots[r.position].barrierCard ELSE 0 MovementPassEvents6(r,l) == IF MovementBarrier6(r,l) = 0 THEN {} ELSE {[tag |-> "PassBarrier",traversalId |-> r.id,phaseId |-> r.phaseId,barrierCard |-> MovementBarrier6(r,l)]} \cup (IF NextInwardPosition6(l,r.attacked,r.position) = "NoValue" THEN {[tag |-> "PassAllBarrier",traversalId |-> r.id,phaseId |-> r.phaseId,barrierCard |-> MovementBarrier6(r,l)]} ELSE {}) BeginMovement6(r,before,after,l,events) == /\ MovementContext6(r,before,"ProcedureCode714dfe070fed") /\ ~before.begun /\ after = [before EXCEPT !.begun = TRUE,!.passedBarrier = MovementBarrier6(r,l), !.passedAll = MovementBarrier6(r,l) # 0 /\ NextInwardPosition6(l,r.attacked,r.position) = "NoValue"] /\ events = MovementPassEvents6(r,l) MovementPassEdge6(m) == [traversalId |-> m.traversalId,standard |-> m.standard /\ m.begun /\ m.passedBarrier # 0,from |-> m.from,to |-> "Pass", fromBarrier |-> m.fromBarrier,toBarrier |-> m.passedBarrier,encounterId |-> m.fromEncounterId] MovementWithdrawTraversal6(before,after,m,l,afterLayout,newPhaseId,sideBChooses,actualDecisionReady,legallyCanWithdrawTraversal,events) == /\ MovementContext6(before.traversal,m,"ProcedureCode9bca3a096549") /\ m.begun /\ ~m.declined /\ WithdrawTraversal6(before,after,newPhaseId,sideBChooses,actualDecisionReady,legallyCanWithdrawTraversal,events) /\ ReleaseDepartedSideBPosition6(l,afterLayout,before.traversal.position,after.traversal.position) DeclineMovementWithdrawTraversal6(r,before,after,actualDecisionReady) == /\ MovementContext6(r,before,"ProcedureCode9bca3a096549") /\ before.begun /\ ~before.declined /\ actualDecisionReady /\ after = [before EXCEPT !.declined = TRUE] AdvanceMovement6(beforeTraversal,afterTraversal,before,after,l,afterLayout) == /\ MovementContext6(beforeTraversal,before,"ProcedureCoded4ddeafb5f2f") /\ before.declined /\ ~before.advanced /\ SideBAdvanceWithPositionCleanup6(beforeTraversal,afterTraversal,l,afterLayout,"ProcedureCoded4ddeafb5f2f") /\ after = [before EXCEPT !.advanced = TRUE,!.movedToNew = afterTraversal.position # "NoValue"] ApproachTargetSite6(r,before,after,events) == /\ MovementContext6(r,before,"ProcedureCode7e82ab2b38b7") /\ before.advanced /\ ~before.movedToNew /\ ~before.approachedTargetSite /\ after = [before EXCEPT !.approachedTargetSite = TRUE] /\ events = {[tag |-> "ApproachTargetSite",traversalId |-> r.id,targetSite |-> r.attacked,phaseId |-> r.phaseId]} CompleteMovementTraversalView6(before,after,m,newPhaseId,actualPhaseIncludingReactionsComplete) == /\ TraversalTimingPresent6(before) /\ ~before.ending /\ before.phase = "Movement" /\ m.id = before.phaseId /\ m.traversalId = before.id /\ m.advanced /\ IF m.movedToNew THEN before.step = "ProcedureCode6c5d14f545f7" /\ before.position # "NoValue" ELSE before.step = "ProcedureCodea732fbc12ae0" /\ m.approachedTargetSite /\ before.position = "NoValue" /\ actualPhaseIncludingReactionsComplete /\ newPhaseId \in Nat \ {0} /\ newPhaseId \notin before.usedPhaseIds /\ after = [before EXCEPT !.phase = IF m.movedToNew THEN "Approach" ELSE "Success", !.step = IF m.movedToNew THEN "ProcedureCode453e949a114f" ELSE "ProcedureCodebbb14496b09b",!.phaseId = newPhaseId, !.usedPhaseIds = @ \cup {newPhaseId},!.reachedSuccess = IF m.movedToNew THEN @ ELSE TRUE] OpenSuccess6(r) == [traversal |-> r,declarationProcessed |-> FALSE,siteInspectionChosen |-> FALSE,siteInspectionFinished |-> FALSE] DeclareSuccessfulTraversal6(before,after,actualDeclarationAllowed,events) == /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending /\ before.traversal.phase = "Success" /\ before.traversal.step = "ProcedureCodebbb14496b09b" /\ before.traversal.reachedSuccess /\ ~before.declarationProcessed /\ after = [before EXCEPT !.declarationProcessed = TRUE,!.traversal.successful = actualDeclarationAllowed] /\ events = IF actualDeclarationAllowed THEN {[tag |-> "SuccessfulTraversal",traversalId |-> before.traversal.id,targetSite |-> before.traversal.attacked]} ELSE {} SuccessfulTraversalReaction6(windowId,pending) == [id |-> windowId,kind |-> "Reaction",open |-> TRUE,beginPhaseId |-> 0, pending |-> pending,lostPending |-> {},priority |-> "NoValue"] IfSuccessfulCondition6(origin,r,sourcePermittedTargetSites) == /\ r.successful /\ origin.traversalId # 0 /\ r.id = origin.traversalId /\ (~origin.targetSiteRestricted \/ r.attacked \in sourcePermittedTargetSites) TraversalInspectionModifierApplies6(binding,r,siteInspection) == /\ TraversalTimingPresent6(r) /\ binding.traversalId = r.id /\ siteInspection.traversalId = r.id /\ siteInspection.origin = "RulesTraversalInspection" ChooseRulesInspection6(before,after,choice,actualAvailableChoices,successReactionsDrained,directive) == /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending /\ before.traversal.phase = "Success" /\ before.traversal.step = "ProcedureCoded75d879e00ff" /\ before.declarationProcessed /\ ~before.siteInspectionChosen /\ successReactionsDrained /\ choice \in actualAvailableChoices /\ after = [before EXCEPT !.siteInspectionChosen = TRUE] /\ directive = [kind |-> IF choice = "Inspection" THEN "Inspection" ELSE "Replacement", choice |-> choice,traversalId |-> before.traversal.id,targetSite |-> before.traversal.attacked,origin |-> "RulesTraversalInspection"] FinishRulesInspectionInstruction6(before,after,actualInspectionOrReplacementAndReactionsComplete) == /\ before.traversal.phase = "Success" /\ before.traversal.step = "ProcedureCoded75d879e00ff" /\ ~before.traversal.ending /\ before.siteInspectionChosen /\ ~before.siteInspectionFinished /\ actualInspectionOrReplacementAndReactionsComplete /\ after = [before EXCEPT !.siteInspectionFinished = TRUE] CompleteSuccessTraversalView6(before,after,newPhaseId,actualPhaseIncludingReactionsComplete) == /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.ending /\ before.traversal.phase = "Success" /\ before.traversal.step = "ProcedureCodec7b41615d673" /\ before.siteInspectionFinished /\ actualPhaseIncludingReactionsComplete /\ newPhaseId \in Nat \ {0} /\ newPhaseId \notin before.traversal.usedPhaseIds /\ after = [before EXCEPT !.traversal.phase = "TraversalEnds",!.traversal.step = "ProcedureCode6ea937bb44ac", !.traversal.ending = TRUE,!.traversal.position = "NoValue",!.traversal.phaseId = newPhaseId, !.traversal.usedPhaseIds = @ \cup {newPhaseId}] TraversalEndWindowClass6(w) == IF w.kind = "Paid" THEN "Close" ELSE IF w.kind = "Reaction" /\ w.beginPhaseId # 0 THEN "CloseBegin" ELSE "CompleteNormally" ProcessTraversalEndWindow6(before,after,finishedWindow,actualOtherWindowCompleted,optionsUsed,startedTimingStructures) == /\ Len(before) > 0 /\ startedTimingStructures = {} /\ LET w == before[Len(before)] mode == TraversalEndWindowClass6(w) IN /\ w.open /\ IF mode \in {"Close","CloseBegin"} THEN optionsUsed = {} ELSE actualOtherWindowCompleted /\ finishedWindow = [w EXCEPT !.open = FALSE,!.pending = {},!.priority = "NoValue", !.lostPending = IF mode = "CloseBegin" THEN @ \cup w.pending ELSE @] /\ after = SubSeq(before,1,Len(before)-1) OpenTraversalEnd6(control,windows) == [traversal |-> control.traversal,phaseEndedIds |-> control.phaseEndedIds,windows |-> windows, windowsDone |-> FALSE,fundReturned |-> FALSE,resultDeclared |-> FALSE,returned |-> FALSE] TraversalEndContext6(e,step) == TraversalTimingPresent6(e.traversal) /\ e.traversal.ending /\ e.traversal.phase = "TraversalEnds" /\ e.traversal.step = step TraversalEndWindowStep6(before,after,finishedWindow,actualOtherWindowCompleted,optionsUsed,startedTimingStructures) == /\ TraversalEndContext6(before,"ProcedureCode6ea937bb44ac") /\ ~before.windowsDone /\ ProcessTraversalEndWindow6(before.windows,after.windows,finishedWindow,actualOtherWindowCompleted,optionsUsed,startedTimingStructures) /\ after = [before EXCEPT !.windows = after.windows] FinishTraversalEndWindows6(before,after) == /\ TraversalEndContext6(before,"ProcedureCode6ea937bb44ac") /\ before.windows = <<>> /\ ~before.windowsDone /\ after = [before EXCEPT !.windowsDone = TRUE] ReturnLiabilityMarkerFund6(before,after,fundBefore,fundAfter,bankBefore,bankAfter) == /\ TraversalEndContext6(before,"ProcedureCode84dea7dc8ecc") /\ before.windowsDone /\ ~before.fundReturned /\ fundBefore \in Nat /\ bankBefore \in Nat /\ fundAfter = 0 /\ bankAfter = bankBefore+fundBefore /\ after = [before EXCEPT !.fundReturned = TRUE] ShouldDeclareUnsuccessful6(r,targetSites) == ~r.reachedSuccess /\ r.attacked \in DOMAIN targetSites DeclareUnsuccessfulTraversal6(before,after,targetSites,events) == /\ TraversalEndContext6(before,"ProcedureCode5e397645e65c") /\ before.windowsDone /\ before.fundReturned /\ ~before.resultDeclared /\ after = [before EXCEPT !.resultDeclared = TRUE,!.traversal.unsuccessful = ShouldDeclareUnsuccessful6(before.traversal,targetSites)] /\ events = IF ShouldDeclareUnsuccessful6(before.traversal,targetSites) THEN {[tag |-> "UnsuccessfulTraversal",traversalId |-> before.traversal.id,targetSite |-> before.traversal.attacked]} ELSE {} CompleteTraversal6(before,after,allStepCReactionsAndCheckpointComplete,events,expiredTraversalIds) == /\ TraversalEndContext6(before,"ProcedureCode9606a4cd52b4") /\ before.windowsDone /\ before.windows = <<>> /\ before.fundReturned /\ before.resultDeclared /\ allStepCReactionsAndCheckpointComplete /\ after = [before EXCEPT !.traversal.complete = TRUE,!.phaseEndedIds = @ \cup {before.traversal.phaseId}] /\ events = {[tag |-> "TraversalEnds",traversalId |-> before.traversal.id]} \cup (IF before.traversal.phaseId \in before.phaseEndedIds THEN {} ELSE {TraversalPhaseEndEvent6(before.traversal)}) /\ expiredTraversalIds = {before.traversal.id} ReturnTraversalToCaller6(before,after,actualTraversalEndReactionsAndCheckpointComplete,caller) == /\ before.traversal.complete /\ before.traversal.id # 0 /\ ~before.returned /\ actualTraversalEndReactionsAndCheckpointComplete /\ caller = before.traversal.caller /\ after = [before EXCEPT !.returned = TRUE] TraversalSteps6 == {"ProcedureCode12371046a2e5","ProcedureCodeacc82dbcc545","ProcedureCode4d6bd06d2c9f","ProcedureCode347de0bdd6b4","ProcedureCode71e36c9e8e04","ProcedureCode7e3f7e5033c8", "ProcedureCode453e949a114f","ProcedureCode3a6daf593ad4","ProcedureCode4d474d346807","ProcedureCodeda7bff1d9270","ProcedureCode8b3260c0010f","ProcedureCodef1914978bb8e","ProcedureCodeaa0828fbf852","ProcedureCode687f72772ab1", "ProcedureCode714dfe070fed","ProcedureCode4f60245a1dde","ProcedureCode9bca3a096549","ProcedureCoded4ddeafb5f2f","ProcedureCode2cd618a9e624","ProcedureCode6c5d14f545f7","ProcedureCode7e82ab2b38b7","ProcedureCodea732fbc12ae0", "ProcedureCodebbb14496b09b","ProcedureCoded75d879e00ff","ProcedureCodec7b41615d673","ProcedureCode6ea937bb44ac","ProcedureCode84dea7dc8ecc","ProcedureCode5e397645e65c","ProcedureCode9606a4cd52b4"} TraversalStepInfo6(step) == [phase |-> CASE step \in {"ProcedureCode12371046a2e5","ProcedureCodeacc82dbcc545","ProcedureCode4d6bd06d2c9f","ProcedureCode347de0bdd6b4","ProcedureCode71e36c9e8e04","ProcedureCode7e3f7e5033c8"} -> "Initiation" [] step \in {"ProcedureCode453e949a114f","ProcedureCode3a6daf593ad4","ProcedureCode4d474d346807"} -> "Approach" [] step \in {"ProcedureCodeda7bff1d9270","ProcedureCode8b3260c0010f","ProcedureCodef1914978bb8e","ProcedureCodeaa0828fbf852","ProcedureCode687f72772ab1"} -> "Encounter" [] step \in {"ProcedureCode714dfe070fed","ProcedureCode4f60245a1dde","ProcedureCode9bca3a096549","ProcedureCoded4ddeafb5f2f","ProcedureCode2cd618a9e624","ProcedureCode6c5d14f545f7","ProcedureCode7e82ab2b38b7","ProcedureCodea732fbc12ae0"} -> "Movement" [] step \in {"ProcedureCodebbb14496b09b","ProcedureCoded75d879e00ff","ProcedureCodec7b41615d673"} -> "Success" [] step \in {"ProcedureCode6ea937bb44ac","ProcedureCode84dea7dc8ecc","ProcedureCode5e397645e65c","ProcedureCode9606a4cd52b4"} -> "TraversalEnds" [] OTHER -> "NoValue", kind |-> CASE step = "ProcedureCode12371046a2e5" -> "AnnounceAndPay" [] step = "ProcedureCodeacc82dbcc545" -> "LiabilityMarker" [] step = "ProcedureCode4d6bd06d2c9f" -> "TraversalBegins" [] step = "ProcedureCode347de0bdd6b4" -> "InitialPosition" [] step \in {"ProcedureCode71e36c9e8e04","ProcedureCode3a6daf593ad4","ProcedureCode8b3260c0010f","ProcedureCode4f60245a1dde","ProcedureCode2cd618a9e624"} -> "PaidWindow" [] step = "ProcedureCode453e949a114f" -> "ApproachBarrier" [] step = "ProcedureCodeda7bff1d9270" -> "EncounterBarrier" [] step = "ProcedureCodef1914978bb8e" -> "NextBarrierInstruction" [] step = "ProcedureCodeaa0828fbf852" -> "BarrierInstructionLoop" [] step = "ProcedureCode714dfe070fed" -> "PassBarrier" [] step = "ProcedureCode9bca3a096549" -> "WithdrawTraversalDecision" [] step = "ProcedureCoded4ddeafb5f2f" -> "AdvancePosition" [] step = "ProcedureCode6c5d14f545f7" -> "MovementBranch" [] step = "ProcedureCode7e82ab2b38b7" -> "ApproachTargetSite" [] step = "ProcedureCodebbb14496b09b" -> "DeclareSuccessful" [] step = "ProcedureCoded75d879e00ff" -> "RulesInspection" [] step = "ProcedureCode6ea937bb44ac" -> "EndWindows" [] step = "ProcedureCode84dea7dc8ecc" -> "ReturnLiabilityMarker" [] step = "ProcedureCode5e397645e65c" -> "DeclareUnsuccessful" [] step = "ProcedureCode9606a4cd52b4" -> "CompleteTraversal" [] step \in TraversalSteps6 -> "CompletePhase" [] OTHER -> "Invalid"] TraversalWindowOptions6(step) == [paid |-> step \in {"ProcedureCode71e36c9e8e04","ProcedureCode3a6daf593ad4","ProcedureCode8b3260c0010f","ProcedureCode4f60245a1dde","ProcedureCode2cd618a9e624"}, nonBarrierActivation |-> step \in {"ProcedureCode71e36c9e8e04","ProcedureCode3a6daf593ad4","ProcedureCode2cd618a9e624"}, approachedBarrierActivation |-> step = "ProcedureCode3a6daf593ad4",score |-> FALSE] NextTraversalStep6(step,branch) == CASE step = "ProcedureCode12371046a2e5" -> "ProcedureCodeacc82dbcc545" [] step = "ProcedureCodeacc82dbcc545" -> "ProcedureCode4d6bd06d2c9f" [] step = "ProcedureCode4d6bd06d2c9f" -> "ProcedureCode347de0bdd6b4" [] step = "ProcedureCode347de0bdd6b4" -> "ProcedureCode71e36c9e8e04" [] step = "ProcedureCode71e36c9e8e04" -> "ProcedureCode7e3f7e5033c8" [] step = "ProcedureCode7e3f7e5033c8" -> IF branch = "Approach" THEN "ProcedureCode453e949a114f" ELSE "ProcedureCode714dfe070fed" [] step = "ProcedureCode453e949a114f" -> "ProcedureCode3a6daf593ad4" [] step = "ProcedureCode3a6daf593ad4" -> "ProcedureCode4d474d346807" [] step = "ProcedureCode4d474d346807" -> IF branch = "Encounter" THEN "ProcedureCodeda7bff1d9270" ELSE "ProcedureCode714dfe070fed" [] step = "ProcedureCodeda7bff1d9270" -> "ProcedureCode8b3260c0010f" [] step = "ProcedureCode8b3260c0010f" -> "ProcedureCodef1914978bb8e" [] step = "ProcedureCodef1914978bb8e" -> IF branch = "BarrierInstruction" THEN "ProcedureCodeaa0828fbf852" ELSE "ProcedureCode687f72772ab1" [] step = "ProcedureCodeaa0828fbf852" -> "ProcedureCodef1914978bb8e" [] step = "ProcedureCode687f72772ab1" -> IF branch = "ReturnForced" THEN "ReturnCaller" ELSE "ProcedureCode714dfe070fed" [] step = "ProcedureCode714dfe070fed" -> "ProcedureCode4f60245a1dde" [] step = "ProcedureCode4f60245a1dde" -> "ProcedureCode9bca3a096549" [] step = "ProcedureCode9bca3a096549" -> IF branch = "WithdrawTraversal" THEN "ProcedureCode6ea937bb44ac" ELSE "ProcedureCoded4ddeafb5f2f" [] step = "ProcedureCoded4ddeafb5f2f" -> "ProcedureCode2cd618a9e624" [] step = "ProcedureCode2cd618a9e624" -> "ProcedureCode6c5d14f545f7" [] step = "ProcedureCode6c5d14f545f7" -> IF branch = "NewPosition" THEN "ProcedureCode453e949a114f" ELSE "ProcedureCode7e82ab2b38b7" [] step = "ProcedureCode7e82ab2b38b7" -> "ProcedureCodea732fbc12ae0" [] step = "ProcedureCodea732fbc12ae0" -> "ProcedureCodebbb14496b09b" [] step = "ProcedureCodebbb14496b09b" -> "ProcedureCoded75d879e00ff" [] step = "ProcedureCoded75d879e00ff" -> "ProcedureCodec7b41615d673" [] step = "ProcedureCodec7b41615d673" -> "ProcedureCode6ea937bb44ac" [] step = "ProcedureCode6ea937bb44ac" -> "ProcedureCode84dea7dc8ecc" [] step = "ProcedureCode84dea7dc8ecc" -> "ProcedureCode5e397645e65c" [] step = "ProcedureCode5e397645e65c" -> "ProcedureCode9606a4cd52b4" [] step = "ProcedureCode9606a4cd52b4" -> "Complete" [] OTHER -> "NoValue" TraversalBranch6(r,l,activationzedDeployedBarrier,e,m,work) == CASE r.step = "ProcedureCode7e3f7e5033c8" -> InitiationDestination6(r,l) [] r.step = "ProcedureCode4d474d346807" -> ApproachDestination6(OpenApproach6(r),l,activationzedDeployedBarrier) [] r.step = "ProcedureCodef1914978bb8e" -> IF work.resolvedSub = 0 THEN "NoValue" ELSE "BarrierInstruction" [] r.step = "ProcedureCode687f72772ab1" -> IF e.forced THEN "ReturnForced" ELSE "Movement" [] r.step = "ProcedureCode9bca3a096549" -> work.jackChoice [] r.step = "ProcedureCode6c5d14f545f7" -> IF m.movedToNew THEN "NewPosition" ELSE "NoPosition" [] OTHER -> "Next" EncounterPostWorkStage6(step) == IF step = "ProcedureCodeda7bff1d9270" THEN "BeginReactions" ELSE IF step = "ProcedureCode687f72772ab1" THEN "Complete" ELSE "BarrierInstructions" BeginNormalTraversalPhaseEnd6(before,after,l,activationzedDeployedBarrier,e,m,work,actualStepAndChildProceduresComplete,events) == /\ TraversalTimingPresent6(before.traversal) /\ before.traversal.step \in {"ProcedureCode7e3f7e5033c8","ProcedureCode4d474d346807","ProcedureCode687f72772ab1","ProcedureCode6c5d14f545f7","ProcedureCodea732fbc12ae0","ProcedureCodec7b41615d673"} /\ before.traversal.phase = TraversalStepInfo6(before.traversal.step).phase /\ before.redirect = NoTraversalRedirect6 /\ ~before.phaseStepsSkipped /\ ~before.redirectCheckpointDue /\ before.traversal.phaseId \notin before.phaseEndedIds /\ actualStepAndChildProceduresComplete /\ IF before.traversal.phase = "Encounter" THEN e.id = before.traversal.phaseId /\ e.traversalId = before.traversal.id /\ ~e.forced /\ ~e.aborted /\ e.stage = "Complete" ELSE TRUE /\ IF before.traversal.phase = "Movement" THEN m.id = before.traversal.phaseId /\ m.traversalId = before.traversal.id ELSE TRUE /\ LET next == NextTraversalStep6(before.traversal.step,TraversalBranch6(before.traversal,l,activationzedDeployedBarrier,e,m,work)) IN next \in TraversalSteps6 /\ TraversalStepInfo6(next).phase # before.traversal.phase /\ after = [before EXCEPT !.phaseEndedIds = @ \cup {before.traversal.phaseId}] /\ events = {TraversalPhaseEndEvent6(before.traversal)} AdvanceNormalTraversalStep6(before,after,l,activationzedDeployedBarrier,e,m,work,newPhaseId, actualStepAndChildProceduresComplete,normalCheckpointAndReactionsDrained,events) == /\ TraversalTimingPresent6(before.traversal) /\ before.traversal.step \in TraversalSteps6 /\ before.traversal.phase = TraversalStepInfo6(before.traversal.step).phase /\ before.redirect = NoTraversalRedirect6 /\ ~before.redirectCheckpointDue /\ ~before.phaseStepsSkipped \/ before.traversal.phase = "TraversalEnds" /\ actualStepAndChildProceduresComplete /\ normalCheckpointAndReactionsDrained /\ IF before.traversal.phase = "Encounter" THEN e.id = before.traversal.phaseId /\ e.traversalId = before.traversal.id /\ ~e.forced /\ ~e.aborted /\ e.stage = EncounterPostWorkStage6(before.traversal.step) ELSE TRUE /\ IF before.traversal.phase = "Movement" THEN m.id = before.traversal.phaseId /\ m.traversalId = before.traversal.id ELSE TRUE /\ work.jackChoice \in {"Continue","WithdrawTraversal"} /\ ~(before.traversal.step = "ProcedureCode9bca3a096549" /\ work.jackChoice = "WithdrawTraversal") /\ IF before.traversal.step = "ProcedureCodef1914978bb8e" THEN (work.resolvedSub # 0 /\ work.resolvedSub \in e.resolved) \/ (work.resolvedSub = 0 /\ NextEncounterSub6(e) = 0) ELSE TRUE /\ before.traversal.step # "ProcedureCode9606a4cd52b4" /\ LET next == NextTraversalStep6(before.traversal.step,TraversalBranch6(before.traversal,l,activationzedDeployedBarrier,e,m,work)) phase == TraversalStepInfo6(next).phase changed == phase # before.traversal.phase r == [before.traversal EXCEPT !.step = next,!.phase = phase, !.phaseId = IF changed THEN newPhaseId ELSE @, !.usedPhaseIds = IF changed THEN @ \cup {newPhaseId} ELSE @, !.reachedSuccess = @ \/ phase = "Success", !.ending = @ \/ phase = "TraversalEnds", !.position = IF phase \in {"Success","TraversalEnds"} THEN "NoValue" ELSE @] IN /\ next \in TraversalSteps6 /\ IF changed THEN before.traversal.phaseId \in before.phaseEndedIds ELSE before.traversal.phaseId \notin before.phaseEndedIds /\ IF changed THEN newPhaseId \in Nat \ {0} /\ newPhaseId \notin before.traversal.usedPhaseIds ELSE newPhaseId = before.traversal.phaseId /\ after = [before EXCEPT !.traversal = r, !.phaseEndedIds = IF changed THEN @ \cup {before.traversal.phaseId} ELSE @, !.encounter = IF phase = "Encounter" THEN r.phaseId ELSE IF before.traversal.phase = "Encounter" THEN 0 ELSE @, !.phaseStepsSkipped = FALSE, !.windowCleanupDue = IF phase = "TraversalEnds" /\ changed THEN TRUE ELSE IF before.traversal.step = "ProcedureCode6ea937bb44ac" THEN FALSE ELSE @] /\ events = {} ForcedEncounterStep6(beforeStep,afterStep,e,afterEncounter,resolvedSub,actualStepAndChildProceduresComplete,normalCheckpointAndReactionsDrained) == /\ beforeStep \in {"ProcedureCodeda7bff1d9270","ProcedureCode8b3260c0010f","ProcedureCodef1914978bb8e","ProcedureCodeaa0828fbf852","ProcedureCode687f72772ab1"} /\ e.forced /\ actualStepAndChildProceduresComplete /\ normalCheckpointAndReactionsDrained /\ ~e.aborted /\ e.stage = EncounterPostWorkStage6(beforeStep) /\ afterEncounter = e /\ afterStep = NextTraversalStep6(beforeStep, IF beforeStep = "ProcedureCodef1914978bb8e" THEN IF resolvedSub = 0 THEN "NoValue" ELSE "BarrierInstruction" ELSE IF beforeStep = "ProcedureCode687f72772ab1" THEN "ReturnForced" ELSE "Next") /\ IF afterStep = "ReturnCaller" THEN e.stage = "Complete" ELSE TRUE /\ IF beforeStep = "ProcedureCodef1914978bb8e" THEN (resolvedSub # 0 /\ resolvedSub \in e.resolved) \/ (resolvedSub = 0 /\ NextEncounterSub6(e) = 0) ELSE TRUE =============================================================================