----------------------------- MODULE OperationContracts ----------------------------- EXTENDS InspectionContracts ActivationStatus8(o) == IF o.form # "Card" \/ o.side # "SideA" \/ ~o.deployed \/ o.zone # "Play" THEN "Neither" ELSE IF o.face = "Down" /\ o.kind \in {"Objective","Facility","Attachment","Barrier"} THEN "Dormant" ELSE IF o.face = "Up" /\ o.kind \in {"Facility","Attachment","Barrier"} THEN "ItemActivated" ELSE "Neither" ItemActivatable8(o) == ActivationStatus8(o) = "Dormant" /\ o.kind # "Objective" ActivationCacheValid8(o) == o.activated = (ActivationStatus8(o) = "ItemActivated") ActivationPermission8(object,o,context) == /\ ItemActivatable8(o) /\ CASE context.route = "CardEffect" -> context.effectAuthorizes [] context.route = "Paid" -> /\ context.open /\ context.kind = "Paid" /\ context.priority = "SideA" /\ IF o.kind = "Barrier" THEN context.step = "ProcedureCode3a6daf593ad4" /\ context.approachedBarrier = object ELSE context.nonBarrierActivationAllowed [] OTHER -> FALSE OpenActivation8(id,object,caller) == [id |-> id,object |-> object,caller |-> caller,stage |-> "Pay",transaction |-> 0, complete |-> FALSE,returned |-> FALSE,result |-> "NoValue"] PayActivation8(before,after,objects,context,actualAllApplicableCostsPaid,actualTransactionId) == /\ before.stage = "Pay" /\ ~before.complete /\ before.object \in DOMAIN objects /\ before.id \in Nat \ {0} /\ ActivationPermission8(before.object,objects[before.object],context) /\ actualAllApplicableCostsPaid /\ actualTransactionId \in Nat \ {0} /\ after = [before EXCEPT !.stage = "CostCheckpoint",!.transaction = actualTransactionId] DrainActivationCostCheckpoint8(before,after,actualTransactionId,normalCostCheckpointAndReactionsComplete) == /\ before.stage = "CostCheckpoint" /\ ~before.complete /\ before.transaction # 0 /\ actualTransactionId = before.transaction /\ normalCostCheckpointAndReactionsComplete /\ after = [before EXCEPT !.stage = "TurnFaceUp"] FinishActivation8(before,after,objects,afterObjects,actualInstructionStillLegal,events) == /\ before.stage = "TurnFaceUp" /\ ~before.complete /\ before.object \in DOMAIN objects /\ ItemActivatable8(objects[before.object]) /\ actualInstructionStillLegal /\ afterObjects = [objects EXCEPT ![before.object].face = "Up",![before.object].activated = TRUE] /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "ItemActivated"] /\ events = {[tag |-> "Activation",object |-> before.object,activationId |-> before.id]} CancelActivation8(before,after,actualActivationInstructionWithoutActivationzingComplete,events) == /\ ~before.complete /\ actualActivationInstructionWithoutActivationzingComplete /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "NotItemActivated"] /\ events = {} ReturnActivation8(before,after,actualInstructionAndEndingReactionsComplete,caller) == /\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualInstructionAndEndingReactionsComplete /\ after = [before EXCEPT !.returned = TRUE] Deactivation8(objects,afterObjects,object,actualCardEffectAuthorizes,events) == /\ object \in DOMAIN objects /\ ActivationStatus8(objects[object]) = "ItemActivated" /\ actualCardEffectAuthorizes /\ afterObjects = [objects EXCEPT ![object].face = "Down",![object].activated = FALSE] /\ events = {[tag |-> "Deactivation",object |-> object]} SideBFacedown8(o) == o.form = "Card" /\ o.side = "SideB" /\ o.zone = "Play" /\ o.deployed /\ o.face = "Down" SideBCharacteristics8(o,normalCharacteristics) == IF SideBFacedown8(o) THEN [key \in {} |-> key] ELSE normalCharacteristics SideBAbilityActivity8(o,otherwiseActive) == ~SideBFacedown8(o) /\ otherwiseActive TurnSideBFace8(objects,afterObjects,object,face,actualCardEffectAuthorizes,events) == /\ object \in DOMAIN objects /\ objects[object].form = "Card" /\ objects[object].side = "SideB" /\ objects[object].deployed /\ objects[object].zone = "Play" /\ face \in {"Up","Down"} /\ objects[object].face # face /\ actualCardEffectAuthorizes /\ afterObjects = [objects EXCEPT ![object].face = face,![object].activated = FALSE] /\ events = {[tag |-> IF face = "Down" THEN "TurnFacedown" ELSE "TurnFaceup",object |-> object]} SideBOriginEventValid8(object,method,serial,ability,event) == /\ method \in {"DeployedFacedown","TurnedFacedown"} /\ serial \in Nat \ {0} /\ event.id \in Nat \ {0} /\ event.object = object /\ event.serial = serial /\ event.ability = ability /\ IF method = "DeployedFacedown" THEN event.tag = "Deployed" /\ event.face = "Down" /\ ~event.previousFaceupProfile.known ELSE event.tag = "TurnFacedown" /\ event.previousFaceupProfile.known RecordSideBFaceOrigin8(before,after,object,method,serial,ability,actualFacedownEvent) == /\ SideBOriginEventValid8(object,method,serial,ability,actualFacedownEvent) /\ IF object \in DOMAIN before THEN serial > before[object].serial ELSE TRUE /\ after = [id \in DOMAIN before \cup {object} |-> IF id = object THEN [method |-> method,serial |-> serial,ability |-> ability,eventId |-> actualFacedownEvent.id] ELSE before[id]] SideBOriginsComplete8(objects,origins,actualPublicEventHistory) == /\ {id \in DOMAIN objects : SideBFacedown8(objects[id])} \subseteq DOMAIN origins /\ \A id \in {i \in DOMAIN objects : SideBFacedown8(objects[i])} : /\ origins[id].eventId \in DOMAIN actualPublicEventHistory /\ actualPublicEventHistory[origins[id].eventId].id = origins[id].eventId /\ SideBOriginEventValid8(id,origins[id].method,origins[id].serial,origins[id].ability, actualPublicEventHistory[origins[id].eventId]) /\ \A e \in DOMAIN actualPublicEventHistory : actualPublicEventHistory[e].object = id => actualPublicEventHistory[e].serial <= origins[id].serial PublicSideBOrigins8(objects,origins,actualPublicEventHistory) == [id \in {i \in DOMAIN objects : SideBFacedown8(objects[i])} |-> [method |-> origins[id].method,serial |-> origins[id].serial,ability |-> origins[id].ability, previousFaceupProfile |-> IF origins[id].method = "TurnedFacedown" THEN actualPublicEventHistory[origins[id].eventId].previousFaceupProfile ELSE [known |-> FALSE,card |-> "Hidden"]]] SideBBDiscardPileFacePost8(o) == (o.form = "Card" /\ o.side = "SideB" /\ o.zone = "SideBDiscard") => o.face = "Up" CardMovements8 == {"Arrange","Draw","Forfeit","Deploy","Play","Search","ObjectiveCompletion","ClaimObjective","Swap","Retire"} MovementRuleBlock8(kind) == CASE kind = "Arrange" -> "ProcedureCode00dc1c832c18" [] kind = "Draw" -> "ProcedureCode163c820d9576" [] kind = "Forfeit" -> "ProcedureCode4cb5f79f70e8" [] kind = "Deploy" -> "ProcedureCodecc6f2aa507f6" [] kind = "Play" -> "ProcedureCode6dc50a2fd3ef" [] kind = "Search" -> "ProcedureCode8719c8b9d63c" [] kind \in {"ObjectiveCompletion","ClaimObjective"} -> "ProcedureCode3d7a51acc5cb" [] kind = "Swap" -> "ProcedureCode01037eaa1fce" [] kind = "Retire" -> "ProcedureCodea93d4fa2a792" [] OTHER -> "NoValue" MovementDispositions8 == {"Complete","ModifiedEffects","ReplacedByName","Prevented","Impossible","NoEffect"} MovementOccurred8(kind,disposition,actualInstructionResolved) == kind \in CardMovements8 /\ actualInstructionResolved /\ disposition \in {"Complete","ModifiedEffects"} MovementEvent8(occurrenceId,kind,originalObjects) == [tag |-> "Movement",occurrenceId |-> occurrenceId,kind |-> kind,originalObjects |-> originalObjects] RecordMovement8(beforeHistory,afterHistory,occurrenceId,kind,originalObjects,disposition,actualInstructionResolved,events) == /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin DOMAIN beforeHistory /\ kind \in CardMovements8 /\ disposition \in MovementDispositions8 /\ actualInstructionResolved /\ IF MovementOccurred8(kind,disposition,actualInstructionResolved) THEN /\ afterHistory = [id \in DOMAIN beforeHistory \cup {occurrenceId} |-> IF id = occurrenceId THEN MovementEvent8(occurrenceId,kind,originalObjects) ELSE beforeHistory[id]] /\ events = {MovementEvent8(occurrenceId,kind,originalObjects)} ELSE afterHistory = beforeHistory /\ events = {} DirectRelocations8 == {"Add","Move","Discard","SetAside","RemoveFromGame"} DirectRelocationPlan8(verb,owner,directedZone) == [valid |-> verb \in DirectRelocations8 /\ owner \in SetupPlayers /\ (verb \in {"Add","Move"} => directedZone \in ZoneInstances4), destination |-> CASE verb \in {"Add","Move"} -> directedZone [] verb = "Discard" -> owner \o "Discard" [] verb = "SetAside" -> "SetAside" [] verb = "RemoveFromGame" -> "Removed" [] OTHER -> "NoValue", namedMovement |-> "NoValue"] ForfeitPlan8(objects,objective,actualProtectedHostedSourceIds) == LET present == objective \in DOMAIN objects validObjective == IF present THEN objects[objective].form = "Card" /\ objects[objective].kind = "Objective" /\ objects[objective].zone \in SetupObjectiveZones ELSE FALSE hosted == {id \in DOMAIN objects : objects[id].host = objective} IN [valid |-> validObjective /\ actualProtectedHostedSourceIds \subseteq hosted, destination |-> "Removed",removeFromObjectiveArea |-> {objective}, trashNow |-> hosted \ actualProtectedHostedSourceIds, cleanupLater |-> actualProtectedHostedSourceIds,cleanupStage |-> "ProcedureCode76ca53ad9dd0"] ForfeitObjectivePost8(beforeObjects,afterObjects,oldObjective,newObject,usedObjectIds) == /\ oldObjective \in DOMAIN beforeObjects /\ beforeObjects[oldObjective].form = "Card" /\ beforeObjects[oldObjective].kind = "Objective" /\ beforeObjects[oldObjective].zone \in SetupObjectiveZones /\ newObject \in Nat \ {0} /\ newObject \notin usedObjectIds /\ newObject \notin DOMAIN beforeObjects /\ oldObjective \notin DOMAIN afterObjects /\ newObject \in DOMAIN afterObjects /\ afterObjects[newObject].form = "Card" /\ afterObjects[newObject].card = beforeObjects[oldObjective].card /\ afterObjects[newObject].zone = "Removed" /\ ~afterObjects[newObject].deployed /\ afterObjects[newObject].host = 0 ForfeitObjectiveCompletionMembership8(beforeIds,afterIds,objective) == objective \in beforeIds /\ afterIds = beforeIds \ {objective} ForfeitHostedCleanup8(plan,actuallyRetireedSourceIds,actualProtectedTransits,owningAbility) == /\ plan.valid /\ plan.trashNow \subseteq actuallyRetireedSourceIds /\ plan.cleanupLater \cap actuallyRetireedSourceIds = {} /\ plan.cleanupLater \subseteq DOMAIN actualProtectedTransits /\ \A id \in plan.cleanupLater : actualProtectedTransits[id].protected /\ actualProtectedTransits[id].ability = owningAbility /\ actualProtectedTransits[id].cleanupStage = "ProcedureCode76ca53ad9dd0" /\ actualProtectedTransits[id].object \in Nat \ {0} ArrangeWord8(word) == word \in {"Arrange","Rearrange"} SmallArrangement8(ids) == Cardinality(ids) <= 1 CardLocation8(o) == [zone |-> o.zone,loc |-> o.loc,area |-> o.area,targetSite |-> o.targetSite, targetSiteKind |-> o.targetSiteKind,position |-> o.position,host |-> o.host] WithCardLocation8(o,l) == [o EXCEPT !.zone = l.zone,!.loc = l.loc,!.area = l.area,!.targetSite = l.targetSite, !.targetSiteKind = l.targetSiteKind,!.position = l.position,!.host = l.host] ExchangeDeployedLocations8(objects,a,b) == [id \in DOMAIN objects |-> IF id=a THEN WithCardLocation8(objects[a],CardLocation8(objects[b])) ELSE IF id=b THEN WithCardLocation8(objects[b],CardLocation8(objects[a])) ELSE objects[id]] OpenBarrierArrangement8(id,targets) == [id |-> id,targets |-> targets,stage |-> "Swaps",complete |-> FALSE,swapEvents |-> {}] DeployedBarrier8(o) == o.form = "Card" /\ o.side = "SideA" /\ o.kind = "Barrier" /\ o.zone = "Play" /\ o.deployed SwapArrangingBarrier8(before,after,objects,afterObjects,a,b,occurrenceId,actualNormalSwapAllowed, checkpointSerial,afterCheckpointSerial,pending,afterPending,events) == /\ before.stage = "Swaps" /\ ~before.complete /\ ~SmallArrangement8(before.targets) /\ a \in before.targets \cap DOMAIN objects /\ b \in before.targets \cap DOMAIN objects /\ a # b /\ DeployedBarrier8(objects[a]) /\ DeployedBarrier8(objects[b]) /\ actualNormalSwapAllowed /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin before.swapEvents /\ afterObjects = ExchangeDeployedLocations8(objects,a,b) /\ checkpointSerial = afterCheckpointSerial /\ pending = afterPending /\ after = [before EXCEPT !.swapEvents = @ \cup {occurrenceId}] /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})} FinishBarrierArrangement8(before,after,actualArrangementResolved,events) == /\ before.stage = "Swaps" /\ ~before.complete /\ actualArrangementResolved /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] /\ events = IF SmallArrangement8(before.targets) THEN {} ELSE {MovementEvent8(before.id,"Arrange",before.targets)} ArrangementInstructionCheckpointAllowed8(frame,actualContainingInstructionResolved) == frame.complete /\ actualContainingInstructionResolved FreshSuccessors8(sources,successors,usedIds) == /\ DOMAIN successors = sources /\ {successors[id] : id \in sources} \subseteq (Nat \ {0}) \ usedIds /\ Cardinality({successors[id] : id \in sources}) = Cardinality(sources) CardBatchTransfer8(beforeObjects,afterObjects,sources,successors,usedIds,destination,face,destinationLocs) == /\ sources \subseteq DOMAIN beforeObjects /\ DOMAIN beforeObjects \subseteq usedIds /\ FreshSuccessors8(sources,successors,usedIds) /\ DOMAIN destinationLocs = sources /\ DOMAIN afterObjects = (DOMAIN beforeObjects \ sources) \cup {successors[id] : id \in sources} /\ \A id \in DOMAIN beforeObjects \ sources : afterObjects[id] = beforeObjects[id] /\ \A id \in sources : /\ beforeObjects[id].form = "Card" /\ beforeObjects[id].host = 0 /\ afterObjects[successors[id]].form = "Card" /\ afterObjects[successors[id]].card = beforeObjects[id].card /\ afterObjects[successors[id]].side = beforeObjects[id].side /\ afterObjects[successors[id]].zone = destination /\ afterObjects[successors[id]].loc = destinationLocs[id] /\ afterObjects[successors[id]].face = face /\ ~afterObjects[successors[id]].deployed /\ ~afterObjects[successors[id]].activated /\ afterObjects[successors[id]].host = 0 /\ afterObjects[successors[id]].marks = {} DeckObjectOrder8(objects,owner,deck) == SubIds6(deck) = {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].zone = owner \o "Deck"} /\ Len(deck) = Cardinality(SubIds6(deck)) AsideGroupIds8(objects,transits,effectId) == {id \in DOMAIN objects \cap DOMAIN transits : objects[id].form = "Card" /\ objects[id].zone = "SetAside" /\ transits[id].effect = effectId} RegisterAsideBatch8(beforeTransits,afterTransits,beforeObjects,sources,successors,effectId,ability) == afterTransits = [id \in (DOMAIN beforeTransits \ sources) \cup {successors[s] : s \in sources} |-> IF id \in {successors[s] : s \in sources} THEN LET old == CHOOSE s \in sources : successors[s] = id IN SetAsideTransit4(id,beforeObjects[old].zone,beforeObjects[old].loc,effectId,ability,FALSE,FALSE) ELSE beforeTransits[id]] OpenDeckArrangement8(id,actor,owner,amount,ability) == [id |-> id,actor |-> actor,owner |-> owner,amount |-> amount,ability |-> ability, stage |-> "Start",complete |-> FALSE,originalIds |-> {},originalCount |-> 0] TopCardCount8(deck,amount) == IF amount < Len(deck) THEN amount ELSE Len(deck) DeckArrangePrefix8(deck,amount) == SubSeq(deck,1,TopCardCount8(deck,amount)) BeginDeckArrangement8(before,after,objects,afterObjects,deck,afterDeck,transits,afterTransits, successors,usedIds,actualCompoundInstructionNeedsAside) == /\ before.stage = "Start" /\ ~before.complete /\ before.id \in Nat \ {0} /\ before.actor \in SetupPlayers /\ before.owner \in SetupPlayers /\ before.amount \in Nat /\ DeckObjectOrder8(objects,before.owner,deck) /\ SetAsideTrackingValid4(objects,transits) /\ LET prefix == DeckArrangePrefix8(deck,before.amount) sources == SubIds6(prefix) IN /\ Cardinality(sources) >= 2 \/ actualCompoundInstructionNeedsAside /\ CardBatchTransfer8(objects,afterObjects,sources,successors,usedIds,"SetAside","Down", [id \in sources |-> "SetAside"]) /\ afterDeck = SubSeq(deck,Len(prefix)+1,Len(deck)) /\ RegisterAsideBatch8(transits,afterTransits,objects,sources,successors,before.id,before.ability) /\ after = [before EXCEPT !.stage = "OtherEffects",!.originalIds = sources,!.originalCount = Len(prefix)] NoOpDeckArrangement8(before,after,objects,deck,actualCompoundInstructionNeedsAside,events) == /\ before.stage = "Start" /\ ~before.complete /\ before.amount \in Nat /\ DeckObjectOrder8(objects,before.owner,deck) /\ ~actualCompoundInstructionNeedsAside /\ Len(DeckArrangePrefix8(deck,before.amount)) <= 1 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] /\ events = {} DeckArrangeMayLook8(frame,viewer) == ~frame.complete /\ frame.stage = "OtherEffects" /\ viewer = frame.actor DeckArrangeEffectiveViewers8(frame,objects,transits,object,ordinaryViewers) == IF ~frame.complete /\ frame.stage = "OtherEffects" /\ object \in AsideGroupIds8(objects,transits,frame.id) THEN (ordinaryViewers \ (IF frame.owner # frame.actor THEN {frame.owner} ELSE {})) \cup {frame.actor} ELSE ordinaryViewers DeckArrangeOtherEffects8(frame,objects,transits,actedOnIds,declaredOriginalPositions) == frame.stage = "OtherEffects" /\ ~frame.complete /\ SetAsideTrackingValid4(objects,transits) /\ actedOnIds \subseteq AsideGroupIds8(objects,transits,frame.id) /\ declaredOriginalPositions = {} ReturnDeckArrangement8(before,after,objects,afterObjects,deck,afterDeck,transits,afterTransits, order,successors,usedIds,actualOtherEffectsComplete) == /\ before.stage = "OtherEffects" /\ ~before.complete /\ actualOtherEffectsComplete /\ DeckObjectOrder8(objects,before.owner,deck) /\ SetAsideTrackingValid4(objects,transits) /\ LET group == AsideGroupIds8(objects,transits,before.id) IN /\ SubIds6(order) = group /\ Len(order) = Cardinality(group) /\ CardBatchTransfer8(objects,afterObjects,group,successors,usedIds,before.owner \o "Deck","Down", [id \in group |-> <<"Deck",before.id,PositionIndex6(order,id)>>]) /\ afterDeck = [i \in 1..Len(order) |-> successors[order[i]]] \o deck /\ afterTransits = [id \in DOMAIN transits \ group |-> transits[id]] /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] DeckArrangementPublicSummary8(frame) == [actor |-> frame.actor,owner |-> frame.owner,count |-> frame.originalCount] DeckArrangementPublicAction8(kind,destination,actualPublicProfile,privateOriginalPosition) == [kind |-> kind,destination |-> destination,profile |-> actualPublicProfile] DrawChoiceOrder8(active,participants) == (IF active \in participants THEN <> ELSE <<>>) \o (IF TurnOtherPlayer5(active) \in participants THEN <> ELSE <<>>) OpenDrawBatch8(id,participants,amounts,optional,active,ability,caller) == [id |-> id,participants |-> participants,amounts |-> amounts, effective |-> [p \in participants |-> 0],countsReady |-> FALSE, order |-> DrawChoiceOrder8(active,participants),nextChoice |-> 1, ability |-> ability,caller |-> caller,stage |-> IF optional THEN "Decisions" ELSE "SetAside", checkpointId |-> 0,reactionId |-> 0,initialDrawn |-> [p \in participants |-> {}], actualCounts |-> [p \in participants |-> 0],complete |-> FALSE,returned |-> FALSE] DrawBatchValid8(b) == /\ b.id \in Nat \ {0} /\ b.participants \subseteq SetupPlayers /\ b.participants # {} /\ DOMAIN b.amounts = b.participants /\ DOMAIN b.effective = b.participants /\ SubIds6(b.order) = b.participants /\ Len(b.order) = Cardinality(b.participants) /\ b.nextChoice \in 1..(Len(b.order)+1) /\ \A p \in b.participants : b.amounts[p] \in Nat /\ b.effective[p] \in Nat /\ b.stage \in {"Decisions","SetAside","Checkpoint","DrawReactions","Return","Complete"} /\ b.complete = (b.stage = "Complete") /\ (b.returned => b.complete) ChooseDrawAmount8(before,after,player,amount,actualAllowedAmounts) == /\ DrawBatchValid8(before) /\ before.stage = "Decisions" /\ before.nextChoice \in 1..Len(before.order) /\ player = before.order[before.nextChoice] /\ amount \in Nat /\ amount \in actualAllowedAmounts[player] /\ after = [before EXCEPT !.amounts[player] = amount,!.nextChoice = @+1, !.stage = IF before.nextChoice = Len(before.order) THEN "SetAside" ELSE "Decisions"] LockDrawCounts8(before,after,actualEffectiveAmounts,actualDrawModifiersResolved) == /\ DrawBatchValid8(before) /\ before.stage = "SetAside" /\ ~before.countsReady /\ actualDrawModifiersResolved /\ DOMAIN actualEffectiveAmounts = before.participants /\ \A p \in before.participants : actualEffectiveAmounts[p] \in Nat /\ after = [before EXCEPT !.effective = actualEffectiveAmounts,!.countsReady = TRUE] DrawDeckoutWinner8(b,decks) == IF "SideA" \in b.participants THEN IF b.effective["SideA"] > Len(decks["SideA"]) THEN "SideB" ELSE "NoValue" ELSE "NoValue" DrawPrefixes8(b,decks) == [p \in b.participants |-> DeckArrangePrefix8(decks[p],b.effective[p])] DrawSources8(b,decks) == UNION {SubIds6(DrawPrefixes8(b,decks)[p]) : p \in b.participants} DrawStartEvents8(b) == {[tag |-> "CardsDrawn",batchId |-> b.id,player |-> p,objects |-> b.initialDrawn[p],count |-> b.actualCounts[p]] : p \in {q \in b.participants : b.actualCounts[q] > 0}} DrawAsideTransits8(beforeTransits,objects,sources,successors,b) == [id \in (DOMAIN beforeTransits \ sources) \cup {successors[s] : s \in sources} |-> IF id \in {successors[s] : s \in sources} THEN LET old == CHOOSE s \in sources : successors[s] = id player == CHOOSE p \in b.participants : objects[old].zone = p \o "Deck" IN [object |-> id,originZone |-> objects[old].zone,originLocation |-> objects[old].loc, effect |-> b.id,ability |-> b.ability,protected |-> FALSE,cleanupStage |-> "ProcedureCode96bfa1b6a970",drawPlayer |-> player] ELSE beforeTransits[id]] BeginDrawBatch8(before,after,objects,afterObjects,decks,afterDecks,transits,afterTransits,successors,usedIds,events) == /\ DrawBatchValid8(before) /\ before.stage = "SetAside" /\ before.countsReady /\ \E p \in before.participants : before.effective[p] > 0 /\ DrawDeckoutWinner8(before,decks) = "NoValue" /\ DOMAIN decks = SetupPlayers /\ \A p \in SetupPlayers : DeckObjectOrder8(objects,p,decks[p]) /\ SetAsideTrackingValid4(objects,transits) /\ LET prefixes == DrawPrefixes8(before,decks) sources == DrawSources8(before,decks) IN /\ CardBatchTransfer8(objects,afterObjects,sources,successors,usedIds,"SetAside","Down",[id \in sources |-> "SetAside"]) /\ afterDecks = [p \in SetupPlayers |-> IF p \in before.participants THEN SubSeq(decks[p],Len(prefixes[p])+1,Len(decks[p])) ELSE decks[p]] /\ afterTransits = DrawAsideTransits8(transits,objects,sources,successors,before) /\ after = [before EXCEPT !.stage = "Checkpoint", !.initialDrawn = [p \in before.participants |-> {successors[id] : id \in SubIds6(prefixes[p])}], !.actualCounts = [p \in before.participants |-> Len(prefixes[p])]] /\ events = DrawStartEvents8(after) CompleteZeroDraw8(before,after,events) == /\ DrawBatchValid8(before) /\ before.stage = "SetAside" /\ before.countsReady /\ \A p \in before.participants : before.effective[p] = 0 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] /\ events = {} OpenDrawReactions8(before,after,actualCheckpointId,actualReactionWindowId,actualNormalCheckpointProcessed) == /\ before.stage = "Checkpoint" /\ ~before.complete /\ actualNormalCheckpointProcessed /\ actualCheckpointId \in Nat \ {0} /\ actualReactionWindowId \in Nat /\ after = [before EXCEPT !.stage = "DrawReactions",!.checkpointId = actualCheckpointId,!.reactionId = actualReactionWindowId] DrawGroupsValid8(b,objects,transits) == /\ SetAsideTrackingValid4(objects,transits) /\ \A id \in AsideGroupIds8(objects,transits,b.id) : "drawPlayer" \in DOMAIN transits[id] /\ transits[id].drawPlayer \in b.participants /\ transits[id].ability = b.ability DrawnIds8(b,objects,transits,player) == {id \in AsideGroupIds8(objects,transits,b.id) : transits[id].drawPlayer = player} DrawLookGrant8(b,objects,transits,controllers,viewer,object) == b.stage \in {"Checkpoint","DrawReactions","Return"} /\ ~b.complete /\ object \in AsideGroupIds8(objects,transits,b.id) /\ object \in DOMAIN controllers /\ controllers[object] = viewer DrawSpecificAbilitySees8(b,objects,transits,object,actualAbility) == b.stage = "DrawReactions" /\ ~b.complete /\ actualAbility.triggerRefersDrawn /\ actualAbility.batchId = b.id /\ object \in DrawnIds8(b,objects,transits,actualAbility.player) DrawTransitObservation8(transit,actualAbilityRefersToDrawn,phase,destination) == IF actualAbilityRefersToDrawn THEN [visible |-> TRUE,fromZone |-> IF phase="Enter" THEN transit.originZone ELSE "SetAside", toZone |-> IF phase="Enter" THEN "SetAside" ELSE destination] ELSE IF phase="Enter" THEN [visible |-> FALSE,fromZone |-> "NoValue",toZone |-> "NoValue"] ELSE [visible |-> TRUE,fromZone |-> transit.originZone,toZone |-> destination] FinishDrawReactions8(before,after,actualAllDrawReactionsAndChildrenComplete) == /\ before.stage = "DrawReactions" /\ ~before.complete /\ actualAllDrawReactionsAndChildrenComplete /\ after = [before EXCEPT !.stage = "Return"] DrawHandTransfer8(objects,afterObjects,sources,successors,usedIds,cardData) == /\ sources \subseteq DOMAIN objects /\ DOMAIN objects \subseteq usedIds /\ FreshSuccessors8(sources,successors,usedIds) /\ DOMAIN afterObjects = (DOMAIN objects \ sources) \cup {successors[id] : id \in sources} /\ \A id \in DOMAIN objects \ sources : afterObjects[id] = objects[id] /\ \A id \in sources : /\ objects[id].form = "Card" /\ objects[id].zone = "SetAside" /\ cardData[objects[id].card].owner \in SetupPlayers /\ afterObjects[successors[id]].form = "Card" /\ afterObjects[successors[id]].card = objects[id].card /\ afterObjects[successors[id]].side = objects[id].side /\ afterObjects[successors[id]].zone = cardData[objects[id].card].owner \o "Hand" /\ afterObjects[successors[id]].loc = cardData[objects[id].card].owner \o "Hand" /\ afterObjects[successors[id]].face = "Down" /\ ~afterObjects[successors[id]].deployed /\ ~afterObjects[successors[id]].activated /\ afterObjects[successors[id]].host = 0 /\ afterObjects[successors[id]].marks = {} ReturnDrawnCards8(before,after,objects,afterObjects,transits,afterTransits,successors,usedIds,cardData,events) == /\ before.stage = "Return" /\ ~before.complete /\ DrawGroupsValid8(before,objects,transits) /\ LET group == AsideGroupIds8(objects,transits,before.id) IN /\ DrawHandTransfer8(objects,afterObjects,group,successors,usedIds,cardData) /\ afterTransits = [id \in DOMAIN transits \ group |-> transits[id]] /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] /\ events = {} ReturnDrawToCaller8(before,after,actualProcedureEndCheckpointAndReactionsComplete,caller) == /\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualProcedureEndCheckpointAndReactionsComplete /\ after = [before EXCEPT !.returned = TRUE] DeploySteps8 == {"ProcedureCodec4ba55e330f8","ProcedureCode6eba7e0bfa75","ProcedureCode61973f2a75d8","ProcedureCode1ff52d705816","CostBarrier","ProcedureCode0f76bcc2eb00","ProcedureCode4585e6a51427","Complete"} NoDeployDestination8 == [zone |-> "Play",loc |-> "NoValue",area |-> "NoValue",targetSite |-> "NoValue",targetSiteKind |-> "NoValue",position |-> "NoValue",host |-> 0] OpenDeploy8(id,object,actor,face,caller,activationMode) == [id |-> id,sourceObject |-> object,object |-> object,actor |-> actor,face |-> face,caller |-> caller, activationMode |-> activationMode,stage |-> "ProcedureCodec4ba55e330f8",destination |-> NoDeployDestination8,newAuxiliarySite |-> FALSE, transaction |-> 0,checkpointRequired |-> FALSE,x |-> [exists |-> FALSE,amount |-> 0], complete |-> FALSE,deployedOccurred |-> FALSE,activationStarted |-> FALSE,activationProcessed |-> FALSE,activationPerformed |-> FALSE, verificationDone |-> FALSE,returned |-> FALSE] DeployEffectiveKind8(o,face) == IF o.side = "SideB" /\ face = "Down" THEN "Facedown" ELSE o.kind DeployTypeAllowed8(o,actor,face,actualSpecialDeployAuthorized) == /\ actor \in SetupPlayers /\ face \in {"Up","Down"} /\ IF o.form = "Counter" THEN actualSpecialDeployAuthorized ELSE /\ o.form = "Card" /\ o.side = actor /\ IF actor = "SideA" THEN o.kind \in {"Objective","Facility","Barrier","Attachment"} /\ (face="Down" \/ actualSpecialDeployAuthorized) ELSE IF face="Down" THEN actualSpecialDeployAuthorized ELSE o.kind \in {"Equipment","Technique","Support"} DeployStagingRow8(o,face,renew) == [o EXCEPT !.zone = "Play",!.loc = "DeployStaging",!.area = "Staging",!.targetSite = "NoValue",!.targetSiteKind = "NoValue", !.position = "NoValue",!.host = 0,!.deployed = FALSE,!.activated = FALSE,!.face = face, !.marks = IF renew THEN {} ELSE @] BeginDeploy8(before,after,objects,afterObjects,newObject,usedIds,actualDeployAuthorized, actualSpecialDeployAuthorized,actualSpecifiedDestinationResolvable) == /\ before.stage = "ProcedureCodec4ba55e330f8" /\ ~before.complete /\ before.id \in Nat \ {0} /\ before.object \in DOMAIN objects /\ ~objects[before.object].deployed /\ actualDeployAuthorized /\ actualSpecifiedDestinationResolvable /\ DeployTypeAllowed8(objects[before.object],before.actor,before.face,actualSpecialDeployAuthorized) /\ LET renew == objects[before.object].zone # "Play" IN /\ IF renew THEN newObject \in Nat \ {0} /\ newObject \notin usedIds \cup DOMAIN objects ELSE newObject = before.object /\ afterObjects = [id \in (DOMAIN objects \ {before.object}) \cup {newObject} |-> IF id=newObject THEN DeployStagingRow8(objects[before.object],before.face,renew) ELSE objects[id]] /\ after = [before EXCEPT !.object = newObject,!.stage = "ProcedureCode6eba7e0bfa75"] DeployDestinationAllowed8(o,actor,face,destination,newAuxiliarySite,targetSites,usedTargetSiteIds,objects, actualHostAllowed,actualSpecifiedDestinationValid,allowedUpgradeTargetSites,activeAuxiliarySiteLimits) == /\ actualSpecifiedDestinationValid /\ destination.zone = "Play" /\ IF destination.host # 0 THEN ~newAuxiliarySite /\ actualHostAllowed /\ destination.host \in DOMAIN objects /\ objects[destination.host].zone = "Play" /\ destination.area = "Hosted" ELSE IF actor = "SideB" THEN destination.area = "SideBRig" /\ destination.targetSite = "NoValue" /\ ~newAuxiliarySite ELSE /\ destination.area \in {"Root","Protecting"} /\ IF newAuxiliarySite THEN destination.targetSiteKind = "SchemaAtom132" /\ destination.targetSite \notin usedTargetSiteIds \cup DOMAIN targetSites \cup {"NoValue"} /\ \A limit \in activeAuxiliarySiteLimits : Cardinality(AuxiliarySiteTargetSiteIds4(targetSites))+1 <= limit ELSE destination.targetSite \in DOMAIN targetSites /\ destination.targetSiteKind = targetSites[destination.targetSite].kind /\ TargetSiteDeployDestinationGate4(actor,o.kind,destination,TRUE, o.kind # "Attachment" \/ destination.targetSite \in allowedUpgradeTargetSites) DeclareDeployDestination8(before,after,objects,destination,newAuxiliarySite,targetSites,usedTargetSiteIds, actualHostAllowed,actualSpecifiedDestinationValid,allowedUpgradeTargetSites,activeAuxiliarySiteLimits) == /\ before.stage = "ProcedureCode6eba7e0bfa75" /\ ~before.complete /\ before.object \in DOMAIN objects /\ DeployDestinationAllowed8(objects[before.object],before.actor,before.face,destination,newAuxiliarySite, targetSites,usedTargetSiteIds,objects,actualHostAllowed,actualSpecifiedDestinationValid,allowedUpgradeTargetSites,activeAuxiliarySiteLimits) /\ after = [before EXCEPT !.destination = destination,!.newAuxiliarySite = newAuxiliarySite,!.stage = "ProcedureCode61973f2a75d8"] DeployPositionBase8(layout,destination,newAuxiliarySite) == IF newAuxiliarySite /\ destination.targetSite \notin DOMAIN layout.orders THEN [layout EXCEPT !.orders = [s \in DOMAIN @ \cup {destination.targetSite} |-> IF s=destination.targetSite THEN <<>> ELSE layout.orders[s]]] ELSE layout DeclareDeployBarrierPosition8(before,after,layout,afterLayout,gap,mode,anchor,rememberedLocation) == /\ before.stage = "ProcedureCode6eba7e0bfa75" /\ after.stage = "ProcedureCode61973f2a75d8" /\ after.id = before.id /\ after.destination.area = "Protecting" /\ DeclareBarrierPosition6(DeployPositionBase8(layout,after.destination,after.newAuxiliarySite),afterLayout, after.destination.position,after.destination.targetSite,gap,mode,anchor,rememberedLocation,before.id,"ProcedureCode6eba7e0bfa75") DeployedProtectingBarrier8(objects,targetSite) == {id \in DOMAIN objects : DeployedBarrier8(objects[id]) /\ objects[id].host = 0 /\ objects[id].area = "Protecting" /\ objects[id].targetSite = targetSite} DeployLikeEligible8(f,objects,effectiveTypes,controllers) == LET kind == DeployEffectiveKind8(objects[f.object],f.face) IN IF f.actor = "SideA" /\ f.destination.area = "Root" /\ kind \in {"Objective","Facility","Attachment"} THEN {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].deployed /\ objects[id].zone = "Play" /\ objects[id].area = "Root" /\ objects[id].targetSite = f.destination.targetSite} ELSE IF f.actor = "SideA" /\ f.destination.area = "Protecting" /\ kind="Barrier" THEN DeployedProtectingBarrier8(objects,f.destination.targetSite) ELSE IF f.actor="SideB" /\ kind="Technique" THEN {id \in DeployedTechniqueIds(objects,effectiveTypes) : controllers[id] = "SideB"} ELSE {} DeployRequiredRootRetire8(f,objects) == LET card == objects[f.object] IN IF f.actor="SideA" /\ f.destination.area="Root" THEN (IF card.kind \in {"Objective","Facility"} THEN ObjectiveFacilityRootOccupants(objects,f.destination.targetSite) ELSE {}) \cup (IF "SchemaAtom130" \in card.subtypes THEN DeployedRootRegions(objects,f.destination.targetSite) ELSE {}) ELSE {} FinishDeployLikeRetire8(before,after,objects,chosen,actuallyRetireed,effectiveTypes,controllers,capacityAfter(_),actualRetireProcedureComplete) == /\ before.stage = "ProcedureCode61973f2a75d8" /\ ~before.complete /\ before.object \in DOMAIN objects /\ actualRetireProcedureComplete /\ chosen \subseteq DeployLikeEligible8(before,objects,effectiveTypes,controllers) /\ actuallyRetireed \subseteq chosen /\ DeployRequiredRootRetire8(before,objects) \subseteq actuallyRetireed /\ IF before.actor="SideB" /\ DeployEffectiveKind8(objects[before.object],before.face)="Technique" THEN TechniqueDeployCapacityChoice(DeployedTechniqueIds(objects,effectiveTypes),before.object,actuallyRetireed,capacityAfter) ELSE TRUE /\ after = [before EXCEPT !.stage = "ProcedureCode1ff52d705816"] DeployRetireArrivalFace8(beforeCard,afterCard) == beforeCard.side = "SideA" /\ afterCard.zone = "SideADiscard" /\ afterCard.face = beforeCard.face DeployInherentPart8(card,face,objects,destination,x) == IF card.form = "Counter" \/ (card.side="SideB" /\ face="Down") THEN [applicable |-> TRUE,exists |-> FALSE,amount |-> 0] ELSE IF card.kind="Barrier" THEN InherentDeployCost(card,Cardinality(DeployedProtectingBarrier8(objects,destination.targetSite))) ELSE InherentDeployCost([card EXCEPT !.deployCost = IF card.deployX THEN x ELSE @],0) PayDeployStep8(before,after,objects,actualTransaction,actualX,actualXLegal) == /\ before.stage = "ProcedureCode1ff52d705816" /\ ~before.complete /\ before.object \in DOMAIN objects /\ actualTransaction.id \in Nat \ {0} /\ actualTransaction.procedureId = before.id /\ actualTransaction.object = before.object /\ actualTransaction.allPaid /\ actualX \in Nat /\ actualXLegal /\ actualTransaction.basePart = DeployInherentPart8(objects[before.object],before.face,objects,before.destination,actualX) /\ (actualTransaction.basePart.exists /\ ~actualTransaction.deployCostIgnored) => actualTransaction.paidSomething /\ actualTransaction.checkpointRequired = actualTransaction.paidSomething /\ after = [before EXCEPT !.stage = "CostBarrier",!.transaction = actualTransaction.id, !.checkpointRequired = actualTransaction.checkpointRequired, !.x = [exists |-> objects[before.object].deployX /\ DeployEffectiveKind8(objects[before.object],before.face) \in {"Equipment","Technique","Support"}, amount |-> IF objects[before.object].deployX /\ DeployEffectiveKind8(objects[before.object],before.face) \in {"Equipment","Technique","Support"} THEN actualX ELSE 0]] DrainDeployCostBarrier8(before,after,actualTransactionId,actualCostCheckpointId,actualNormalCostReactionsComplete) == /\ before.stage = "CostBarrier" /\ ~before.complete /\ before.transaction = actualTransactionId /\ actualNormalCostReactionsComplete /\ IF before.checkpointRequired THEN actualCostCheckpointId \in Nat \ {0} ELSE actualCostCheckpointId = 0 /\ after = [before EXCEPT !.stage = "ProcedureCode0f76bcc2eb00"] DeployAtDestination8(before,after,objects,afterObjects,targetSites,afterTargetSites,usedTargetSiteIds,activeAuxiliarySiteLimits, actualAllLocationAndCapacityRestrictionsSatisfied) == /\ before.stage = "ProcedureCode0f76bcc2eb00" /\ ~before.complete /\ before.object \in DOMAIN objects /\ ~objects[before.object].deployed /\ actualAllLocationAndCapacityRestrictionsSatisfied /\ IF before.newAuxiliarySite THEN NewAuxiliarySiteDeclaration4(targetSites,afterTargetSites,before.destination.targetSite,usedTargetSiteIds, before.destination,TRUE,activeAuxiliarySiteLimits) ELSE afterTargetSites = targetSites /\ (before.actor = "SideB" \/ before.destination.host # 0 \/ before.destination.targetSite \in DOMAIN targetSites) /\ afterObjects = [objects EXCEPT ![before.object] = [WithCardLocation8(objects[before.object],before.destination) EXCEPT !.deployed = TRUE, !.activated = objects[before.object].form="Card" /\ before.actor="SideA" /\ before.face="Up" /\ objects[before.object].kind \in {"Facility","Attachment","Barrier"}]] /\ after = [before EXCEPT !.stage = "ProcedureCode4585e6a51427"] OccupyDeployBarrierPosition8(before,after,layout,afterLayout,actualDeployAuthorized) == before.stage = "ProcedureCode0f76bcc2eb00" /\ after.stage = "ProcedureCode4585e6a51427" /\ before.id = after.id /\ OccupyDeclaredPosition6(layout,afterLayout,before.destination.position,before.id,before.object,"ProcedureCode0f76bcc2eb00",actualDeployAuthorized) DeployPendingProjection8(frames,currentOrPastObjects) == LET eligible == {i \in DOMAIN frames : ~frames[i].complete /\ frames[i].stage # "ProcedureCodec4ba55e330f8" /\ frames[i].destination.targetSite # "NoValue"} IN [object \in {frames[id].object : id \in eligible} |-> LET f == CHOOSE id \in eligible : frames[id].object = object IN [form |-> currentOrPastObjects[object].form,kind |-> currentOrPastObjects[object].kind, subtypes |-> currentOrPastObjects[object].subtypes,destination |-> frames[f].destination]] DeployBeginEvent8(f) == [tag |-> "Deployed",object |-> f.object,deployId |-> f.id,actor |-> f.actor,face |-> f.face] FinishDeploy8(before,after,objects,events) == /\ before.stage = "ProcedureCode4585e6a51427" /\ ~before.complete /\ before.object \in DOMAIN objects /\ objects[before.object].deployed /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.deployedOccurred = TRUE] /\ events = {DeployBeginEvent8(before)} DeployCardDefaultActive8(frame,o) == IF ~frame.complete /\ frame.stage # "ProcedureCode4585e6a51427" THEN FALSE ELSE o.form="Card" /\ o.face="Up" /\ o.deployed /\ (o.side="SideB" \/ o.activated) DeployAndActivationChoiceAllowed8(mode,actualDeployPossible,actualActivationPossible,declinesActivationAdditionalCost) == mode \in {"NoValue","Normal","IfAble"} /\ actualDeployPossible /\ (mode # "IfAble" \/ (actualActivationPossible /\ ~declinesActivationAdditionalCost)) StartDeployActivation8(before,after,request) == /\ before.complete /\ before.deployedOccurred /\ before.activationMode \in {"Normal","IfAble"} /\ ~before.activationStarted /\ after = [before EXCEPT !.activationStarted = TRUE] /\ request = [kind |-> "Activation",object |-> before.object,caller |-> <<"DeployAndActivation",before.id>>] FinishDeployActivation8(before,after,actualActivationFrame) == /\ before.complete /\ before.activationStarted /\ ~before.activationProcessed /\ actualActivationFrame.complete /\ actualActivationFrame.returned /\ actualActivationFrame.object = before.object /\ actualActivationFrame.caller = <<"DeployAndActivation",before.id>> /\ after = [before EXCEPT !.activationProcessed = TRUE,!.activationPerformed = actualActivationFrame.result = "ItemActivated"] DeployRevealRequired8(hasOtherRequirements,actuallyOtherwiseVerified,failedDeployAndActivation) == (hasOtherRequirements /\ ~actuallyOtherwiseVerified) \/ failedDeployAndActivation VerifyDeployedCard8(before,after,hasOtherRequirements,actuallyOtherwiseVerified,actualRevealReceipt) == /\ before.complete /\ ~before.verificationDone /\ (before.activationMode = "NoValue" \/ before.activationProcessed) /\ DeployRevealRequired8(hasOtherRequirements,actuallyOtherwiseVerified,before.activationMode # "NoValue" /\ ~before.activationPerformed) => actualRevealReceipt.performed /\ actualRevealReceipt.object = before.object /\ actualRevealReceipt.afterDeployment /\ after = [before EXCEPT !.verificationDone = TRUE] ReturnDeployToCaller8(before,after,actualWholeInstructionAndCheckpointReactionsComplete,caller) == /\ before.complete /\ before.verificationDone /\ ~before.returned /\ caller = before.caller /\ (before.activationMode = "NoValue" \/ before.activationProcessed) /\ actualWholeInstructionAndCheckpointReactionsComplete /\ after = [before EXCEPT !.returned = TRUE] NextDeployInBatch8(beforeIndex,afterIndex,previous,actualPreviousSeparateInstructionAndCheckpointComplete) == previous.returned /\ actualPreviousSeparateInstructionAndCheckpointComplete /\ beforeIndex \in Nat \ {0} /\ afterIndex = beforeIndex+1 UninstallationOccurred8(beforeCard,afterCard) == beforeCard.deployed /\ ~afterCard.deployed UninstalledEvent8(object) == [tag |-> "Uninstalled",object |-> object] FinishDeployWithoutDeployment8(before,after,actualFailureDispositionAndReservationsComplete) == /\ ~before.complete /\ actualFailureDispositionAndReservationsComplete /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.verificationDone = TRUE, !.activationProcessed = TRUE,!.activationPerformed = FALSE,!.deployedOccurred = FALSE] DeployPublicLayout8(kind) == [orientation |-> IF kind="Barrier" THEN "Horizontal" ELSE "Vertical", rootTypeShown |-> FALSE] PlayTypeAllowed8(o,actor) == o.form = "Card" /\ o.side = actor /\ ((actor = "SideA" /\ o.kind = "Plan") \/ (actor = "SideB" /\ o.kind = "Action")) OpenPlay8(id,object,actor,caller) == [id |-> id,object |-> object,actor |-> actor,caller |-> caller,stage |-> "ProcedureCodebfd1895de2c0", kind |-> "NoValue",subtypes |-> {},activationReached |-> FALSE,transaction |-> 0, checkpointRequired |-> FALSE,x |-> [exists |-> FALSE,amount |-> 0], complete |-> FALSE,returned |-> FALSE] PlayedPlacementRow8(o,renew) == [WithCardLocation8(o,[NoDeployDestination8 EXCEPT !.loc = "Played",!.area = "Played"]) EXCEPT !.deployed = FALSE,!.face = "Up",!.activated = FALSE,!.marks = IF renew THEN {} ELSE @] BeginPlay8(before,after,objects,afterObjects,newObject,usedIds,actualPlayAuthorized) == /\ before.stage = "ProcedureCodebfd1895de2c0" /\ ~before.complete /\ before.id \in Nat \ {0} /\ before.object \in DOMAIN objects /\ actualPlayAuthorized /\ PlayTypeAllowed8(objects[before.object],before.actor) /\ ~objects[before.object].deployed /\ LET renew == objects[before.object].zone # "Play" IN /\ IF renew THEN newObject \in Nat \ {0} /\ newObject \notin usedIds \cup DOMAIN objects ELSE newObject = before.object /\ afterObjects = [id \in (DOMAIN objects \ {before.object}) \cup {newObject} |-> IF id = newObject THEN PlayedPlacementRow8(objects[before.object],renew) ELSE objects[id]] /\ after = [before EXCEPT !.object = newObject,!.stage = "ProcedureCode0f076861472c", !.kind = objects[before.object].kind,!.subtypes = objects[before.object].subtypes] PlayEffectiveCardActivity8(frame,object,o,ordinaryCardActivity) == IF object = frame.object /\ ~frame.returned THEN PlayedCardActive(o,frame.activationReached) ELSE ordinaryCardActivity PlayInherentPart8(o,x) == InherentPlayCost([o EXCEPT !.playCost = IF o.playX THEN x ELSE @]) PayPlayStep8(before,after,objects,actualTransaction,actualIgnorePlayCostAuthorized,actualX,actualXLegal) == /\ before.stage = "ProcedureCode0f076861472c" /\ ~before.complete /\ before.object \in DOMAIN objects /\ actualTransaction.id \in Nat \ {0} /\ actualTransaction.procedureId = before.id /\ actualTransaction.object = before.object /\ actualTransaction.allPaid /\ actualX \in Nat /\ actualXLegal /\ actualTransaction.basePart = PlayInherentPart8(objects[before.object],actualX) /\ actualTransaction.playCostIgnored => actualIgnorePlayCostAuthorized /\ ~actualTransaction.playCostIgnored => actualTransaction.paidSomething /\ actualTransaction.checkpointRequired = actualTransaction.paidSomething /\ after = [before EXCEPT !.stage = "CostBarrier",!.transaction = actualTransaction.id, !.checkpointRequired = actualTransaction.checkpointRequired, !.x = [exists |-> objects[before.object].playX,amount |-> IF objects[before.object].playX THEN actualX ELSE 0]] DrainPlayCostBarrier8(before,after,actualTransactionId,actualCostCheckpointId,actualNormalCostReactionsComplete) == /\ before.stage = "CostBarrier" /\ ~before.complete /\ before.transaction = actualTransactionId /\ actualNormalCostReactionsComplete /\ IF before.checkpointRequired THEN actualCostCheckpointId \in Nat \ {0} ELSE actualCostCheckpointId = 0 /\ after = [before EXCEPT !.stage = "ProcedureCodecbf6b11f0ae0"] ActivatePlayedCard8(before,after) == /\ before.stage = "ProcedureCodecbf6b11f0ae0" /\ ~before.complete /\ after = [before EXCEPT !.stage = "ProcedureCode7647b901fcb1",!.activationReached = TRUE] PlayedCondition8(f) == [tag |-> "Played",object |-> f.object,kind |-> f.kind,subtypes |-> f.subtypes,actor |-> f.actor,playId |-> f.id] MeetPlayedConditions8(before,after,events) == /\ before.stage = "ProcedureCode7647b901fcb1" /\ before.activationReached /\ ~before.complete /\ after = [before EXCEPT !.stage = "ProcedureCodebddd9a1a600b"] /\ events = {PlayedCondition8(before)} OpenPlayAbilities8(before,after,actualCheckpointId,actualCheckpointAndReactionsComplete) == /\ before.stage = "ProcedureCodebddd9a1a600b" /\ ~before.complete /\ actualCheckpointId \in Nat \ {0} /\ actualCheckpointAndReactionsComplete /\ after = [before EXCEPT !.stage = "ProcedureCode3d7f756d78f7"] PlayAbilitiesCompletion8(f,receipt) == /\ receipt.playId = f.id /\ receipt.object = f.object /\ receipt.allPlayAbilitiesResolved /\ receipt.ownedTimingIds \subseteq receipt.returnedTimingIds /\ receipt.ownEndTriggersResolved FinishPlayAbilities8(before,after,actualCompletionReceipt) == /\ before.stage = "ProcedureCode3d7f756d78f7" /\ ~before.complete /\ PlayAbilitiesCompletion8(before,actualCompletionReceipt) /\ after = [before EXCEPT !.stage = "ProcedureCodee977e478b45b"] PlayCleanupDisposition8(f,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval) == IF f.object \notin DOMAIN objects THEN "LeftPlay" ELSE IF objects[f.object].zone # "Play" THEN "LeftPlay" ELSE IF objects[f.object].form = "Counter" \/ objects[f.object].host # 0 THEN "ConvertedOrHosted" ELSE IF actualSelfRetentionText THEN "RetainSelf" ELSE IF actualNestedAfterResolveRemoval THEN "NestedRemoval" ELSE "Retire" CreatePlayRetention8(beforeEffects,afterEffects,frame,actualReceipt) == /\ actualReceipt.id \in Nat \ {0} /\ actualReceipt.id \notin DOMAIN beforeEffects /\ actualReceipt.playId = frame.id /\ actualReceipt.source = frame.object /\ actualReceipt.created /\ actualReceipt.expiryEffect # "NoValue" /\ afterEffects = [id \in DOMAIN beforeEffects \cup {actualReceipt.id} |-> IF id = actualReceipt.id THEN actualReceipt ELSE beforeEffects[id]] FinishPlayCleanup8(before,after,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval, actualCleanupReceipt,effects,afterEffects,actualRetentionReceipt) == /\ before.stage = "ProcedureCodee977e478b45b" /\ ~before.complete /\ actualCleanupReceipt.playId = before.id /\ actualCleanupReceipt.object = before.object /\ LET disposition == PlayCleanupDisposition8(before,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval) IN /\ actualCleanupReceipt.disposition = disposition /\ IF disposition = "Retire" THEN /\ PlayedResolutionRetireDue(objects[before.object],TRUE,FALSE,FALSE) /\ actualCleanupReceipt.trashInstructionComplete ELSE TRUE /\ IF disposition = "RetainSelf" THEN CreatePlayRetention8(effects,afterEffects,before,actualRetentionReceipt) ELSE afterEffects = effects /\ after = [before EXCEPT !.stage = "ProcedureCodec610fc738935"] MeetPlayResolvedConditions8(before,after,events) == /\ before.stage = "ProcedureCodec610fc738935" /\ ~before.complete /\ after = [before EXCEPT !.stage = "ProcedureCode03de9212dc90"] /\ events = {[tag |-> "PlayResolved",object |-> before.object,kind |-> before.kind,actor |-> before.actor,playId |-> before.id]} CompletePlay8(before,after) == /\ before.stage = "ProcedureCode03de9212dc90" /\ ~before.complete /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] ReturnPlayToCaller8(before,after,actualSeparateInstructionAndEndingReactionsComplete,caller) == /\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualSeparateInstructionAndEndingReactionsComplete /\ after = [before EXCEPT !.returned = TRUE] NextPlayInBatch8(index,nextIndex,previous,actualPreviousSeparateInstructionComplete) == /\ index \in Nat \ {0} /\ previous.returned /\ actualPreviousSeparateInstructionComplete /\ nextIndex = index+1 OpenSearch8(id,actor,zone,amount,hasCriteria,followup,ability,caller) == [id |-> id,actor |-> actor,zone |-> zone,amount |-> amount,hasCriteria |-> hasCriteria, followup |-> followup,ability |-> ability,caller |-> caller,stage |-> "Searching", foundCount |-> 0,complete |-> FALSE,shuffled |-> FALSE,conditionsMarked |-> FALSE,returned |-> FALSE] SearchZoneIds8(objects,zone) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].zone = zone} SearchDeck8(f) == f.zone \in {"SideADeck","SideBDeck"} SearchLookGrant8(f,viewer,object,objects) == f.stage = "Searching" /\ ~f.complete /\ viewer = f.actor /\ object \in SearchZoneIds8(objects,f.zone) SearchLegalFindSelections8(f,objects,actualCriteriaMatches,actualFeasibleSelections) == {selection \in SUBSET SearchZoneIds8(objects,f.zone) : selection \subseteq actualCriteriaMatches /\ Cardinality(selection) <= f.amount /\ (f.followup = "NoValue" \/ selection = {} \/ selection \in actualFeasibleSelections)} SearchMaximumFeasibleCount8(selections) == CHOOSE count \in {Cardinality(selection) : selection \in selections} : \A selection \in selections : Cardinality(selection) <= count SearchChoiceAllowed8(f,objects,chosen,actualCriteriaMatches,actualFeasibleSelections,actualAllowedCounts) == LET available == SearchZoneIds8(objects,f.zone) legal == SearchLegalFindSelections8(f,objects,actualCriteriaMatches,actualFeasibleSelections) IN /\ f.amount \in Nat /\ f.followup \in {"NoValue","Deploy","Play"} /\ (~f.hasCriteria => available \subseteq actualCriteriaMatches) /\ chosen \in legal /\ IF ~f.hasCriteria THEN Cardinality(chosen) = SearchMaximumFeasibleCount8(legal) ELSE (Cardinality(chosen) \in actualAllowedCounts \/ (SearchDeck8(f) /\ chosen = {})) SearchFoundRows8(beforeObjects,afterObjects,chosen,successors,usedIds) == /\ chosen \subseteq DOMAIN beforeObjects /\ DOMAIN beforeObjects \subseteq usedIds /\ FreshSuccessors8(chosen,successors,usedIds) /\ chosen \cap DOMAIN afterObjects = {} /\ {successors[id] : id \in chosen} \subseteq DOMAIN afterObjects /\ \A id \in chosen : LET o == afterObjects[successors[id]] IN /\ o.form = "Card" /\ o.card = beforeObjects[id].card /\ o.side = beforeObjects[id].side /\ o.zone = "SetAside" /\ o.face = "Down" /\ ~o.deployed /\ ~o.activated /\ o.host = 0 /\ o.marks = {} FinishSearchChoice8(before,after,objects,afterObjects,chosen,successors,usedIds, actualCriteriaMatches,actualFeasibleSelections,actualAllowedCounts, actualFindMovementReceipt,deck,afterDeck,transits,afterTransits) == /\ before.stage = "Searching" /\ ~before.complete /\ before.id \in Nat \ {0} /\ before.actor \in SetupPlayers /\ SearchChoiceAllowed8(before,objects,chosen,actualCriteriaMatches,actualFeasibleSelections,actualAllowedCounts) /\ actualFindMovementReceipt.searchId = before.id /\ actualFindMovementReceipt.ability = before.ability /\ actualFindMovementReceipt.sources = chosen /\ actualFindMovementReceipt.successors = successors /\ actualFindMovementReceipt.complete /\ SearchFoundRows8(objects,afterObjects,chosen,successors,usedIds) /\ IF SearchDeck8(before) THEN /\ DeckObjectOrder8(objects,IF before.zone = "SideADeck" THEN "SideA" ELSE "SideB",deck) /\ afterDeck = SelectSeq(deck,LAMBDA id : id \notin chosen) ELSE afterDeck = deck /\ RegisterAsideBatch8(transits,afterTransits,objects,chosen,successors,before.id,before.ability) /\ after = [before EXCEPT !.complete = TRUE,!.foundCount = Cardinality(chosen), !.stage = IF SearchDeck8(before) THEN "Shuffle" ELSE "Conditions"] SearchShuffle8(before,after,objects,afterObjects,deck,afterDeck,oldOrder,successors,usedIds, actualShuffleReceipt,transits,afterTransits) == /\ before.stage = "Shuffle" /\ before.complete /\ SearchDeck8(before) /\ ~before.shuffled /\ actualShuffleReceipt.searchId = before.id /\ actualShuffleReceipt.zone = before.zone /\ actualShuffleReceipt.performed /\ LET owner == IF before.zone = "SideADeck" THEN "SideA" ELSE "SideB" sources == SubIds6(deck) IN /\ DeckObjectOrder8(objects,owner,deck) /\ Len(oldOrder) = Len(deck) /\ SubIds6(oldOrder) = sources /\ CardBatchTransfer8(objects,afterObjects,sources,successors,usedIds,before.zone,"Down", [id \in sources |-> <>]) /\ afterDeck = [i \in 1..Len(oldOrder) |-> successors[oldOrder[i]]] /\ DeckObjectOrder8(afterObjects,owner,afterDeck) /\ DeckSearchCompletion4([i \in 1..Len(deck) |-> objects[deck[i]].card], [i \in 1..Len(afterDeck) |-> afterObjects[afterDeck[i]].card],actualShuffleReceipt.performed) /\ afterTransits = transits /\ after = [before EXCEPT !.stage = "Conditions",!.shuffled = TRUE] MarkSearchConditions8(before,after,actualPendingReceipt,events) == /\ before.stage = "Conditions" /\ before.complete /\ ~before.conditionsMarked /\ (SearchDeck8(before) => before.shuffled) /\ actualPendingReceipt.searchId = before.id /\ actualPendingReceipt.allRequiredMarked /\ after = [before EXCEPT !.stage = "Resume",!.conditionsMarked = TRUE] /\ events = {[tag |-> "Searched",searchId |-> before.id,actor |-> before.actor,zone |-> before.zone,foundCount |-> before.foundCount]} ResumeSearchAbility8(before,after,caller) == /\ before.stage = "Resume" /\ before.complete /\ before.conditionsMarked /\ ~before.returned /\ (SearchDeck8(before) => before.shuffled) /\ caller = before.caller /\ after = [before EXCEPT !.stage = "Resumed",!.returned = TRUE] SearchFoundActionAllowed8(f) == f.returned /\ f.stage = "Resumed" /\ f.conditionsMarked /\ (SearchDeck8(f) => f.shuffled) SearchRevealRequired8(f,actualAbilityInstructsReveal) == SearchFoundActionAllowed8(f) /\ actualAbilityInstructsReveal SearchRevealFound8(f,objects,transits,object,actualAbilityInstructsReveal,actualRevealReceipt) == /\ SearchRevealRequired8(f,actualAbilityInstructsReveal) /\ object \in AsideGroupIds8(objects,transits,f.id) /\ actualRevealReceipt.performed /\ actualRevealReceipt.object = object /\ actualRevealReceipt.searchId = f.id SearchChainReactionsAllowed8(f) == f.complete /\ f.conditionsMarked /\ (SearchDeck8(f) => f.shuffled) SearchRemainingEffectsContinue8(f) == SearchFoundActionAllowed8(f) SwapLegal8(objects,a,b,actualDestinationChecks) == /\ a # b /\ {a,b} \subseteq DOMAIN objects /\ objects[a].form = "Card" /\ objects[b].form = "Card" /\ DOMAIN actualDestinationChecks = {a,b} /\ \A id \in {a,b} : LET other == IF id = a THEN b ELSE a IN /\ actualDestinationChecks[id].destination = CardLocation8(objects[other]) /\ actualDestinationChecks[id].gameRulesHold /\ actualDestinationChecks[id].cardAbilitiesHold SwapNoLegalExchange8(actualLegalPairs,objects,afterObjects,events) == actualLegalPairs = {} /\ afterObjects = objects /\ events = {} SwapDeployedCards8(objects,afterObjects,a,b,actualDestinationChecks,occurrenceId,usedOccurrenceIds,events) == /\ SwapLegal8(objects,a,b,actualDestinationChecks) /\ objects[a].deployed /\ objects[b].deployed /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin usedOccurrenceIds /\ afterObjects = ExchangeDeployedLocations8(objects,a,b) /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})} RECURSIVE HostDescendantsStep8(_,_,_) HostDescendantsStep8(objects,frontier,visited) == IF frontier = {} THEN visited ELSE LET next == ({id \in DOMAIN objects : objects[id].host \in frontier} \ visited) \ frontier IN HostDescendantsStep8(objects,next,visited \cup frontier) HostDescendants8(objects,root) == HostDescendantsStep8(objects,{id \in DOMAIN objects : objects[id].host = root},{}) ObjectiveAreaObjectSwap8(objects,a,b) == /\ {a,b} \subseteq DOMAIN objects /\ a # b /\ objects[a].kind = "Objective" /\ objects[b].kind = "Objective" /\ objects[a].zone \in SetupObjectiveZones /\ objects[b].zone \in SetupObjectiveZones /\ objects[a].zone # objects[b].zone SwapHostedRetireDue8(objects,a,b) == IF objects[a].zone = objects[b].zone \/ ObjectiveAreaObjectSwap8(objects,a,b) THEN {} ELSE HostDescendants8(objects,a) \cup HostDescendants8(objects,b) SwapRenewalRequired8(source,destination,actualDestinationHidden) == source.zone # destination.zone \/ actualDestinationHidden SwapTargetPost8(source,destination,result,renew,actualArrival) == /\ actualArrival.complete /\ actualArrival.row = result /\ actualArrival.destination = CardLocation8(destination) /\ result.form = "Card" /\ result.card = source.card /\ result.side = source.side /\ CardLocation8(result) = CardLocation8(destination) /\ result.deployed = destination.deployed /\ ActivationCacheValid8(result) /\ result.marks = IF renew THEN {} ELSE source.marks /\ IF source.zone # destination.zone THEN /\ IF actualArrival.faceExceptionAuthorized THEN TRUE ELSE CASE destination.zone = "SideADiscard" -> result.face = IF actualArrival.sideBCouldSee THEN "Up" ELSE "Down" [] destination.zone = "SideBDiscard" -> result.face = "Up" [] ZoneType4(destination.zone) \in {"Deck","Hand"} -> result.face = "Down" [] destination.zone \in SetupObjectiveZones -> result.face = "Up" [] destination.zone = "Play" -> result.face = IF source.side = "SideA" THEN "Down" ELSE "Up" [] destination.zone = "SetAside" -> result.face = destination.face [] OTHER -> TRUE ELSE TRUE SwapOtherCards8(objects,afterObjects,a,b,successors,usedIds,actualDestinationChecks,actualArrivals, actualMovementReceipt,pendingRetire,afterPendingRetire,occurrenceId,usedOccurrenceIds,events) == /\ SwapLegal8(objects,a,b,actualDestinationChecks) /\ ~(objects[a].deployed /\ objects[b].deployed) /\ ~ObjectiveAreaObjectSwap8(objects,a,b) /\ DOMAIN successors = {a,b} /\ DOMAIN actualArrivals = {a,b} /\ Cardinality({successors[a],successors[b]}) = 2 /\ DOMAIN objects \subseteq usedIds /\ actualMovementReceipt.complete /\ actualMovementReceipt.sources = {a,b} /\ actualMovementReceipt.successors = successors /\ ~actualMovementReceipt.deployProcedurePerformed /\ ~actualMovementReceipt.deployCostPaid /\ ~actualMovementReceipt.likeCardsRetireed /\ \A id \in {a,b} : LET other == IF id = a THEN b ELSE a renew == SwapRenewalRequired8(objects[id],objects[other],actualArrivals[id].destinationHidden) IN /\ actualArrivals[id].source = id /\ IF renew THEN successors[id] \in (Nat \ {0}) \ usedIds ELSE successors[id] = id /\ successors[id] \in DOMAIN afterObjects /\ SwapTargetPost8(objects[id],objects[other],afterObjects[successors[id]],renew,actualArrivals[id]) /\ DOMAIN afterObjects = (DOMAIN objects \ {a,b}) \cup {successors[a],successors[b]} /\ \A id \in DOMAIN objects \ {a,b} : afterObjects[id] = objects[id] /\ afterPendingRetire = pendingRetire \cup SwapHostedRetireDue8(objects,a,b) /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin usedOccurrenceIds /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})} SwapObjectiveFamilies8(objects,afterObjects,a,b,successors,usedIds,actualDestinationChecks, occurrenceId,usedOccurrenceIds,events) == /\ SwapLegal8(objects,a,b,actualDestinationChecks) /\ ObjectiveAreaObjectSwap8(objects,a,b) /\ LET familyA == {a} \cup HostDescendants8(objects,a) familyB == {b} \cup HostDescendants8(objects,b) all == familyA \cup familyB IN /\ familyA \cap familyB = {} /\ DOMAIN objects \subseteq usedIds /\ FreshSuccessors8(all,successors,usedIds) /\ DOMAIN afterObjects = (DOMAIN objects \ all) \cup {successors[id] : id \in all} /\ \A id \in DOMAIN objects \ all : afterObjects[id] = objects[id] /\ \A id \in all : LET root == IF id \in familyA THEN a ELSE b other == IF root = a THEN b ELSE a row == objects[id] location == IF id = root THEN CardLocation8(objects[other]) ELSE [CardLocation8(row) EXCEPT !.zone = objects[other].zone, !.host = successors[row.host],!.loc = <<"Host",successors[row.host]>>] IN afterObjects[successors[id]] = [WithCardLocation8(row,location) EXCEPT !.marks = {},!.deployed = FALSE,!.activated = FALSE] /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin usedOccurrenceIds /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})} SwapAsideTransit8(incoming,outgoing,successor,objects,transits) == LET ownOrigin == objects[incoming].zone = "SetAside" /\ incoming \in DOMAIN transits target == transits[outgoing] IN [key \in DOMAIN target |-> CASE key = "object" -> successor [] key = "originZone" -> IF ownOrigin THEN transits[incoming].originZone ELSE objects[incoming].zone [] key = "originLocation" -> IF ownOrigin THEN transits[incoming].originLocation ELSE objects[incoming].loc [] OTHER -> target[key]] TransferSwapAsideGroups8(objects,afterObjects,transits,afterTransits,a,b,successors) == /\ DOMAIN successors = {a,b} /\ SetAsideTrackingValid4(objects,transits) /\ {successors[a],successors[b]} \subseteq DOMAIN afterObjects /\ LET entering == {id \in {a,b} : afterObjects[successors[id]].zone = "SetAside"} IN /\ \A id \in entering : (IF id = a THEN b ELSE a) \in DOMAIN transits /\ afterTransits = [id \in (DOMAIN transits \ {a,b}) \cup {successors[s] : s \in entering} |-> IF id \in {successors[s] : s \in entering} THEN LET incoming == CHOOSE s \in entering : successors[s] = id outgoing == IF incoming = a THEN b ELSE a IN SwapAsideTransit8(incoming,outgoing,id,objects,transits) ELSE transits[id]] /\ SetAsideTrackingValid4(afterObjects,afterTransits) OpenSwapCheckpoint8(swapId,objects,afterObjects,a,b,successors,checkpointSerial) == [swapId |-> swapId,createdSerial |-> checkpointSerial,met |-> FALSE, uninstalled |-> {id \in {a,b} : objects[id].deployed /\ ~afterObjects[successors[id]].deployed}, deployed |-> {successors[id] : id \in {i \in {a,b} : ~objects[i].deployed /\ afterObjects[successors[i]].deployed}}] MeetSwapDeployConditions8(before,after,actualCheckpointSerial,actualNormalConditionsProcessing,events) == /\ ~before.met /\ actualCheckpointSerial = before.createdSerial+1 /\ actualNormalConditionsProcessing /\ after = [before EXCEPT !.met = TRUE] /\ events = {[tag |-> "Uninstalled",object |-> id,swapId |-> before.swapId] : id \in before.uninstalled} \cup {[tag |-> "Deployed",object |-> id,swapId |-> before.swapId] : id \in before.deployed} ComposeArrangementSwap8(before,after,objects,afterObjects,a,b,occurrenceId,usedOccurrenceIds, actualDestinationChecks,checkpointSerial,afterCheckpointSerial,pending,afterPending,events) == /\ SwapDeployedCards8(objects,afterObjects,a,b,actualDestinationChecks,occurrenceId,usedOccurrenceIds,events) /\ SwapArrangingBarrier8(before,after,objects,afterObjects,a,b,occurrenceId,TRUE, checkpointSerial,afterCheckpointSerial,pending,afterPending,events) ComposeSwapBarrierPosition8(layout,afterLayout,position,incoming,otherPosition,actualSwapCompleted) == SwapIntoPosition6(layout,afterLayout,position,incoming,otherPosition,actualSwapCompleted) SwapDeployedBarrierTraversalPlan8(traversal,newPosition,newTargetSite) == BarrierChangeTraversalPlan6(traversal,"Swap",newPosition,newTargetSite) SwapBarrierTraversalPlan8(traversal,afterObjects,actualCurrentBarrierSuccessor) == LET barrierCard == afterObjects[actualCurrentBarrierSuccessor] IN BarrierChangeTraversalPlan6(traversal,IF traversal.phase = "Encounter" /\ ~barrierCard.deployed THEN "Uninstall" ELSE "Swap",barrierCard.position,barrierCard.targetSite) =============================================================================