r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

ObjectRuntime¶

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

id · operator

reference-profile · input revision 2 · CC0 1.0

id == Least(ids)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Least

n · operator

reference-profile · input revision 2 · CC0 1.0

n == IF t.obj[id].card = NoCard THEN 0
                  ELSE CardData[t.obj[id].card].recurring

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: id, CardData, NoCard

u · operator

reference-profile · input revision 2 · CC0 1.0

u == Mint(t, "ResourceUnit", n, t.obj[id].zone, id,
                       Controller(t, id), FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: id, n, Controller, Mint

newlyActive · operator

reference-profile · input revision 2 · CC0 1.0

newlyActive == {i \in DOMAIN after.obj :
           Active(after, i) /\ (IF Live(before, i) THEN ~Active(before, i) ELSE TRUE)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Active, Live

o · operator

reference-profile · input revision 2 · CC0 1.0

o == t.obj[id]

Exact module download · Source bundle and reproduction instructions

next · operator

reference-profile · input revision 2 · CC0 1.0

next == UNION {Children(t, i) : i \in frontier} \ visited

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Children

delta · operator

reference-profile · input revision 2 · CC0 1.0

delta == IF c.mode = "Gain" THEN c.amount ELSE -c.amount

Exact module download · Source bundle and reproduction instructions

t · operator

reference-profile · input revision 2 · CC0 1.0

t == IF winners = {} THEN RetireMany(s, s.pendingRetire) ELSE s

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: winners, RetireMany, s

winners · operator

reference-profile · input revision 2 · CC0 1.0

winners == ObjectiveWinners(s) \cup c.simultaneous

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveWinners, s

damageFatal · operator

reference-profile · input revision 2 · CC0 1.0

damageFatal == c.reason = "Damage" /\ c.amount >
                               Cardinality(CardsIn(s, Hand("SideB")))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardsIn, Hand, s

drawFatal · operator

reference-profile · input revision 2 · CC0 1.0

drawFatal == c.reason = "RequiredDraw" /\ c.required /\
                               CardsIn(s, Deck("SideA")) = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardsIn, Deck, s

handFatal · operator

reference-profile · input revision 2 · CC0 1.0

handFatal == c.reason = "DiscardStep" /\ s.handLimit["SideB"] < 0

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s

winners · operator

reference-profile · input revision 2 · CC0 1.0

winners == (IF damageFatal \/ handFatal THEN {"SideA"} ELSE {}) \cup
                      (IF drawFatal THEN {"SideB"} ELSE {}) \cup c.simultaneous

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: damageFatal, drawFatal, handFatal

child · operator

reference-profile · input revision 2 · CC0 1.0

child == s.obj[c.object]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s

host · operator

reference-profile · input revision 2 · CC0 1.0

host == s.obj[c.host]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s

id · operator

reference-profile · input revision 2 · CC0 1.0

id == moved.successor

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: moved

moved · operator

reference-profile · input revision 2 · CC0 1.0

moved == Relocate(s, c.object, host.zone, c.host, FALSE, c.actor)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: host, Relocate, s

sideAOnSideB · operator

reference-profile · input revision 2 · CC0 1.0

sideAOnSideB == child.card # NoCard /\ host.card # NoCard /\
                CardData[child.card].side = "SideA" /\
                CardData[host.card].side = "SideB"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: child, host, CardData, NoCard

t · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: child, id, moved, sideAOnSideB

cleaned · operator

reference-profile · input revision 2 · CC0 1.0

cleaned == IF c.mode = "Add" THEN t
                      ELSE Remove(t, {i \in Children(s, c.object) :
                                        s.obj[i].kind = "Progress"})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: t, Children, Remove, s

lastAdv · operator

reference-profile · input revision 2 · CC0 1.0

lastAdv == HostedCount(s, c.object, "Progress")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostedCount, s

moved · operator

reference-profile · input revision 2 · CC0 1.0

moved == Relocate(s, c.object, ObjectiveArea(c.player), "score", FALSE, c.player)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveArea, Relocate, s

t · operator

reference-profile · input revision 2 · CC0 1.0

t == [moved.state EXCEPT !.obj[moved.successor].face = "Up",
                           !.obj[moved.successor].deployed = FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: moved

have · operator

reference-profile · input revision 2 · CC0 1.0

have == HostedCount(s, c.object, "ResourceUnit")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostedCount, s

n · operator

reference-profile · input revision 2 · CC0 1.0

n == CardData[s.obj[c.object].card].recurring

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardData, s

host · operator

reference-profile · input revision 2 · CC0 1.0

host == s.obj[i].host

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s

id · operator

reference-profile · input revision 2 · CC0 1.0

id == chronology[j]

Exact module download · Source bundle and reproduction instructions

indices · operator

reference-profile · input revision 2 · CC0 1.0

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}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: id, Live

added · operator

reference-profile · input revision 2 · CC0 1.0

added == [i \in fresh |-> Token(kind, zone, host, actor, virtual)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: fresh, Token

fresh · operator

reference-profile · input revision 2 · CC0 1.0

fresh == t.next .. (t.next + amount - 1)

Exact module download · Source bundle and reproduction instructions

base · operator

reference-profile · input revision 2 · CC0 1.0

base == IF renew
                THEN [Remove(t, {id}) EXCEPT
                        !.obj = Put(@, newId, row), !.next = @ + 1]
                ELSE [t EXCEPT !.obj[id] = row]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: newId, renew, row, Put, Remove

family · operator

reference-profile · input revision 2 · CC0 1.0

family == {id} \cup Desc(t, id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Desc

moved · operator

reference-profile · input revision 2 · CC0 1.0

moved == IF renew /\ ~objectiveAreaTransfer
                 THEN [rebound EXCEPT !.pendingRetire = @ \cup Desc(t, id)]
                 ELSE rebound

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: objectiveAreaTransfer, rebound, renew, Desc

newId · operator

reference-profile · input revision 2 · CC0 1.0

newId == IF renew THEN t.next ELSE id

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: renew

objectiveAreaTransfer · operator

reference-profile · input revision 2 · CC0 1.0

objectiveAreaTransfer == old.zone \in ObjectiveZones /\ zone \in ObjectiveZones

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old, ObjectiveZones

objectiveCompletionIds · operator

reference-profile · input revision 2 · CC0 1.0

objectiveCompletionIds == {successors[i] : i \in family}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: family, successors

objectiveCompletionObjects · operator

reference-profile · input revision 2 · CC0 1.0

objectiveCompletionObjects == [n \in objectiveCompletionIds |->
            objectiveCompletionRows[CHOOSE i \in family : successors[i] = n]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: family, objectiveCompletionIds, objectiveCompletionRows, successors

objectiveCompletionRows · operator

reference-profile · input revision 2 · CC0 1.0

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 = {}]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: family, successors, NoHost, RelocatedFace

old · operator

reference-profile · input revision 2 · CC0 1.0

old == t.obj[id]

Exact module download · Source bundle and reproduction instructions

rebound · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: base, family, objectiveAreaTransfer, objectiveCompletionIds, objectiveCompletionObjects, renew, successors, Remove

renew · operator

reference-profile · input revision 2 · CC0 1.0

renew == old.zone # zone \/
                 (old.form = "Card" /\ hiddenDestination)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old

row · operator

reference-profile · input revision 2 · CC0 1.0

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 @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old, renew, NoHost, RelocatedFace

successors · operator

reference-profile · input revision 2 · CC0 1.0

successors == [i \in family |->
                        t.next + Cardinality({j \in family : j < i})]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: family

id · operator

reference-profile · input revision 2 · CC0 1.0

id == Least(ids)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Least

moved · operator

reference-profile · input revision 2 · CC0 1.0

moved == Relocate(t, id, Discard(Owner(t, id)),
                               "discard", FALSE, NoPlayer)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Discard, NoPlayer, Owner, Relocate

CardData · constant

reference-profile · input revision 2 · CC0 1.0

CardData

Exact module download · Source bundle and reproduction instructions

CardOverride · constant

reference-profile · input revision 2 · CC0 1.0

CardOverride(_, _, _)

Exact module download · Source bundle and reproduction instructions

CheckpointOverrideAllowed · constant

reference-profile · input revision 2 · CC0 1.0

CheckpointOverrideAllowed(_, _)

Exact module download · Source bundle and reproduction instructions

Commands · constant

reference-profile · input revision 2 · CC0 1.0

Commands(_)

Exact module download · Source bundle and reproduction instructions

InitialState · constant

reference-profile · input revision 2 · CC0 1.0

InitialState

Exact module download · Source bundle and reproduction instructions

AbilityActive · operator

reference-profile · input revision 2 · CC0 1.0

AbilityActive(cardActive, inactiveAbilityException) ==
    cardActive \/ inactiveAbilityException

Exact module download · Source bundle and reproduction instructions

AbilityController · operator

reference-profile · input revision 2 · CC0 1.0

AbilityController(t, id, specifiedPlayer) ==
    DefaultAbilityController(t.obj[id], Controller(t, id), specifiedPlayer)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, DefaultAbilityController

Active · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardData, Live, DefaultActive

AddRecurring · operator

reference-profile · input revision 2 · CC0 1.0

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})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: id, u, AddRecurring

AnnouncementValid · operator

reference-profile · input revision 2 · CC0 1.0

AnnouncementValid(chosen, available, wanted) ==
    /\ chosen \subseteq available
    /\ Cardinality(chosen) = MinOf(wanted, Cardinality(available))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinOf

CanAddProgress · operator

reference-profile · input revision 2 · CC0 1.0

CanAddProgress(t, id, printedOrGrantedPermission) ==
    t.obj[id].deployed /\
    (t.obj[id].kind = "Objective" \/ printedOrGrantedPermission)

Exact module download · Source bundle and reproduction instructions

CanPayWith · operator

reference-profile · input revision 2 · CC0 1.0

CanPayWith(t, p, id, exception) ==
    ~t.obj[id].virtual /\
    (Controller(t, id) = p \/ exception \/
     SetupPlayerCounterCostException(t.obj[id]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, SetupPlayerCounterCostException

CardKinds · operator

reference-profile · input revision 2 · CC0 1.0

CardKinds == {"Objective", "Facility", "Barrier", "Profile", "Plan", "Attachment",
              "Action", "Equipment", "Technique", "Support", "ReferenceAid"}

Exact module download · Source bundle and reproduction instructions

CardOverrideAuthorized · operator

reference-profile · input revision 2 · CC0 1.0

CardOverrideAuthorized(c) ==
    c.authorized /\ c.directContradiction /\ ~c.prohibited

Exact module download · Source bundle and reproduction instructions

CardsIn · operator

reference-profile · input revision 2 · CC0 1.0

CardsIn(t, zone) ==
    {id \in DOMAIN t.obj : t.obj[id].form = "Card" /\ t.obj[id].zone = zone}

Exact module download · Source bundle and reproduction instructions

CheckpointOrderAllows · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointOrderAllows(t, c) ==
    IF ~t.checkpointDue \/ c.op = "Checkpoint" THEN TRUE
    ELSE IF c.op = "CardOverride"
         THEN CardOverrideAuthorized(c) /\ CheckpointOverrideAllowed(t, c)
         ELSE FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointOverrideAllowed, CardOverrideAuthorized

Children · operator

reference-profile · input revision 2 · CC0 1.0

Children(t, id) == {i \in DOMAIN t.obj : t.obj[i].host = id}

Exact module download · Source bundle and reproduction instructions

Commit · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: newlyActive, AddRecurring

Controller · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: o, CardData, Controller, Live, NoHost, NoPlayer, SetupCardController

CounterCount · operator

reference-profile · input revision 2 · CC0 1.0

CounterCount(t, kind, zone, host) ==
    Cardinality(CounterSet(t, kind, zone, host))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterSet

CounterKinds · operator

reference-profile · input revision 2 · CC0 1.0

CounterKinds == {"ResourceUnit", "ActionPoint", "ExposureMarker", "LiabilityMarker", "PersistentCapacityLoss",
                 "Progress", "SchemaAtom180", "Power", "Objective", "SchemaAtom043"}

Exact module download · Source bundle and reproduction instructions

CounterSet · operator

reference-profile · input revision 2 · CC0 1.0

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}

Exact module download · Source bundle and reproduction instructions

CountsAsCounterPlacement · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Live, NoHost

Deck · operator

reference-profile · input revision 2 · CC0 1.0

Deck(p) == p \o "Deck"

Exact module download · Source bundle and reproduction instructions

DefaultTarget · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayerCounterZones

Desc · operator

reference-profile · input revision 2 · CC0 1.0

Desc(t, id) == Descendants(t, Children(t, id), {})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Children, Descendants

Descendants · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: next, Descendants

Discard · operator

reference-profile · input revision 2 · CC0 1.0

Discard(p) == p \o "Discard"

Exact module download · Source bundle and reproduction instructions

Dispatch · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DoAbilityEnd, DoActionPoints, DoAddProgress, DoAnnounce, DoBeginInstruction, DoCardOverride, DoCheckpoint, DoDiscard, DoFatal, DoFlip, DoGainResourceUnits, DoHost, DoLoseResourceUnits, DoMint, DoMove, DoObjective, DoPay, DoRefill, DoResolve, DoRetire, DoReveal, DoSpendResourceUnits, DoTakeResourceUnits, DoTurnStart

DoAbilityEnd · operator

reference-profile · input revision 2 · CC0 1.0

DoAbilityEnd(c) ==
    s' = [s EXCEPT !.reveals = {v \in @ : v.ability # c.ability},
                  !.event = "AbilityEnd"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s

DoActionPoints · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: delta, Players, s

DoAddProgress · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Live, Mint, s

DoAnnounce · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AnnouncementValid, s

DoBeginInstruction · operator

reference-profile · input revision 2 · CC0 1.0

DoBeginInstruction(c) ==
    /\ s.instruction.phase = "Finished"
    /\ s' = [s EXCEPT !.instruction.phase = "Choosing",
                       !.instruction.announcements = <<>>,
                       !.instruction.ability = c.ability,
                       !.instruction.ifAble = FALSE,
                       !.event = "BeginInstruction"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s

DoCardOverride · operator

reference-profile · input revision 2 · CC0 1.0

DoCardOverride(c) ==
    /\ CardOverrideAuthorized(c)
    /\ CardOverride(s, c, s')

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardOverride, CardOverrideAuthorized, s

DoCheckpoint · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: t, winners, Commit, Result, s

DoDiscard · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commit, Discard, Live, NoCard, NoPlayer, Owner, Relocate, s

DoFatal · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: winners, Result, s

DoFlip · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commit, Live, PublicZones, s

DoGainResourceUnits · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Mint, NoHost, Players, Pool, s

DoHost · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: t, Commit, Desc, Live, Players, s

DoLoseResourceUnits · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinOf, CounterSet, NoHost, PhysicalCounters, Players, Pool, Remove, s

DoMint · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterKinds, Live, Mint, NoHost, s

DoMove · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commit, Live, Players, Relocate, Zones, s

DoObjective · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cleaned, lastAdv, moved, Commit, HostedCount, Live, Players, s

DoPay · operator

reference-profile · input revision 2 · CC0 1.0

DoPay(c) ==
    /\ PaymentValid(s, c.player, c.bundle, c.candidate, c.evidence)
    /\ s' = Commit(s, [c.candidate EXCEPT !.checkpointDue = TRUE], "Pay")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commit, PaymentValid, s

DoRefill · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, have, n, Active, Controller, Live, Mint, s

DoResolve · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commit, InstructionParts, s

DoRetire · operator

reference-profile · input revision 2 · CC0 1.0

DoRetire(c) ==
    /\ Live(s, c.object) /\ ~s.obj[c.object].virtual
    /\ c.allowed
    /\ s' = Commit(s, RetireOne(s, c.object), "Retire")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commit, Live, RetireOne, s

DoReveal · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Dormant, Live, Players, s

DoSpendResourceUnits · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoHost, Remove, SpendResourceUnitsOK, s

DoTakeResourceUnits · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinOf, CounterSet, Live, Mint, NoHost, PhysicalCounters, Players, Pool, Remove, s

DoTurnStart · operator

reference-profile · input revision 2 · CC0 1.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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Players, s

Dormant · operator

reference-profile · input revision 2 · CC0 1.0

Dormant(o) ==                                                       
    /\ o.form = "Card" /\ CardData[o.card].side = "SideA"
    /\ o.deployed /\ o.face = "Down"
    /\ o.kind \in {"Objective", "Facility", "Attachment", "Barrier"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardData

DrawView · operator

reference-profile · input revision 2 · CC0 1.0

DrawView(deckSequence, amount) ==
    [drawn |-> SubSeq(deckSequence, 1, MinOf(amount, Len(deckSequence))),
     remaining |-> SubSeq(deckSequence, MinOf(amount, Len(deckSequence)) + 1,
                          Len(deckSequence))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinOf

EffectExecutor · operator

reference-profile · input revision 2 · CC0 1.0

EffectExecutor(abilityController, specifiedPlayer) ==
    IF specifiedPlayer = NoPlayer THEN abilityController ELSE specifiedPlayer

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoPlayer

FacedownArrivalGroup · operator

reference-profile · input revision 2 · CC0 1.0

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}

Exact module download · Source bundle and reproduction instructions

Hand · operator

reference-profile · input revision 2 · CC0 1.0

Hand(p) == p \o "Hand"

Exact module download · Source bundle and reproduction instructions

HostIntegrity · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: host, Desc, Live, NoHost, s

HostedCount · operator

reference-profile · input revision 2 · CC0 1.0

HostedCount(t, host, kind) ==
    Cardinality({i \in Children(t, host) : t.obj[i].kind = kind})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Children

HostedDeployedOrder · operator

reference-profile · input revision 2 · CC0 1.0

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]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: indices

HostedFacedownGroup · operator

reference-profile · input revision 2 · CC0 1.0

HostedFacedownGroup(t, host) ==
    {i \in Children(t, host) : t.obj[i].form = "Card" /\
        t.obj[i].face = "Down" /\ ~t.obj[i].deployed}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Children

Ids · operator

reference-profile · input revision 2 · CC0 1.0

Ids(t, kind) == {id \in DOMAIN t.obj : t.obj[id].kind = kind}

Exact module download · Source bundle and reproduction instructions

Init · operator

reference-profile · input revision 2 · CC0 1.0

Init == s = InitialState

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitialState, s

InstructionParts · operator

reference-profile · input revision 2 · CC0 1.0

InstructionParts(ifAble, requested, feasible) ==
    IF ifAble /\ feasible # requested THEN {} ELSE feasible \cap requested

Exact module download · Source bundle and reproduction instructions

ItemInspectionRevealRequired · operator

reference-profile · input revision 2 · CC0 1.0

ItemInspectionRevealRequired(zone, revealInADrawPileAbility, itemInspectionInProgress) ==
    zone = "SideADeck" /\ revealInADrawPileAbility /\ itemInspectionInProgress

Exact module download · Source bundle and reproduction instructions

Least · operator

reference-profile · input revision 2 · CC0 1.0

Least(ids) == CHOOSE x \in ids : \A y \in ids : x <= y

Exact module download · Source bundle and reproduction instructions

Live · operator

reference-profile · input revision 2 · CC0 1.0

Live(t, id) == id \in DOMAIN t.obj

Exact module download · Source bundle and reproduction instructions

MayLook · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, PublicZones

Mint · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: added, fresh

MustClaimObjective · operator

reference-profile · input revision 2 · CC0 1.0

MustClaimObjective(hasAdditionalCost, acceptsAdditionalCost, canPayAdditionalCost) ==
    ~hasAdditionalCost \/ (acceptsAdditionalCost /\ canPayAdditionalCost)

Exact module download · Source bundle and reproduction instructions

Next · operator

reference-profile · input revision 2 · CC0 1.0

Next ==
    /\ s.outcome = "Playing"
    /\ \E c \in Commands(s) :
         /\ CheckpointOrderAllows(s, c)
         /\ Dispatch(c)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Commands, CheckpointOrderAllows, Dispatch, s

NoCard · operator

reference-profile · input revision 2 · CC0 1.0

NoCard == "none"

Exact module download · Source bundle and reproduction instructions

NoHost · operator

reference-profile · input revision 2 · CC0 1.0

NoHost == 0

Exact module download · Source bundle and reproduction instructions

NoPlayer · operator

reference-profile · input revision 2 · CC0 1.0

NoPlayer == "none"

Exact module download · Source bundle and reproduction instructions

ObjectTarget · operator

reference-profile · input revision 2 · CC0 1.0

ObjectTarget(id) == [tag |-> "Object", object |-> id, sub |-> 0]

Exact module download · Source bundle and reproduction instructions

ObjectType · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardData, CardKinds, CounterKinds, NoCard, Players, PrivateZones, Zones

ObjectiveArea · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveArea(p) == p \o "ObjectiveCompletion"

Exact module download · Source bundle and reproduction instructions

ObjectiveWinners · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveWinners(t) == {p \in Players : Points(t, p) >= 7}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Players, Points

ObjectiveZones · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveZones == {"SideAObjectiveCompletion", "SideBObjectiveCompletion"}

Exact module download · Source bundle and reproduction instructions

Owner · operator

reference-profile · input revision 2 · CC0 1.0

Owner(t, id) == IF t.obj[id].card = NoCard THEN NoPlayer
                ELSE CardData[t.obj[id].card].owner

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardData, NoCard, NoPlayer

PaymentValid · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanPayWith

PhysicalCounters · operator

reference-profile · input revision 2 · CC0 1.0

PhysicalCounters(t, ids) == {i \in ids : ~t.obj[i].virtual}

Exact module download · Source bundle and reproduction instructions

PhysicalUniqueness · operator

reference-profile · input revision 2 · CC0 1.0

PhysicalUniqueness ==
    \A i, j \in DOMAIN s.obj :
       (s.obj[i].card # NoCard /\ s.obj[i].card = s.obj[j].card) => i = j

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoCard, s

PlayerCounterZones · operator

reference-profile · input revision 2 · CC0 1.0

PlayerCounterZones == {"SideAResourceUnits",
         "SideBResourceUnits", "SideAExposureMarkers", "SideBExposureMarkers", "SideALiabilityMarker",
         "SideBLiabilityMarker", "SideAPersistentCapacityLoss", "SideBPersistentCapacityLoss"}

Exact module download · Source bundle and reproduction instructions

PlayerCounters · operator

reference-profile · input revision 2 · CC0 1.0

PlayerCounters(t, p, kind) ==                                  
    Cardinality({i \in Ids(t, kind) :
        t.obj[i].host = NoHost /\ Controller(t, i) = p})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, Ids, NoHost

Players · operator

reference-profile · input revision 2 · CC0 1.0

Players == {"SideA", "SideB"}

Exact module download · Source bundle and reproduction instructions

Points · operator

reference-profile · input revision 2 · CC0 1.0

Points(t, p) ==
    SumMap([i \in CardsIn(t, ObjectiveArea(p)) |->
             IF t.obj[i].kind = "Objective"
             THEN t.obj[i].objectivePoints ELSE 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap, CardsIn, ObjectiveArea

Pool · operator

reference-profile · input revision 2 · CC0 1.0

Pool(p) == p \o "ResourceUnits"

Exact module download · Source bundle and reproduction instructions

PriorityAllowed · operator

reference-profile · input revision 2 · CC0 1.0

PriorityAllowed(t, player, basicPlayAction) ==
    t.turn = player /\ basicPlayAction /\ t.spent[player] = 0

Exact module download · Source bundle and reproduction instructions

PrivateZones · operator

reference-profile · input revision 2 · CC0 1.0

PrivateZones == {"SideADeck", "SideBDeck", "SideAHand", "SideBHand"}

Exact module download · Source bundle and reproduction instructions

ProgressAdded · operator

reference-profile · input revision 2 · CC0 1.0

ProgressAdded(t, id) == HostedCount(t, id, "Progress") >= 1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostedCount

PublicZones · operator

reference-profile · input revision 2 · CC0 1.0

PublicZones == {"Play", "SideAObjectiveCompletion", "SideBObjectiveCompletion",
                "SideADiscard", "SideBDiscard", "SetAside", "Removed"}

Exact module download · Source bundle and reproduction instructions

Put · operator

reference-profile · input revision 2 · CC0 1.0

Put(f, k, v) == [i \in DOMAIN f \cup {k} |-> IF i = k THEN v ELSE f[i]]

Exact module download · Source bundle and reproduction instructions

Relocate · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: moved, newId, objectiveAreaTransfer, old, renew, successors

RelocatedFace · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardData, ObjectiveZones, PrivateZones

Remember · operator

reference-profile · input revision 2 · CC0 1.0

Remember(t, ids) ==
    [t EXCEPT !.past = [i \in DOMAIN @ \cup ids |->
                       IF i \in ids THEN t.obj[i] ELSE @[i]]]

Exact module download · Source bundle and reproduction instructions

Remove · operator

reference-profile · input revision 2 · CC0 1.0

Remove(t, ids) ==
    [Remember(t, ids) EXCEPT !.obj = Without(@, ids),
       !.pendingRetire = (@ \cup UNION {Desc(t, i) : i \in ids}) \ ids]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Desc, Remember, Without

ResourceUnits · operator

reference-profile · input revision 2 · CC0 1.0

ResourceUnits(t, p) == CounterCount(t, "ResourceUnit", Pool(p), NoHost)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterCount, NoHost, Pool

Result · operator

reference-profile · input revision 2 · CC0 1.0

Result(winners) == CASE winners = {} -> "Playing"
                    [] winners = Players -> "Draw"
                    [] OTHER -> CHOOSE p \in winners : TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Players

RetireMany · operator

reference-profile · input revision 2 · CC0 1.0

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})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: id, Live, RetireMany, RetireOne

RetireOne · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: moved, NoCard, Remove

RuleAllowed · operator

reference-profile · input revision 2 · CC0 1.0

RuleAllowed(base, overridePresent, overrideAllows, prohibited) ==
    ~prohibited /\ (IF overridePresent THEN overrideAllows ELSE base)

Exact module download · Source bundle and reproduction instructions

Spec · operator

reference-profile · input revision 2 · CC0 1.0

Spec == Init /\ [][Next]_s

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Init, Next, s

SpendResourceUnitsOK · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, Ids, NoHost, Pool

SubTarget · operator

reference-profile · input revision 2 · CC0 1.0

SubTarget(id, sub) == [tag |-> "BarrierInstruction", object |-> id, sub |-> sub]

Exact module download · Source bundle and reproduction instructions

TargetExists · operator

reference-profile · input revision 2 · CC0 1.0

TargetExists(t, target, existingBarrierInstructions) ==
    Live(t, target.object) /\
    (target.tag = "Object" \/ target \in existingBarrierInstructions)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Live

Threat · operator

reference-profile · input revision 2 · CC0 1.0

Threat(t) == MaxOf(Points(t, "SideA"), Points(t, "SideB"))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, Points

Token · operator

reference-profile · input revision 2 · CC0 1.0

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 |-> {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoCard

TypeOK · operator

reference-profile · input revision 2 · CC0 1.0

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"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectType, Players, s

UsedRetireAbility · operator

reference-profile · input revision 2 · CC0 1.0

UsedRetireAbility(actualTriggerComponents) ==
    \E i \in 1 .. Len(actualTriggerComponents) :
         actualTriggerComponents[i].kind = "RetireSelf"

Exact module download · Source bundle and reproduction instructions

Without · operator

reference-profile · input revision 2 · CC0 1.0

Without(f, keys) == [k \in DOMAIN f \ keys |-> f[k]]

Exact module download · Source bundle and reproduction instructions

Zones · operator

reference-profile · input revision 2 · CC0 1.0

Zones == PublicZones \cup PrivateZones \cup {"Outside"} \cup PlayerCounterZones

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayerCounterZones, PrivateZones, PublicZones

s · variable

reference-profile · input revision 2 · CC0 1.0

Exact module download · Source bundle and reproduction instructions