----------------------------- MODULE ObjectRuntime ----------------------------- EXTENDS BasicContracts, SetupContracts CONSTANTS CardData, InitialState, Commands(_), CardOverride(_, _, _), CheckpointOverrideAllowed(_, _) VARIABLE s Players == {"SideA", "SideB"} NoHost == 0 NoCard == "none" NoPlayer == "none" PublicZones == {"Play", "SideAObjectiveCompletion", "SideBObjectiveCompletion", "SideADiscard", "SideBDiscard", "SetAside", "Removed"} PrivateZones == {"SideADeck", "SideBDeck", "SideAHand", "SideBHand"} ObjectiveZones == {"SideAObjectiveCompletion", "SideBObjectiveCompletion"} PlayerCounterZones == {"SideAResourceUnits", "SideBResourceUnits", "SideAExposureMarkers", "SideBExposureMarkers", "SideALiabilityMarker", "SideBLiabilityMarker", "SideAPersistentCapacityLoss", "SideBPersistentCapacityLoss"} Zones == PublicZones \cup PrivateZones \cup {"Outside"} \cup PlayerCounterZones CounterKinds == {"ResourceUnit", "ActionPoint", "ExposureMarker", "LiabilityMarker", "PersistentCapacityLoss", "Progress", "SchemaAtom180", "Power", "Objective", "SchemaAtom043"} CardKinds == {"Objective", "Facility", "Barrier", "Profile", "Plan", "Attachment", "Action", "Equipment", "Technique", "Support", "ReferenceAid"} Pool(p) == p \o "ResourceUnits" Hand(p) == p \o "Hand" Deck(p) == p \o "Deck" Discard(p) == p \o "Discard" ObjectiveArea(p) == p \o "ObjectiveCompletion" Without(f, keys) == [k \in DOMAIN f \ keys |-> f[k]] Put(f, k, v) == [i \in DOMAIN f \cup {k} |-> IF i = k THEN v ELSE f[i]] Least(ids) == CHOOSE x \in ids : \A y \in ids : x <= y Live(t, id) == id \in DOMAIN t.obj Ids(t, kind) == {id \in DOMAIN t.obj : t.obj[id].kind = kind} CardsIn(t, zone) == {id \in DOMAIN t.obj : t.obj[id].form = "Card" /\ t.obj[id].zone = zone} Children(t, id) == {i \in DOMAIN t.obj : t.obj[i].host = id} RECURSIVE Descendants(_, _, _) Descendants(t, frontier, visited) == IF frontier = {} THEN visited ELSE LET next == UNION {Children(t, i) : i \in frontier} \ visited IN Descendants(t, next, visited \cup frontier) Desc(t, id) == Descendants(t, Children(t, id), {}) ObjectType(o) == /\ o.card \in DOMAIN CardData \cup {NoCard} /\ o.form \in {"Card", "Counter"} /\ o.kind \in CardKinds \cup CounterKinds /\ o.zone \in Zones /\ o.deployed \in BOOLEAN /\ o.activated \in BOOLEAN /\ o.face \in {"Up", "Down", "NA"} /\ o.front \in BOOLEAN /\ o.host \in Nat /\ o.placedBy \in Players /\ o.virtual \in BOOLEAN /\ o.objectivePoints \in Int /\ (o.form = "Card" => o.card # NoCard /\ o.kind \in CardKinds) /\ (o.form = "Counter" => o.kind \in CounterKinds) /\ (o.card # NoCard => ~o.virtual) /\ (o.zone \in PrivateZones => o.face = "NA") Owner(t, id) == IF t.obj[id].card = NoCard THEN NoPlayer ELSE CardData[t.obj[id].card].owner RECURSIVE Controller(_, _) Controller(t, id) == LET o == t.obj[id] IN IF o.form = "Card" THEN SetupCardController(o, CardData) ELSE IF o.kind \in {"ActionPoint", "PersistentCapacityLoss"} THEN NoPlayer ELSE IF o.host # NoHost /\ Live(t, o.host) THEN Controller(t, o.host) ELSE IF o.kind = "ExposureMarker" THEN "SideB" ELSE IF o.kind = "LiabilityMarker" THEN "SideA" ELSE IF o.zone = "SideAResourceUnits" THEN "SideA" ELSE IF o.zone = "SideBResourceUnits" THEN "SideB" ELSE NoPlayer Active(t, id) == IF t.obj[id].form = "Counter" THEN t.obj[id].kind = "SchemaAtom043" /\ Live(t, t.obj[id].host) ELSE DefaultActive(t.obj[id], t.started, CardData) AbilityController(t, id, specifiedPlayer) == DefaultAbilityController(t.obj[id], Controller(t, id), specifiedPlayer) EffectExecutor(abilityController, specifiedPlayer) == IF specifiedPlayer = NoPlayer THEN abilityController ELSE specifiedPlayer CounterSet(t, kind, zone, host) == {i \in DOMAIN t.obj : /\ t.obj[i].form = "Counter" /\ t.obj[i].kind = kind /\ t.obj[i].zone = zone /\ t.obj[i].host = host} CounterCount(t, kind, zone, host) == Cardinality(CounterSet(t, kind, zone, host)) PhysicalCounters(t, ids) == {i \in ids : ~t.obj[i].virtual} HostedCount(t, host, kind) == Cardinality({i \in Children(t, host) : t.obj[i].kind = kind}) ResourceUnits(t, p) == CounterCount(t, "ResourceUnit", Pool(p), NoHost) PlayerCounters(t, p, kind) == Cardinality({i \in Ids(t, kind) : t.obj[i].host = NoHost /\ Controller(t, i) = p}) Token(kind, zone, host, actor, virtual) == [card |-> NoCard, form |-> "Counter", kind |-> kind, zone |-> zone, loc |-> host, deployed |-> FALSE, face |-> "Up", front |-> TRUE, activated |-> FALSE, host |-> host, placedBy |-> actor, virtual |-> virtual, objectivePoints |-> 0, marks |-> {}] Mint(t, kind, amount, zone, host, actor, virtual) == LET fresh == t.next .. (t.next + amount - 1) added == [i \in fresh |-> Token(kind, zone, host, actor, virtual)] IN [t EXCEPT !.obj = [i \in DOMAIN @ \cup fresh |-> IF i \in fresh THEN added[i] ELSE @[i]], !.next = @ + amount] Remember(t, ids) == [t EXCEPT !.past = [i \in DOMAIN @ \cup ids |-> IF i \in ids THEN t.obj[i] ELSE @[i]]] Remove(t, ids) == [Remember(t, ids) EXCEPT !.obj = Without(@, ids), !.pendingRetire = (@ \cup UNION {Desc(t, i) : i \in ids}) \ ids] RelocatedFace(o, zone) == IF o.form = "Card" /\ o.kind = "Objective" /\ zone \in ObjectiveZones THEN "Up" ELSE IF o.form = "Card" /\ zone = "SideBDiscard" /\ CardData[o.card].side = "SideB" THEN "Up" ELSE IF zone \in PrivateZones THEN "NA" ELSE IF o.face = "NA" THEN "Up" ELSE o.face Relocate(t, id, zone, loc, hiddenDestination, actor) == LET old == t.obj[id] renew == old.zone # zone \/ (old.form = "Card" /\ hiddenDestination) objectiveAreaTransfer == old.zone \in ObjectiveZones /\ zone \in ObjectiveZones row == [old EXCEPT !.zone = zone, !.loc = loc, !.placedBy = IF old.form = "Card" /\ old.zone # "Play" /\ zone = "Play" THEN actor ELSE @, !.host = IF old.zone = zone THEN @ ELSE NoHost, !.face = RelocatedFace(old, zone), !.deployed = IF old.zone = zone THEN @ ELSE FALSE, !.activated = IF old.zone = zone THEN @ ELSE FALSE, !.marks = IF renew THEN {} ELSE @] newId == IF renew THEN t.next ELSE id base == IF renew THEN [Remove(t, {id}) EXCEPT !.obj = Put(@, newId, row), !.next = @ + 1] ELSE [t EXCEPT !.obj[id] = row] family == {id} \cup Desc(t, id) successors == [i \in family |-> t.next + Cardinality({j \in family : j < i})] objectiveCompletionRows == [i \in family |-> [t.obj[i] EXCEPT !.zone = zone, !.face = RelocatedFace(t.obj[i], zone), !.loc = IF i = id THEN loc ELSE successors[t.obj[i].host], !.host = IF i = id THEN NoHost ELSE successors[t.obj[i].host], !.deployed = FALSE, !.activated = FALSE, !.marks = {}]] objectiveCompletionIds == {successors[i] : i \in family} objectiveCompletionObjects == [n \in objectiveCompletionIds |-> objectiveCompletionRows[CHOOSE i \in family : successors[i] = n]] rebound == IF renew /\ objectiveAreaTransfer THEN [Remove(t, family) EXCEPT !.obj = [i \in DOMAIN @ \cup objectiveCompletionIds |-> IF i \in objectiveCompletionIds THEN objectiveCompletionObjects[i] ELSE @[i]], !.next = @ + Cardinality(family), !.pendingRetire = @ \cup {successors[i] : i \in t.pendingRetire \cap family}, !.reveals = {v \in @ : v.object \notin family}] ELSE base moved == IF renew /\ ~objectiveAreaTransfer THEN [rebound EXCEPT !.pendingRetire = @ \cup Desc(t, id)] ELSE rebound IN [state |-> [moved EXCEPT !.reveals = {v \in @ : v.object # id \/ (~renew /\ old.zone = zone /\ old.loc = loc)}], successor |-> IF renew /\ objectiveAreaTransfer THEN successors[id] ELSE newId] RECURSIVE RetireMany(_, _) RetireOne(t, id) == IF t.obj[id].card = NoCard THEN Remove(t, {id}) ELSE LET moved == Relocate(t, id, Discard(Owner(t, id)), "discard", FALSE, NoPlayer) IN [moved.state EXCEPT !.obj[moved.successor].deployed = FALSE, !.obj[moved.successor].activated = FALSE] RetireMany(t, ids) == IF ids = {} THEN t ELSE LET id == Least(ids) IN RetireMany(IF Live(t, id) THEN RetireOne(t, id) ELSE t, ids \ {id}) RECURSIVE AddRecurring(_, _) AddRecurring(t, ids) == IF ids = {} THEN t ELSE LET id == Least(ids) n == IF t.obj[id].card = NoCard THEN 0 ELSE CardData[t.obj[id].card].recurring u == Mint(t, "ResourceUnit", n, t.obj[id].zone, id, Controller(t, id), FALSE) IN AddRecurring(u, ids \ {id}) Commit(before, after, event) == LET newlyActive == {i \in DOMAIN after.obj : Active(after, i) /\ (IF Live(before, i) THEN ~Active(before, i) ELSE TRUE)} IN [AddRecurring(after, newlyActive) EXCEPT !.event = event] Points(t, p) == SumMap([i \in CardsIn(t, ObjectiveArea(p)) |-> IF t.obj[i].kind = "Objective" THEN t.obj[i].objectivePoints ELSE 0]) Threat(t) == MaxOf(Points(t, "SideA"), Points(t, "SideB")) ObjectiveWinners(t) == {p \in Players : Points(t, p) >= 7} Result(winners) == CASE winners = {} -> "Playing" [] winners = Players -> "Draw" [] OTHER -> CHOOSE p \in winners : TRUE TypeOK == /\ s.next \in Nat \ {0} /\ IsFiniteSet(DOMAIN s.obj) /\ \A i \in DOMAIN s.obj : i \in 1 .. (s.next - 1) /\ ObjectType(s.obj[i]) /\ DOMAIN s.past \cap DOMAIN s.obj = {} /\ \A i \in DOMAIN s.past : i \in 1 .. (s.next - 1) /\ s.pendingRetire \subseteq DOMAIN s.obj /\ s.started \in BOOLEAN /\ s.turn \in Players /\ s.actionPoints \in [Players -> Int] /\ s.spent \in [Players -> Nat] /\ s.handLimit \in [Players -> Int] /\ s.checkpointDue \in BOOLEAN /\ s.outcome \in {"Playing", "SideA", "SideB", "Draw"} PhysicalUniqueness == \A i, j \in DOMAIN s.obj : (s.obj[i].card # NoCard /\ s.obj[i].card = s.obj[j].card) => i = j HostIntegrity == \A i \in DOMAIN s.obj : LET host == s.obj[i].host IN host = NoHost \/ i \in s.pendingRetire \/ (/\ Live(s, host) /\ host # i /\ s.obj[host].zone \in {"Play", "SideAObjectiveCompletion", "SideBObjectiveCompletion"} /\ (s.obj[host].form = "Card" \/ s.obj[host].kind = "SchemaAtom043") /\ s.obj[i].zone = s.obj[host].zone /\ i \notin Desc(s, i)) RuleAllowed(base, overridePresent, overrideAllows, prohibited) == ~prohibited /\ (IF overridePresent THEN overrideAllows ELSE base) CanPayWith(t, p, id, exception) == ~t.obj[id].virtual /\ (Controller(t, id) = p \/ exception \/ SetupPlayerCounterCostException(t.obj[id])) PaymentValid(t, p, bundle, candidate, evidence) == /\ evidence.announced /\ evidence.full /\ evidence.restrictionBefore /\ evidence.restrictionAfter /\ ~evidence.mandatoryPrevents /\ ~evidence.staticPrevents /\ evidence.additionalAccepted /\ bundle \subseteq DOMAIN t.obj /\ \A i \in bundle : CanPayWith(t, p, i, i \in evidence.controlExceptions) /\ evidence.procedureValid ObjectTarget(id) == [tag |-> "Object", object |-> id, sub |-> 0] SubTarget(id, sub) == [tag |-> "BarrierInstruction", object |-> id, sub |-> sub] TargetExists(t, target, existingBarrierInstructions) == Live(t, target.object) /\ (target.tag = "Object" \/ target \in existingBarrierInstructions) DefaultTarget(t, target, explicitZone, eligible) == /\ target \in eligible /\ IF target.tag = "BarrierInstruction" THEN TRUE ELSE IF explicitZone # "none" THEN t.obj[target.object].zone = explicitZone ELSE t.obj[target.object].deployed \/ (t.obj[target.object].form = "Counter" /\ t.obj[target.object].zone \in ({"Play"} \cup PlayerCounterZones)) AnnouncementValid(chosen, available, wanted) == /\ chosen \subseteq available /\ Cardinality(chosen) = MinOf(wanted, Cardinality(available)) InstructionParts(ifAble, requested, feasible) == IF ifAble /\ feasible # requested THEN {} ELSE feasible \cap requested DoMove(c) == /\ Live(s, c.object) /\ ~s.obj[c.object].virtual /\ c.zone \in Zones /\ c.actor \in Players /\ s' = Commit(s, Relocate(s, c.object, c.zone, c.loc, c.hidden, c.actor).state, "Move") DoFlip(c) == /\ Live(s, c.object) /\ s.obj[c.object].form = "Card" /\ s.obj[c.object].zone \in PublicZones /\ c.face \in {"Up", "Down"} /\ s' = Commit(s, [s EXCEPT !.obj[c.object].face = c.face], "Flip") DoHost(c) == /\ Live(s, c.object) /\ Live(s, c.host) /\ c.object # c.host /\ ~s.obj[c.object].virtual /\ c.host \notin Desc(s, c.object) /\ s.obj[c.host].zone \in {"Play", "SideAObjectiveCompletion", "SideBObjectiveCompletion"} /\ (s.obj[c.host].form = "Card" \/ s.obj[c.host].kind = "SchemaAtom043") /\ c.permission /\ c.capacityOK /\ c.requiredDestinationOK /\ c.actor \in Players /\ (~s.obj[c.object].deployed \/ c.explicitRehost) /\ LET child == s.obj[c.object] host == s.obj[c.host] moved == Relocate(s, c.object, host.zone, c.host, FALSE, c.actor) id == moved.successor sideAOnSideB == child.card # NoCard /\ host.card # NoCard /\ CardData[child.card].side = "SideA" /\ CardData[host.card].side = "SideB" t == [moved.state EXCEPT !.obj[id].host = c.host, !.obj[id].deployed = child.deployed /\ ~sideAOnSideB, !.obj[id].face = IF child.form = "Counter" THEN "Up" ELSE IF c.face # "Default" THEN c.face ELSE "Up"] IN s' = Commit(s, t, "Host") DoMint(c) == /\ c.amount \in Nat /\ c.kind \in CounterKinds /\ c.host = NoHost \/ Live(s, c.host) /\ s' = [Mint(s, c.kind, c.amount, c.zone, c.host, c.actor, c.virtual) EXCEPT !.event = IF c.virtual THEN "ConsiderCounters" ELSE "PlaceCounters"] DoLoseResourceUnits(c) == /\ c.amount \in Nat /\ c.player \in Players /\ c.selected \subseteq PhysicalCounters(s, CounterSet(s, "ResourceUnit", Pool(c.player), NoHost)) /\ Cardinality(c.selected) = MinOf(c.amount, Cardinality(PhysicalCounters(s, CounterSet(s, "ResourceUnit", Pool(c.player), NoHost)))) /\ s' = [Remove(s, c.selected) EXCEPT !.event = "LoseResourceUnits"] DoGainResourceUnits(c) == /\ c.amount \in Nat /\ c.player \in Players /\ s' = [Mint(s, "ResourceUnit", c.amount, Pool(c.player), NoHost, c.player, FALSE) EXCEPT !.event = "GainResourceUnits"] DoTakeResourceUnits(c) == /\ Live(s, c.host) /\ c.player \in Players /\ c.amount \in Nat /\ c.selected \subseteq PhysicalCounters(s, CounterSet(s, "ResourceUnit", s.obj[c.host].zone, c.host)) /\ Cardinality(c.selected) = MinOf(c.amount, Cardinality(PhysicalCounters(s, CounterSet(s, "ResourceUnit", s.obj[c.host].zone, c.host)))) /\ s' = [Mint(Remove(s, c.selected), "ResourceUnit", Cardinality(c.selected), Pool(c.player), NoHost, c.player, FALSE) EXCEPT !.event = "GainResourceUnits"] SpendResourceUnitsOK(t, p, selected, amount, permittedHosted) == /\ amount \in Nat /\ selected \subseteq Ids(t, "ResourceUnit") /\ Cardinality(selected) = amount /\ \A i \in selected : ~t.obj[i].virtual /\ ((t.obj[i].zone = Pool(p) /\ t.obj[i].host = NoHost) \/ (t.obj[i].host \in permittedHosted /\ Controller(t, i) = p)) DoSpendResourceUnits(c) == /\ SpendResourceUnitsOK(s, c.player, c.selected, c.amount, c.permittedHosted) /\ c.announced /\ c.restrictionsHold /\ ~c.mandatoryPrevents /\ s' = [Remove(s, c.selected) EXCEPT !.checkpointDue = TRUE, !.used = {c.permissionSources[s.obj[i].host] : i \in {j \in c.selected : s.obj[j].host # NoHost}}, !.event = "PayResourceUnits"] DoRefill(c) == /\ Live(s, c.object) /\ Active(s, c.object) /\ Controller(s, c.object) = s.turn /\ LET n == CardData[s.obj[c.object].card].recurring have == HostedCount(s, c.object, "ResourceUnit") IN s' = [Mint(s, "ResourceUnit", MaxOf(0, n - have), s.obj[c.object].zone, c.object, s.turn, FALSE) EXCEPT !.event = "RefillRecurring"] DoActionPoints(c) == /\ c.player \in Players /\ c.amount \in Nat /\ c.mode \in {"Gain", "Lose", "Spend"} /\ (c.mode = "Spend" => s.actionPoints[c.player] >= c.amount /\ s.turn = c.player) /\ (c.mode = "Spend" => c.announced) /\ LET delta == IF c.mode = "Gain" THEN c.amount ELSE -c.amount IN s' = [s EXCEPT !.actionPoints[c.player] = @ + delta, !.spent[c.player] = IF c.mode = "Spend" THEN @ + c.amount ELSE @, !.checkpointDue = IF c.mode = "Spend" THEN TRUE ELSE @, !.event = c.mode \o "ActionPoints"] PriorityAllowed(t, player, basicPlayAction) == t.turn = player /\ basicPlayAction /\ t.spent[player] = 0 DoTurnStart(c) == /\ c.player \in Players /\ s' = [s EXCEPT !.turn = c.player, !.actionPoints[c.player] = @ + IF c.player = "SideA" THEN 3 ELSE 4, !.spent[c.player] = 0, !.event = "TurnStart"] DoPay(c) == /\ PaymentValid(s, c.player, c.bundle, c.candidate, c.evidence) /\ s' = Commit(s, [c.candidate EXCEPT !.checkpointDue = TRUE], "Pay") DoBeginInstruction(c) == /\ s.instruction.phase = "Finished" /\ s' = [s EXCEPT !.instruction.phase = "Choosing", !.instruction.announcements = <<>>, !.instruction.ability = c.ability, !.instruction.ifAble = FALSE, !.event = "BeginInstruction"] DoAnnounce(c) == /\ s.instruction.phase = "Choosing" /\ Len(c.announcements) = Len(c.available) /\ Len(c.wanted) = Len(c.available) /\ \A i \in 1 .. Len(c.available) : AnnouncementValid(c.announcements[i], c.available[i], c.wanted[i]) /\ s' = [s EXCEPT !.instruction.phase = "Imminent", !.instruction.announcements = c.announcements, !.instruction.ability = c.ability, !.instruction.ifAble = c.ifAble, !.event = "AnnounceTargets"] DoResolve(c) == /\ s.instruction.phase = "Imminent" /\ c.feasible \subseteq c.requested /\ c.revalidated /\ c.applied = InstructionParts(s.instruction.ifAble, c.requested, c.feasible) /\ c.effectContract /\ s' = Commit(s, [c.candidate EXCEPT !.instruction.phase = "Finished", !.checkpointDue = TRUE], "ResolveInstruction") Dormant(o) == /\ o.form = "Card" /\ CardData[o.card].side = "SideA" /\ o.deployed /\ o.face = "Down" /\ o.kind \in {"Objective", "Facility", "Attachment", "Barrier"} DoReveal(c) == /\ Live(s, c.object) /\ s.obj[c.object].form = "Card" /\ c.mode \in {"Look", "Reveal", "Expose", "ItemInspection"} /\ (c.mode = "Expose" => Dormant(s.obj[c.object])) /\ c.viewers \subseteq Players /\ (c.mode \in {"Reveal", "Expose"} => c.viewers = Players) /\ s' = [s EXCEPT !.reveals = @ \cup {[object |-> c.object, loc |-> s.obj[c.object].loc, viewers |-> c.viewers, ability |-> c.ability]}, !.event = c.mode] DoAbilityEnd(c) == s' = [s EXCEPT !.reveals = {v \in @ : v.ability # c.ability}, !.event = "AbilityEnd"] MayLook(t, player, id) == (t.obj[id].face = "Up" /\ t.obj[id].zone \in PublicZones) \/ (t.obj[id].face = "Down" /\ Controller(t, id) = player) \/ \E v \in t.reveals : v.object = id /\ v.loc = t.obj[id].loc /\ player \in v.viewers HostedFacedownGroup(t, host) == {i \in Children(t, host) : t.obj[i].form = "Card" /\ t.obj[i].face = "Down" /\ ~t.obj[i].deployed} HostedDeployedOrder(t, host, chronology) == LET indices == {j \in 1..Len(chronology) : LET id == chronology[j] IN IF ~Live(t, id) THEN FALSE ELSE /\ t.obj[id].host = host /\ t.obj[id].deployed /\ t.obj[id].face = "Down" /\ \A k \in (j+1)..Len(chronology) : chronology[k] # id} IN [rank \in 1..Cardinality(indices) |-> chronology[CHOOSE j \in indices : Cardinality({k \in indices : k < j}) = rank - 1]] FacedownArrivalGroup(t, simultaneousArrivals, id) == {i \in simultaneousArrivals : t.obj[i].face = "Down" /\ t.obj[i].zone = t.obj[id].zone /\ t.obj[i].host = t.obj[id].host} ItemInspectionRevealRequired(zone, revealInADrawPileAbility, itemInspectionInProgress) == zone = "SideADeck" /\ revealInADrawPileAbility /\ itemInspectionInProgress AbilityActive(cardActive, inactiveAbilityException) == cardActive \/ inactiveAbilityException DrawView(deckSequence, amount) == [drawn |-> SubSeq(deckSequence, 1, MinOf(amount, Len(deckSequence))), remaining |-> SubSeq(deckSequence, MinOf(amount, Len(deckSequence)) + 1, Len(deckSequence))] CanAddProgress(t, id, printedOrGrantedPermission) == t.obj[id].deployed /\ (t.obj[id].kind = "Objective" \/ printedOrGrantedPermission) MustClaimObjective(hasAdditionalCost, acceptsAdditionalCost, canPayAdditionalCost) == ~hasAdditionalCost \/ (acceptsAdditionalCost /\ canPayAdditionalCost) CountsAsCounterPlacement(before, after, id, destinationHost) == /\ Live(after, id) /\ after.obj[id].form = "Counter" /\ ~after.obj[id].virtual /\ after.obj[id].host = destinationHost /\ destinationHost # NoHost /\ (IF Live(before, id) THEN before.obj[id].host # destinationHost ELSE TRUE) DoAddProgress(c) == /\ Live(s, c.object) /\ s.obj[c.object].deployed /\ c.canAddProgress /\ c.actor = "SideA" /\ s' = [Mint(s, "Progress", 1, s.obj[c.object].zone, c.object, "SideA", FALSE) EXCEPT !.event = "AddProgress"] ProgressAdded(t, id) == HostedCount(t, id, "Progress") >= 1 DoObjective(c) == /\ Live(s, c.object) /\ c.player \in Players /\ s.obj[c.object].kind = "Objective" /\ c.mode \in {"ObjectiveCompletion", "ClaimObjective", "Add"} /\ (c.mode = "ObjectiveCompletion" => c.player = "SideA" /\ s.turn = "SideA" /\ c.objectivePlacementWindow /\ s.obj[c.object].deployed /\ HostedCount(s, c.object, "Progress") >= c.progressRequirement) /\ (c.mode = "ClaimObjective" => c.player = "SideB" /\ c.accessing) /\ c.costsComplete /\ c.allowed /\ LET lastAdv == HostedCount(s, c.object, "Progress") moved == Relocate(s, c.object, ObjectiveArea(c.player), "score", FALSE, c.player) t == [moved.state EXCEPT !.obj[moved.successor].face = "Up", !.obj[moved.successor].deployed = FALSE] cleaned == IF c.mode = "Add" THEN t ELSE Remove(t, {i \in Children(s, c.object) : s.obj[i].kind = "Progress"}) IN s' = Commit(s, [cleaned EXCEPT !.lastObjective = [mode |-> c.mode, before |-> c.object, after |-> moved.successor, progress |-> lastAdv], !.checkpointDue = TRUE], c.mode) DoRetire(c) == /\ Live(s, c.object) /\ ~s.obj[c.object].virtual /\ c.allowed /\ s' = Commit(s, RetireOne(s, c.object), "Retire") DoDiscard(c) == /\ Live(s, c.object) /\ s.obj[c.object].card # NoCard /\ s' = Commit(s, Relocate(s, c.object, Discard(Owner(s, c.object)), "discard", FALSE, NoPlayer).state, "Discard") UsedRetireAbility(actualTriggerComponents) == \E i \in 1 .. Len(actualTriggerComponents) : actualTriggerComponents[i].kind = "RetireSelf" DoFatal(c) == /\ c.reason \in {"Damage", "DiscardStep", "RequiredDraw"} /\ c.validProcedure /\ LET damageFatal == c.reason = "Damage" /\ c.amount > Cardinality(CardsIn(s, Hand("SideB"))) handFatal == c.reason = "DiscardStep" /\ s.handLimit["SideB"] < 0 drawFatal == c.reason = "RequiredDraw" /\ c.required /\ CardsIn(s, Deck("SideA")) = {} winners == (IF damageFatal \/ handFatal THEN {"SideA"} ELSE {}) \cup (IF drawFatal THEN {"SideB"} ELSE {}) \cup c.simultaneous IN s' = [s EXCEPT !.outcome = Result(winners), !.event = c.reason] DoCheckpoint(c) == /\ c.readyForSection1Checks /\ LET winners == ObjectiveWinners(s) \cup c.simultaneous t == IF winners = {} THEN RetireMany(s, s.pendingRetire) ELSE s IN s' = Commit(s, [t EXCEPT !.checkpointDue = FALSE, !.outcome = Result(winners)], "Checkpoint") CardOverrideAuthorized(c) == c.authorized /\ c.directContradiction /\ ~c.prohibited DoCardOverride(c) == /\ CardOverrideAuthorized(c) /\ CardOverride(s, c, s') CheckpointOrderAllows(t, c) == IF ~t.checkpointDue \/ c.op = "Checkpoint" THEN TRUE ELSE IF c.op = "CardOverride" THEN CardOverrideAuthorized(c) /\ CheckpointOverrideAllowed(t, c) ELSE FALSE Dispatch(c) == CASE c.op = "Move" -> DoMove(c) [] c.op = "Flip" -> DoFlip(c) [] c.op = "Host" -> DoHost(c) [] c.op = "Mint" -> DoMint(c) [] c.op = "LoseResourceUnits" -> DoLoseResourceUnits(c) [] c.op = "GainResourceUnits" -> DoGainResourceUnits(c) [] c.op = "TakeResourceUnits" -> DoTakeResourceUnits(c) [] c.op = "SpendResourceUnits" -> DoSpendResourceUnits(c) [] c.op = "Refill" -> DoRefill(c) [] c.op = "ActionPoints" -> DoActionPoints(c) [] c.op = "TurnStart" -> DoTurnStart(c) [] c.op = "Pay" -> DoPay(c) [] c.op = "BeginInstruction" -> DoBeginInstruction(c) [] c.op = "Announce" -> DoAnnounce(c) [] c.op = "Resolve" -> DoResolve(c) [] c.op = "Reveal" -> DoReveal(c) [] c.op = "AbilityEnd" -> DoAbilityEnd(c) [] c.op = "AddProgress" -> DoAddProgress(c) [] c.op = "Objective" -> DoObjective(c) [] c.op = "Retire" -> DoRetire(c) [] c.op = "Discard" -> DoDiscard(c) [] c.op = "Fatal" -> DoFatal(c) [] c.op = "Checkpoint" -> DoCheckpoint(c) [] c.op = "CardOverride" -> DoCardOverride(c) [] OTHER -> FALSE Init == s = InitialState Next == /\ s.outcome = "Playing" /\ \E c \in Commands(s) : /\ CheckpointOrderAllows(s, c) /\ Dispatch(c) Spec == Init /\ [][Next]_s =============================================================================