----------------------------- MODULE LocationContracts ----------------------------- EXTENDS TypeContracts ZoneTypes4 == {"Deck","Hand","Discard","ObjectiveCompletion","Play","Bank","SetAside","Removed"} PrivateZoneInstances4 == {"SideADeck","SideBDeck","SideAHand","SideBHand", "SideADiscard","SideBDiscard","SideAObjectiveCompletion","SideBObjectiveCompletion"} SharedZoneInstances4 == {"Play","Bank","SetAside","Removed"} ZoneInstances4 == PrivateZoneInstances4 \cup SharedZoneInstances4 CounterPlayAliases4 == {"SideAResourceUnits","SideBResourceUnits","SideAExposureMarkers","SideBExposureMarkers", "SideALiabilityMarker","SideBLiabilityMarker","SideAPersistentCapacityLoss","SideBPersistentCapacityLoss"} CanonicalZone4(runtimeZone) == IF runtimeZone \in CounterPlayAliases4 THEN "Play" ELSE runtimeZone ZoneType4(zone) == CASE zone \in {"SideADeck","SideBDeck"} -> "Deck" [] zone \in {"SideAHand","SideBHand"} -> "Hand" [] zone \in {"SideADiscard","SideBDiscard"} -> "Discard" [] zone \in {"SideAObjectiveCompletion","SideBObjectiveCompletion"} -> "ObjectiveCompletion" [] OTHER -> zone ZoneClass4(zone) == CASE ZoneType4(zone) = "Deck" -> "Hidden" [] ZoneType4(zone) = "Hand" -> "Secret" [] zone \in ZoneInstances4 -> "SchemaAtom128" [] OTHER -> "Outside" ZonePartition4(inGameIds, occupants) == /\ DOMAIN occupants = ZoneInstances4 /\ UNION {occupants[z] : z \in ZoneInstances4} = inGameIds /\ \A a,b \in ZoneInstances4 : a # b => occupants[a] \intersect occupants[b] = {} MoveRevealRequired4(sourceZone, facedown, requiresAttribute, deploying, deployRevealRequired) == IF deploying THEN deployRevealRequired ELSE requiresAttribute /\ (facedown \/ ZoneClass4(sourceZone) = "Hidden") AtomicZoneMove4(inGameIds, before, after, id, source, destination, movementAuthorized, revealRequired, revealedBeforeMove) == /\ source \in ZoneInstances4 /\ destination \in ZoneInstances4 /\ source # destination /\ ZonePartition4(inGameIds,before) /\ id \in before[source] /\ movementAuthorized /\ (revealRequired => revealedBeforeMove) /\ after = [z \in ZoneInstances4 |-> IF z = source THEN before[z] \ {id} ELSE IF z = destination THEN before[z] \cup {id} ELSE before[z]] /\ ZonePartition4(inGameIds,after) OutsideCardCanAffect4(zone) == zone # "Outside" OutsideCardCanBeAffected4(zone, explicitlyBringsExtraCardIn) == zone # "Outside" \/ explicitlyBringsExtraCardIn DefaultZoneLook4(zone, face, viewer, controller) == CASE ZoneClass4(zone) = "Hidden" -> FALSE [] ZoneClass4(zone) = "Secret" -> viewer = controller [] ZoneClass4(zone) = "SchemaAtom128" -> face = "Up" \/ viewer = controller [] OTHER -> FALSE ObjectLocation4(o, deckPosition, actualPlayLocation) == IF o.host # 0 THEN [kind |-> "Host",object |-> o.host] ELSE IF ZoneType4(o.zone) = "Deck" THEN [kind |-> "DeckPosition",zone |-> o.zone,position |-> deckPosition] ELSE IF o.zone = "Play" THEN actualPlayLocation ELSE [kind |-> "Zone",zone |-> o.zone] DeckSequenceValid4(deck) == Cardinality(SetupRange(deck)) = Len(deck) DeckStartHandoff4(completedSetup, drawDecks) == /\ completedSetup.gameStarted /\ completedSetup.stage = "Done" /\ DOMAIN drawDecks = SetupPlayers /\ drawDecks = completedSetup.deck /\ \A p \in SetupPlayers : DeckSequenceValid4(drawDecks[p]) DeckPhysicalFace4 == "Down" DeckMayLook4(viewer, explicitlyDirected) == viewer \in SetupPlayers /\ explicitlyDirected DeckReorder4(before, after, explicitlyDirected, searchingThisDeck) == /\ DeckSequenceValid4(before) /\ DeckSequenceValid4(after) /\ SetupRange(before) = SetupRange(after) /\ (after = before \/ explicitlyDirected \/ searchingThisDeck) DeckSearchCompletion4(remainingCards, after, shuffleExecuted) == /\ DeckSequenceValid4(remainingCards) /\ DeckSequenceValid4(after) /\ SetupRange(after) = SetupRange(remainingCards) /\ shuffleExecuted DeckCount4(deck) == Len(deck) DeckCardInactive4(o, gameStarted, cardData) == ZoneType4(o.zone) = "Deck" => ~DefaultActive(o,gameStarted,cardData) DeckName4(player) == IF player = "SideA" THEN "SchemaAtom129" ELSE "DrawPile" DeckCentralTargetSite4(player) == IF player = "SideA" THEN "SchemaAtom129" ELSE "NoValue" RequiredEmptyDeckWinner4(player, deck, drawRequired, validDrawProcedure) == IF player = "SideA" /\ deck = <<>> /\ drawRequired /\ validDrawProcedure THEN "SideB" ELSE "NoValue" UnorderedArrangement4(before, after) == DeckSequenceValid4(before) /\ DeckSequenceValid4(after) /\ SetupRange(before) = SetupRange(after) HandSetupProjection4(setupHands) == [p \in SetupPlayers |-> SetupRange(setupHands[p])] HandArrival4(before, after, incoming, movementAuthorized) == /\ movementAuthorized /\ before \intersect incoming = {} /\ after = before \cup incoming HandVisibleCards4(hand, viewer, controller, explicitlyVisibleIds) == IF viewer = controller THEN hand ELSE hand \intersect explicitlyVisibleIds HandCount4(hand) == Cardinality(hand) HandCardInactive4(o, gameStarted, cardData) == ZoneType4(o.zone) = "Hand" => ~DefaultActive(o,gameStarted,cardData) StandardMaximumHandSize4 == 5 HandHeldCountAllowed4(count) == count \in Nat HandWithinMaximum4(hand, effectiveMaximum) == Cardinality(hand) <= effectiveMaximum HandDiscardDemand4(hand, effectiveMaximum, discardStepDue) == IF discardStepDue THEN MaxOf(0,Cardinality(hand)-effectiveMaximum) ELSE 0 SideBHandHarmElimination4(player, effectiveMaximum, beginningOfActualDiscardStep) == player = "SideB" /\ beginningOfActualDiscardStep /\ effectiveMaximum < 0 HandDiscardResult4(before, after, discarded, effectiveMaximum, actualDiscardStep, harmEliminationCheckPassed) == /\ actualDiscardStep /\ harmEliminationCheckPassed /\ discarded \subseteq before /\ Cardinality(discarded) = HandDiscardDemand4(before,effectiveMaximum,TRUE) /\ after = before \ discarded HandName4(player) == IF player = "SideA" THEN "SchemaAtom082" ELSE "BHand" HandCentralTargetSite4(player) == IF player = "SideA" THEN "SchemaAtom082" ELSE "NoValue" CentralASpecimen0139Layout4 == [NeutralValue00012 |-> "SideAProfile",markerZone |-> "Play",markerInsideCentralA |-> FALSE, protectingBarrier |-> "InFront",rootUpgrades |-> "Behind"] DiscardPilesInitiallyEmpty4(zoneCards) == zoneCards["SideADiscard"] = {} /\ zoneCards["SideBDiscard"] = {} DiscardDestination4(owner) == owner \o "Discard" DiscardArrivalFace4(owner, sourceZone, movementKind, visibleToSideB) == IF owner = "SideB" THEN "Up" ELSE IF sourceZone = "SideAHand" /\ movementKind = "Discard" THEN "Down" ELSE IF visibleToSideB THEN "Up" ELSE "Down" DiscardArrivalPost4(o, owner, sourceZone, movementKind, visibleToSideB) == /\ movementKind \in {"Retire","Discard"} /\ o.form = "Card" /\ o.zone = DiscardDestination4(owner) /\ ~o.deployed /\ o.face = DiscardArrivalFace4(owner,sourceZone,movementKind,visibleToSideB) DiscardCount4(cards) == Cardinality(cards) DiscardCardInactive4(o, gameStarted, cardData) == ZoneType4(o.zone) = "Discard" => ~DefaultActive(o,gameStarted,cardData) DiscardName4(player) == IF player = "SideA" THEN "SchemaAtom018" ELSE "BDiscardPile" DiscardCentralTargetSite4(player) == IF player = "SideA" THEN "SchemaAtom018" ELSE "NoValue" DiscardSiteFaceValid4(face) == face \in {"Up","Down"} DiscardSiteFacedownOrientation4(face) == IF face = "Down" THEN "Horizontal" ELSE "Unspecified" DiscardSiteVisibleCards4(cards, faces, viewer, explicitlyVisibleIds) == {id \in cards : faces[id] = "Up" \/ viewer = "SideA" \/ id \in explicitlyVisibleIds} BDiscardPileVisibleCards4(cards) == cards BDiscardPileFaceValid4(face) == face = "Up" ObjectiveAreasInitiallyEmpty4(zoneCards) == zoneCards["SideAObjectiveCompletion"] = {} /\ zoneCards["SideBObjectiveCompletion"] = {} ObjectiveAreaZone4(player) == player \o "ObjectiveCompletion" NormalObjectiveCompletionClaimObjectivePost4(o, player, movementKind, objectiveCompletionClaimObjectiveAuthorized) == /\ player \in SetupPlayers /\ objectiveCompletionClaimObjectiveAuthorized /\ movementKind = IF player = "SideA" THEN "Scored" ELSE "ClaimedObjective" /\ o.form = "Card" /\ o.kind = "Objective" /\ ~o.deployed /\ o.zone = ObjectiveAreaZone4(player) /\ o.face = "Up" ObjectiveAreaObjectiveIds4(objects, player) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].kind = "Objective" /\ objects[id].zone = ObjectiveAreaZone4(player)} ObjectiveAreaOpenObjectives4(objects, player) == ObjectiveAreaObjectiveIds4(objects,player) ObjectiveAreaCount4(objects, player) == Cardinality(ObjectiveAreaObjectiveIds4(objects,player)) ObjectiveAreaObjectActive4(o, gameStarted, cardData, sideBObjectiveAreaCardTextActive) == /\ gameStarted /\ o.form = "Card" /\ o.kind = "Objective" /\ o.zone \in {"SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ (DefaultActive(o,gameStarted,cardData) \/ (o.zone = "SideBObjectiveCompletion" /\ sideBObjectiveAreaCardTextActive)) ObjectiveAreaPoints4(objects, player, effectivePoints) == SumMap([id \in ObjectiveAreaObjectiveIds4(objects,player) |-> ObjectivePointsInObjectiveArea(objects[id],ObjectiveAreaZone4(player),effectivePoints[id])]) PlayCardIds4(objects) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].zone = "Play"} StartingPlayCards4(objects, profileIds, actualAuthorizedSetupCards) == PlayCardIds4(objects) = profileIds \cup actualAuthorizedSetupCards PlayCardCount4(objects) == Cardinality(PlayCardIds4(objects)) PlayCardVisible4(o, viewer, controller, currentLookGrant) == /\ o.form = "Card" /\ o.zone = "Play" /\ (o.face = "Up" \/ viewer = controller \/ currentLookGrant) PlayCardDefaultActive4(o, gameStarted, cardData, playActivationReached) == /\ o.zone = "Play" /\ o.form = "Card" /\ gameStarted /\ ~(o.host # 0 /\ ~o.deployed) /\ IF o.kind \in {"Plan","Action"} THEN PlayedCardActive(o,playActivationReached) ELSE DefaultActive(o,gameStarted,cardData) PlayLocation4(o, barrierPosition) == IF o.host # 0 THEN [kind |-> "Host",object |-> o.host] ELSE IF o.form = "Card" /\ o.area = "Protecting" THEN [kind |-> "Protecting",targetSite |-> o.targetSite,position |-> barrierPosition] ELSE IF o.form = "Card" /\ o.area = "Root" THEN [kind |-> "Root",targetSite |-> o.targetSite] ELSE IF o.form = "Counter" /\ o.kind = "ResourceUnit" THEN [kind |-> "ResourceUnitLocation",location |-> o.resourceUnitLocation] ELSE [kind |-> "Zone",zone |-> "Play"] PlayResourceUnitLocationValid4(o) == o.form = "Counter" /\ o.kind = "ResourceUnit" /\ o.zone = "Play" => (o.host # 0 \/ o.resourceUnitLocation \in {"SideAPool","SideBPool","LiabilityMarkerFund"}) NonfunctionalOrHostedCounter4(o, isNonfunctionalAid) == o.form = "Counter" /\ o.zone = "Play" /\ o.kind \notin {"ResourceUnit","ExposureMarker","LiabilityMarker"} => (o.host # 0 \/ isNonfunctionalAid) HostPlayRelationship4(hostId, host, child, deployedByThisHosting, hostingAuthorized) == /\ hostingAuthorized /\ host.zone = "Play" /\ child.zone = "Play" /\ hostId # 0 /\ child.host = hostId /\ child.deployed = deployedByThisHosting CentralTargetSites4 == {"SchemaAtom082","SchemaAtom129","SchemaAtom018"} TargetSiteKinds4 == {"SchemaAtom033","SchemaAtom132"} TargetSiteRegistryValid4(targetSites) == /\ CentralTargetSites4 \subseteq DOMAIN targetSites /\ "NoValue" \notin DOMAIN targetSites /\ \A id \in DOMAIN targetSites : targetSites[id].kind = IF id \in CentralTargetSites4 THEN "SchemaAtom033" ELSE "SchemaAtom132" TargetSiteRegistryAtStart4(targetSites) == TargetSiteRegistryValid4(targetSites) /\ DOMAIN targetSites = CentralTargetSites4 CentralTargetSiteZone4(targetSite) == CASE targetSite = "SchemaAtom082" -> "SideAHand" [] targetSite = "SchemaAtom129" -> "SideADeck" [] targetSite = "SchemaAtom018" -> "SideADiscard" [] OTHER -> "NoValue" CentralTargetSiteForZone4(zone) == CASE zone = "SideAHand" -> "SchemaAtom082" [] zone = "SideADeck" -> "SchemaAtom129" [] zone = "SideADiscard" -> "SchemaAtom018" [] OTHER -> "NoValue" TargetSiteTraversalTargetGate4(actor, targetSites, targetSite, traversalAuthorized) == actor = "SideB" /\ targetSite \in DOMAIN targetSites /\ traversalAuthorized TargetSiteDeployDestinationGate4(actor, kind, destination, destinationExists, upgradeRestrictionHolds) == /\ destinationExists /\ CASE kind = "Objective" -> ObjectiveDeployTypeLocation(actor,kind,destination) [] kind = "Facility" -> FacilityDeployTypeLocation(actor,kind,destination) [] kind = "Attachment" -> UpgradeDeployTypeLocation(actor,kind,destination) /\ upgradeRestrictionHolds [] kind = "Barrier" -> BarrierDeployTypeLocation(actor,kind,destination) [] OTHER -> FALSE DeployedTargetSiteMoveGate4(beforeTargetSite, afterTargetSite, explicitlyDirected) == beforeTargetSite = afterTargetSite \/ explicitlyDirected DirectTargetSiteCards4(objects, targetSite) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].zone = "Play" /\ objects[id].area \in {"Root","Protecting"} /\ objects[id].targetSite = targetSite} DeployedTargetSiteCards4(objects, targetSite) == {id \in DirectTargetSiteCards4(objects,targetSite) : objects[id].deployed} TargetSiteRootTypeValid4(o, targetSiteKind) == o.form = "Card" /\ o.zone = "Play" /\ o.deployed /\ o.area = "Root" => (IF targetSiteKind = "SchemaAtom033" THEN o.kind = "Attachment" ELSE o.kind \in {"Objective","Facility","Attachment"}) UpgradeTargetSiteRestriction4(o, allowedTargetSites) == o.form = "Card" /\ o.kind = "Attachment" /\ o.deployed /\ o.area = "Root" => o.targetSite \in allowedTargetSites TargetSiteRootLimits4(objects, deploying, targetSite) == ObjectiveFacilityRootLimit(objects,targetSite) /\ RegionRootLimit(objects,deploying,targetSite) RootCardLayout4(targetSite, publicDeploymentOrder) == [orientation |-> "Vertical",location |-> [kind |-> "Root",targetSite |-> targetSite], deploymentOrder |-> publicDeploymentOrder] CentralSpecimen0139Layout4(targetSite) == [NeutralValue00012 |-> CASE targetSite = "SchemaAtom082" -> "SideAProfile" [] targetSite = "SchemaAtom129" -> "SideADeck" [] OTHER -> "SideADiscard", markerDefinesMembership |-> FALSE,upgrades |-> "VerticalNearSpecimen0139", barrierCard |-> "HorizontalInFrontOutward"] RECURSIVE AssociatedTargetSite4(_,_) AssociatedTargetSite4(objects, id) == IF id \notin DOMAIN objects THEN "NoValue" ELSE LET o == objects[id] IN IF o.host # 0 THEN AssociatedTargetSite4(objects,o.host) ELSE IF CentralTargetSiteForZone4(o.zone) # "NoValue" THEN CentralTargetSiteForZone4(o.zone) ELSE IF o.zone = "Play" /\ o.area \in {"Root","Protecting"} THEN o.targetSite ELSE "NoValue" ThisTargetSiteBinding4(currentTargetSite, triggerOrCostMovedFromTargetSite, targetSiteBeforeThatMove) == LET retainOld == triggerOrCostMovedFromTargetSite /\ targetSiteBeforeThatMove # "NoValue" IN [targetSite |-> IF retainOld THEN targetSiteBeforeThatMove ELSE currentTargetSite, frozen |-> retainOld] ThisTargetSiteDuringResolution4(before, sourceMovedNow, targetSiteBeforeMove, currentTargetSite) == IF before.frozen THEN before ELSE IF sourceMovedNow THEN [targetSite |-> targetSiteBeforeMove,frozen |-> TRUE] ELSE [targetSite |-> currentTargetSite,frozen |-> FALSE] AnotherTargetSiteContextValid4(mode, sourceCaseApplies, linkedChoiceCaseApplies, traversalActive) == CASE mode = "SchemaAtom149" -> sourceCaseApplies [] mode = "LinkedChoice" -> linkedChoiceCaseApplies [] mode = "SchemaAtom138" -> ~sourceCaseApplies /\ ~linkedChoiceCaseApplies /\ traversalActive [] mode = "NoValue" -> ~sourceCaseApplies /\ ~linkedChoiceCaseApplies /\ ~traversalActive [] OTHER -> FALSE AnotherTargetSiteReference4(mode, sourceBinding, chosenTargetSite, attackedTargetSite) == CASE mode = "SchemaAtom149" -> sourceBinding.targetSite [] mode = "LinkedChoice" -> chosenTargetSite [] mode = "SchemaAtom138" -> attackedTargetSite [] OTHER -> "NoValue" AnotherTargetSiteCandidates4(targetSites, reference) == IF reference = "NoValue" THEN {} ELSE DOMAIN targetSites \ {reference} AuxiliarySiteTargetSiteIds4(targetSites) == {id \in DOMAIN targetSites : targetSites[id].kind = "SchemaAtom132"} StandardAuxiliarySiteCountAllowed4(count) == count \in Nat NewAuxiliarySiteDeclaration4(before, after, newId, usedIds, destination, deployAuthorized, activeLimits) == /\ TargetSiteRegistryValid4(before) /\ newId \notin usedIds \cup DOMAIN before \cup {"NoValue"} /\ deployAuthorized /\ destination.targetSite = newId /\ destination.zone = "Play" /\ destination.area \in {"Root","Protecting"} /\ \A limit \in activeLimits : Cardinality(AuxiliarySiteTargetSiteIds4(before))+1 <= limit /\ after = [id \in DOMAIN before \cup {newId} |-> IF id = newId THEN [kind |-> "SchemaAtom132"] ELSE before[id]] /\ TargetSiteRegistryValid4(after) PendingTargetSiteDeploy4(deploying, targetSite) == \E id \in DOMAIN deploying : deploying[id].form = "Card" /\ deploying[id].destination.zone = "Play" /\ deploying[id].destination.targetSite = targetSite /\ deploying[id].destination.area \in {"Root","Protecting"} AuxiliarySiteSurvivesCheckpoint4(targetSite, objects, deploying) == DeployedTargetSiteCards4(objects,targetSite) # {} \/ PendingTargetSiteDeploy4(deploying,targetSite) AuxiliarySiteRegistryCheckpoint4(before, after, objects, deploying, stage) == /\ stage = "ProcedureCode2d73b20aa788" /\ TargetSiteRegistryValid4(before) /\ after = [id \in {s \in DOMAIN before : before[s].kind = "SchemaAtom033" \/ AuxiliarySiteSurvivesCheckpoint4(s,objects,deploying)} |-> before[id]] /\ TargetSiteRegistryValid4(after) AuxiliarySiteLimitPlan4(targetSites, keep, effectiveLimit, objects) == LET remotes == AuxiliarySiteTargetSiteIds4(targetSites) excess == Cardinality(remotes) > effectiveLimit valid == keep \subseteq remotes /\ (IF excess THEN Cardinality(keep) = effectiveLimit ELSE keep = remotes) IN [valid |-> valid,chooser |-> "SideA",stage |-> "ProcedureCodea488e1ba6ca3", trash |-> IF valid THEN UNION {DirectTargetSiteCards4(objects,s) : s \in remotes \ keep} ELSE {}] TraversalAfterAuxiliarySiteCleanup4(traversal, targetSitesAfter, paidAbilityWindowOpen) == IF traversal.active /\ traversal.attacked \notin DOMAIN targetSitesAfter THEN IF paidAbilityWindowOpen THEN [traversal EXCEPT !.targetSiteGone = TRUE] ELSE [traversal EXCEPT !.targetSiteGone = TRUE,!.active = FALSE, !.result = IF @ = "Undeclared" THEN "Neither" ELSE @] ELSE traversal AuxiliarySiteTableLayout4 == [roots |-> "VerticalRowAwayFromCentrals",barrierCard |-> "HorizontalInFrontOutward"] DeployedProtectingBarrier4(objects, targetSite) == {id \in DeployedTargetSiteCards4(objects,targetSite) : objects[id].kind = "Barrier" /\ objects[id].area = "Protecting"} ProtectionLayoutValid4(objects, orders, targetSites) == /\ DOMAIN orders = DOMAIN targetSites /\ \A targetSite \in DOMAIN targetSites : DeckSequenceValid4(orders[targetSite]) /\ SetupRange(orders[targetSite]) = DeployedProtectingBarrier4(objects,targetSite) BarrierPosition4(order, id) == [exists |-> id \in SetupRange(order), amount |-> IF id \in SetupRange(order) THEN (CHOOSE i \in 1..Len(order) : order[i] = id)-1 ELSE 0] InnermostBarrier4(order, id) == Len(order) > 0 /\ order[1] = id OutermostBarrier4(order, id) == Len(order) > 0 /\ order[Len(order)] = id SameBarrierPosition4(orderA, idA, orderB, idB) == /\ BarrierPosition4(orderA,idA).exists /\ BarrierPosition4(orderB,idB).exists /\ BarrierPosition4(orderA,idA).amount = BarrierPosition4(orderB,idB).amount SideBPositionAfterBarrierShift4(traversal, barrierId, beforeOrder, afterOrder) == IF traversal.active /\ traversal.currentBarrier = barrierId /\ traversal.phase \in {"Approach","Encounter","Pass"} /\ BarrierPosition4(beforeOrder,barrierId).exists /\ BarrierPosition4(afterOrder,barrierId).exists THEN [traversal EXCEPT !.position = @ + BarrierPosition4(afterOrder,barrierId).amount-BarrierPosition4(beforeOrder,barrierId).amount] ELSE traversal BankProfile4 == [shared |-> TRUE,active |-> FALSE,unlimited |-> TRUE,cardsAllowed |-> FALSE] BankPhysicalToken4(o) == o.form = "Counter" /\ o.card = "none" /\ ~o.virtual BankObjectsValid4(objects) == \A id \in DOMAIN objects : objects[id].zone = "Bank" => BankPhysicalToken4(objects[id]) BankSupplyAvailable4(amount) == amount \in Nat BankDefaultSource4(operation, explicitAlternative, actualAlternative) == IF operation \in {"Place","Load","Gain"} THEN IF explicitAlternative THEN actualAlternative ELSE [kind |-> "Zone",zone |-> "Bank"] ELSE [kind |-> "NoValue"] BankMintProjection4(before, after, added, amount, kind, usedIds, actualSource, creationAuthorized, destinationsLegal) == /\ actualSource = [kind |-> "Zone",zone |-> "Bank"] /\ creationAuthorized /\ destinationsLegal /\ BankSupplyAvailable4(amount) /\ Cardinality(DOMAIN added) = amount /\ DOMAIN added \intersect (usedIds \cup DOMAIN before) = {} /\ \A id \in DOMAIN added : BankPhysicalToken4(added[id]) /\ added[id].kind = kind /\ added[id].zone # "Bank" /\ after = [id \in DOMAIN before \cup DOMAIN added |-> IF id \in DOMAIN added THEN added[id] ELSE before[id]] BankSpendReturn4(before, after, selected, actualPaymentAuthorized) == /\ actualPaymentAuthorized /\ selected \subseteq DOMAIN before /\ \A id \in selected : BankPhysicalToken4(before[id]) /\ after = [id \in DOMAIN before \ selected |-> before[id]] IllegalPhysicalCounterIds4(objects, actualLocationLegal) == {id \in DOMAIN objects : BankPhysicalToken4(objects[id]) /\ ~actualLocationLegal[id]} BankCheckpointReturn4(before, after, actualLocationLegal, returnStageAuthorized) == /\ returnStageAuthorized /\ after = [id \in DOMAIN before \ IllegalPhysicalCounterIds4(before,actualLocationLegal) |-> before[id]] SetAsideProfile4 == [shared |-> TRUE,active |-> FALSE,temporary |-> TRUE] SetAsideDefaultActivity4(zone, otherwiseActive) == IF zone = "SetAside" THEN FALSE ELSE otherwiseActive SetAsideFace4(foundDuringSearch, specificallyFacedown) == IF foundDuringSearch \/ specificallyFacedown THEN "Down" ELSE "Up" SetAsideEntryPost4(o, foundDuringSearch, specificallyFacedown, setAsideAuthorized) == /\ setAsideAuthorized /\ o.zone = "SetAside" /\ ~o.deployed /\ IF o.form = "Card" THEN o.face = SetAsideFace4(foundDuringSearch,specificallyFacedown) ELSE TRUE SetAsideTransit4(currentObject, originalZone, originalLocation, effectInstance, owningAbility, protectedForHostedCost, sourceWasForfeited) == [object |-> currentObject,originZone |-> originalZone,originLocation |-> originalLocation, effect |-> effectInstance,ability |-> owningAbility,protected |-> protectedForHostedCost, cleanupStage |-> IF sourceWasForfeited THEN "ProcedureCode76ca53ad9dd0" ELSE "ProcedureCode96bfa1b6a970"] SetAsideAbilityCanSee4(transit, abilityId, specificallySetsAside, refersToSetAside) == /\ (specificallySetsAside \/ refersToSetAside) /\ (~transit.protected \/ abilityId = transit.ability) SetAsideExitView4(transit, abilityId, specificallySetsAside, refersToSetAside, destinationZone) == LET sees == SetAsideAbilityCanSee4(transit,abilityId,specificallySetsAside,refersToSetAside) IN [fromZone |-> IF sees THEN "SetAside" ELSE transit.originZone, fromLocation |-> IF sees THEN [kind |-> "Zone",zone |-> "SetAside"] ELSE transit.originLocation, toZone |-> destinationZone] HostedCostSetAsideRequired4(uninstallsOrForfeitsSource, effectsReferToHosted) == uninstallsOrForfeitsSource /\ effectsReferToHosted HostedCostSetAsideChoice4(actualHostedIds, selected, uninstallsOrForfeitsSource, effectsReferToHosted) == selected = IF HostedCostSetAsideRequired4(uninstallsOrForfeitsSource,effectsReferToHosted) THEN actualHostedIds ELSE {} CostAsideStillHosted4(transit, abilityId, currentlySetAside, abilityResolving) == transit.protected /\ transit.ability = abilityId /\ currentlySetAside /\ abilityResolving CostAsideCleanupIds4(transits, objects, finishedAbilities, stage) == {id \in DOMAIN transits \intersect DOMAIN objects : transits[id].protected /\ transits[id].ability \in finishedAbilities /\ transits[id].cleanupStage = stage /\ objects[id].zone = "SetAside"} SetAsideIds4(objects) == {id \in DOMAIN objects : objects[id].zone = "SetAside"} SetAsideTrackingValid4(objects, transits) == /\ SetAsideIds4(objects) \subseteq DOMAIN transits /\ \A id \in SetAsideIds4(objects) : transits[id].object = id FacedownSetAsideGroupView4(objects, transits) == LET valid == SetAsideTrackingValid4(objects,transits) ids == {id \in SetAsideIds4(objects) : objects[id].form = "Card" /\ objects[id].face = "Down"} effects == IF valid THEN {transits[id].effect : id \in ids} ELSE {} IN [valid |-> valid, groups |-> [e \in effects |-> {id \in ids : transits[id].effect = e}]] SetAsidePublicGroupCounts4(groupView) == [valid |-> groupView.valid, counts |-> [effect \in DOMAIN groupView.groups |-> Cardinality(groupView.groups[effect])]] SetAsideGroupRearrangement4(viewer, controller, before, after) == viewer = controller /\ UnorderedArrangement4(before,after) SetAsidePlayerVisibleCards4(objects, controllers, viewer, currentLookGrants) == {id \in SetAsideIds4(objects) : objects[id].form = "Card" /\ (objects[id].face = "Up" \/ controllers[id] = viewer \/ id \in currentLookGrants)} RemovedProfile4 == [shared |-> TRUE,active |-> FALSE,open |-> TRUE,controller |-> "none"] RemovedCardPost4(before, after, removalAuthorized) == /\ removalAuthorized /\ before.form = "Card" /\ after.form = "Card" /\ before.zone \in ZoneInstances4 \ {"Removed"} /\ after.card = before.card /\ after.zone = "Removed" /\ ~after.deployed /\ after.host = 0 /\ after.face = "Up" ForfeitObjectivePost4(before, after, objectiveAreaPlayer, forfeitAuthorized) == /\ objectiveAreaPlayer \in SetupPlayers /\ before.kind = "Objective" /\ before.zone = ObjectiveAreaZone4(objectiveAreaPlayer) /\ RemovedCardPost4(before,after,forfeitAuthorized) RemovedController4(zone, otherwiseController) == IF zone = "Removed" THEN "none" ELSE otherwiseController RemovedDefaultActivity4(zone, otherwiseActive) == IF zone = "Removed" THEN FALSE ELSE otherwiseActive RemovedObjectInteractionGate4(zone, operation) == zone # "Removed" \/ operation \in {"Look","Count","ReadOpenInformation"} RemovedSourceMoveGate4(sourceZone) == sourceZone # "Removed" RemovedCardZonePersistence4(beforeCardZones, afterCardZones) == \A card \in {c \in DOMAIN beforeCardZones : beforeCardZones[c] = "Removed"} : card \in DOMAIN afterCardZones /\ afterCardZones[card] = "Removed" RemovedOpenCardIds4(objects) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].zone = "Removed"} RemovedCardCount4(objects) == Cardinality(RemovedOpenCardIds4(objects)) ZoneDefaultActivityGate4(canonicalZone, otherwiseActive) == CASE canonicalZone = "Bank" -> BankProfile4.active [] canonicalZone = "SetAside" -> SetAsideProfile4.active [] canonicalZone = "Removed" -> RemovedProfile4.active [] canonicalZone = "Outside" -> FALSE [] OTHER -> otherwiseActive =============================================================================