AdditionalContracts

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.

bHand · operator

reference-profile · input revision 2 · CC0 1.0

bHand==DamageBHand104(world.objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageBHand104

fatal · operator

reference-profile · input revision 2 · CC0 1.0

fatal==packet.amount>Cardinality(bHand)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: bHand

ordinal · operator

reference-profile · input revision 2 · CC0 1.0

ordinal==1+Cardinality({old \in DOMAIN world.escalatingResourceContestHistory : world.escalatingResourceContestHistory[old].turnId=world.turn.id})

Exact module download · Source bundle and reproduction instructions

e · operator

reference-profile · input revision 2 · CC0 1.0

e==world.lingering.effects[id]

Exact module download · Source bundle and reproduction instructions

candidates · operator

reference-profile · input revision 2 · CC0 1.0

candidates==EscalatingResourceContestPoolIds108(world.objects,player) \cup fund \cup hosted

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: fund, hosted, EscalatingResourceContestPoolIds108

fund · operator

reference-profile · input revision 2 · CC0 1.0

fund==IF player="SideB" /\ BidTraversalLive1014(world) THEN LiabilityMarkerFundIds106(world.objects) ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidTraversalLive1014, LiabilityMarkerFundIds106

hosted · operator

reference-profile · input revision 2 · CC0 1.0

hosted==IF player="SideB" THEN
       UNION {{id \in DOMAIN world.objects : world.objects[id].form="Counter" /\ world.objects[id].kind="ResourceUnit" /\ ~world.objects[id].virtual /\ world.objects[id].host=world.lingering.effects[e].value.host /\ world.objects[id].zone="Play"} :
          e \in {e \in DOMAIN world.lingering.effects : BidHostedPermission1014(world,e,cardFacts)}} ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidHostedPermission1014

r · operator

reference-profile · input revision 2 · CC0 1.0

r==world.bidValueRestrictions[id]

Exact module download · Source bundle and reproduction instructions

sources · operator

reference-profile · input revision 2 · CC0 1.0

sources=={world.abilitySources[id].object : id \in EscalatingResourceContestRoleIds108(world,"BidForbidTwo","Specimen0102")}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestRoleIds108

e · operator

reference-profile · input revision 2 · CC0 1.0

e==world.lingering.effects[id]

Exact module download · Source bundle and reproduction instructions

e · operator

reference-profile · input revision 2 · CC0 1.0

e==world.lingering.effects[effectId]

Exact module download · Source bundle and reproduction instructions

host · operator

reference-profile · input revision 2 · CC0 1.0

host==e.value.host

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: e

e · operator

reference-profile · input revision 2 · CC0 1.0

e==context.actualEffects[operation]

Exact module download · Source bundle and reproduction instructions

t · operator

reference-profile · input revision 2 · CC0 1.0

t==context.templates[operation]

Exact module download · Source bundle and reproduction instructions

f · operator

reference-profile · input revision 2 · CC0 1.0

f==world.bidFrames[event.bidId]

Exact module download · Source bundle and reproduction instructions

refs · operator

reference-profile · input revision 2 · CC0 1.0

refs==IF spec.mode="Chosen" THEN plan.targets ELSE {spec.particular}

Exact module download · Source bundle and reproduction instructions

count · operator

reference-profile · input revision 2 · CC0 1.0

count==Cardinality(physical)+world.consideredProgress[begin.object]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: physical

fact · operator

reference-profile · input revision 2 · CC0 1.0

fact==DividendFacts1013!DividendPrintedFacts1013[begin.sourceCard]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DividendFacts1013!DividendPrintedFacts1013

physical · operator

reference-profile · input revision 2 · CC0 1.0

physical==DividendPhysicalProgress1013(world,begin.object)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DividendPhysicalProgress1013

e · operator

reference-profile · input revision 2 · CC0 1.0

e==context.actualEffects[id]

Exact module download · Source bundle and reproduction instructions

indicated · operator

reference-profile · input revision 2 · CC0 1.0

indicated==IF spec.setRule="YourDeployedCards" THEN
       {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.controllers[id]=spec.actor}
       ELSE spec.compiledSet

Exact module download · Source bundle and reproduction instructions

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==AuxiliarySiteLimitPlan4(remaining,keep,effectiveLimit,objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: remaining, AuxiliarySiteLimitPlan4

remaining · operator

reference-profile · input revision 2 · CC0 1.0

remaining==Without101(targetSites,before.retiredRemotes)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Without101

retired · operator

reference-profile · input revision 2 · CC0 1.0

retired==AuxiliarySiteTargetSiteIds4(remaining) \ keep

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: remaining, AuxiliarySiteTargetSiteIds4

added · operator

reference-profile · input revision 2 · CC0 1.0

added==CheckpointNewUninstallDepartures103(objects,due)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: due, CheckpointNewUninstallDepartures103

due · operator

reference-profile · input revision 2 · CC0 1.0

due==CheckpointHostedTargets103(objects,departures,before.point,transits,paidProcedures)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointHostedTargets103

finished · operator

reference-profile · input revision 2 · CC0 1.0

finished=={p \in DOMAIN paidProcedures : paidProcedures[p].ability.lastFinished}

Exact module download · Source bundle and reproduction instructions

historical · operator

reference-profile · input revision 2 · CC0 1.0

historical==UNION {departures[id].children : id \in {id \in DOMAIN departures :
                         IF kind="ProcedureCode76ca53ad9dd0" THEN departures[id].objectiveCompletionLeft ELSE departures[id].uninstalled \/ departures[id].hostRemoved}}

Exact module download · Source bundle and reproduction instructions

choices · operator

reference-profile · input revision 2 · CC0 1.0

choices==AppropriateRetireSets103(eligible,LegalAfterRetire)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AppropriateRetireSets103

points · operator

reference-profile · input revision 2 · CC0 1.0

points==[p \in SetupPlayers |-> ObjectiveAreaPoints4(objects,p,effectivePoints)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveAreaPoints4, SetupPlayers

winners · operator

reference-profile · input revision 2 · CC0 1.0

winners=={p \in SetupPlayers : points[p]>=7}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: points, SetupPlayers

LAMBDA · operator

reference-profile · input revision 2 · CC0 1.0

LAMBDA p : p \notin remove

Exact module download · Source bundle and reproduction instructions

pendingTargetSites · operator

reference-profile · input revision 2 · CC0 1.0

pendingTargetSites==CheckpointPendingBarrierTargetSites103(deploying)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPendingBarrierTargetSites103

remove · operator

reference-profile · input revision 2 · CC0 1.0

remove=={p \in DOMAIN layout.slots : layout.slots[p].barrierCard=0 /\ p#currentSideBPosition /\ layout.slots[p].targetSite \notin pendingTargetSites}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: pendingTargetSites

cards · operator

reference-profile · input revision 2 · CC0 1.0

cards=={id \in selected : objects[id].card#"none"}

Exact module download · Source bundle and reproduction instructions

fresh · operator

reference-profile · input revision 2 · CC0 1.0

fresh=={successors[id] : id \in cards}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cards

o · operator

reference-profile · input revision 2 · CC0 1.0

o==objects[old]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old

old · operator

reference-profile · input revision 2 · CC0 1.0

old==CHOOSE old \in cards : successors[old]=id

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cards

due · operator

reference-profile · input revision 2 · CC0 1.0

due=={id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].zone \in {"SideADiscard","SideBDiscard"}}

Exact module download · Source bundle and reproduction instructions

arrivals · operator

reference-profile · input revision 2 · CC0 1.0

arrivals=={entries[id].object : id \in {id \in DOMAIN entries : entries[id].tag="RootEntry" /\ entries[id].siteInspectionId=siteInspection.id /\
                entries[id].serial>previousBoundary /\ entries[id].serial<=currentBoundary /\ entries[id].targetSite=siteInspection.targetSite}}

Exact module download · Source bundle and reproduction instructions

observed · operator

reference-profile · input revision 2 · CC0 1.0

observed==[capacity EXCEPT !.admittedRoots=(@ \cap InspectionRootCards7(siteInspection,objects)) \ arrivals,
                    !.pendingRoots=(@ \cup arrivals) \cap InspectionRootCards7(siteInspection,objects)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: arrivals, InspectionRootCards7

rest · operator

reference-profile · input revision 2 · CC0 1.0

rest==SubSeq(before.owed,2,Len(before.owed))

Exact module download · Source bundle and reproduction instructions

activeCards · operator

reference-profile · input revision 2 · CC0 1.0

activeCards==active \cap {id \in DOMAIN objects : objects[id].form="Card"}

Exact module download · Source bundle and reproduction instructions

consoleGroups · operator

reference-profile · input revision 2 · CC0 1.0

consoleGroups=={{id \in consoles \cap DOMAIN objects : objects[id].deployed /\ controllers[id]=player} : player \in SetupPlayers}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

groups · operator

reference-profile · input revision 2 · CC0 1.0

groups=={group \in uniqueGroups \cup consoleGroups : Cardinality(group)>1}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: consoleGroups, uniqueGroups

mixed · operator

reference-profile · input revision 2 · CC0 1.0

mixed==\E name \in uniqueNames : \E id \in activeCards \ unique : names[id]=name

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: activeCards, uniqueNames

supported · operator

reference-profile · input revision 2 · CC0 1.0

supported==~mixed /\ \A group \in groups : CheckpointLatestExists103(group,activationOrder)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: groups, mixed, CheckpointLatestExists103

uniqueGroups · operator

reference-profile · input revision 2 · CC0 1.0

uniqueGroups=={{id \in unique \cap activeCards : names[id]=name} : name \in uniqueNames}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: activeCards, uniqueNames

uniqueNames · operator

reference-profile · input revision 2 · CC0 1.0

uniqueNames=={names[id] : id \in unique \cap activeCards}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: activeCards

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==CheckpointUniquePlan103(objects,names,unique,active,consoles,controllers,activationOrder)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointUniquePlan103

result · operator

reference-profile · input revision 2 · CC0 1.0

result==CheckpointObjectiveOutcome103(objects,effectivePoints)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointObjectiveOutcome103

count · operator

reference-profile · input revision 2 · CC0 1.0

count==Cardinality(decision.aHand)

Exact module download · Source bundle and reproduction instructions

total · operator

reference-profile · input revision 2 · CC0 1.0

total==SabotageTotal1012(world,packet.amount)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SabotageTotal1012

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==ConversionExitPlan101(c,printed,sourceObjects[oldObject].zone,destination,movement)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConversionExitPlan101

choices · operator

reference-profile · input revision 2 · CC0 1.0

choices==PublicChoiceFacts102(actualOpenRememberedChoices,snapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PublicChoiceFacts102

keys · operator

reference-profile · input revision 2 · CC0 1.0

keys=={<<"CardProfile",id>> : id \in {i \in DOMAIN objects : objects[i].form="Card"}} \cup
           {<<"ZoneCount",z>> : z \in {"SideAHand","SideADeck","SideBHand","SideBDeck"}} \cup
           {<<"ResourceUnitPool",p>> : p \in SetupPlayers} \cup
           {<<"Choice",id>> : id \in DOMAIN actualOpenRememberedChoices}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

e · operator

reference-profile · input revision 2 · CC0 1.0

e==context.actualEffects[id]

Exact module download · Source bundle and reproduction instructions

link · operator

reference-profile · input revision 2 · CC0 1.0

link==world.loadLinks[key]

Exact module download · Source bundle and reproduction instructions

candidates · operator

reference-profile · input revision 2 · CC0 1.0

candidates==IF spec.mode="Chosen" THEN admission.announced \cap ChargeSet1010(world,spec) ELSE {spec.particular}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ChargeSet1010

initial · operator

reference-profile · input revision 2 · CC0 1.0

initial==IF spec.mode="Particular" THEN {id \in legal : admission.initialPower[id]} ELSE legal

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: legal

legal · operator

reference-profile · input revision 2 · CC0 1.0

legal=={id \in candidates : id \in DOMAIN admission.physical /\ id \in DOMAIN world.objects /\ world.objects[id].card=admission.physical[id] /\ ChargePower1010(world.objects,id)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: candidates, ChargePower1010

d · operator

reference-profile · input revision 2 · CC0 1.0

d==declarations[id]

Exact module download · Source bundle and reproduction instructions

d · operator

reference-profile · input revision 2 · CC0 1.0

d==declarations[id]

Exact module download · Source bundle and reproduction instructions

virtual · operator

reference-profile · input revision 2 · CC0 1.0

virtual==LiabilityMarkerIds106(world.objects) \ MovableLiabilityMarkerIds106(world.objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiabilityMarkerIds106, MovableLiabilityMarkerIds106

d · operator

reference-profile · input revision 2 · CC0 1.0

d==declarations[id]

Exact module download · Source bundle and reproduction instructions

definition · operator

reference-profile · input revision 2 · CC0 1.0

definition==LinkDefinition107(world,object)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: object, LinkDefinition107

eligible · operator

reference-profile · input revision 2 · CC0 1.0

eligible==EligiblePrintedLinkSources107(world)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EligiblePrintedLinkSources107

object · operator

reference-profile · input revision 2 · CC0 1.0

object==world.objects[source]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: source

printed · operator

reference-profile · input revision 2 · CC0 1.0

printed=={id \in DOMAIN declarations : declarations[id].origin="PrintedLink"}

Exact module download · Source bundle and reproduction instructions

source · operator

reference-profile · input revision 2 · CC0 1.0

source==d.projection.source.object

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: d

keys · operator

reference-profile · input revision 2 · CC0 1.0

keys=={key \in DOMAIN before.persistent : before.persistent[key].phase="Persisting" /\ before.persistent[key].traversalId=afterEnd.traversal.id}

Exact module download · Source bundle and reproduction instructions

first · operator

reference-profile · input revision 2 · CC0 1.0

first==DamageOwnerMoveMap104(objects,sideB,[id \in sideB |-> successors[id]],"SideB")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: sideB, DamageOwnerMoveMap104

sideA · operator

reference-profile · input revision 2 · CC0 1.0

sideA==selected \ sideB

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: sideB

sideB · operator

reference-profile · input revision 2 · CC0 1.0

sideB=={id \in selected : owners[objects[id].card]="SideB"}

Exact module download · Source bundle and reproduction instructions

sideBFresh · operator

reference-profile · input revision 2 · CC0 1.0

sideBFresh=={successors[id] : id \in sideB}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: sideB

amount · operator

reference-profile · input revision 2 · CC0 1.0

amount==IF packet.damageType="PersistentCapacityHarm" THEN packet.amount ELSE 0

Exact module download · Source bundle and reproduction instructions

fresh · operator

reference-profile · input revision 2 · CC0 1.0

fresh=={successors[id] : id \in selected}

Exact module download · Source bundle and reproduction instructions

effect · operator

reference-profile · input revision 2 · CC0 1.0

effect==context.actualEffects[id]

Exact module download · Source bundle and reproduction instructions

result · operator

reference-profile · input revision 2 · CC0 1.0

result==IF before.strengths["SideA"].value>before.strengths["SideB"].value THEN "Successful" ELSE "Unsuccessful"

Exact module download · Source bundle and reproduction instructions

binding · operator

reference-profile · input revision 2 · CC0 1.0

binding==world.dividendBindings[event.scored.objectiveCompletionId]

Exact module download · Source bundle and reproduction instructions

capture · operator

reference-profile · input revision 2 · CC0 1.0

capture==world.dividendCaptures[event.scored.objectiveCompletionId]

Exact module download · Source bundle and reproduction instructions

scope · operator

reference-profile · input revision 2 · CC0 1.0

scope==CASE before.phase="BaseCostCheckpoint" -> "BaseCost" [] before.phase="AdditionalCostCheckpoint" -> "AdditionalCost" [] OTHER -> "Effect"

Exact module download · Source bundle and reproduction instructions

p · operator

reference-profile · input revision 2 · CC0 1.0

p==world.escalatingResourceContestLinkPolicies[id]

Exact module download · Source bundle and reproduction instructions

p · operator

reference-profile · input revision 2 · CC0 1.0

p==world.escalatingResourceContestOrderPolicies[id]

Exact module download · Source bundle and reproduction instructions

a · operator

reference-profile · input revision 2 · CC0 1.0

a==effect.associations[clause]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: effect

effect · operator

reference-profile · input revision 2 · CC0 1.0

effect==context.actualEffects[id]

Exact module download · Source bundle and reproduction instructions

player · operator

reference-profile · input revision 2 · CC0 1.0

player==before.pendingPlayer

Exact module download · Source bundle and reproduction instructions

value · operator

reference-profile · input revision 2 · CC0 1.0

value==IF player="SideA" THEN before.packet.base+before.boosts[player].amount ELSE contextualLink+before.boosts[player].amount

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: player

created · operator

reference-profile · input revision 2 · CC0 1.0

created==IF e.kind="RemoveCounters" THEN {} ELSE first..(first+e.value-1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: e, first

e · operator

reference-profile · input revision 2 · CC0 1.0

e==context.actualEffects[id]

Exact module download · Source bundle and reproduction instructions

first · operator

reference-profile · input revision 2 · CC0 1.0

first==world.nextCounterObject

Exact module download · Source bundle and reproduction instructions

history · operator

reference-profile · input revision 2 · CC0 1.0

history==[tag |-> "CompletedLoad",host |-> e.target,kind |-> e.counterKind,loadDefinition |-> e.loadDefinition,
             reference |-> reference,sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA,amount |-> e.value,createdCounterIds |-> created,snapshotId |-> world.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: created, e

stage · operator

reference-profile · input revision 2 · CC0 1.0

stage==IF before.guess="NoValue" THEN "Selection" ELSE "Guess"

Exact module download · Source bundle and reproduction instructions

e · operator

reference-profile · input revision 2 · CC0 1.0

e==world.history[id]

Exact module download · Source bundle and reproduction instructions

blueprint · operator

reference-profile · input revision 2 · CC0 1.0

blueprint==MarkBlueprint1011(context.currentRef.source,IF origin.plan.origin="Rule" THEN "Rule" ELSE origin.parent.kind,targetSite,cutoff,before.turn.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cutoff, targetSite, MarkBlueprint1011

cutoff · operator

reference-profile · input revision 2 · CC0 1.0

cutoff==before.eventSerial+1

Exact module download · Source bundle and reproduction instructions

event · operator

reference-profile · input revision 2 · CC0 1.0

event==[id |-> eventId,kind |-> "MarkDesignated",serial |-> cutoff,turn |-> before.turn.id,targetSite |-> targetSite,effectId |-> effectId,reference |-> context.currentRef,source |-> context.currentRef.source]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cutoff, targetSite

targetSite · operator

reference-profile · input revision 2 · CC0 1.0

targetSite==draw.targetSite

Exact module download · Source bundle and reproduction instructions

objects · operator

reference-profile · input revision 2 · CC0 1.0

objects==UNION choices

Exact module download · Source bundle and reproduction instructions

players · operator

reference-profile · input revision 2 · CC0 1.0

players=={controllers[id] : id \in objects}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: objects

cards · operator

reference-profile · input revision 2 · CC0 1.0

cards=={id \in selected : objects[id].card#"none"}

Exact module download · Source bundle and reproduction instructions

actual · operator

reference-profile · input revision 2 · CC0 1.0

actual==IF kept THEN context.actualEffects[id] ELSE original

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: kept, original

kept · operator

reference-profile · input revision 2 · CC0 1.0

kept==id \in DOMAIN context.actualEffects

Exact module download · Source bundle and reproduction instructions

original · operator

reference-profile · input revision 2 · CC0 1.0

original==context.templates[id]

Exact module download · Source bundle and reproduction instructions

definition · operator

reference-profile · input revision 2 · CC0 1.0

definition==LinkDefinition107(world,object)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: object, LinkDefinition107

object · operator

reference-profile · input revision 2 · CC0 1.0

object==world.objects[world.sideBProfile]

Exact module download · Source bundle and reproduction instructions

properties · operator

reference-profile · input revision 2 · CC0 1.0

properties==SideBCharacteristics8(object,world.properties[world.sideBProfile])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: object, SideBCharacteristics8

h · operator

reference-profile · input revision 2 · CC0 1.0

h==world.loadHistory[id]

Exact module download · Source bundle and reproduction instructions

kind · operator

reference-profile · input revision 2 · CC0 1.0

kind==CASE rule.role="FirstSuccess" -> "TraversalSuccessful" [] rule.role="FirstTraversalEnd" -> "TraversalEnded" [] OTHER -> "EncounterBarrier"

Exact module download · Source bundle and reproduction instructions

mark · operator

reference-profile · input revision 2 · CC0 1.0

mark==row.mark

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: row

matches · operator

reference-profile · input revision 2 · CC0 1.0

matches==HistoricalMark1011(world,mark) /\ event.kind=kind /\ event.actor="SideB" /\
          IF rule.role="EncounterDuringMarkTraversal" THEN event.id \in MarkRelatedEvents1011(world,mark,"EncounterBarrier")
          ELSE FirstMarkEvent1011(world,mark,kind,event.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: kind, mark, FirstMarkEvent1011, HistoricalMark1011, MarkRelatedEvents1011

row · operator

reference-profile · input revision 2 · CC0 1.0

row==world.history[event.id]

Exact module download · Source bundle and reproduction instructions

e · operator

reference-profile · input revision 2 · CC0 1.0

e==context.actualEffects[operation]

Exact module download · Source bundle and reproduction instructions

id · operator

reference-profile · input revision 2 · CC0 1.0

id==CHOOSE id \in ids : TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ids

ids · operator

reference-profile · input revision 2 · CC0 1.0

ids==LiveMarkIds1011(world.lingering,a.current)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiveMarkIds1011

value · operator

reference-profile · input revision 2 · CC0 1.0

value==world.lingering.effects[id].value

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: id

e · operator

reference-profile · input revision 2 · CC0 1.0

e==registry.effects[id]

Exact module download · Source bundle and reproduction instructions

e · operator

reference-profile · input revision 2 · CC0 1.0

e==world.history[id]

Exact module download · Source bundle and reproduction instructions

mark · operator

reference-profile · input revision 2 · CC0 1.0

mark==row.mark

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: row

row · operator

reference-profile · input revision 2 · CC0 1.0

row==world.history[event.id]

Exact module download · Source bundle and reproduction instructions

siteInspections · operator

reference-profile · input revision 2 · CC0 1.0

siteInspections=={id \in MarkRelatedEvents1011(world,mark,"Inspection") : world.history[id].traversalId=row.traversalId /\ world.history[id].serial<=row.serial}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mark, row, MarkRelatedEvents1011

e · operator

reference-profile · input revision 2 · CC0 1.0

e==registry.effects[id]

Exact module download · Source bundle and reproduction instructions

local · operator

reference-profile · input revision 2 · CC0 1.0

local==[afterRegistry EXCEPT !.frontier=beforeRegistry.frontier]

Exact module download · Source bundle and reproduction instructions

canonicalOpening · operator

reference-profile · input revision 2 · CC0 1.0

canonicalOpening==[opening EXCEPT !.completion=opening.completion]

Exact module download · Source bundle and reproduction instructions

pending · operator

reference-profile · input revision 2 · CC0 1.0

pending=={id \in DOMAIN before.recognized : ledger.instances[id].status="Pending"}

Exact module download · Source bundle and reproduction instructions

raw · operator

reference-profile · input revision 2 · CC0 1.0

raw==Append(beforeStack,NewPriorityWindow9(opening.windowId,"Reaction",PriorityOpeningSite9(beforeStack,site),
                   before.recognized,opening.group,opening.beginning,opening.instruction,opening.effectRevision))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, PriorityOpeningSite9

fund · operator

reference-profile · input revision 2 · CC0 1.0

fund==IF player="SideB" /\ EscalatingResourceContestDuringTraversal108(world) THEN LiabilityMarkerFundIds106(world.objects) ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestDuringTraversal108, LiabilityMarkerFundIds106

hosted · operator

reference-profile · input revision 2 · CC0 1.0

hosted==UNION {permissions[id].counters : id \in DOMAIN permissions}

Exact module download · Source bundle and reproduction instructions

action · operator

reference-profile · input revision 2 · CC0 1.0

action==NewAction5(before.id,before.player,ExposureMarkerActionKey105(before.kind))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerActionKey105, NewAction5

newEvents · operator

reference-profile · input revision 2 · CC0 1.0

newEvents==[cost \in DOMAIN assignments |-> MovementEvent8(eventIds[cost],"Retire",assignments[cost])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MovementEvent8

selected · operator

reference-profile · input revision 2 · CC0 1.0

selected==UNION {assignments[id] : id \in DOMAIN assignments}

Exact module download · Source bundle and reproduction instructions

costs · operator

reference-profile · input revision 2 · CC0 1.0

costs==IF before.kind="RetireResource" /\ ~removed /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions THEN world.additionalResourceCosts ELSE [key \in {} |-> key]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: removed, ResourceTargetIds105

removed · operator

reference-profile · input revision 2 · CC0 1.0

removed==id \notin DOMAIN context.actualEffects

Exact module download · Source bundle and reproduction instructions

unit · operator

reference-profile · input revision 2 · CC0 1.0

unit==CHOOSE unit \in DOMAIN allocation : allocation[unit]=id

Exact module download · Source bundle and reproduction instructions

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==PurgeClusterPlan101(objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PurgeClusterPlan101

targets · operator

reference-profile · input revision 2 · CC0 1.0

targets==PurgeClusterIds101(objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PurgeClusterIds101

card · operator

reference-profile · input revision 2 · CC0 1.0

card==world.definitions[world.objects[objective].card]

Exact module download · Source bundle and reproduction instructions

sources · operator

reference-profile · input revision 2 · CC0 1.0

sources=={id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].kind="Attachment" /\ world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.objects[id].activated /\ world.objects[id].face="Up" /\
          world.definitions[world.objects[id].card]="Specimen0208" /\ world.objects[id].area="Root" /\ world.objects[id].targetSite=world.objects[objective].targetSite /\ world.objects[objective].deployed /\ world.objects[objective].area="Root"}

Exact module download · Source bundle and reproduction instructions

moved · operator

reference-profile · input revision 2 · CC0 1.0

moved=={frame.successors[id] : id \in DOMAIN frame.successors}

Exact module download · Source bundle and reproduction instructions

advanced · operator

reference-profile · input revision 2 · CC0 1.0

advanced==[after EXCEPT !.recognition=before.recognition,!.recognized=before.recognized]

Exact module download · Source bundle and reproduction instructions

current · operator

reference-profile · input revision 2 · CC0 1.0

current=={IF id \in DOMAIN hostedSuccessors THEN hostedSuccessors[id] ELSE id : id \in hosted}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: hosted

hosted · operator

reference-profile · input revision 2 · CC0 1.0

hosted=={id \in DOMAIN beforeObjects : beforeObjects[id].host=source}

Exact module download · Source bundle and reproduction instructions

objectiveCompletionLeft · operator

reference-profile · input revision 2 · CC0 1.0

objectiveCompletionLeft==beforeObjects[source].form="Card" /\ beforeObjects[source].kind="Objective" /\
                   beforeObjects[source].zone \in SetupObjectiveZones /\ afterObjects[sourceAfter].zone \notin SetupObjectiveZones

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupObjectiveZones

uninstalled · operator

reference-profile · input revision 2 · CC0 1.0

uninstalled==beforeObjects[source].form="Card" /\ beforeObjects[source].deployed /\ ~afterObjects[sourceAfter].deployed

Exact module download · Source bundle and reproduction instructions

w · operator

reference-profile · input revision 2 · CC0 1.0

w==WindowTop9(beforeStack)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9

targets · operator

reference-profile · input revision 2 · CC0 1.0

targets==CurrentChargeTargets1010(world,admission,spec)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CurrentChargeTargets1010

cardsAfter · operator

reference-profile · input revision 2 · CC0 1.0

cardsAfter==DamageOwnerMoveMap104(
           DamageOwnerMoveMap104(objects,{id \in before.selected : owners[objects[id].card]="SideB"},
             [id \in {i \in before.selected : owners[objects[i].card]="SideB"} |-> successors[id]],"SideB"),
           {id \in before.selected : owners[objects[id].card]="SideA"},
             [id \in {i \in before.selected : owners[objects[i].card]="SideA"} |-> successors[id]],"SideA")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageOwnerMoveMap104

damageEvent · operator

reference-profile · input revision 2 · CC0 1.0

damageEvent==DamageSufferedEvent104(before,batchId,successors)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageSufferedEvent104

fresh · operator

reference-profile · input revision 2 · CC0 1.0

fresh=={successors[id] : id \in before.selected}

Exact module download · Source bundle and reproduction instructions

movementEvents · operator

reference-profile · input revision 2 · CC0 1.0

movementEvents=={MovementEvent8(batchId,"Retire",before.selected)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MovementEvent8

blocked · operator

reference-profile · input revision 2 · CC0 1.0

blocked==IF before.kind="RetireResource" THEN world.currentRetireProhibitions ELSE world.currentExposureMarkerRemovalProhibitions

Exact module download · Source bundle and reproduction instructions

cards · operator

reference-profile · input revision 2 · CC0 1.0

cards=={id \in due : world.objects[id].card#"none"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: due

due · operator

reference-profile · input revision 2 · CC0 1.0

due==IF before.effective.mode="Kept" /\ before.target \in ExposureMarkerActionTargets105(before,world) /\ before.target \notin blocked THEN {before.target} ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: blocked, ExposureMarkerActionTargets105

event · operator

reference-profile · input revision 2 · CC0 1.0

event==SabotageRetireEvent1012(eventId,before,world,afterId,successors)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SabotageRetireEvent1012

selected · operator

reference-profile · input revision 2 · CC0 1.0

selected==SabotageSelected1012(before,world)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SabotageSelected1012

c · operator

reference-profile · input revision 2 · CC0 1.0

c==frame.effectCosts[id]

Exact module download · Source bundle and reproduction instructions

observed · operator

reference-profile · input revision 2 · CC0 1.0

observed=={costs[id].source.object : id \in {id \in DOMAIN costs : costs[id].source.object \in DOMAIN world.objects /\
          world.objects[costs[id].source.object].card \in {"Specimen0212","Specimen0136"}}}

Exact module download · Source bundle and reproduction instructions

required · operator

reference-profile · input revision 2 · CC0 1.0

required==ResourceKnownCostSources105(world,target,cardFacts)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ResourceKnownCostSources105

due · operator

reference-profile · input revision 2 · CC0 1.0

due=={id \in DOMAIN objects \cap DOMAIN conversions : objects[id].zone \in {"SideADiscard","SideBDiscard"} /\ objects[id].card#"none"}

Exact module download · Source bundle and reproduction instructions

e · operator

reference-profile · input revision 2 · CC0 1.0

e==context.actualEffects[operation]

Exact module download · Source bundle and reproduction instructions

matched · operator

reference-profile · input revision 2 · CC0 1.0

matched==event.actor=rule.role.actor /\ (IF rule.role.scope="CentralABatch" THEN event.unit=0 /\ event.batch.fromCentralA#{} ELSE event.unit \in event.batch.objects)

Exact module download · Source bundle and reproduction instructions

index · operator

reference-profile · input revision 2 · CC0 1.0

index==Len(before.selectionOrder)+1

Exact module download · Source bundle and reproduction instructions

selected · operator

reference-profile · input revision 2 · CC0 1.0

selected==before.selected \cup {card}

Exact module download · Source bundle and reproduction instructions

slot · operator

reference-profile · input revision 2 · CC0 1.0

slot==before.policy.slots[index]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: index

selections · operator

reference-profile · input revision 2 · CC0 1.0

selections==ReplacementOverlay99(before.selections,[p \in {player} |-> amount])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99

effect · operator

reference-profile · input revision 2 · CC0 1.0

effect==context.actualEffects[id]

Exact module download · Source bundle and reproduction instructions

applicable · operator

reference-profile · input revision 2 · CC0 1.0

applicable == newlyActive \in DOMAIN objects /\ newlyActive \in DOMAIN names /\
                   newlyActive \in unique /\ newlyActive \notin beforeActive /\ newlyActive \in afterActive

Exact module download · Source bundle and reproduction instructions

cohort · operator

reference-profile · input revision 2 · CC0 1.0

cohort == IF newlyActive \in DOMAIN names
               THEN {i \in ((afterActive \ beforeActive) \cap DOMAIN objects \cap DOMAIN names) : names[i]=names[newlyActive]}
               ELSE {}

Exact module download · Source bundle and reproduction instructions

disposition · operator

reference-profile · input revision 2 · CC0 1.0

disposition == IF ~applicable THEN "NotApplicable"
                    ELSE IF cohort={newlyActive} THEN "Supported" ELSE "UnsupportedSimultaneousActivation"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: applicable, cohort

AnnounceChargeTargets1010 · operator

reference-profile · input revision 2 · CC0 1.0

AnnounceChargeTargets1010(before,after,ability,world,cardFacts,spec,targets,receipt) ==
 /\ ChargeSpec1010(world,InstructionWindowRef93(before),cardFacts,spec) /\ spec.mode="Chosen" /\ before.requiresTargets
 /\ targets \subseteq ChargeEligible1010(world,spec) /\ Cardinality(targets)=MinOf(spec.requested,Cardinality(ChargeEligible1010(world,spec)))
 /\ receipt=ChargeTargetReceipt1010(before,targets)
 /\ AnnounceInstructionTargets93(before,after,receipt,ability,"NoValue")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AnnounceInstructionTargets93, InstructionWindowRef93, ChargeEligible1010, ChargeSpec1010, ChargeTargetReceipt1010, MinOf

AnnounceExposureMarkerTarget105 · operator

reference-profile · input revision 2 · CC0 1.0

AnnounceExposureMarkerTarget105(before,after,world,target,instructionId) ==
 /\ before.phase="Targets" /\ before.action.status="Effects" /\ world.outcome="Playing" /\ instructionId \in Nat \ {0}
 /\ IF ExposureMarkerActionTargets105(before,world)={} THEN target=0 ELSE target \in ExposureMarkerActionTargets105(before,world)
 /\ after=[before EXCEPT !.phase="Targeted",!.target=target,!.instruction=instructionId]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerActionTargets105

ApplyDividendPlacement1013 · operator

reference-profile · input revision 2 · CC0 1.0

ApplyDividendPlacement1013(before,after,context,world,next,selected,added,eventId,event) ==
 /\ world.outcome="Playing" /\ DividendPlanBound1013(world,before) /\ ~before.complete /\ before.cursor \in 1..before.basis.repetitions /\ DividendTargetStatus1013(world,before)="SupportedPlacementTarget"
 /\ context.id=before.instance /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ context.currentRef=before.reference
 /\ DividendApplicationSupport1013(before,context)="SupportedOrdinaryPlacementApplications"
 /\ context.actualEffects[before.cursor].value=before.basis.multiplier
 /\ ExecuteBankHostedCounterInstruction109(context,before.reference,world,before.cursor,world.cardFacts,next.objects,next.loadHistory,next.completedCounterInstructions,selected,added,next.nextCounterObject,eventId,event)
 /\ next.id \in (Nat \ {0}) \ world.usedWorlds
 /\ next=[world EXCEPT !.id=next.id,!.objects=next.objects,!.loadHistory=next.loadHistory,!.completedCounterInstructions=next.completedCounterInstructions,!.nextCounterObject=next.nextCounterObject,
       !.usedObjects=@ \cup DOMAIN added,!.usedWorlds=@ \cup {next.id},!.counterEventIds=@ \cup {eventId},!.dividendPlacementEvents=ReplacementOverlay99(@,[id \in {eventId} |-> event])]
 /\ after=[before EXCEPT !.cursor=@+1,!.applied=@ \cup {before.cursor},!.totalPlaced=@+before.basis.multiplier]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, DividendApplicationSupport1013, DividendPlanBound1013, DividendTargetStatus1013, ExecuteBankHostedCounterInstruction109

AppropriateRetireSets103 · operator

reference-profile · input revision 2 · CC0 1.0

AppropriateRetireSets103(eligible,LegalAfterRetire(_)) ==
 {selected \in SUBSET eligible : LegalAfterRetire(selected) /\ \A smaller \in SUBSET selected : smaller#selected => ~LegalAfterRetire(smaller)}

Exact module download · Source bundle and reproduction instructions

BaseSideBPoolIds106 · operator

reference-profile · input revision 2 · CC0 1.0

BaseSideBPoolIds106(objects) ==
 {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ResourceUnit" /\ objects[id].host=0 /\
      (objects[id].zone="SideBResourceUnits" \/ (objects[id].zone="Play" /\ objects[id].resourceUnitLocation="SideBPool"))}

Exact module download · Source bundle and reproduction instructions

BeginBid1014 · operator

reference-profile · input revision 2 · CC0 1.0

BeginBid1014(context,reference,world,operation,cardFacts,id,packet,frame,frames,usedFrames) ==
 /\ BidPacket1014(context,reference,world,operation,cardFacts,packet) /\ BidWalletFresh1014(world)
 /\ id \in (Nat \ {0}) \ (DOMAIN world.bidFrames \cup world.usedBidFrames)
 /\ ~\E previous \in DOMAIN world.bidFrames : world.bidFrames[previous].packet.key=packet.key
 /\ usedFrames=world.usedBidFrames \cup {id}
 /\ frame=BidInitial1014(id,packet,world) /\ frames=ReplacementOverlay99(world.bidFrames,[key \in {id} |-> frame])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, BidInitial1014, BidPacket1014, BidWalletFresh1014

BeginCheckpointSite103 · operator

reference-profile · input revision 2 · CC0 1.0

BeginCheckpointSite103(beforeSites,afterSites,beforeFrames,afterFrames,frame,id,site,event,insideStructures) ==
 /\ CheckpointSiteKey103(site) \notin beforeSites
 /\ \A old \in DOMAIN beforeFrames : beforeFrames[old].phase \notin {"Steps","Completed"}
 /\ OpenCheckpointAtSite103(frame,id,site,event,insideStructures,DOMAIN beforeFrames)
 /\ afterSites=beforeSites \cup {CheckpointSiteKey103(site)}
 /\ afterFrames=[key \in DOMAIN beforeFrames \cup {id} |-> IF key=id THEN frame ELSE beforeFrames[key]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointSiteKey103, OpenCheckpointAtSite103

BeginDamage104 · operator

reference-profile · input revision 2 · CC0 1.0

BeginDamage104(context,reference,world,id,cardFacts,packet,frame,usedPackets,afterOutcome,actualOtherWinners) ==
 /\ DamagePacketFromExpected104(context,reference,world,id,cardFacts,packet) /\ packet.key \notin usedPackets
 /\ actualOtherWinners \subseteq SetupPlayers
 /\ LET bHand==DamageBHand104(world.objects)
        fatal==packet.amount>Cardinality(bHand)
    IN /\ (~fatal => actualOtherWinners={})
       /\ afterOutcome=IF fatal THEN (IF "SideB" \in actualOtherWinners THEN "Draw" ELSE "SideA") ELSE "Playing"
       /\ frame=[packet |-> packet,beforeObjects |-> world.objects,bHand |-> bHand,selected |-> {},selectionOrder |-> <<>>,
            selections |-> <<>>,policy |-> [id |-> 0],phase |-> IF fatal THEN "EliminatedByHarm" ELSE "Selecting",
            outcome |-> afterOutcome,completion |-> [batchId |-> 0],finalObjects |-> [emptyId \in {} |-> emptyId]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: bHand, fatal, DamagePacketFromExpected104, SetupPlayers

BeginEscalatingResourceContest108 · operator

reference-profile · input revision 2 · CC0 1.0

BeginEscalatingResourceContest108(context,reference,world,id,cardFacts,escalatingResourceContestId,eventId,packet,frame,afterFrames,afterHistory,event) ==
 /\ EscalatingResourceContestPacket108(context,reference,world,id,cardFacts,packet)
 /\ escalatingResourceContestId \in (Nat \ {0}) \ (DOMAIN world.escalatingResourceContestFrames \cup DOMAIN world.escalatingResourceContestHistory)
 /\ \A old \in DOMAIN world.escalatingResourceContestHistory : world.escalatingResourceContestHistory[old].key#packet.key
 /\ eventId \in (Nat \ {0}) \ world.eventIds
 /\ LET ordinal==1+Cardinality({old \in DOMAIN world.escalatingResourceContestHistory : world.escalatingResourceContestHistory[old].turnId=world.turn.id}) IN
    /\ frame=EscalatingResourceContestInitialFrame108(escalatingResourceContestId,packet,world.turn.id,ordinal)
    /\ afterFrames=ReplacementOverlay99(world.escalatingResourceContestFrames,[i \in {escalatingResourceContestId} |-> frame])
    /\ afterHistory=ReplacementOverlay99(world.escalatingResourceContestHistory,[i \in {escalatingResourceContestId} |-> [key |-> packet.key,turnId |-> world.turn.id,ordinal |-> ordinal]])
    /\ event=[id |-> eventId,kind |-> "EscalatingResourceContestInitiated",escalatingResourceContestId |-> escalatingResourceContestId,actor |-> "SideA",source |-> packet.source,reference |-> reference,snapshotId |-> world.id]
    /\ InstructionPausePoint911([id |-> reference.abilityInstance],reference,context,"EscalatingResourceContest",frame,"ProcedureCoded1e36ce96789",id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionPausePoint911, ReplacementOverlay99, ordinal, EscalatingResourceContestInitialFrame108, EscalatingResourceContestPacket108

BeginExampleFamily009Damage104 · operator

reference-profile · input revision 2 · CC0 1.0

BeginExampleFamily009Damage104(before,after,objects,authority,compiled,cardFacts,actualDamageHistory) ==
 /\ BeginSequentialDamage104(before,after,objects,authority,compiled,cardFacts)
 /\ ExampleFamily009SelectionShape104(before.packet,authority,actualDamageHistory)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginSequentialDamage104, ExampleFamily009SelectionShape104

BeginSequentialDamage104 · operator

reference-profile · input revision 2 · CC0 1.0

BeginSequentialDamage104(before,after,objects,authority,compiled,cardFacts) ==
 /\ before.phase="Selecting" /\ before.outcome="Playing" /\ objects=before.beforeObjects /\ before.selected={}
 /\ authority.id \in DOMAIN compiled /\ compiled[authority.id]=authority /\ authority.tag="SourceBoundDamageSelectionOverride"
 /\ authority.packet=before.packet.key /\ authority.reference=before.packet.reference /\ authority.snapshotId=before.packet.snapshotId
 /\ authority.source.kind="Object" /\ authority.source.object \in DOMAIN objects
 /\ authority.card \in DOMAIN cardFacts /\ authority.sourceSHA=cardFacts[authority.card].sourceSHA
 /\ authority.sourceObject=objects[authority.source.object]
 /\ authority.sourceObject.card=authority.card
 /\ Len(authority.slots)=before.packet.amount
 /\ \A i \in 1..Len(authority.slots) : authority.slots[i].mode \in {"Random","Choose"} /\ authority.slots[i].actor \in SetupPlayers
       /\ (authority.slots[i].mode="Random" => authority.slots[i].actor=before.packet.responsible)
 /\ after=[before EXCEPT !.policy=authority,!.phase="SelectingSequentially"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

BidCheckpointReady1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidCheckpointReady1014(frame,world,checkpoint,ledger) ==
 /\ world.outcome="Playing" /\ world.bidOwners[frame.id]=frame.caller
 /\ frame.phase="PaidCheckpointDue" /\ frame.paid /\ frame.id \in DOMAIN world.bidFrames /\ world.bidFrames[frame.id]=frame
 /\ checkpoint.id \in DOMAIN world.checkpoints /\ world.checkpoints[checkpoint.id]=checkpoint /\ checkpoint.site=BidCheckpointSite1014(frame)
 /\ checkpoint.caller=BidCheckpointSite1014(frame) /\ checkpoint.returned /\ CheckpointDrained103(checkpoint,ledger,<<>>) /\ world.conditionalLedger=ledger
 /\ \A p \in frame.packet.participants :
      /\ frame.transactions[p] \in DOMAIN world.bidCosts /\ world.bidCosts[frame.transactions[p]]=BidCompletedCost1014(frame.costs[p],frame.plans[p])
 /\ {e \in DOMAIN world.bidEvents : world.bidEvents[e].bidId=frame.id}#{}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidCheckpointSite1014, BidCompletedCost1014, CheckpointDrained103

BidCheckpointSite1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidCheckpointSite1014(frame) ==
 [kind |-> "BidBatchPaymentCheckpoint",bidId |-> frame.id,caller |-> frame.caller,paymentInstruction |-> frame.revealCaller,transactions |-> frame.transactions,cause |-> "CostPaid",simultaneousBidComparison |-> frame.packet.kind="SimultaneousBidComparisonGame"]

Exact module download · Source bundle and reproduction instructions

BidCompletedCost1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidCompletedCost1014(cost,selected) ==
 [tag |-> "CompletedCostTransaction",id |-> cost.id,instance |-> cost.instance,instruction |-> cost.instruction,source |-> cost.source,payer |-> cost.payer,
  specification |-> cost.specification,allCostsPaid |-> TRUE,announced |-> TRUE,selected |-> selected,bidId |-> cost.bidId,
  permissionSources |-> {ObjectAbilitySource9(cost.resourceUnitHosts[id]) : id \in {id \in selected : cost.resourceUnitHosts[id]#0}}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9

BidCurrent1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidCurrent1014(frame,world) ==
 /\ frame.id \in DOMAIN world.bidFrames /\ world.bidFrames[frame.id]=frame /\ ~frame.returned /\ world.outcome="Playing"
 /\ world.turn.id=frame.turnId /\ world.turn.owner=frame.active /\ world.bidOwners[frame.id]=frame.caller /\ BidWalletFresh1014(world)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidWalletFresh1014

BidEffectIds1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidEffectIds1014(world,key,definition) ==
 {id \in ActiveLingeringIds910(world.lingering,world.lifetimeAuthority.current) :
   LET e==world.lingering.effects[id] IN
   /\ e.kind="Ordinary" /\ e.choicePolicy="NoValue" /\ e.choiceKey=key /\ e.definitionId=definition
   /\ e.baseDuration=[kind |-> "Timing",ref |-> TimingRef9("SchemaAtom138",world.traversal.id)] /\ e.durationClass="SchemaAtom138"
   /\ e.value.traversalId=world.traversal.id}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActiveLingeringIds910, TimingRef9, e

BidEligibleResourceUnits1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidEligibleResourceUnits1014(world,player,cardFacts) ==
 LET hosted==IF player="SideB" THEN
       UNION {{id \in DOMAIN world.objects : world.objects[id].form="Counter" /\ world.objects[id].kind="ResourceUnit" /\ ~world.objects[id].virtual /\ world.objects[id].host=world.lingering.effects[e].value.host /\ world.objects[id].zone="Play"} :
          e \in {e \in DOMAIN world.lingering.effects : BidHostedPermission1014(world,e,cardFacts)}} ELSE {}
     fund==IF player="SideB" /\ BidTraversalLive1014(world) THEN LiabilityMarkerFundIds106(world.objects) ELSE {}
     candidates==EscalatingResourceContestPoolIds108(world.objects,player) \cup fund \cup hosted
 IN {id \in candidates : id \in CheckpointPhysicalIds103(world.objects) /\ SetupMayUseForCost(player,world.objects[id],LiabilityMarkerFundController106(world.objects[id],world.controllers[id]),FALSE)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: candidates, CheckpointPhysicalIds103, LiabilityMarkerFundController106, SetupMayUseForCost

BidExampleFamily022Ids1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidExampleFamily022Ids1014(world,cardFacts) ==
 {id \in DOMAIN world.bidValueRestrictions :
   LET r==world.bidValueRestrictions[id] IN
   /\ r.tag="CurrentBidValueRestriction" /\ r.snapshotId=world.id /\ r.forbidden=2
   /\ r.ability \in world.activeAbilities /\ world.abilitySources[r.ability]=r.source /\ world.abilityRoles[r.ability]="BidForbidTwo"
   /\ r.source.kind="Object" /\ r.source.object \in DOMAIN world.objects
   /\ r.sourceObject=world.objects[r.source.object] /\ r.sourceSHA=cardFacts["Specimen0102"].sourceSHA
   /\ LinkDefinition107(world,r.sourceObject)="Specimen0102"
   /\ DefaultActive([r.sourceObject EXCEPT !.card="Specimen0102"],world.gameStarted,cardFacts)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: r, LinkDefinition107, DefaultActive

BidExampleFamily022ProjectionValid1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidExampleFamily022ProjectionValid1014(world,cardFacts) ==
 LET sources=={world.abilitySources[id].object : id \in EscalatingResourceContestRoleIds108(world,"BidForbidTwo","Specimen0102")} IN
 /\ DOMAIN world.bidValueRestrictions=sources
 /\ BidExampleFamily022Ids1014(world,cardFacts)=sources
 /\ \A id \in sources : world.bidValueRestrictions[id].source=ObjectAbilitySource9(id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, sources, BidExampleFamily022Ids1014

BidExampleFamily050Lock1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidExampleFamily050Lock1014(world,cardFacts) ==
 BidTraversalLive1014(world) /\ \E id \in BidEffectIds1014(world,"ExampleFamily050SpendLock",141402) :
   LET e==world.lingering.effects[id] IN
   /\ e.value.kind="CannotSpendResourceUnits" /\ e.value.player="SideB"
   /\ e.value.sourceCard="Specimen0205" /\ e.value.sourceSHA=cardFacts["Specimen0205"].sourceSHA

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: e, BidEffectIds1014, BidTraversalLive1014

BidGuessCorrect1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidGuessCorrect1014(frame) ==
 frame.packet.participants={"SideB"} /\ frame.guess \in {"Even","Odd"} /\ frame.paid /\
 IF frame.guess="Even" THEN frame.selections["SideB"] % 2=0 ELSE frame.selections["SideB"] % 2=1

Exact module download · Source bundle and reproduction instructions

BidHostedPermission1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidHostedPermission1014(world,effectId,cardFacts) ==
 LET e==world.lingering.effects[effectId] host==e.value.host IN
 /\ BidTraversalLive1014(world) /\ effectId \in BidEffectIds1014(world,"ExampleFamily019Spend",141401)
 /\ e.source=ObjectAbilitySource9(host) /\ e.target=host /\ e.value.kind="SpendHostedResourceUnits" /\ e.value.player="SideB"
 /\ host \in DOMAIN world.objects /\ world.objects[host].form="Card" /\ world.objects[host].zone="Play"
 /\ LinkDefinition107(world,world.objects[host])="Specimen0089" /\ world.controllers[host]="SideB"
 /\ e.value.sourceSHA=cardFacts["Specimen0089"].sourceSHA

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, e, host, BidEffectIds1014, BidTraversalLive1014, LinkDefinition107

BidInitial1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidInitial1014(id,packet,world) ==
 [tag |-> "OwnedBiddingProcedure",id |-> id,packet |-> packet,caller |-> packet.reference,turnId |-> world.turn.id,active |-> world.turn.owner,
  phase |-> "Selecting",revealCaller |-> packet.reference,generalStages |-> {},generalCheckpoints |-> {},selections |-> [p \in {} |-> p],revealed |-> {},plans |-> [p \in {} |-> p],choiceOrder |-> <<>>,
  guess |-> "NoValue",paymentWorld |-> 0,paymentScope |-> [tag |-> "NoValue"],costs |-> [p \in {} |-> p],transactions |-> [p \in {} |-> p],result |-> "Undetermined",paid |-> FALSE,complete |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

BidInstructionSupport1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidInstructionSupport1014(effect) ==
 IF effect.costProfile="UnmodifiedNestedResourceUnits" THEN "Supported" ELSE "RequiresModifiedNestedCostAdapter"

Exact module download · Source bundle and reproduction instructions

BidMultipleChoicePlayers1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidMultipleChoicePlayers1014(frame,world,cardFacts) ==
 {p \in frame.packet.participants : Cardinality(BidPaymentPlans1014(world,p,frame.selections[p],cardFacts))>1}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidPaymentPlans1014

BidNestedCost1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidNestedCost1014(frame,world,player,transaction) ==
 [tag |-> "BidNestedResourceUnitCost",id |-> transaction,transaction |-> transaction,instance |-> frame.caller.abilityInstance,instruction |-> frame.revealCaller,
  source |-> frame.caller.source,payer |-> player,specification |-> BidNestedSpecification1014(frame,player),bidId |-> frame.id,
  sourceRule |-> "ProcedureCode3b2e1996810a",snapshotId |-> world.id,amount |-> frame.selections[player],status |-> "Paying",optionalInterrupts |-> {},
  resourceUnitHosts |-> [id \in DOMAIN world.objects |-> world.objects[id].host]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidNestedSpecification1014

BidNestedSpecification1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidNestedSpecification1014(frame,player) ==
 <<[category |-> "Nested",kind |-> "ResourceUnit",amount |-> frame.selections[player],eventId |-> <<frame.id,player>>]>>

Exact module download · Source bundle and reproduction instructions

BidObserverCondition1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidObserverCondition1014(rule,event,priorEvents,cardFacts) ==
 CASE rule="BothReveal" -> event.participants=SetupPlayers
   [] rule="FirstReveal" -> "SideA" \in event.participants /\ ~\E id \in DOMAIN priorEvents : priorEvents[id].turnId=event.turnId /\ "SideA" \in priorEvents[id].participants
   [] rule="SideBSpentFromSideATraversalAbility" -> "SideB" \in event.participants /\ event.amounts["SideB"]>0 /\ event.duringTraversal /\ event.sourceCard \in DOMAIN cardFacts /\ cardFacts[event.sourceCard].side="SideA"
   [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

BidObserverRule1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidObserverRule1014(card) ==
 CASE card \in {"Specimen0161","Specimen0096"} -> "BothReveal"
   [] card="Specimen0113" -> "FirstReveal"
   [] card="Specimen0097" -> "SideBSpentFromSideATraversalAbility"
   [] OTHER -> "UnsupportedObserver"

Exact module download · Source bundle and reproduction instructions

BidPacket1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPacket1014(context,reference,world,operation,cardFacts,packet) ==
 /\ cardFacts=world.cardFacts /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \in DOMAIN context.actualEffects /\ operation \in DOMAIN context.templates
 /\ LET e==context.actualEffects[operation] t==context.templates[operation] IN
    /\ BidInstructionSupport1014(e)="Supported" /\ e.kind \in {"SimultaneousBidComparisonGame","SecretBid"} /\ t.kind=e.kind /\ e.baseOrigin=reference.source
    /\ e.sourceCard=t.sourceCard /\ e.sourceSHA=t.sourceSHA /\ e.sourceCard \in DOMAIN cardFacts /\ e.sourceSHA=cardFacts[e.sourceCard].sourceSHA
    /\ e.participants \subseteq SetupPlayers /\ e.participants#{} /\ DOMAIN e.allowed=e.participants /\ \A p \in e.participants : e.allowed[p] \subseteq Nat /\ 0 \in e.allowed[p]
    /\ (e.kind="SimultaneousBidComparisonGame" => e.participants=SetupPlayers /\ e.allowed=[p \in SetupPlayers |-> {0,1,2}] /\ e.reveal="Immediate")
    /\ e.rangeMode \in {"SchemaAtom127","AtMost","AnyAffordable"} /\ (e.kind="SimultaneousBidComparisonGame")=(e.rangeMode="SchemaAtom127")
    /\ e.reveal \in {"Immediate","LaterInstruction"} /\ e.classification \in {"PrintedSimultaneousBidComparison","LegacyPairedSimultaneousBidComparison","GeneralBid"}
    /\ (e.kind="SimultaneousBidComparisonGame")=(e.classification \in {"PrintedSimultaneousBidComparison","LegacyPairedSimultaneousBidComparison"})
    /\ packet=[key |-> <<context.id,reference,operation>>,reference |-> reference,sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA,
       participants |-> e.participants,allowed |-> e.allowed,rangeMode |-> e.rangeMode,kind |-> e.kind,reveal |-> e.reveal,classification |-> e.classification]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, e, t, BidInstructionSupport1014, SetupPlayers

BidPaidFrame1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPaidFrame1014(frame) ==
 [frame EXCEPT !.phase="PaidCheckpointDue",!.paid=TRUE,
   !.result=IF frame.packet.kind="SimultaneousBidComparisonGame" THEN IF frame.selections["SideA"]=frame.selections["SideB"] THEN "Equal" ELSE "Different" ELSE "SingleBid"]

Exact module download · Source bundle and reproduction instructions

BidPaymentEvent1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPaymentEvent1014(frame,world,eventId,snapshot) ==
 [id |-> eventId,kind |-> "BidsRevealedAndPaid",bidId |-> frame.id,source |-> frame.caller.source,sourceCard |-> frame.packet.sourceCard,
  sourceSHA |-> frame.packet.sourceSHA,participants |-> frame.packet.participants,amounts |-> frame.selections,result |-> frame.result,turnId |-> frame.turnId,
  duringTraversal |-> BidTraversalLive1014(world),serial |-> world.bidEventSerial+1,reference |-> frame.caller,snapshot |-> snapshot,transactionIds |-> frame.transactions]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidTraversalLive1014

BidPaymentPlans1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPaymentPlans1014(world,player,amount,cardFacts) ==
 IF amount=0 THEN {{}}
 ELSE IF amount \notin Nat \/ (player="SideB" /\ BidExampleFamily050Lock1014(world,cardFacts)) \/ (amount=2 /\ BidExampleFamily022Ids1014(world,cardFacts)#{}) THEN {}
 ELSE {selected \in SUBSET BidEligibleResourceUnits1014(world,player,cardFacts) : Cardinality(selected)=amount}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidEligibleResourceUnits1014, BidExampleFamily022Ids1014, BidExampleFamily050Lock1014

BidPaymentScope1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPaymentScope1014(world) ==
 [id |-> world.id,objects |-> world.objects,controllers |-> world.controllers,traversal |-> world.traversal,inside |-> world.inside,
  lingering |-> world.lingering,authority |-> world.lifetimeAuthority,restrictions |-> world.bidValueRestrictions,
  definitions |-> world.definitions,facts |-> world.cardFacts,abilities |-> world.activeAbilities,abilitySources |-> world.abilitySources,roles |-> world.abilityRoles,
  printed |-> world.printed,owners |-> world.owners,visible |-> world.visible,usedObjects |-> world.usedObjects,history |-> world.movementHistory]

Exact module download · Source bundle and reproduction instructions

BidPublish1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPublish1014(frame,world,afterWorld,cardFacts,afterObjects,successors,batchId,history,events,receipts,event,eventId,snapshot) ==
 /\ frame.phase="PaidCheckpointDue" /\ frame.paid /\ frame.id \in DOMAIN world.bidFrames /\ world.bidFrames[frame.id].phase="ChoosePayment"
 /\ CommitBidPayments1014(world.bidFrames[frame.id],frame,world,cardFacts,afterObjects,successors,batchId,history,events,receipts)
 /\ snapshot.objects=afterObjects /\ snapshot.id \in (Nat \ {0}) \ world.usedWorlds
 /\ event=BidPaymentEvent1014(frame,world,eventId,snapshot) /\ eventId \in (Nat \ {0}) \ DOMAIN world.bidEvents
 /\ afterWorld=[world EXCEPT !.id=snapshot.id,!.objects=afterObjects,!.movementHistory=history,!.bidFrames[frame.id]=frame,
       !.usedWorlds=@ \cup {snapshot.id},!.usedObjects=@ \cup DOMAIN afterObjects,
       !.controllers=[id \in DOMAIN afterObjects |-> IF id \in DOMAIN world.controllers THEN world.controllers[id] ELSE world.owners[afterObjects[id].card]],
       !.bidEventSerial=@+1,!.usedCostTransactions=@ \cup {frame.transactions[p] : p \in frame.packet.participants},!.bidCosts=ReplacementOverlay99(@,[id \in {frame.transactions[p] : p \in frame.packet.participants} |->
          receipts[CHOOSE p \in frame.packet.participants : frame.transactions[p]=id]]),!.bidEvents=ReplacementOverlay99(@,[id \in {eventId} |-> event])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, BidPaymentEvent1014, CommitBidPayments1014

BidPublished1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidPublished1014(event,world) ==
 /\ event.id \in DOMAIN world.bidEvents /\ world.bidEvents[event.id]=event
 /\ event.bidId \in DOMAIN world.bidFrames /\ world.bidFrames[event.bidId].paid
 /\ LET f==world.bidFrames[event.bidId] IN
    /\ event.kind="BidsRevealedAndPaid" /\ event.source=f.caller.source /\ event.sourceCard=f.packet.sourceCard /\ event.sourceSHA=f.packet.sourceSHA /\ event.reference=f.caller /\ event.turnId=f.turnId
    /\ event.amounts=f.selections /\ event.participants=f.packet.participants /\ event.transactionIds=f.transactions /\ event.result=f.result
    /\ \A p \in event.participants : f.transactions[p] \in DOMAIN world.bidCosts /\ world.bidCosts[f.transactions[p]]=BidCompletedCost1014(f.costs[p],f.plans[p])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f, BidCompletedCost1014

BidReservedCosts1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidReservedCosts1014(world) ==
 world.usedCostTransactions \cup UNION {{world.bidFrames[id].transactions[p] : p \in DOMAIN world.bidFrames[id].transactions} : id \in DOMAIN world.bidFrames}

Exact module download · Source bundle and reproduction instructions

BidRevealSupport1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidRevealSupport1014(frame,world,cardFacts) ==
 IF \A p \in frame.packet.participants : BidPaymentPlans1014(world,p,frame.selections[p],cardFacts)#{}
 THEN "OrdinaryFullPayment" ELSE "RequiresChangedPayabilityAdapter"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidPaymentPlans1014

BidTraversalLive1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidTraversalLive1014(world) == EscalatingResourceContestDuringTraversal108(world) /\ ~world.traversal.complete

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestDuringTraversal108

BidView1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidView1014(frame,player) ==
 [id |-> frame.id,phase |-> frame.phase,committed |-> DOMAIN frame.selections,guess |-> frame.guess,
  knownValues |-> [p \in {p \in DOMAIN frame.selections : p=player \/ p \in frame.revealed} |-> frame.selections[p]],
  sourceChoices |-> IF frame.revealed=frame.packet.participants THEN frame.plans ELSE [p \in {} |-> p]]

Exact module download · Source bundle and reproduction instructions

BidWalletFresh1014 · operator

reference-profile · input revision 2 · CC0 1.0

BidWalletFresh1014(world) ==
 /\ world.bidWalletProfile="PoolFundAndExampleFamily019" /\ LifetimeWorldProjection910(world)=world.lifetimeAuthority.current
 /\ LifetimeReady910(world.lingering,world.lifetimeAuthority)
 /\ world.traversal=world.control.traversal /\ BidExampleFamily022ProjectionValid1014(world,world.cardFacts)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LifetimeReady910, LifetimeWorldProjection910, BidExampleFamily022ProjectionValid1014

CaptureChargeImminence1010 · operator

reference-profile · input revision 2 · CC0 1.0

CaptureChargeImminence1010(plan,ability,world,cardFacts,spec,admission) ==
 /\ InstructionImminentAtOrigin93(plan,ability,"NoValue") /\ ChargeSpec1010(world,InstructionWindowRef93(plan),cardFacts,spec)
 /\ IF spec.mode="Chosen" THEN
       /\ plan.requiresTargets /\ plan.announced /\ plan.targets \subseteq ChargeEligible1010(world,spec)
       /\ Cardinality(plan.targets)=MinOf(spec.requested,Cardinality(ChargeEligible1010(world,spec)))
     ELSE /\ ~plan.requiresTargets /\ plan.targets={}
 /\ LET refs==IF spec.mode="Chosen" THEN plan.targets ELSE {spec.particular}
    IN admission=[tag |-> "ChargeAtImminence",reference |-> InstructionWindowRef93(plan),snapshotId |-> world.id,spec |-> spec,
       announced |-> plan.targets,initialPower |-> [id \in refs |-> ChargePower1010(world.objects,id)],
       physical |-> [id \in refs \cap DOMAIN world.objects |-> world.objects[id].card]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionImminentAtOrigin93, InstructionWindowRef93, refs, ChargeEligible1010, ChargePower1010, ChargeSpec1010, MinOf

CaptureDividendBegin1013 · operator

reference-profile · input revision 2 · CC0 1.0

CaptureDividendBegin1013(world,begin,cardFacts,capture) ==
 /\ begin.id \in DOMAIN world.objectiveCompletionBeginnings /\ begin=world.objectiveCompletionBeginnings[begin.id]
 /\ DividendBeginSupport1013(begin)="SupportedObjectiveCompletionBegin" /\ begin.actor="SideA" /\ begin.point="ObjectiveCompletionBegins" /\ begin.snapshotId=world.id
 /\ begin.object \in DOMAIN world.objects /\ world.objects[begin.object].form="Card" /\ world.objects[begin.object].kind="Objective"
 /\ world.objects[begin.object].zone="Play" /\ world.objects[begin.object].deployed /\ world.objects[begin.object].side="SideA"
 /\ world.objects[begin.object].card \in DOMAIN world.definitions /\ begin.sourceCard=world.definitions[world.objects[begin.object].card]
 /\ DividendFact1013(begin.sourceCard,cardFacts) /\ cardFacts=world.cardFacts
 /\ begin.object \in DOMAIN world.requirements /\ world.requirements[begin.object] \in Int
 /\ begin.object \in DOMAIN world.consideredProgress /\ world.consideredProgress[begin.object] \in Nat
 /\ \A id \in DividendPhysicalProgress1013(world,begin.object) : ~world.objects[id].virtual
 /\ LET fact==DividendFacts1013!DividendPrintedFacts1013[begin.sourceCard]
        physical==DividendPhysicalProgress1013(world,begin.object)
        count==Cardinality(physical)+world.consideredProgress[begin.object]
    IN capture=[tag |-> "DividendObjectiveCompletionBegin",objectiveCompletionId |-> begin.id,beginSnapshot |-> world.id,oldObject |-> begin.object,physical |-> world.objects[begin.object].card,
         sourceCard |-> begin.sourceCard,sourceSHA |-> fact.sourceSHA,requirement |-> world.requirements[begin.object],progress |-> count,
         physicalProgress |-> physical,considered |-> world.consideredProgress[begin.object],multiplier |-> fact.multiplier,excess |-> MaxOf(0,count-world.requirements[begin.object]),beforeObjects |-> world.objects]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: count, fact, physical, DividendBeginSupport1013, DividendFact1013, DividendPhysicalProgress1013, MaxOf

CaptureMarkEvent1011 · operator

reference-profile · input revision 2 · CC0 1.0

CaptureMarkEvent1011(before,after,a,event,mark) ==
 /\ MarkRead1011(before,a,event.actor,mark) /\ event.id \in (Nat \ {0}) \ DOMAIN before.history
 /\ event.id \in DOMAIN before.sourceOccurrences /\ event=before.sourceOccurrences[event.id]
 /\ event.snapshot.id=before.id /\ event.snapshot.objects=before.objects
 /\ event.kind \in {"TraversalSuccessful","TraversalEnded","Inspection","EncounterBarrier"}
 /\ event.journalSerial=before.eventSerial+1 /\ event.turnId=before.turn.id
 /\ event.kind \in {"TraversalSuccessful","TraversalEnded","EncounterBarrier"} => event.targetSite=event.traversal.attacked
 /\ event.kind="EncounterBarrier" => event.traversal=before.control.traversal /\ DuringTraversal6(event.traversal) /\ TimingRef9("SchemaAtom138",event.traversal.id) \in before.inside
 /\ after=[before EXCEPT !.eventSerial=@+1,!.history=ReplacementOverlay99(@,[id \in {event.id} |->
       [id |-> event.id,kind |-> event.kind,serial |-> event.journalSerial,turn |-> event.turnId,targetSite |-> event.targetSite,traversalId |-> event.traversal.id,
        actor |-> event.actor,mark |-> mark,occurrence |-> event]])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, TimingRef9, MarkRead1011, DuringTraversal6

CardProfileFact102 · operator

reference-profile · input revision 2 · CC0 1.0

CardProfileFact102(object,objects,controllers,actualLiveGrants,snapshot) ==
 InformationFact102(objects[object].card,
   {p \in SetupPlayers : DefaultZoneLook4(objects[object].zone,objects[object].face,p,controllers[object])} \cup
       CurrentLookViewers102(object,objects,actualLiveGrants),snapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CurrentLookViewers102, InformationFact102, DefaultZoneLook4, SetupPlayers

ChargeAdmissionKey1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeAdmissionKey1010(context,id) == <<context.id,context.initialRef,id>>

Exact module download · Source bundle and reproduction instructions

ChargeEligible1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeEligible1010(world,spec) == {id \in ChargeSet1010(world,spec) : ChargePower1010(world.objects,id)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ChargePower1010, ChargeSet1010

ChargeOmitted1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeOmitted1010(context,world,id,afterObjects,afterHistory) ==
 /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates /\ context.templates[id].kind="Charge"
 /\ id \notin DOMAIN context.actualEffects /\ afterObjects=world.objects /\ afterHistory=world.loadHistory

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99

ChargePacket1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargePacket1010(context,world,id,cardFacts,admission,currentSpec) ==
 /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ id \in DOMAIN context.templates
 /\ ChargeAdmissionKey1010(context,id) \in DOMAIN world.chargeAdmissions /\ admission=world.chargeAdmissions[ChargeAdmissionKey1010(context,id)]
 /\ admission.tag="ChargeAtImminence" /\ admission.reference=context.initialRef /\ WouldContextKey99(context.initialRef)=WouldContextKey99(context.currentRef)
 /\ ChargeSpec1010(world,context.currentRef,cardFacts,currentSpec) /\ ChargeSameMeaning1010(admission.spec,currentSpec)
 /\ LET e==context.actualEffects[id] IN
    /\ e.kind="Charge" /\ context.templates[id].kind="Charge" /\ e.value=1 /\ e.counterKind="Power"
    /\ e.actor=currentSpec.actor /\ e.baseOrigin=context.currentRef.source
    /\ e.sourceCard=currentSpec.sourceCard /\ e.sourceSHA=currentSpec.sourceSHA
    /\ e.sourceCard=context.templates[id].sourceCard /\ e.sourceSHA=context.templates[id].sourceSHA
    /\ e.admissionKey=ChargeAdmissionKey1010(context,id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, WouldContextKey99, e, ChargeAdmissionKey1010, ChargeSameMeaning1010, ChargeSpec1010

ChargePower1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargePower1010(objects,id) ==
 id \in DOMAIN objects /\ objects[id].form="Card" /\ objects[id].zone \in {"Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ HostedCounterIds109(objects,id,"Power")#{}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostedCounterIds109

ChargeSameMeaning1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeSameMeaning1010(before,after) ==
 /\ before.source=after.source /\ before.sourceCard=after.sourceCard /\ before.sourceSHA=after.sourceSHA /\ before.actor=after.actor
 /\ before.targetView=after.targetView /\ before.targetZone=after.targetZone
 /\ before.mode=after.mode /\ before.requested=after.requested /\ before.ifAble=after.ifAble /\ before.setRule=after.setRule /\ before.particular=after.particular

Exact module download · Source bundle and reproduction instructions

ChargeSet1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeSet1010(world,spec) ==
 LET indicated==IF spec.setRule="YourDeployedCards" THEN
       {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.controllers[id]=spec.actor}
       ELSE spec.compiledSet
 IN {id \in indicated : id \in DOMAIN world.objects /\ world.objects[id].form="Card" /\
        IF spec.targetZone="DefaultDeployed" THEN world.objects[id].deployed ELSE world.objects[id].zone=spec.targetZone}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: indicated

ChargeSpec1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeSpec1010(world,reference,cardFacts,spec) ==
 /\ ChargeSpecKey1010(reference) \in DOMAIN world.chargeSpecs /\ spec=world.chargeSpecs[ChargeSpecKey1010(reference)]
 /\ spec.tag="CurrentChargeSpec" /\ spec.reference=reference /\ spec.snapshotId=world.id
 /\ spec.sourceCard \in DOMAIN cardFacts /\ spec.sourceSHA=cardFacts[spec.sourceCard].sourceSHA
 /\ spec.source=reference.source /\ spec.actor \in SetupPlayers /\ spec.mode \in {"Chosen","Particular"}
 /\ spec.requested \in Nat /\ spec.ifAble \in BOOLEAN /\ spec.setRule \in {"YourDeployedCards","CompiledSet"}
 /\ spec.targetZone \in {"DefaultDeployed","Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ spec.targetView="OrdinaryHosting"
 /\ spec.mode="Particular" => spec.requested=1 /\ spec.particular \in Nat \ {0}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ChargeSpecKey1010, SetupPlayers

ChargeSpecKey1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeSpecKey1010(reference) == WouldContextKey99(reference)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WouldContextKey99

ChargeTargetReceipt1010 · operator

reference-profile · input revision 2 · CC0 1.0

ChargeTargetReceipt1010(plan,targets) ==
 [tag |-> "InstructionTargets",instruction |-> plan.id,abilityInstance |-> plan.abilityInstance,source |-> plan.source,
  sourceZone |-> plan.sourceZone,index |-> plan.index,targets |-> targets,valid |-> TRUE]

Exact module download · Source bundle and reproduction instructions

CheckpointAt103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointAt103(f,stage) ==
 f.id \in Nat \ {0} /\ f.phase="Steps" /\ ~f.returned /\ Len(f.owed)>0 /\ f.point=stage /\ f.owed[1]=stage

Exact module download · Source bundle and reproduction instructions

CheckpointAuxiliarySiteCleanup103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointAuxiliarySiteCleanup103(before,after,targetSites,afterTargetSites,objects,deploying,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCode2d73b20aa788")
 /\ AuxiliarySiteRegistryCheckpoint4(targetSites,afterTargetSites,objects,deploying,"ProcedureCode2d73b20aa788")
 /\ CheckpointStageAdvance103(before,after,"ProcedureCode2d73b20aa788",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointAt103, CheckpointStageAdvance103, AuxiliarySiteRegistryCheckpoint4

CheckpointAuxiliarySiteLimit103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointAuxiliarySiteLimit103(before,after,targetSites,objects,afterObjects,keep,effectiveLimit,
                         successors,usedIds,printed,owners,sideBVisible,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCodea488e1ba6ca3")
 /\ LET remaining==Without101(targetSites,before.retiredRemotes)
        plan==AuxiliarySiteLimitPlan4(remaining,keep,effectiveLimit,objects)
        retired==AuxiliarySiteTargetSiteIds4(remaining) \ keep
    IN /\ Cardinality(AuxiliarySiteTargetSiteIds4(remaining))>effectiveLimit /\ plan.valid /\ plan.chooser="SideA"
       /\ CheckpointRetirePost103(objects,afterObjects,plan.trash,successors,usedIds,printed,owners,sideBVisible)
       /\ after=[before EXCEPT !.retiredRemotes=@ \cup retired,!.snapshotId=newSnapshotId]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: plan, remaining, retired, CheckpointAt103, CheckpointRetirePost103, AuxiliarySiteTargetSiteIds4

CheckpointCaptured103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointCaptured103(frame,ledger) ==
 /\ frame.recognition.id#0 /\ frame.recognition.id=frame.id /\ frame.recognition.caller=frame.caller
 /\ frame.id \in DOMAIN ledger.checkpoints /\ ledger.checkpoints[frame.id].caller=frame.caller
 /\ frame.recognized=CheckpointMemberMap103(ledger,frame.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointMemberMap103

CheckpointCleanupEffects103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointCleanupEffects103(before,after,beforeRegistry,afterRegistry,beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack,
                             beforeSnapshot,afterSnapshot,world,cleanupFrame,afterCleanupFrame,actualCleanup) ==
 /\ CheckpointAt103(before,"ProcedureCode88eda145024f") /\ CheckpointCaptured103(before,beforeLedger)
 /\ cleanupFrame.checkpointId=before.id /\ cleanupFrame.recognition=before.recognition
 /\ CleanupLingeringConditionals910(beforeRegistry,afterRegistry,beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack,
       beforeSnapshot,afterSnapshot,world,cleanupFrame,afterCleanupFrame,actualCleanup)
 /\ CheckpointStageAdvance103(before,after,"ProcedureCode88eda145024f",world.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CleanupLingeringConditionals910, CheckpointAt103, CheckpointCaptured103, CheckpointStageAdvance103

CheckpointCompletion103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointCompletion103(frame,ledger,world,receipt) ==
 /\ frame.phase="Completed" /\ ~frame.returned /\ frame.point="ProcedureCodeb74d673a0fc6" /\ frame.owed= <<>>
 /\ frame.done \cup frame.discharged=CheckpointStageSet103 /\ frame.done \cap frame.discharged={}
 /\ CheckpointCaptured103(frame,ledger) /\ frame.snapshotId=world.id /\ frame.outcome="Playing"
 /\ receipt=PersistentCheckpointCompletion912(ledger,frame.recognition,world)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointCompletion912, CheckpointCaptured103, CheckpointStageSet103

CheckpointDrained103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointDrained103(frame,ledger,stack) ==
 /\ frame.phase="Returned" /\ frame.returned /\ frame.owed = <<>> /\ frame.outcome="Playing"
 /\ frame.done \cup frame.discharged=CheckpointStageSet103 /\ CheckpointCaptured103(frame,ledger)
 /\ ConditionalCheckpointDrained96(ledger,stack,frame.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalCheckpointDrained96, CheckpointCaptured103, CheckpointStageSet103

CheckpointHostedCleanup103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointHostedCleanup103(before,after,objects,afterObjects,departures,afterDepartures,transits,paidProcedures,
                           successors,usedIds,printed,owners,sideBVisible,newSnapshotId) ==
 /\ before.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} /\ CheckpointAt103(before,before.point)
 /\ \A p \in DOMAIN paidProcedures : paidProcedures[p].id=p /\ PaidHeldProvenance95(paidProcedures[p],objects,transits)
 /\ LET due==CheckpointHostedTargets103(objects,departures,before.point,transits,paidProcedures)
        added==CheckpointNewUninstallDepartures103(objects,due)
    IN /\ CheckpointRetirePost103(objects,afterObjects,due,successors,usedIds,printed,owners,sideBVisible)
       /\ afterDepartures=MergeCheckpointDepartures103(departures,added)
       /\ IF before.point="ProcedureCode96bfa1b6a970" /\ due#{} THEN after=[before EXCEPT !.snapshotId=newSnapshotId,!.hostPasses=@+1]
          ELSE CheckpointStageAdvance103(before,after,before.point,newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidHeldProvenance95, added, due, CheckpointAt103, CheckpointRetirePost103, CheckpointStageAdvance103, MergeCheckpointDepartures103

CheckpointHostedTargets103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointHostedTargets103(objects,departures,kind,transits,paidProcedures) ==
 LET historical==UNION {departures[id].children : id \in {id \in DOMAIN departures :
                         IF kind="ProcedureCode76ca53ad9dd0" THEN departures[id].objectiveCompletionLeft ELSE departures[id].uninstalled \/ departures[id].hostRemoved}}
     finished=={p \in DOMAIN paidProcedures : paidProcedures[p].ability.lastFinished}
 IN ((historical \cap DOMAIN objects) \ CheckpointProtectedIds103(objects,transits,paidProcedures)) \cup
       CostAsideCleanupIds4(transits,objects,finished,kind)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: finished, historical, CheckpointProtectedIds103, CostAsideCleanupIds4

CheckpointIllegalDisposition103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointIllegalDisposition103(eligible,LegalAfterRetire(_)) ==
 IF AppropriateRetireSets103(eligible,LegalAfterRetire)={} THEN "UnsupportedNoLegalizingSet" ELSE "Supported"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AppropriateRetireSets103

CheckpointIllegalRetire103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointIllegalRetire103(before,after,objects,afterObjects,eligible,LegalAfterRetire(_),controllers,activePlayer,auxiliarySiteTargetSites,auxiliarySiteLimit,chooser,selected,
                          successors,usedIds,printed,owners,sideBVisible,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCodea488e1ba6ca3") /\ eligible \subseteq CheckpointPhysicalIds103(objects)
 /\ IF auxiliarySiteLimit.applies THEN Cardinality(AuxiliarySiteTargetSiteIds4(Without101(auxiliarySiteTargetSites,before.retiredRemotes)))<=auxiliarySiteLimit.value ELSE TRUE
 /\ LET choices==AppropriateRetireSets103(eligible,LegalAfterRetire)
    IN /\ selected \in choices /\ chooser=IllegalRetireChooser103(choices,controllers,activePlayer)
       /\ CheckpointRetirePost103(objects,afterObjects,selected,successors,usedIds,printed,owners,sideBVisible)
       /\ CheckpointStageAdvance103(before,after,"ProcedureCodea488e1ba6ca3",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: choices, CheckpointAt103, CheckpointPhysicalIds103, CheckpointRetirePost103, CheckpointStageAdvance103, IllegalRetireChooser103, Without101, AuxiliarySiteTargetSiteIds4

CheckpointLatest103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointLatest103(group,activationOrder) ==
 CHOOSE id \in group : \A other \in group \ {id} : activationOrder[id]>activationOrder[other]

Exact module download · Source bundle and reproduction instructions

CheckpointLatestExists103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointLatestExists103(group,activationOrder) ==
 group \subseteq DOMAIN activationOrder /\ \E id \in group : \A other \in group \ {id} : activationOrder[id]>activationOrder[other]

Exact module download · Source bundle and reproduction instructions

CheckpointMemberMap103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointMemberMap103(ledger,cpId) ==
 [id \in PersistentRecognizedIds912(ledger,cpId) |-> ledger.instances[id].member]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentRecognizedIds912

CheckpointNewUninstallDepartures103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointNewUninstallDepartures103(objects,selected) ==
 [key \in {<<"CleanupUninstall",i>> : i \in selected} |->
    [source |-> key[2],objectiveCompletionLeft |-> FALSE,uninstalled |-> objects[key[2]].form="Card" /\ objects[key[2]].deployed,hostRemoved |-> TRUE,
     children |-> {child \in DOMAIN objects : objects[child].host=key[2]}]]

Exact module download · Source bundle and reproduction instructions

CheckpointObjectiveOutcome103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointObjectiveOutcome103(objects,effectivePoints) ==
 LET points==[p \in SetupPlayers |-> ObjectiveAreaPoints4(objects,p,effectivePoints)]
     winners=={p \in SetupPlayers : points[p]>=7}
 IN CASE winners={} -> "Playing" [] winners=SetupPlayers -> "Draw" [] OTHER -> CHOOSE p \in winners : TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: winners, SetupPlayers

CheckpointPendingBarrierTargetSites103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointPendingBarrierTargetSites103(deploying) ==
 {deploying[id].destination.targetSite : id \in {id \in DOMAIN deploying : deploying[id].form="Card" /\ deploying[id].kind="Barrier" /\
       deploying[id].destination.zone="Play" /\ deploying[id].destination.area="Protecting"}}

Exact module download · Source bundle and reproduction instructions

CheckpointPhysicalIds103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointPhysicalIds103(objects) == {id \in DOMAIN objects : ~objects[id].virtual}

Exact module download · Source bundle and reproduction instructions

CheckpointPositionCleanup103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointPositionCleanup103(before,after,layout,afterLayout,currentSideBPosition,deploying,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCode2d6279f9d639")
 /\ LET pendingTargetSites==CheckpointPendingBarrierTargetSites103(deploying)
        remove=={p \in DOMAIN layout.slots : layout.slots[p].barrierCard=0 /\ p#currentSideBPosition /\ layout.slots[p].targetSite \notin pendingTargetSites}
    IN /\ afterLayout=[layout EXCEPT !.slots=[p \in DOMAIN layout.slots \ remove |->
          [layout.slots[p] EXCEPT !.retained=(p=currentSideBPosition /\ layout.slots[p].barrierCard=0)]],
          !.orders=[targetSite \in DOMAIN @ |-> SelectSeq(layout.orders[targetSite],LAMBDA p : p \notin remove)]]
       /\ CheckpointStageAdvance103(before,after,"ProcedureCode2d6279f9d639",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LAMBDA, remove, CheckpointAt103, CheckpointStageAdvance103

CheckpointPrivatePersistentBound103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointPrivatePersistentBound103(frame,registry,ledger) ==
 /\ frame.phase \in {"Steps","Completed"} /\ CheckpointCaptured103(frame,ledger)
 /\ PersistentCheckpointBound912(registry,[ledger EXCEPT !.checkpoints=Without101(@,{frame.id})])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointBound912, CheckpointCaptured103, Without101

CheckpointProtectedIds103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointProtectedIds103(objects,transits,paidProcedures) ==
 UNION {{id \in DOMAIN objects : PaidHeldObject95(paidProcedures[p],objects,transits,id)} : p \in
    {p \in DOMAIN paidProcedures : paidProcedures[p].id=p /\ PaidProtectionAlive95(paidProcedures[p])}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidHeldObject95, PaidProtectionAlive95

CheckpointRecognizedWindow103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointRecognizedWindow103(frame) ==
 IF DOMAIN frame.recognized={} THEN 0 ELSE frame.recognized[CHOOSE id \in DOMAIN frame.recognized : TRUE].windowId

Exact module download · Source bundle and reproduction instructions

CheckpointRestoreDiscard103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointRestoreDiscard103(before,after,objects,afterObjects,conversions,afterConversions,printed,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCodeda83a77a1f12") /\ RestoreDiscardConversions103(objects,afterObjects,conversions,afterConversions,printed)
 /\ CheckpointStageAdvance103(before,after,"ProcedureCodeda83a77a1f12",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointAt103, CheckpointStageAdvance103, RestoreDiscardConversions103

CheckpointRetentionRetire103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointRetentionRetire103(frame,retentions,afterRetentions,objects,afterObjects,liveIds,successors,usedIds,printed,owners,sideBVisible) ==
 /\ CheckpointAt103(frame,"ProcedureCode88eda145024f") /\ liveIds \subseteq DOMAIN retentions
 /\ CheckpointRetirePost103(objects,afterObjects,ExpiredRetainedPlayIds103(retentions,objects,liveIds),successors,usedIds,printed,owners,sideBVisible)
 /\ afterRetentions=Without101(retentions,DOMAIN retentions \ liveIds)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointAt103, CheckpointRetirePost103, ExpiredRetainedPlayIds103, Without101

CheckpointRetireMap103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointRetireMap103(objects,selected,successors,printed,owners,sideBVisible) ==
 LET cards=={id \in selected : objects[id].card#"none"}
     fresh=={successors[id] : id \in cards}
 IN [id \in (DOMAIN objects \ selected) \cup fresh |-> IF id \notin fresh THEN objects[id]
      ELSE LET old==CHOOSE old \in cards : successors[old]=id
               o==objects[old]
           IN [o EXCEPT !.form="Card",!.kind=printed[o.card].kind,!.properties=printed[o.card],
                 !.zone=owners[o.card] \o "Discard",!.loc="discard",!.host=0,!.deployed=FALSE,!.activated=FALSE,!.marks={},
                 !.face=DiscardArrivalFace4(owners[o.card],o.zone,"Retire",old \in sideBVisible)]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: fresh, o, old, DiscardArrivalFace4

CheckpointRetirePost103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointRetirePost103(objects,afterObjects,selected,successors,usedIds,printed,owners,sideBVisible) ==
 /\ selected \subseteq CheckpointPhysicalIds103(objects) /\ DOMAIN objects \subseteq usedIds
 /\ FreshSuccessors8({id \in selected : objects[id].card#"none"},successors,usedIds)
 /\ afterObjects=CheckpointRetireMap103(objects,selected,successors,printed,owners,sideBVisible)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPhysicalIds103, CheckpointRetireMap103, FreshSuccessors8

CheckpointReturnDiscardCounters103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointReturnDiscardCounters103(before,after,objects,afterObjects,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCode0811ebc5f40e")
 /\ LET due=={id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].zone \in {"SideADiscard","SideBDiscard"}}
    IN /\ \A id \in due : objects[id].card="none" /\ ~objects[id].virtual
       /\ afterObjects=Without101(objects,due)
       /\ CheckpointStageAdvance103(before,after,"ProcedureCode0811ebc5f40e",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: due, CheckpointAt103, CheckpointStageAdvance103, Without101

CheckpointRootAdmissions103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointRootAdmissions103(before,after,capacity,afterCapacity,siteInspection,objects,entries,previousBoundary,currentBoundary,accepted,actor,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCode7f181ce21011") /\ previousBoundary<=currentBoundary
 /\ IF siteInspection.active /\ ~siteInspection.complete THEN
     /\ actor="SideB"
     /\ LET arrivals=={entries[id].object : id \in {id \in DOMAIN entries : entries[id].tag="RootEntry" /\ entries[id].siteInspectionId=siteInspection.id /\
                entries[id].serial>previousBoundary /\ entries[id].serial<=currentBoundary /\ entries[id].targetSite=siteInspection.targetSite}}
            observed==[capacity EXCEPT !.admittedRoots=(@ \cap InspectionRootCards7(siteInspection,objects)) \ arrivals,
                    !.pendingRoots=(@ \cup arrivals) \cap InspectionRootCards7(siteInspection,objects)]
        IN /\ ObserveRootEntries7(capacity,observed,siteInspection,objects,arrivals)
           /\ DecideRootAdmissions7(observed,afterCapacity,siteInspection,objects,accepted,"ProcedureCode7f181ce21011",TRUE)
    ELSE afterCapacity=capacity /\ accepted={} /\ actor="NoValue"
 /\ CheckpointStageAdvance103(before,after,"ProcedureCode7f181ce21011",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: arrivals, observed, CheckpointAt103, CheckpointStageAdvance103, DecideRootAdmissions7, ObserveRootEntries7

CheckpointSite103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointSite103(site,event,insideStructures) ==
 /\ site.snapshotId \in Nat \ {0} /\ site.caller=event.caller /\ site.eventId=event.id
 /\ event.id \in Nat \ {0} /\ event.complete
 /\ CASE site.kind="SchemaAtom126" -> event.tag="PriorityAboutToBeReceived" /\ event.player \in SetupPlayers
      [] site.kind="Cost" -> event.tag="CostPaid" /\ event.transactionId \in Nat \ {0}
      [] site.kind="Instruction" -> event.tag="InstructionFinished" /\ event.origin \in {"Ability","TimingStep"}
                                        /\ event.instruction \notin CheckpointStageSet103 \cup {"ProcedureCodeb74d673a0fc6"}
      [] site.kind="StructureEnd" -> event.tag="TimingStructureEnded" /\ TimingRefValid9(event.structure)
      [] OTHER -> FALSE
 /\ site.inside=IF site.kind="StructureEnd" THEN insideStructures \ {event.structure} ELSE insideStructures

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRefValid9, CheckpointStageSet103, SetupPlayers

CheckpointSiteKey103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointSiteKey103(site) == <<site.kind,site.eventId,site.caller>>

Exact module download · Source bundle and reproduction instructions

CheckpointStageAdvance103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointStageAdvance103(before,after,stage,newSnapshotId) ==
 /\ CheckpointAt103(before,stage) /\ stage \in CheckpointStageSet103
 /\ LET rest==SubSeq(before.owed,2,Len(before.owed))
    IN after=[before EXCEPT !.owed=rest,!.done=@ \cup {stage},!.snapshotId=newSnapshotId,
       !.point=IF rest= <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE rest[1],!.phase=IF rest= <<>> THEN "Completed" ELSE "Steps"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: rest, CheckpointAt103, CheckpointStageSet103

CheckpointStageSet103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointStageSet103 == {CheckpointStages103[i] : i \in 1..Len(CheckpointStages103)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointStages103

CheckpointStages103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointStages103 == <<"ProcedureCodee605a78f5d5e","ProcedureCode88eda145024f","ProcedureCodeb681cc249a04","ProcedureCodefe50c31480ea","ProcedureCodea488e1ba6ca3","ProcedureCode76ca53ad9dd0",
                         "ProcedureCode96bfa1b6a970","ProcedureCode2d73b20aa788","ProcedureCode2d6279f9d639","ProcedureCode7f181ce21011","ProcedureCodeda83a77a1f12","ProcedureCode0811ebc5f40e">>

Exact module download · Source bundle and reproduction instructions

CheckpointUniquePlan103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointUniquePlan103(objects,names,unique,active,consoles,controllers,activationOrder) ==
 LET activeCards==active \cap {id \in DOMAIN objects : objects[id].form="Card"}
     uniqueNames=={names[id] : id \in unique \cap activeCards}
     mixed==\E name \in uniqueNames : \E id \in activeCards \ unique : names[id]=name
     uniqueGroups=={{id \in unique \cap activeCards : names[id]=name} : name \in uniqueNames}
     consoleGroups=={{id \in consoles \cap DOMAIN objects : objects[id].deployed /\ controllers[id]=player} : player \in SetupPlayers}
     groups=={group \in uniqueGroups \cup consoleGroups : Cardinality(group)>1}
     supported==~mixed /\ \A group \in groups : CheckpointLatestExists103(group,activationOrder)
 IN [disposition |-> IF mixed THEN "UnsupportedMixedUniqueness" ELSE IF supported THEN "Supported" ELSE "UnsupportedActivationTie",
     targets |-> IF supported THEN UNION {group \ {CheckpointLatest103(group,activationOrder)} : group \in groups} ELSE {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: groups, mixed, supported, CheckpointLatest103

CheckpointUniqueRetire103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointUniqueRetire103(before,after,objects,afterObjects,names,unique,active,consoles,controllers,activationOrder,
                         successors,usedIds,printed,owners,sideBVisible,newSnapshotId) ==
 /\ CheckpointAt103(before,"ProcedureCodefe50c31480ea")
 /\ LET plan==CheckpointUniquePlan103(objects,names,unique,active,consoles,controllers,activationOrder)
    IN /\ plan.disposition="Supported"
       /\ CheckpointRetirePost103(objects,afterObjects,plan.targets,successors,usedIds,printed,owners,sideBVisible)
       /\ CheckpointStageAdvance103(before,after,"ProcedureCodefe50c31480ea",newSnapshotId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: plan, CheckpointAt103, CheckpointRetirePost103, CheckpointStageAdvance103

CheckpointVictory103 · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointVictory103(before,after,objects,effectivePoints,currentSnapshot) ==
 /\ CheckpointAt103(before,"ProcedureCodeb681cc249a04") /\ before.snapshotId=currentSnapshot
 /\ LET result==CheckpointObjectiveOutcome103(objects,effectivePoints)
    IN IF result="Playing" THEN CheckpointStageAdvance103(before,after,"ProcedureCodeb681cc249a04",currentSnapshot)
       ELSE after=[before EXCEPT !.outcome=result,!.phase="SchemaAtom160",!.point="GameEnded"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: result, CheckpointAt103, CheckpointStageAdvance103

ChooseBidPaymentSources1014 · operator

reference-profile · input revision 2 · CC0 1.0

ChooseBidPaymentSources1014(before,after,world,player,selected,cardFacts) ==
 /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase="ChoosePayment" /\ before.revealed=before.packet.participants /\ world.id=before.paymentWorld /\ BidPaymentScope1014(world)=before.paymentScope
 /\ player \in before.packet.participants \ DOMAIN before.plans /\ selected \in BidPaymentPlans1014(world,player,before.selections[player],cardFacts)
 /\ (BidMultipleChoicePlayers1014(before,world,cardFacts)=SetupPlayers /\ DOMAIN before.plans={} => player=before.active)
 /\ after=[before EXCEPT !.plans=ReplacementOverlay99(@,[p \in {player} |-> selected]),!.choiceOrder=Append(@,player)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, BidCurrent1014, BidMultipleChoicePlayers1014, BidPaymentPlans1014, BidPaymentScope1014, SetupPlayers

ChooseSabotageCentralA1012 · operator

reference-profile · input revision 2 · CC0 1.0

ChooseSabotageCentralA1012(before,after,context,operation,world,packet,decision) ==
 /\ SabotageFrameBound1012(before,context,operation,world,packet) /\ before.phase="Choose" /\ ~before.choiceSealed
 /\ decision.tag="SideASabotageCentralAChoice" /\ decision.actor="SideA" /\ decision.frameId=before.id /\ decision.snapshotId=world.id
 /\ decision.view=SideASabotageView1012(world,packet) /\ decision.aHand \subseteq world.aHand
 /\ LET total==SabotageTotal1012(world,packet.amount) count==Cardinality(decision.aHand)
    IN /\ MaxOf(0,total-Len(world.aDrawPile))<=count /\ count<=MinOf(total,Cardinality(world.aHand))
       /\ after=[before EXCEPT !.phase="ReadyRetire",!.choiceSealed=TRUE,!.aHandChosen=decision.aHand,!.aDrawPileCount=total-count]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: count, total, SabotageFrameBound1012, SideASabotageView1012, MaxOf, MinOf

CommitBidPayments1014 · operator

reference-profile · input revision 2 · CC0 1.0

CommitBidPayments1014(before,after,world,cardFacts,afterObjects,successors,batchId,afterHistory,events,receipts) ==
 /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase="ChoosePayment" /\ world.id=before.paymentWorld /\ BidPaymentScope1014(world)=before.paymentScope /\ before.revealed=before.packet.participants
 /\ DOMAIN before.plans=before.packet.participants
 /\ \A p \in before.packet.participants :
      /\ before.plans[p] \in BidPaymentPlans1014(world,p,before.selections[p],cardFacts)
      /\ before.costs[p]=BidNestedCost1014(before,world,p,before.transactions[p]) /\ before.costs[p].optionalInterrupts={}
      /\ EffectiveCosts(before.costs[p].specification,{},FALSE,FALSE)=BidNestedSpecification1014(before,p)
      /\ AlternatePaymentPreservesValue(before.selections[p],Cardinality(before.plans[p]))
 /\ \A p,q \in before.packet.participants : p#q => before.plans[p] \cap before.plans[q]={}
 /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,UNION {before.plans[p] : p \in before.packet.participants},successors,world.usedObjects,
       world.printed,world.owners,world.visible,batchId,world.movementHistory,afterHistory,events)
 /\ receipts=[p \in before.packet.participants |-> BidCompletedCost1014(before.costs[p],before.plans[p])]
 /\ after=BidPaidFrame1014(before)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidCompletedCost1014, BidCurrent1014, BidNestedCost1014, BidNestedSpecification1014, BidPaidFrame1014, BidPaymentPlans1014, BidPaymentScope1014, LiabilityMarkerCounterDeparture106, AlternatePaymentPreservesValue, EffectiveCosts

CommunicateInformation102 · operator

reference-profile · input revision 2 · CC0 1.0

CommunicateInformation102(beforeTranscript,afterTranscript,beforeTruth,afterTruth,
                          facts,fact,speaker,recipient,claimedValue,currentSnapshot) ==
 /\ speaker \in SetupPlayers /\ recipient \in SetupPlayers \ {speaker}
 /\ fact \in DOMAIN facts /\ facts[fact].snapshot=currentSnapshot /\ speaker \in facts[fact].viewers
 /\ InformationClass102(facts[fact].viewers)="Open" => claimedValue=facts[fact].value
 /\ afterTruth=beforeTruth
 /\ afterTranscript=Append(beforeTranscript,[tag |-> "Claim",speaker |-> speaker,recipient |-> recipient,
       fact |-> fact,value |-> claimedValue,snapshot |-> currentSnapshot,
       verifiedOpen |-> InformationClass102(facts[fact].viewers)="Open"])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InformationClass102, SetupPlayers

CompleteDividendPlan1013 · operator

reference-profile · input revision 2 · CC0 1.0

CompleteDividendPlan1013(before,after,world,completion) ==
 /\ world.outcome="Playing" /\ DividendPlanBound1013(world,before) /\ ~before.complete /\ before.cursor=before.basis.repetitions+1
 /\ \A i \in before.applied : <<before.instance,before.reference,i>> \in world.completedCounterInstructions
 /\ before.applied \cap before.skipped={} /\ before.applied \cup before.skipped=1..before.basis.repetitions
 /\ before.totalPlaced=before.basis.multiplier*Cardinality(before.applied)
 /\ after=[before EXCEPT !.complete=TRUE]
 /\ completion=[tag |-> "DividendInstructionComplete",instance |-> before.instance,reference |-> before.reference,objectiveCompletionId |-> before.basis.objectiveCompletionId,applications |-> before.applied,
      skipped |-> before.skipped,totalPlaced |-> before.totalPlaced,complete |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DividendPlanBound1013

CompleteEscalatingResourceContest108 · operator

reference-profile · input revision 2 · CC0 1.0

CompleteEscalatingResourceContest108(before,after,world) ==
 /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="Determined" /\ before.result \in {"Successful","Unsuccessful"}
 /\ after=[before EXCEPT !.phase="Complete",!.complete=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestCurrent108

ConversionExitPlan101 · operator

reference-profile · input revision 2 · CC0 1.0

ConversionExitPlan101(c,printed,oldZone,newZone,movement) ==
 [converted |-> ConversionRetained101(c,oldZone,newZone),
  properties |-> ConversionProperties101(c,printed,oldZone,newZone),
  trashImmediately |-> ~ConversionRetained101(c,oldZone,newZone) /\ ~(c.mode="Objective" /\ movement="Forfeit")]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConversionProperties101, ConversionRetained101

ConversionExitPost101 · operator

reference-profile · input revision 2 · CC0 1.0

ConversionExitPost101(c,printed,oldObject,successor,sourceObjects,afterObjects,usedIds,
                     destination,movement,actualRetireReceipt) ==
 /\ ConversionValid101(c) /\ oldObject \in DOMAIN sourceObjects /\ sourceObjects[oldObject].card=c.card
 /\ successor \in DOMAIN afterObjects /\ afterObjects[successor].card=c.card
 /\ DOMAIN sourceObjects \subseteq usedIds /\ DOMAIN afterObjects=(DOMAIN sourceObjects \ {oldObject}) \cup {successor}
 /\ \A i \in DOMAIN sourceObjects \ {oldObject} : afterObjects[i]=sourceObjects[i]
 /\ sourceObjects[oldObject].owner=c.owner /\ afterObjects[successor].owner=c.owner
 /\ sourceObjects[oldObject].kind=c.gained.kind
 /\ sourceObjects[oldObject].form=(IF c.mode="Objective" THEN "Card" ELSE "Counter")
 /\ oldObject#successor /\ successor \notin usedIds /\ oldObject \notin DOMAIN afterObjects
 /\ sourceObjects[oldObject].zone#destination
 /\ LET plan==ConversionExitPlan101(c,printed,sourceObjects[oldObject].zone,destination,movement)
    IN /\ ~plan.converted
       /\ afterObjects[successor].form="Card" /\ afterObjects[successor].properties=printed
       /\ afterObjects[successor].kind=printed.kind
       /\ afterObjects[successor].host=0 /\ ~afterObjects[successor].deployed
       /\ IF plan.trashImmediately THEN
            /\ actualRetireReceipt.original=oldObject /\ actualRetireReceipt.successor=successor
            /\ actualRetireReceipt.physical=c.card /\ actualRetireReceipt.complete
            /\ actualRetireReceipt.owner=c.owner
            /\ afterObjects[successor].zone=actualRetireReceipt.owner \o "Discard"
          ELSE movement="Forfeit" /\ destination="Removed" /\ afterObjects[successor].zone="Removed"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: plan, ConversionValid101

ConversionProperties101 · operator

reference-profile · input revision 2 · CC0 1.0

ConversionProperties101(c,printed,oldZone,newZone) ==
 IF ConversionRetained101(c,oldZone,newZone) THEN c.gained ELSE printed

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConversionRetained101

ConversionRetained101 · operator

reference-profile · input revision 2 · CC0 1.0

ConversionRetained101(c,oldZone,newZone) ==
 IF c.mode="Objective" THEN oldZone \in SetupObjectiveZones /\ newZone \in SetupObjectiveZones ELSE oldZone=newZone

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupObjectiveZones

ConversionValid101 · operator

reference-profile · input revision 2 · CC0 1.0

ConversionValid101(c) ==
 /\ c.mode \in {"Objective","Counter"} /\ c.card#"none"
 /\ c.createdBy \in Nat \ {0} /\ c.owner \in SetupPlayers
 /\ IF c.mode="Objective" THEN
      /\ "kind" \in DOMAIN c.gained /\ c.gained.kind="Objective"
      /\ "objectivePoints" \in DOMAIN c.gained /\ c.gained.objectivePoints \in Int
    ELSE /\ "kind" \in DOMAIN c.gained /\ c.gained.kind \in CounterKinds101

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterKinds101, SetupPlayers

CoreInformationCatalog102 · operator

reference-profile · input revision 2 · CC0 1.0

CoreInformationCatalog102(objects,controllers,actualLiveGrants,actualOpenRememberedChoices,snapshot) ==
 LET keys=={<<"CardProfile",id>> : id \in {i \in DOMAIN objects : objects[i].form="Card"}} \cup
           {<<"ZoneCount",z>> : z \in {"SideAHand","SideADeck","SideBHand","SideBDeck"}} \cup
           {<<"ResourceUnitPool",p>> : p \in SetupPlayers} \cup
           {<<"Choice",id>> : id \in DOMAIN actualOpenRememberedChoices}
     choices==PublicChoiceFacts102(actualOpenRememberedChoices,snapshot)
 IN [key \in keys |-> CASE key[1]="CardProfile" -> CardProfileFact102(key[2],objects,controllers,actualLiveGrants,snapshot)
                       [] key[1]="ZoneCount" -> ZoneCountFact102(key[2],objects,snapshot)
                       [] key[1]="ResourceUnitPool" -> ResourceUnitPoolFact102(key[2],objects,snapshot)
                       [] OTHER -> choices[key[2]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: choices, keys, CardProfileFact102, ResourceUnitPoolFact102, ZoneCountFact102

CounterInstruction109 · operator

reference-profile · input revision 2 · CC0 1.0

CounterInstruction109(context,reference,world,id,cardFacts) ==
 /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ id \in DOMAIN context.templates
 /\ LET e==context.actualEffects[id] IN
    /\ e.kind \in {"LoadCounters","PlaceCounters","RemoveCounters"} /\ e.kind=context.templates[id].kind
    /\ e.value \in Nat /\ CounterInstructionDisposition109(e)="Supported" /\ e.actor \in SetupPlayers /\ e.baseOrigin=reference.source
    /\ e.sourceCard=context.templates[id].sourceCard /\ e.sourceSHA=context.templates[id].sourceSHA
    /\ e.sourceCard \in DOMAIN cardFacts /\ e.sourceSHA=cardFacts[e.sourceCard].sourceSHA
    /\ e.target \in DOMAIN world.objects /\ world.objects[e.target].form="Card" /\ world.objects[e.target].zone \in {"Play","SideAObjectiveCompletion","SideBObjectiveCompletion"}
    /\ e.counterKinds=context.templates[id].counterKinds /\ e.counterKind=context.templates[id].counterKind
    /\ e.loadDefinition=context.templates[id].loadDefinition
    /\ IF e.kind="LoadCounters" THEN e.loadDefinition \in Nat \ {0} ELSE e.loadDefinition=0
    /\ \A key \in DOMAIN world.loadLinks :
         LET link==world.loadLinks[key] IN
         (e.kind="LoadCounters" /\ e.target=link.host /\ e.baseOrigin=ObjectAbilitySource9(link.host) /\ e.loadDefinition=link.loadDefinition) => e.counterKind=link.kind

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, ObjectAbilitySource9, e, link, CounterInstructionDisposition109, SetupPlayers

CounterInstructionDisposition109 · operator

reference-profile · input revision 2 · CC0 1.0

CounterInstructionDisposition109(effect) ==
 IF effect.kind \notin {"LoadCounters","PlaceCounters","RemoveCounters"} THEN "UnsupportedCounterOperation"
 ELSE IF effect.value \notin Nat THEN "RequiresQuantityNormalization"
 ELSE IF Cardinality(effect.counterKinds)#1 THEN "UnsupportedCounterTypeOrMultiType"
 ELSE IF effect.counterKind \notin CounterKinds101 \/ effect.counterKinds#{effect.counterKind} THEN "UnsupportedCounterTypeOrMultiType"
 ELSE IF effect.kind="LoadCounters" /\ effect.value=0 THEN "UnsupportedZeroLoad"
 ELSE "Supported"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterKinds101

CounterInstructionKey109 · operator

reference-profile · input revision 2 · CC0 1.0

CounterInstructionKey109(context,reference,id) == <<context.id,reference,id>>

Exact module download · Source bundle and reproduction instructions

CounterKinds101 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

CurrentChargeTargets1010 · operator

reference-profile · input revision 2 · CC0 1.0

CurrentChargeTargets1010(world,admission,spec) ==
 LET candidates==IF spec.mode="Chosen" THEN admission.announced \cap ChargeSet1010(world,spec) ELSE {spec.particular}
     legal=={id \in candidates : id \in DOMAIN admission.physical /\ id \in DOMAIN world.objects /\ world.objects[id].card=admission.physical[id] /\ ChargePower1010(world.objects,id)}
     initial==IF spec.mode="Particular" THEN {id \in legal : admission.initialPower[id]} ELSE legal
 IN IF spec.ifAble /\ Cardinality(initial)<spec.requested THEN {} ELSE initial

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: initial

CurrentExposureMarkerState105 · operator

reference-profile · input revision 2 · CC0 1.0

CurrentExposureMarkerState105(world,declarations,cardFacts,state) ==
 /\ \A id \in DOMAIN declarations :
       LET d==declarations[id] IN
       /\ d.snapshotId=world.id /\ d.projection.property="HasExposureMarkers" /\ d.projection.target="SideB" /\ d.projection.value=TRUE
       /\ d.projection.mode="Continuous" /\ ~d.projection.resolving /\ ~d.projection.lingering
       /\ d.projection.source.kind="Object" /\ d.projection.source.object \in DOMAIN world.objects
       /\ d.sourceObject=world.objects[d.projection.source.object]
       /\ d.sourceObject.card \in DOMAIN cardFacts /\ d.sourceSHA=cardFacts[d.sourceObject.card].sourceSHA
       /\ d.projection.ability \in world.activeAbilities /\ DefaultActive(d.sourceObject,world.started,cardFacts)
 /\ state=ExposureMarkerStateView105(world.objects,declarations)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: d, ExposureMarkerStateView105, DefaultActive

CurrentLiabilityMarker106 · operator

reference-profile · input revision 2 · CC0 1.0

CurrentLiabilityMarker106(world,declarations,cardFacts,quantity) ==
 /\ LET virtual==LiabilityMarkerIds106(world.objects) \ MovableLiabilityMarkerIds106(world.objects)
    IN /\ UNION {declarations[id].counters : id \in DOMAIN declarations}=virtual
       /\ \A a,b \in DOMAIN declarations : a#b => declarations[a].counters \cap declarations[b].counters={}
 /\ \A id \in DOMAIN declarations :
       LET d==declarations[id] IN
       /\ d.snapshotId=world.id /\ d.projection.property="AdditionalLiabilityMarker" /\ d.projection.target="SideA"
       /\ d.projection.mode="Continuous" /\ ~d.projection.resolving /\ ~d.projection.lingering
       /\ d.projection.value=Cardinality(d.counters) /\ d.counters \subseteq LiabilityMarkerIds106(world.objects)
       /\ d.projection.source.kind="Object" /\ d.projection.source.object \in DOMAIN world.objects
       /\ d.sourceObject=world.objects[d.projection.source.object] /\ d.sourceObject.card \in DOMAIN cardFacts
       /\ d.sourceSHA=cardFacts[d.sourceObject.card].sourceSHA /\ d.projection.ability \in world.activeAbilities
       /\ DefaultActive(d.sourceObject,world.started,cardFacts)
 /\ quantity=LiabilityMarkerQuantity106(world.objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: d, virtual, LiabilityMarkerIds106, LiabilityMarkerQuantity106, DefaultActive

CurrentLinkDeclarations107 · operator

reference-profile · input revision 2 · CC0 1.0

CurrentLinkDeclarations107(world,cardFacts,declarations) ==
 /\ declarations=world.linkDeclarations /\ DOMAIN world.printedLinkAbilities=PrintedLinkObjectIds107(world)
 /\ \A id \in DOMAIN declarations : declarations[id].projection.source.kind="Object"
 /\ \A a,b \in DOMAIN declarations : a#b => <<declarations[a].projection.ability,declarations[a].projection.part,declarations[a].projection.source>>#<<declarations[b].projection.ability,declarations[b].projection.part,declarations[b].projection.source>>
 /\ \A a,b \in DOMAIN world.printedLinkAbilities : a#b => world.printedLinkAbilities[a]#world.printedLinkAbilities[b]
 /\ LET eligible==EligiblePrintedLinkSources107(world)
        printed=={id \in DOMAIN declarations : declarations[id].origin="PrintedLink"}
    IN /\ {declarations[id].projection.source.object : id \in printed}=eligible
       /\ \A source \in eligible : Cardinality({id \in printed : declarations[id].projection.source=ObjectAbilitySource9(source)})=1
 /\ \A id \in DOMAIN declarations :
       LET d==declarations[id]
           source==d.projection.source.object
           object==world.objects[source]
           definition==LinkDefinition107(world,object)
       IN /\ d.origin \in {"PrintedLink","OtherCompiled"} /\ d.snapshotId=world.id
          /\ d.projection.property="Connection" /\ d.projection.target="SideB" /\ d.projection.mode="Continuous"
          /\ ~d.projection.resolving /\ ~d.projection.lingering /\ d.projection.value \in Int
          /\ d.projection.source.kind="Object" /\ source \in DOMAIN world.objects /\ d.sourceObject=object
          /\ object.form="Card" /\ object.side="SideB" /\ object.deployed /\ object.zone="Play" /\ world.controllers[source]="SideB"
          /\ SideBAbilityActivity8(object,d.projection.ability \in world.activeAbilities)
          /\ definition \in DOMAIN cardFacts /\ d.definition=definition /\ d.sourceSHA=cardFacts[definition].sourceSHA
          /\ IF d.origin="PrintedLink" THEN
               /\ definition \in DOMAIN world.linkSymbolFacts /\ world.linkSymbolFacts[definition].sourceSHA=d.sourceSHA
               /\ d.projection.ability=world.printedLinkAbilities[source] /\ d.projection.value=world.linkSymbolFacts[definition].link
             ELSE TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, d, definition, eligible, object, printed, source, PrintedLinkObjectIds107, SideBAbilityActivity8

CurrentLookViewers102 · operator

reference-profile · input revision 2 · CC0 1.0

CurrentLookViewers102(object,objects,actualLiveGrants) ==
 UNION {actualLiveGrants[g].viewers : g \in {g \in DOMAIN actualLiveGrants :
    actualLiveGrants[g].object=object /\ actualLiveGrants[g].zone=objects[object].zone /\
    actualLiveGrants[g].loc=objects[object].loc}}

Exact module download · Source bundle and reproduction instructions

CutoffPersistentAtCheckpoint103 · operator

reference-profile · input revision 2 · CC0 1.0

CutoffPersistentAtCheckpoint103(before,after,ledger,frame,completion,beforeEnd,afterEnd,events,expired,boundary) ==
 /\ CheckpointCompletion103(frame,ledger,before.frontier.world,completion)
 /\ CompleteTraversal6(beforeEnd,afterEnd,TRUE,events,expired)
 /\ CheckpointPrivatePersistentBound103(frame,before,ledger)
 /\ PersistentRegistryWorldBound912(before,before.frontier.world)
 /\ before.frontier.world.control.traversal=afterEnd.traversal
 /\ frame.caller=PersistentTraversalEndCaller912(afterEnd.traversal.id)
 /\ \E id \in DOMAIN frame.recognition.occurrences :
       /\ frame.recognition.occurrences[id].kind="TraversalEnds" /\ frame.recognition.occurrences[id].traversal=afterEnd.traversal
       /\ frame.recognition.occurrences[id].actualEvent \in events
       /\ frame.recognition.occurrences[id].actualEvent=[tag |-> "TraversalEnds",traversalId |-> afterEnd.traversal.id]
 /\ \A id \in DOMAIN frame.recognized : frame.recognized[id].windowId=CheckpointRecognizedWindow103(frame)
 /\ boundary=[tag |-> "PersistentLastCreationCheckpoint",traversal |-> afterEnd.traversal,checkpointId |-> frame.id,caller |-> frame.caller,
       windowId |-> CheckpointRecognizedWindow103(frame),completion |-> completion]
 /\ LET keys=={key \in DOMAIN before.persistent : before.persistent[key].phase="Persisting" /\ before.persistent[key].traversalId=afterEnd.traversal.id}
    IN /\ keys#{} /\ \A key \in keys : before.persistent[key].creationOpen
       /\ after=[before EXCEPT !.persistent=[key \in DOMAIN @ |-> IF key \in keys THEN
          [@[key] EXCEPT !.creationOpen=FALSE,!.endCheckpoint=frame.id,!.endWindow=boundary.windowId,
                        !.endMembers=DOMAIN frame.recognized] ELSE @[key]]]
       /\ PersistentRegistryWorldBound912(after,after.frontier.world) /\ PersistentCheckpointBound912(after,ledger)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointBound912, PersistentRegistryWorldBound912, PersistentTraversalEndCaller912, keys, CheckpointCompletion103, CheckpointPrivatePersistentBound103, CheckpointRecognizedWindow103, CompleteTraversal6

DamageBHand104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageBHand104(objects) == {id \in DOMAIN objects : objects[id].form="Card" /\ objects[id].zone="SideBHand"}

Exact module download · Source bundle and reproduction instructions

DamageBatchReadyForConditionals104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageBatchReadyForConditionals104(frame,objects,event) ==
 /\ frame.phase="Complete" /\ frame.outcome="Playing" /\ objects=frame.finalObjects
 /\ event=frame.completion.damageEvent /\ event=DamageSufferedEvent104(frame,frame.completion.batchId,event.successors)
 /\ frame.selected \cap DOMAIN objects={}
 /\ \A id \in frame.selected : event.successors[id] \in DOMAIN objects /\ objects[event.successors[id]].zone \in {"SideADiscard","SideBDiscard"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageSufferedEvent104

DamageCardBatchTransfer104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageCardBatchTransfer104(objects,afterObjects,selected,successors,usedIds,owners) ==
 /\ selected \subseteq DamageBHand104(objects) /\ DOMAIN objects \subseteq usedIds /\ FreshSuccessors8(selected,successors,usedIds)
 /\ \A id \in selected : objects[id].card \in DOMAIN owners /\ owners[objects[id].card] \in SetupPlayers
 /\ LET sideB=={id \in selected : owners[objects[id].card]="SideB"}
        sideA==selected \ sideB
        first==DamageOwnerMoveMap104(objects,sideB,[id \in sideB |-> successors[id]],"SideB")
        sideBFresh=={successors[id] : id \in sideB}
    IN /\ CardBatchTransfer8(objects,first,sideB,[id \in sideB |-> successors[id]],usedIds,"SideBDiscard","Up",[id \in sideB |-> "discard"])
       /\ CardBatchTransfer8(first,afterObjects,sideA,[id \in sideA |-> successors[id]],usedIds \cup sideBFresh,"SideADiscard","Up",[id \in sideA |-> "discard"])
       /\ afterObjects=DamageOwnerMoveMap104(first,sideA,[id \in sideA |-> successors[id]],"SideA")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: first, sideA, sideB, sideBFresh, DamageBHand104, DamageOwnerMoveMap104, CardBatchTransfer8, FreshSuccessors8, SetupPlayers

DamageCoreCounterRow104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageCoreCounterRow104 ==
 [card |-> "none",form |-> "Counter",kind |-> "PersistentCapacityLoss",zone |-> "SideBPersistentCapacityLoss",loc |-> 0,
  deployed |-> FALSE,face |-> "Up",front |-> TRUE,activated |-> FALSE,host |-> 0,placedBy |-> "SideB",virtual |-> FALSE,
  objectivePoints |-> 0,marks |-> {}]

Exact module download · Source bundle and reproduction instructions

DamageCoreCounters104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageCoreCounters104(packet,objects,afterObjects,added,usedIds) ==
 LET amount==IF packet.damageType="PersistentCapacityHarm" THEN packet.amount ELSE 0
 IN /\ DOMAIN added \subseteq (Nat \ {0}) \ usedIds
    /\ \A id \in DOMAIN added : added[id]=DamageCoreCounterRow104
    /\ BankMintProjection4(objects,afterObjects,added,amount,"PersistentCapacityLoss",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE)
    /\ PersistentCapacityLossAccrual5(PersistentCapacityLossQuantity104(objects),PersistentCapacityLossQuantity104(afterObjects),amount)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: amount, DamageCoreCounterRow104, PersistentCapacityLossQuantity104, BankMintProjection4, PersistentCapacityLossAccrual5

DamageFirstNetThisTurn104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageFirstNetThisTurn104(packet,actualDamageHistory) ==
 packet.damageType="HarmClassA" /\ ~\E id \in DOMAIN actualDamageHistory : actualDamageHistory[id].tag="DamageSuffered" /\
     actualDamageHistory[id].turnId=packet.turnId /\ actualDamageHistory[id].damageType="HarmClassA" /\ actualDamageHistory[id].amount>0

Exact module download · Source bundle and reproduction instructions

DamageMaximumHandSize104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageMaximumHandSize104(objects,effectiveOtherAdjustment) == MaximumHandSize5("SideB",PersistentCapacityLossQuantity104(objects),effectiveOtherAdjustment)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCapacityLossQuantity104, MaximumHandSize5

DamageNetMeatRetireObservation104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageNetMeatRetireObservation104(frame,objects,event,originalObject) ==
 /\ DamageBatchReadyForConditionals104(frame,objects,event) /\ originalObject \in frame.selected
 /\ frame.packet.damageType \in {"HarmClassA","HarmClassB"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageBatchReadyForConditionals104

DamageOmitted104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageOmitted104(context,reference,world,id,receipt) ==
 /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects)
 /\ id \in DOMAIN context.templates /\ context.templates[id].kind="Damage"
 /\ id \notin DOMAIN context.actualEffects
 /\ receipt=[tag |-> "NoActualDamagePacket",contextId |-> context.id,reference |-> reference,effectId |-> id,snapshotId |-> world.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99

DamageOwnerMoveMap104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageOwnerMoveMap104(objects,selected,successors,owner) ==
 LET fresh=={successors[id] : id \in selected}
 IN [id \in (DOMAIN objects \ selected) \cup fresh |-> IF id \notin fresh THEN objects[id]
      ELSE [objects[CHOOSE old \in selected : successors[old]=id] EXCEPT !.zone=owner \o "Discard",!.loc="discard",
            !.deployed=FALSE,!.activated=FALSE,!.host=0,!.face="Up",!.marks={}]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: fresh

DamagePacketFromExpected104 · operator

reference-profile · input revision 2 · CC0 1.0

DamagePacketFromExpected104(context,reference,world,id,cardFacts,packet) ==
 /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ ExpectedEffectsValid99(context.actualEffects)
 /\ id \in DOMAIN context.actualEffects
 /\ LET effect==context.actualEffects[id]
    IN /\ effect.kind="Damage" /\ effect.value>0 /\ effect.damageType \in DamageTypes104
       /\ effect.damageVerb \in {"Do","Suffer"} /\ effect.actor=DamageResponsible104(effect.damageVerb)
       /\ effect.baseOrigin=reference.source /\ effect.sourceCard \in DOMAIN cardFacts
       /\ effect.sourceSHA=cardFacts[effect.sourceCard].sourceSHA
       /\ (effect.damageVerb="Do" => cardFacts[effect.sourceCard].side="SideA")
       /\ packet=[key |-> DamagePacketKey104(context,id),contextId |-> context.id,imminenceId |-> context.imminenceId,effectId |-> id,
            reference |-> reference,snapshotId |-> world.id,turnId |-> world.turn.id,source |-> effect.baseOrigin,
            sourceCard |-> effect.sourceCard,sourceSHA |-> effect.sourceSHA,verb |-> effect.damageVerb,
            responsible |-> effect.actor,damageType |-> effect.damageType,amount |-> effect.value]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, ExpectedEffectsValid99, effect, DamagePacketKey104, DamageResponsible104, DamageTypes104

DamagePacketKey104 · operator

reference-profile · input revision 2 · CC0 1.0

DamagePacketKey104(context,id) == <<context.id,context.imminenceId,id,context.currentRef.revision>>

Exact module download · Source bundle and reproduction instructions

DamageRandomReceipt104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageRandomReceipt104(packet,remaining,amount,selected,actor,receipt) ==
 /\ selected \in RandomDamageChoices104(remaining,amount) /\ actor=packet.responsible
 /\ receipt=[tag |-> "ActualRandomDamageSelection",packet |-> packet.key,reference |-> packet.reference,
       population |-> remaining,amount |-> amount,selected |-> selected,actor |-> actor]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RandomDamageChoices104

DamageResponsible104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageResponsible104(verb) == CASE verb="Do" -> "SideA" [] verb="Suffer" -> "SideB" [] OTHER -> "UnsupportedDamageWording"

Exact module download · Source bundle and reproduction instructions

DamageSufferedEvent104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageSufferedEvent104(frame,batchId,successors) ==
 [tag |-> "DamageSuffered",packet |-> frame.packet.key,reference |-> frame.packet.reference,source |-> frame.packet.source,
  sourceCard |-> frame.packet.sourceCard,responsible |-> frame.packet.responsible,damageType |-> frame.packet.damageType,
  amount |-> frame.packet.amount,turnId |-> frame.packet.turnId,batchId |-> batchId,
  originalObjects |-> frame.selected,successors |-> successors,simultaneous |-> TRUE]

Exact module download · Source bundle and reproduction instructions

DamageTypes104 · operator

reference-profile · input revision 2 · CC0 1.0

DamageTypes104 == {"HarmClassB","HarmClassA","PersistentCapacityHarm"}

Exact module download · Source bundle and reproduction instructions

DeclineEscalatingResourceContestBoost108 · operator

reference-profile · input revision 2 · CC0 1.0

DeclineEscalatingResourceContestBoost108(before,after,world,player,announcement) ==
 /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="ChooseBoost" /\ before.nextPlayer=player /\ player \in SetupPlayers /\ player \notin before.acted
 /\ announcement=[tag |-> "EscalatingResourceContestBoostChoice",escalatingResourceContestId |-> before.id,player |-> player,mode |-> "Decline",amount |-> 0,viewers |-> SetupPlayers]
 /\ after=[before EXCEPT !.phase="SetStrength",!.pendingPlayer=player,!.acted=@ \cup {player},!.boosts[player]=[mode |-> "Decline",amount |-> 0,transaction |-> 0]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestCurrent108, SetupPlayers

DetermineEscalatingResourceContest108 · operator

reference-profile · input revision 2 · CC0 1.0

DetermineEscalatingResourceContest108(before,after,world,afterObjects,eventId,event) ==
 /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="Determine" /\ before.acted=SetupPlayers /\ \A p \in SetupPlayers : before.strengths[p].set
 /\ eventId \in (Nat \ {0}) \ world.eventIds /\ afterObjects=world.objects
 /\ LET result==IF before.strengths["SideA"].value>before.strengths["SideB"].value THEN "Successful" ELSE "Unsuccessful" IN
    /\ event=[id |-> eventId,kind |-> "EscalatingResourceContestResult",escalatingResourceContestId |-> before.id,actor |-> "SideA",source |-> before.packet.source,reference |-> before.caller,
         snapshotId |-> world.id,result |-> result,escalatingResourceContestStrength |-> before.strengths["SideA"].value,linkStrength |-> before.strengths["SideB"].value]
    /\ after=[before EXCEPT !.phase="Determined",!.point="ProcedureCode0cb35cf3f8e6",!.result=result,!.resultEvent=event]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: result, EscalatingResourceContestCurrent108, SetupPlayers

DiscoverOpenInformation102 · operator

reference-profile · input revision 2 · CC0 1.0

DiscoverOpenInformation102(facts,player,requested,responses,currentSnapshot) ==
 /\ player \in SetupPlayers /\ requested \subseteq DOMAIN facts
 /\ \A id \in requested : facts[id].viewers=SetupPlayers /\ facts[id].snapshot=currentSnapshot
 /\ responses=[id \in requested |-> [value |-> facts[id].value,snapshot |-> currentSnapshot]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

DividendApplicationSupport1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendApplicationSupport1013(plan,context) ==
 IF context.templates#DividendEffects1013(plan) THEN "RequiresDividendsCompilerAdapter"
 ELSE IF context.state.effects#DividendEffects1013(plan) \/ context.actualEffects#ActualExpectedEffects99(context.state.effects) THEN "RequiresModifiedPlacementAdapter"
 ELSE "SupportedOrdinaryPlacementApplications"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, DividendEffects1013

DividendBasis1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendBasis1013(world,instance,event,basis) ==
 /\ DividendEventSupport1013(event)="SupportedOrdinaryObjectiveCompletion" /\ instance.member.id \in DOMAIN world.conditionalLedger.instances /\ instance=world.conditionalLedger.instances[instance.member.id]
 /\ instance.occurrence=event.id /\ instance.definition.source=ObjectAbilitySource9(event.object) /\ instance.definitionCopy.syntax.source=ObjectAbilitySource9(event.object)
 /\ event.id \in DOMAIN world.objectiveCompletionEvents /\ event.scored=world.objectiveCompletionEvents[event.id] /\ event.object=event.scored.object
 /\ instance.definition \in DOMAIN world.dividendDefinitions /\ world.dividendDefinitions[instance.definition].definition=instance.definitionCopy
 /\ "WhenScored" \in ConditionalClasses96(instance.definitionCopy)
 /\ event.scored.objectiveCompletionId \in DOMAIN world.dividendBindings /\ event.scored.binding=world.dividendBindings[event.scored.objectiveCompletionId]
 /\ LET binding==world.dividendBindings[event.scored.objectiveCompletionId] capture==world.dividendCaptures[event.scored.objectiveCompletionId]
    IN /\ capture.tag="DividendObjectiveCompletionBegin" /\ capture.objectiveCompletionId=binding.objectiveCompletionId /\ capture.oldObject=binding.oldObject /\ capture.physical=binding.physical
       /\ world.dividendDefinitions[instance.definition].card=capture.sourceCard /\ world.dividendDefinitions[instance.definition].sourceSHA=capture.sourceSHA
       /\ capture.beginSnapshot=binding.beforeSnapshot /\ binding.newObject=event.object /\ event.scored.kind="ObjectivePlacementd" /\ event.scored.actor="SideA"
       /\ basis=[tag |-> "DividendCapturedBasis",instance |-> instance.member.id,occurrence |-> event.id,objectiveCompletionId |-> capture.objectiveCompletionId,target |-> binding.newObject,
            physical |-> binding.physical,sourceCard |-> capture.sourceCard,sourceSHA |-> capture.sourceSHA,requirement |-> capture.requirement,progress |-> capture.progress,
            repetitions |-> capture.excess,multiplier |-> capture.multiplier]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalClasses96, ObjectAbilitySource9, binding, capture, DividendEventSupport1013

DividendBeginSupport1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendBeginSupport1013(begin) ==
 CASE begin.mode="Replay" -> "RequiresAsIfObjectiveCompletionCaptureAdapter"
   [] begin.mode#"ObjectiveCompletion" -> "NotAnOrdinaryObjectiveCompletion"
   [] begin.costProfile#"OrdinaryCostlessObjectiveCompletion" -> "RequiresAdditionalCostCapturePointAdapter"
   [] OTHER -> "SupportedObjectiveCompletionBegin"

Exact module download · Source bundle and reproduction instructions

DividendCleanupSupport1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendCleanupSupport1013(world,capture) ==
 IF \E id \in DOMAIN world.objects : world.objects[id].host=capture.oldObject /\ world.objects[id].kind#"Progress" THEN "RequiresOtherHostedCleanupAdapter"
 ELSE IF \E id \in capture.physicalProgress : ~BankPhysicalToken4(world.objects[id]) THEN "RequiresConvertedCounterCleanupAdapter"
 ELSE "SupportedNativeProgressCleanup"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BankPhysicalToken4

DividendEffects1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendEffects1013(plan) ==
 [id \in 1..plan.basis.repetitions |-> [id |-> id,kind |-> "PlaceCounters",actor |-> "SideA",value |-> plan.basis.multiplier,target |-> plan.basis.target,counterKind |-> "Objective",counterKinds |-> {"Objective"},
   loadDefinition |-> 0,sourceCard |-> plan.basis.sourceCard,sourceSHA |-> plan.basis.sourceSHA,baseOrigin |-> plan.reference.source,dividendInstance |-> plan.instance,application |-> id]]

Exact module download · Source bundle and reproduction instructions

DividendEventSupport1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendEventSupport1013(event) ==
 IF event.kind#"ObjectivePlacementd" THEN "NotAScoredOccurrence" ELSE IF event.scopeKind="Ability" THEN "RequiresAsIfObjectiveCompletionCaptureAdapter" ELSE "SupportedOrdinaryObjectiveCompletion"

Exact module download · Source bundle and reproduction instructions

DividendFact1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendFact1013(card,cardFacts) ==
 card \in DividendSources1013 /\ card \in DOMAIN cardFacts /\ DividendFacts1013!DividendPrintedFacts1013[card].sourceSHA=cardFacts[card].sourceSHA

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DividendFacts1013!DividendPrintedFacts1013, DividendSources1013

DividendFacts1013!DividendPrintedFacts1013 · operator

reference-profile · input revision 2 · CC0 1.0

Instantiated alias. This exact declaration supplies its substitutions; original operator body: DividendPrintedFacts1013

DividendFacts1013 == INSTANCE SettlementFacts

Exact module download · Source bundle and reproduction instructions

DividendObjectiveCompletionMap1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendObjectiveCompletionMap1013(objects,old,new) ==
 ReplacementOverlay99(Without101(objects,{old}),[id \in {new} |-> [objects[old] EXCEPT !.zone="SideAObjectiveCompletion",!.deployed=FALSE,!.face="Up",!.loc=0,!.host=0,!.activated=FALSE,!.marks={},!.area="NoValue",!.targetSite="NoValue"]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, Without101

DividendPhysicalProgress1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendPhysicalProgress1013(world,host) ==
 {id \in DOMAIN world.objects : world.objects[id].form="Counter" /\ world.objects[id].kind="Progress" /\ world.objects[id].host=host /\ world.objects[id].zone=world.objects[host].zone}

Exact module download · Source bundle and reproduction instructions

DividendPlanBound1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendPlanBound1013(world,plan) ==
 /\ plan.instance \in DOMAIN world.dividendBodyAnchors
 /\ world.dividendBodyAnchors[plan.instance]=[basis |-> plan.basis,reference |-> plan.reference]
 /\ plan.reference.source=ObjectAbilitySource9(plan.basis.target)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9

DividendSources1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendSources1013 == DOMAIN DividendFacts1013!DividendPrintedFacts1013

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DividendFacts1013!DividendPrintedFacts1013

DividendTargetStatus1013 · operator

reference-profile · input revision 2 · CC0 1.0

DividendTargetStatus1013(world,plan) ==
 IF plan.basis.target \notin DOMAIN world.objects THEN "ReferencedObjectGone"
 ELSE IF world.objects[plan.basis.target].form#"Card" \/ world.objects[plan.basis.target].zone \notin {"Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} THEN "UnhostableReferencedObject"
 ELSE IF world.objects[plan.basis.target].card#plan.basis.physical THEN "DifferentPhysicalObject" ELSE "SupportedPlacementTarget"

Exact module download · Source bundle and reproduction instructions

DrainEscalatingResourceContestCheckpoint108 · operator

reference-profile · input revision 2 · CC0 1.0

DrainEscalatingResourceContestCheckpoint108(before,after,world,cardFacts,cp,ledger,stack,order) ==
 /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase \in {"InitialCheckpoint","BoostCheckpoint"}
 /\ cp.id \in DOMAIN world.checkpointFrames /\ world.checkpointFrames[cp.id]=cp /\ ledger=world.checkpointLedger
 /\ cp.caller=EscalatingResourceContestCheckpointCaller108(before) /\ cp.id \notin before.checkpoints
 /\ CheckpointDrained103(cp,ledger,stack)
 /\ IF before.phase="InitialCheckpoint" THEN
       /\ EscalatingResourceContestOrder108(world,before,cardFacts,order)
       /\ after=[before EXCEPT !.phase="ChooseBoost",!.point=IF order[1]="SideA" THEN "ProcedureCode083016920358" ELSE "ProcedureCode785a8b2e5de4",!.order=order,!.nextPlayer=order[1],!.checkpoints=@ \cup {cp.id}]
    ELSE /\ order=before.order
         /\ after=[before EXCEPT !.phase="SetStrength",!.checkpoints=@ \cup {cp.id}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, EscalatingResourceContestCheckpointCaller108, EscalatingResourceContestCurrent108, EscalatingResourceContestOrder108

DrainExposureMarkerAction105 · operator

reference-profile · input revision 2 · CC0 1.0

DrainExposureMarkerAction105(before,after,world,cp,ledger,stack) ==
 /\ before.phase \in {"BaseCostCheckpoint","AdditionalCostCheckpoint","EffectCheckpoint"} /\ world.outcome="Playing"
 /\ LET scope==CASE before.phase="BaseCostCheckpoint" -> "BaseCost" [] before.phase="AdditionalCostCheckpoint" -> "AdditionalCost" [] OTHER -> "Effect"
    IN /\ cp.caller=ExposureMarkerCheckpointCaller105(before,scope) /\ cp.snapshotId=world.id /\ CheckpointDrained103(cp,ledger,stack)
       /\ IF scope="BaseCost" THEN
            /\ ActionEffectsBegin5(before.action,after.action,TRUE) /\ after=[before EXCEPT !.phase="Targets",!.action=after.action]
          ELSE IF scope="AdditionalCost" THEN after=[before EXCEPT !.phase="EffectReady"]
          ELSE /\ ActionComplete5(before.action,after.action,TRUE) /\ after=[before EXCEPT !.phase="Complete",!.action=after.action]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: scope, CheckpointDrained103, ExposureMarkerCheckpointCaller105, ActionComplete5, ActionEffectsBegin5

EligiblePrintedLinkSources107 · operator

reference-profile · input revision 2 · CC0 1.0

EligiblePrintedLinkSources107(world) ==
 {id \in PrintedLinkObjectIds107(world) : world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.objects[id].face="Up" /\
    world.controllers[id]="SideB" /\ world.printedLinkAbilities[id] \in world.activeAbilities}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PrintedLinkObjectIds107

EmptyLink109 · operator

reference-profile · input revision 2 · CC0 1.0

EmptyLink109(world,cardFacts,link) ==
 /\ link.id \in DOMAIN world.loadLinks /\ link=world.loadLinks[link.id] /\ link.kind \in CounterKinds101 /\ link.loadDefinition \in Nat \ {0}
 /\ link.host \in DOMAIN world.objects /\ world.objects[link.host].form="Card" /\ world.objects[link.host].card=link.physical
 /\ LinkDefinition107(world,world.objects[link.host])=link.card /\ link.card \in DOMAIN cardFacts /\ link.sourceSHA=cardFacts[link.card].sourceSHA
 /\ ConditionalDefinitionValid96(link.emptyDefinition) /\ link.emptyDefinition.primaryKind="Static"
 /\ link.emptyDefinition.syntax.source=ObjectAbilitySource9(link.host)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionValid96, ObjectAbilitySource9, CounterKinds101, LinkDefinition107

EmptyStaticTruth109 · operator

reference-profile · input revision 2 · CC0 1.0

EmptyStaticTruth109(world,cardFacts,link,cp,read,truth) ==
 /\ ReadEmpty109(world,cardFacts,link,read) /\ world.id=cp.beginSnapshot.id /\ cp.beginSnapshot.loadState=LoadState109(world)
 /\ ConditionalKey96(link.emptyDefinition) \in DOMAIN cp.beginSnapshot.definitions
 /\ cp.beginSnapshot.definitions[ConditionalKey96(link.emptyDefinition)]=link.emptyDefinition
 /\ truth=[tag |-> "ConditionalStaticTruth",ability |-> link.emptyDefinition.syntax.id,source |-> link.emptyDefinition.syntax.source,
       checkpointId |-> cp.id,snapshotId |-> cp.beginSnapshot.id,condition |-> link.emptyDefinition.primaryCondition,holds |-> read.empty]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, LoadState109, ReadEmpty109

EscalatingResourceContestAssociatedBodyGate108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestAssociatedBodyGate108(frame,a) ==
 frame.result \in {"Successful","Unsuccessful"} /\ (a.bodyCondition.kind="NoValue" \/ (a.bodyCondition.kind="EscalatingResourceContestStrengthAtLeast" /\ frame.resultEvent.escalatingResourceContestStrength>=a.bodyCondition.amount))

Exact module download · Source bundle and reproduction instructions

EscalatingResourceContestAssociatedCandidate108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestAssociatedCandidate108(frame,a,event,stipulation) ==
 /\ EscalatingResourceContestAssociatedOccurrence108(frame,a,event,event.snapshot)
 /\ stipulation=EscalatingResourceContestAssociatedStipulation108(frame,a,event)
 /\ TriggerPattern96(a.definition,event) /\ TriggerStipulations96(a.definition,event,stipulation)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TriggerPattern96, TriggerStipulations96, EscalatingResourceContestAssociatedOccurrence108, EscalatingResourceContestAssociatedStipulation108

EscalatingResourceContestAssociatedInstructionCondition108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestAssociatedInstructionCondition108(frame,a,event,instance,condition) ==
 /\ EscalatingResourceContestAssociatedOccurrence108(frame,a,event,event.snapshot)
 /\ instance.occurrence=event.id /\ instance.definition=ConditionalKey96(a.definition) /\ instance.definitionCopy=a.definition
 /\ condition=[tag |-> "EscalatingResourceContestAssociatedInstructionCondition",escalatingResourceContestId |-> frame.id,occurrence |-> event.id,
       definition |-> instance.definition,instance |-> instance.member.id,holds |-> EscalatingResourceContestAssociatedBodyGate108(frame,a)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, EscalatingResourceContestAssociatedBodyGate108, EscalatingResourceContestAssociatedOccurrence108

EscalatingResourceContestAssociatedMatches108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestAssociatedMatches108(frame,a) ==
 frame.result \in {"Successful","Unsuccessful"} /\
 (a.trigger="AnyResult" \/ (a.trigger="Successful" /\ frame.result="Successful") \/ (a.trigger="Unsuccessful" /\ frame.result="Unsuccessful"))

Exact module download · Source bundle and reproduction instructions

EscalatingResourceContestAssociatedOccurrence108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestAssociatedOccurrence108(frame,a,event,snapshot) ==
 /\ a.id \in DOMAIN frame.packet.associations /\ a=frame.packet.associations[a.id]
 /\ frame.result \in {"Successful","Unsuccessful"} /\ event.id \in Nat \ {0}
 /\ event.rawResultId=frame.resultEvent.id /\ event.escalatingResourceContestId=frame.id
 /\ event.kind="EscalatingResourceContestAssociatedResult" /\ event.actor="SideA" /\ event.side="SideA" /\ event.snapshot=snapshot
 /\ snapshot.id=frame.resultEvent.snapshotId /\ event.scopeKind="Ability" /\ event.scopeDefinition=ConditionalKey96(a.definition)
 /\ event.escalatingResourceContestStrength=frame.resultEvent.escalatingResourceContestStrength /\ event.linkStrength=frame.resultEvent.linkStrength /\ event.result=frame.result
 /\ event.object=frame.packet.source.object

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96

EscalatingResourceContestAssociatedStipulation108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestAssociatedStipulation108(frame,a,event) ==
 [tag |-> "ConditionalTriggerStipulations",ability |-> a.definition.syntax.id,source |-> a.definition.syntax.source,
  occurrence |-> event.id,snapshotId |-> event.snapshot.id,results |-> [id \in a.definition.triggerRequirements |-> EscalatingResourceContestAssociatedMatches108(frame,a)]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestAssociatedMatches108

EscalatingResourceContestBoostRule108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestBoostRule108(player) == RuleAbilitySource9(IF player="SideA" THEN "ProcedureCode000048c944c1" ELSE "ProcedureCode306f617c02aa")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9

EscalatingResourceContestCheckpointCaller108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestCheckpointCaller108(frame) ==
 IF frame.phase="InitialCheckpoint" THEN InstructionPauseCaller911([id |-> frame.instance],frame.caller,"EscalatingResourceContest",frame,"ProcedureCoded1e36ce96789")
 ELSE [kind |-> "EscalatingResourceContestBoostCostCheckpoint",escalatingResourceContestId |-> frame.id,instance |-> frame.instance,caller |-> frame.caller,
       player |-> frame.pendingPlayer,transactionId |-> frame.boosts[frame.pendingPlayer].transaction,point |-> frame.point]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionPauseCaller911

EscalatingResourceContestContextualLink108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestContextualLink108(frame,world,cardFacts,base,declarations,read,value) ==
 /\ ReadSideBLink107(world,cardFacts,base,declarations,read)
 /\ DOMAIN world.escalatingResourceContestLinkPolicies=IF frame.ordinal=1 THEN EscalatingResourceContestRoleIds108(world,"EscalatingResourceContestLinkZero","Specimen0154") ELSE {}
 /\ \A id \in DOMAIN world.escalatingResourceContestLinkPolicies :
      LET p==world.escalatingResourceContestLinkPolicies[id] IN
      /\ p.snapshotId=world.id /\ p.escalatingResourceContestId=frame.id /\ p.value=0 /\ p.ability=id
      /\ EscalatingResourceContestSourceRead108(world,p.source,p.sourceObject,p.sourceSHA,id,cardFacts)
      /\ p.sourceObject.zone="SideAObjectiveCompletion" /\ LinkDefinition107(world,p.sourceObject)="Specimen0154"
 /\ value=IF DOMAIN world.escalatingResourceContestLinkPolicies={} THEN read.value ELSE 0

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p, EscalatingResourceContestRoleIds108, EscalatingResourceContestSourceRead108, LinkDefinition107, ReadSideBLink107

EscalatingResourceContestCurrent108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestCurrent108(frame,world) ==
 frame.id \in DOMAIN world.escalatingResourceContestFrames /\ world.escalatingResourceContestFrames[frame.id]=frame /\ ~frame.complete /\ ~frame.returned /\ world.outcome="Playing" /\ world.turn.id=frame.turnId

Exact module download · Source bundle and reproduction instructions

EscalatingResourceContestDuringTraversal108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestDuringTraversal108(world) == DuringTraversal6(world.traversal) /\ TimingRef9("SchemaAtom138",world.traversal.id) \in world.inside

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, DuringTraversal6

EscalatingResourceContestInitialFrame108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestInitialFrame108(id,packet,turnId,ordinal) ==
 [tag |-> "ActualEscalatingResourceContestProcedure",id |-> id,instance |-> packet.reference.abilityInstance,caller |-> packet.reference,packet |-> packet,
  turnId |-> turnId,ordinal |-> ordinal,phase |-> "InitialCheckpoint",point |-> "ProcedureCoded1e36ce96789",order |-> <<>>,nextPlayer |-> "NoValue",acted |-> {},
  boosts |-> [p \in SetupPlayers |-> [mode |-> "NoValue",amount |-> 0,transaction |-> 0]],
  strengths |-> [p \in SetupPlayers |-> [set |-> FALSE,value |-> 0]],pendingPlayer |-> "NoValue",checkpoints |-> {},
  result |-> "Undetermined",resultEvent |-> [id |-> 0],complete |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

EscalatingResourceContestOmitted108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestOmitted108(context,reference,world,id) ==
 context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\
 id \in DOMAIN context.templates /\ context.templates[id].kind="EscalatingResourceContest" /\ id \notin DOMAIN context.actualEffects

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99

EscalatingResourceContestOrder108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestOrder108(world,frame,cardFacts,order) ==
 /\ DOMAIN world.escalatingResourceContestOrderPolicies=IF EscalatingResourceContestDuringTraversal108(world) THEN EscalatingResourceContestRoleIds108(world,"EscalatingResourceContestOrder","Specimen0231") ELSE {}
 /\ \A id \in DOMAIN world.escalatingResourceContestOrderPolicies :
      LET p==world.escalatingResourceContestOrderPolicies[id] IN
      /\ p.snapshotId=world.id /\ p.escalatingResourceContestId=frame.id /\ p.order= <<"SideB","SideA">> /\ p.ability=id
      /\ EscalatingResourceContestSourceRead108(world,p.source,p.sourceObject,p.sourceSHA,id,cardFacts)
      /\ world.controllers[p.source.object]="SideA" /\ LinkDefinition107(world,p.sourceObject)="Specimen0231"
 /\ order=IF DOMAIN world.escalatingResourceContestOrderPolicies={} THEN <<"SideA","SideB">> ELSE <<"SideB","SideA">>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p, EscalatingResourceContestDuringTraversal108, EscalatingResourceContestRoleIds108, EscalatingResourceContestSourceRead108, LinkDefinition107

EscalatingResourceContestPacket108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestPacket108(context,reference,world,id,cardFacts,packet) ==
 /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ id \in DOMAIN context.templates
 /\ context.templates[id].kind="EscalatingResourceContest"
 /\ LET effect==context.actualEffects[id] IN
    /\ effect.kind="EscalatingResourceContest" /\ effect.value \in Int /\ effect.actor="SideA" /\ effect.baseOrigin=reference.source
    /\ effect.sourceCard=context.templates[id].sourceCard /\ effect.sourceSHA=context.templates[id].sourceSHA
    /\ effect.sourceCard \in DOMAIN cardFacts /\ effect.sourceSHA=cardFacts[effect.sourceCard].sourceSHA
    /\ \A clause \in DOMAIN effect.associations :
         LET a==effect.associations[clause] IN
         /\ a.id=clause /\ a.trigger \in {"Successful","Unsuccessful","AnyResult"}
         /\ a.source=reference.source /\ a.sourceSHA=effect.sourceSHA
         /\ ConditionalDefinitionValid96(a.definition) /\ a.definition.syntax.source=reference.source
         /\ a.definition.primaryKind="Trigger" /\ a.definition.trigger.kinds={"EscalatingResourceContestAssociatedResult"}
         /\ a.definition.triggerRequirements=IF a.trigger="AnyResult" THEN {} ELSE {1}
         /\ a.bodyCondition.kind \in {"NoValue","EscalatingResourceContestStrengthAtLeast"}
         /\ (a.bodyCondition.kind="EscalatingResourceContestStrengthAtLeast" => a.bodyCondition.amount \in Int)
    /\ packet=[key |-> <<context.id,reference,id>>,contextId |-> context.id,reference |-> reference,effectId |-> id,
         source |-> effect.baseOrigin,sourceCard |-> effect.sourceCard,sourceSHA |-> effect.sourceSHA,base |-> effect.value,associations |-> effect.associations]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, ConditionalDefinitionValid96, a, effect

EscalatingResourceContestPermissionUseSources108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestPermissionUseSources108(payment,permissions) ==
 CounterPermissionUseSources9(payment,[id \in DOMAIN permissions |-> [source |-> permissions[id].source,paymentId |-> permissions[id].paymentId,allowsPayment |-> TRUE,paidCounters |-> permissions[id].counters \cap payment.paidCounterIds]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterPermissionUseSources9

EscalatingResourceContestPoolIds108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestPoolIds108(objects,player) ==
 IF player="SideB" THEN BaseSideBPoolIds106(objects)
 ELSE {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ResourceUnit" /\ objects[id].host=0 /\
      (objects[id].zone="SideAResourceUnits" \/ (objects[id].zone="Play" /\ objects[id].resourceUnitLocation="SideAPool"))}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BaseSideBPoolIds106

EscalatingResourceContestRecurringPermission108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestRecurringPermission108(frame,world,payer,transaction,p,cardFacts) ==
 /\ EscalatingResourceContestCurrent108(frame,world)
 /\ p.escalatingResourceContestId=frame.id /\ p.snapshotId=world.id /\ p.player=payer /\ p.paymentId=transaction /\ p.purpose="EscalatingResourceContest"
 /\ EscalatingResourceContestSourceRead108(world,p.source,p.sourceObject,p.sourceSHA,p.ability,cardFacts)
 /\ world.controllers[p.source.object]=payer /\ world.abilityRoles[p.ability]="EscalatingResourceContestPermission"
 /\ LinkDefinition107(world,p.sourceObject)=IF payer="SideA" THEN "Specimen0184" ELSE "Specimen0056"
 /\ \A id \in p.counters : id \in DOMAIN world.objects /\ world.objects[id].form="Counter" /\ world.objects[id].kind="ResourceUnit" /\
       ~world.objects[id].virtual /\ world.objects[id].host=p.source.object /\ world.controllers[id]=payer

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EscalatingResourceContestCurrent108, EscalatingResourceContestSourceRead108, LinkDefinition107

EscalatingResourceContestRoleIds108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestRoleIds108(world,role,definition) ==
 {id \in world.activeAbilities \cap DOMAIN world.abilityRoles \cap DOMAIN world.abilitySources :
   world.abilityRoles[id]=role /\ world.abilitySources[id].kind="Object" /\ world.abilitySources[id].object \in DOMAIN world.objects /\
   LinkDefinition107(world,world.objects[world.abilitySources[id].object])=definition}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LinkDefinition107

EscalatingResourceContestSourceRead108 · operator

reference-profile · input revision 2 · CC0 1.0

EscalatingResourceContestSourceRead108(world,source,object,sourceSHA,ability,cardFacts) ==
 /\ source.kind="Object" /\ source.object \in DOMAIN world.objects /\ object=world.objects[source.object]
 /\ object.card \in DOMAIN world.definitions /\ LinkDefinition107(world,object) \in DOMAIN cardFacts
 /\ sourceSHA=cardFacts[LinkDefinition107(world,object)].sourceSHA
 /\ ability \in world.activeAbilities /\ ability \in DOMAIN world.abilitySources /\ world.abilitySources[ability]=source
 /\ DefaultActive([object EXCEPT !.card=LinkDefinition107(world,object)],world.started,cardFacts)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LinkDefinition107, DefaultActive

EstablishEscalatingResourceContestStrength108 · operator

reference-profile · input revision 2 · CC0 1.0

EstablishEscalatingResourceContestStrength108(before,after,world,cardFacts,base,declarations,linkRead,contextualLink) ==
 /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="SetStrength" /\ before.pendingPlayer \in before.acted
 /\ LET player==before.pendingPlayer
        value==IF player="SideA" THEN before.packet.base+before.boosts[player].amount ELSE contextualLink+before.boosts[player].amount
    IN /\ ~before.strengths[player].set
       /\ IF player="SideB" THEN EscalatingResourceContestContextualLink108(before,world,cardFacts,base,declarations,linkRead,contextualLink) ELSE contextualLink=0
       /\ after=[before EXCEPT !.strengths[player]=[set |-> TRUE,value |-> value],!.pendingPlayer="NoValue",
            !.phase=IF before.acted=SetupPlayers THEN "Determine" ELSE "ChooseBoost",
            !.nextPlayer=IF before.acted=SetupPlayers THEN "NoValue" ELSE before.order[2],
            !.point=IF before.acted=SetupPlayers THEN "ProcedureCode42d1fb0bb9d2" ELSE IF before.order[2]="SideA" THEN "ProcedureCode083016920358" ELSE "ProcedureCode785a8b2e5de4"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: player, value, EscalatingResourceContestContextualLink108, EscalatingResourceContestCurrent108, SetupPlayers

ExampleFamily009SelectionShape104 · operator

reference-profile · input revision 2 · CC0 1.0

ExampleFamily009SelectionShape104(packet,authority,actualDamageHistory) ==
 /\ authority.card="Specimen0051" /\ DamageFirstNetThisTurn104(packet,actualDamageHistory)
 /\ authority.slots[1]=[mode |-> "Choose",actor |-> "SideA"]
 /\ \A i \in 2..Len(authority.slots) : authority.slots[i]=[mode |-> "Random",actor |-> packet.responsible]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageFirstNetThisTurn104

ExampleFamily011ExposureMarkerPermission105 · operator

reference-profile · input revision 2 · CC0 1.0

ExampleFamily011ExposureMarkerPermission105(world,kind,transaction,permission,cardFacts) ==
 /\ kind="RemoveExposureMarker" /\ permission.action=kind /\ permission.player="SideB" /\ permission.paymentId=transaction
 /\ permission.snapshotId=world.id /\ permission.allowsPayment /\ permission.sourceObject.card="Specimen0058"
 /\ ExposureMarkerSourceBound105(world,permission.source,permission.sourceObject,permission.sourceSHA,cardFacts)
 /\ \A id \in permission.paidCounters : id \in DOMAIN world.objects /\ BankPhysicalToken4(world.objects[id])
       /\ world.objects[id].kind="ResourceUnit" /\ world.objects[id].host=permission.source.object /\ world.controllers[id]="SideB"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerSourceBound105, BankPhysicalToken4

ExampleFamily049DeployedReference1010 · operator

reference-profile · input revision 2 · CC0 1.0

ExampleFamily049DeployedReference1010(beforeObjects,afterObjects,old,new,successors,used,source,deployReference,reference) ==
 /\ deployReference.source=source /\ old \in DOMAIN beforeObjects /\ beforeObjects[old].zone="SideBHand"
 /\ successors=[id \in {old} |-> new]
 /\ CardBatchTransfer8(beforeObjects,afterObjects,{old},successors,used,"Play","Up",[id \in {old} |-> 0])
 /\ reference=[tag |-> "InstructionDeployedObject",source |-> source,fromInstruction |-> deployReference,oldObject |-> old,object |-> new,physical |-> beforeObjects[old].card]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardBatchTransfer8

ExampleFamily094ExposureMarkerCostShape105 · operator

reference-profile · input revision 2 · CC0 1.0

ExampleFamily094ExposureMarkerCostShape105(kind,sourceObject,chosenReduction,delta) ==
 /\ sourceObject.card="Specimen0233"
 /\ IF sourceObject.front THEN delta=IF kind="RemoveExposureMarker" THEN 1 ELSE 0
    ELSE delta=IF kind="RetireResource" /\ chosenReduction THEN -2 ELSE 0

Exact module download · Source bundle and reproduction instructions

ExecuteBankHostedCounterInstruction109 · operator

reference-profile · input revision 2 · CC0 1.0

ExecuteBankHostedCounterInstruction109(context,reference,world,id,cardFacts,afterObjects,afterHistory,afterCompleted,selected,added,afterNext,eventId,event) ==
 /\ CounterInstruction109(context,reference,world,id,cardFacts)
 /\ HostedCounterExecutionDisposition109(world,context.actualEffects[id])="Supported"
 /\ eventId \in (Nat \ {0}) \ (world.counterEventIds \cup DOMAIN world.loadHistory)
 /\ CounterInstructionKey109(context,reference,id) \notin world.completedCounterInstructions
 /\ LET e==context.actualEffects[id]
        first==world.nextCounterObject
        created==IF e.kind="RemoveCounters" THEN {} ELSE first..(first+e.value-1)
        history==[tag |-> "CompletedLoad",host |-> e.target,kind |-> e.counterKind,loadDefinition |-> e.loadDefinition,
             reference |-> reference,sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA,amount |-> e.value,createdCounterIds |-> created,snapshotId |-> world.id]
    IN /\ IF e.kind="RemoveCounters" THEN
             /\ added=[emptyId \in {} |-> emptyId] /\ afterNext=first
             /\ selected \subseteq MovableHostedTokens109(world.objects,e.target,e.counterKind)
             /\ Cardinality(selected)=MinOf(e.value,Cardinality(MovableHostedTokens109(world.objects,e.target,e.counterKind)))
             /\ BankSpendReturn4(world.objects,afterObjects,selected,TRUE)
           ELSE
             /\ selected={} /\ first \in Nat \ {0} /\ created \cap world.usedObjects={}
             /\ added=[i \in created |-> LoadedCounterToken109(e.counterKind,world.objects[e.target].zone,e.target,e.actor)]
             /\ afterNext=first+e.value
             /\ BankMintProjection4(world.objects,afterObjects,added,e.value,e.counterKind,world.usedObjects,BankDefaultSource4(IF e.kind="LoadCounters" THEN "Load" ELSE "Place",FALSE,[kind |-> "NoValue"]),TRUE,TRUE)
       /\ afterHistory=IF e.kind="LoadCounters" THEN ReplacementOverlay99(world.loadHistory,[i \in {eventId} |-> history]) ELSE world.loadHistory
       /\ afterCompleted=world.completedCounterInstructions \cup {CounterInstructionKey109(context,reference,id)}
       /\ event=[tag |-> "HostedCounterInstructionComplete",id |-> eventId,operation |-> e.kind,reference |-> reference,host |-> e.target,
             kind |-> e.counterKind,amount |-> e.value,selected |-> selected,created |-> created,snapshotId |-> world.id,complete |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, created, e, first, history, CounterInstruction109, CounterInstructionKey109, HostedCounterExecutionDisposition109, LoadedCounterToken109, MovableHostedTokens109, MinOf, BankDefaultSource4, BankMintProjection4, BankSpendReturn4

ExpiredRetainedPlayIds103 · operator

reference-profile · input revision 2 · CC0 1.0

ExpiredRetainedPlayIds103(retentions,objects,liveIds) ==
 {retentions[id].source : id \in {i \in DOMAIN retentions \ liveIds : retentions[i].source \in DOMAIN objects /\ objects[retentions[i].source].zone="Play"}}

Exact module download · Source bundle and reproduction instructions

ExposureMarkerActionActor105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerActionActor105(kind) == IF kind="RetireResource" THEN "SideA" ELSE "SideB"

Exact module download · Source bundle and reproduction instructions

ExposureMarkerActionKey105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerActionKey105(kind) == BasicActionKey5(ExposureMarkerActionActor105(kind),kind)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerActionActor105, BasicActionKey5

ExposureMarkerActionRule105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerActionRule105(kind) == IF kind="RetireResource" THEN "ProcedureCodeef666cf169ed" ELSE "ProcedureCode383141df25e9"

Exact module download · Source bundle and reproduction instructions

ExposureMarkerActionStatusGate105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerActionStatusGate105(kind,hasExposureMarkers) == kind="RemoveExposureMarker" \/ (kind="RetireResource" /\ hasExposureMarkers)

Exact module download · Source bundle and reproduction instructions

ExposureMarkerActionTargets105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerActionTargets105(frame,world) == IF frame.kind="RetireResource" THEN ResourceTargetIds105(world) ELSE MovableExposureMarkerIds105(world.objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MovableExposureMarkerIds105, ResourceTargetIds105

ExposureMarkerCheckpointCaller105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerCheckpointCaller105(frame,scope) ==
 [kind |-> "BasicExposureMarkerActionCheckpoint",action |-> frame.id,scope |-> scope,
  transaction |-> IF scope="BaseCost" THEN frame.transaction ELSE IF scope="AdditionalCost" THEN frame.nestedTransaction ELSE 0]

Exact module download · Source bundle and reproduction instructions

ExposureMarkerCostModifiers105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerCostModifiers105(world,kind,mods,cardFacts) ==
 /\ mods=world.exposureMarkerCostModifiers[kind]
 /\ \A source \in world.activeSources \cap DOMAIN world.objects :
       IF world.objects[source].card="Specimen0233" /\ DefaultActive(world.objects[source],world.started,cardFacts) THEN
          /\ Cardinality({id \in DOMAIN mods : mods[id].source.object=source})<=1
          /\ (world.objects[source].front /\ kind="RemoveExposureMarker" => Cardinality({id \in DOMAIN mods : mods[id].source.object=source})=1)
       ELSE TRUE
 /\ \A id \in DOMAIN mods : mods[id].snapshotId=world.id /\ mods[id].action=kind /\ mods[id].delta \in Int
       /\ ExposureMarkerSourceBound105(world,mods[id].source,mods[id].sourceObject,mods[id].sourceSHA,cardFacts)
       /\ (mods[id].sourceObject.card="Specimen0233" => ExampleFamily094ExposureMarkerCostShape105(kind,mods[id].sourceObject,mods[id].chosenReduction,mods[id].delta))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExampleFamily094ExposureMarkerCostShape105, ExposureMarkerSourceBound105, DefaultActive

ExposureMarkerCounterRow105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerCounterRow105 == [DamageCoreCounterRow104 EXCEPT !.kind="ExposureMarker",!.zone="SideBExposureMarkers"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageCoreCounterRow104

ExposureMarkerIds105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerIds105(objects) == {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ExposureMarker" /\ objects[id].zone="SideBExposureMarkers" /\ objects[id].host=0}

Exact module download · Source bundle and reproduction instructions

ExposureMarkerPaymentPermissionSources105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerPaymentPermissionSources105(payment,permissions) ==
 CounterPermissionUseSources9(payment,[id \in DOMAIN permissions |-> [permissions[id] EXCEPT !.paidCounters=@ \cap payment.paidCounterIds]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterPermissionUseSources9

ExposureMarkerQuantity105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerQuantity105(objects) == Cardinality(ExposureMarkerIds105(objects))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerIds105

ExposureMarkerResourceUnitCost105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerResourceUnitCost105(mods) ==
 ModifiedCost(2,<<SumMap([id \in {i \in DOMAIN mods : mods[i].delta>0} |-> mods[id].delta])>>,
                <<SumMap([id \in {i \in DOMAIN mods : mods[i].delta<0} |-> -mods[id].delta])>>)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ModifiedCost, SumMap

ExposureMarkerResourceUnitEligible105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerResourceUnitEligible105(world,player,permissions) ==
 {id \in DOMAIN world.objects : BankPhysicalToken4(world.objects[id]) /\ world.objects[id].kind="ResourceUnit" /\ world.controllers[id]=player /\
    ((world.objects[id].zone=player \o "ResourceUnits" /\ world.objects[id].host=0) \/
      \E p \in DOMAIN permissions : id \in permissions[p].paidCounters)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BankPhysicalToken4

ExposureMarkerSourceBound105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerSourceBound105(world,source,object,sourceSHA,cardFacts) ==
 /\ source.kind="Object" /\ source.object \in DOMAIN world.objects /\ object=world.objects[source.object]
 /\ object.card \in DOMAIN cardFacts /\ sourceSHA=cardFacts[object.card].sourceSHA
 /\ source.object \in world.activeSources /\ DefaultActive(object,world.started,cardFacts)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive

ExposureMarkerStateView105 · operator

reference-profile · input revision 2 · CC0 1.0

ExposureMarkerStateView105(objects,declarations) ==
 [quantity |-> ExposureMarkerQuantity105(objects),hasExposureMarkers |-> ExposureMarkerQuantity105(objects)>0 \/ DOMAIN declarations#{},movable |-> MovableExposureMarkerIds105(objects)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerQuantity105, MovableExposureMarkerIds105

FinishBid1014 · operator

reference-profile · input revision 2 · CC0 1.0

FinishBid1014(before,after,world,checkpoint,ledger,completion) ==
 /\ BidCheckpointReady1014(before,world,checkpoint,ledger)
 /\ completion=[tag |-> "BiddingInstructionComplete",bidId |-> before.id,caller |-> before.revealCaller,result |-> before.result,checkpoint |-> checkpoint.id,paid |-> TRUE]
 /\ after=[before EXCEPT !.phase="Complete",!.complete=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidCheckpointReady1014

FirstMarkEvent1011 · operator

reference-profile · input revision 2 · CC0 1.0

FirstMarkEvent1011(world,mark,kind,event) ==
 event \in MarkRelatedEvents1011(world,mark,kind) /\ \A earlier \in MarkRelatedEvents1011(world,mark,kind) : world.history[earlier].serial>=world.history[event].serial

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MarkRelatedEvents1011

GeneralBidInstructionCheckpoint1014 · operator

reference-profile · input revision 2 · CC0 1.0

GeneralBidInstructionCheckpoint1014(before,after,world,checkpoint,ledger) ==
 /\ BidCurrent1014(before,world) /\ before.phase="WaitingReveal" /\ ~before.paid
 /\ checkpoint.id \in DOMAIN world.checkpoints /\ world.checkpoints[checkpoint.id]=checkpoint /\ world.conditionalLedger=ledger
 /\ LET stage==IF before.guess="NoValue" THEN "Selection" ELSE "Guess" IN
    /\ checkpoint.caller=[kind |-> "GeneralBiddingInstructionEnd",bidId |-> before.id,caller |-> before.caller,stage |-> stage]
    /\ stage \notin before.generalStages /\ CheckpointDrained103(checkpoint,ledger,<<>>)
    /\ after=[before EXCEPT !.generalStages=@ \cup {stage},!.generalCheckpoints=@ \cup {checkpoint.id}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: stage, BidCurrent1014, CheckpointDrained103

GrantLiabilityMarkerFund106 · operator

reference-profile · input revision 2 · CC0 1.0

GrantLiabilityMarkerFund106(before,after,world,afterObjects,declarations,cardFacts,added,usedIds,events) ==
 /\ world.traversal=before.traversal /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.formalBegun /\ world.outcome="Playing"
 /\ CurrentLiabilityMarker106(world,declarations,cardFacts,LiabilityMarkerQuantity106(world.objects))
 /\ AddInitiationLiabilityMarker6(before,after,Cardinality(LiabilityMarkerFundIds106(world.objects)),Cardinality(LiabilityMarkerFundIds106(afterObjects)),LiabilityMarkerQuantity106(world.objects))
 /\ \A id \in DOMAIN added : added[id]=LiabilityMarkerFundRow106
 /\ BankMintProjection4(world.objects,afterObjects,added,LiabilityMarkerQuantity106(world.objects),"ResourceUnit",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE)
 /\ events=IF DOMAIN added={} THEN {} ELSE {[tag |-> "LiabilityMarkerFundLoaded",traversalId |-> before.traversal.id,source |-> RuleAbilitySource9("ProcedureCode5da712559aad"),
       snapshotId |-> world.id,added |-> DOMAIN added,amount |-> LiabilityMarkerQuantity106(world.objects)]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9, CurrentLiabilityMarker106, LiabilityMarkerFundIds106, LiabilityMarkerFundRow106, LiabilityMarkerQuantity106, BankMintProjection4, AddInitiationLiabilityMarker6, TraversalTimingPresent6

HistoricalMark1011 · operator

reference-profile · input revision 2 · CC0 1.0

HistoricalMark1011(world,mark) ==
 mark.tag="CurrentGlobalMark" /\ mark.present /\
 \E id \in DOMAIN world.history : LET e==world.history[id] IN
   e.kind="MarkDesignated" /\ e.effectId=mark.effectId /\ e.targetSite=mark.targetSite /\ e.turn=mark.turn /\ e.serial=mark.cutoff

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: e

HostedCounterExecutionDisposition109 · operator

reference-profile · input revision 2 · CC0 1.0

HostedCounterExecutionDisposition109(world,e) ==
 IF CounterInstructionDisposition109(e)#"Supported" THEN CounterInstructionDisposition109(e)
 ELSE IF e.kind="RemoveCounters" /\ e.value>Cardinality(MovableHostedTokens109(world.objects,e.target,e.counterKind)) /\
      {id \in HostedCounterIds109(world.objects,e.target,e.counterKind) : ~world.objects[id].virtual /\ world.objects[id].card#"none"}#{}
      THEN "RequiresConvertedCounterDeparture" ELSE "Supported"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterInstructionDisposition109, HostedCounterIds109, MovableHostedTokens109

HostedCounterIds109 · operator

reference-profile · input revision 2 · CC0 1.0

HostedCounterIds109(objects,host,kind) ==
 {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind=kind /\ objects[id].host=host /\ objects[id].zone=objects[host].zone}

Exact module download · Source bundle and reproduction instructions

IdentifyMark1011 · operator

reference-profile · input revision 2 · CC0 1.0

IdentifyMark1011(before,after,a,context,origin,operation,cardFacts,read,draw,sampler,effectId,eventId,execution,completion,events) ==
 /\ MarkInstruction1011(context,origin,before,operation,cardFacts) /\ MarkRead1011(before,a,context.actualEffects[operation].actor,read)
 /\ IF read.present THEN
       /\ context.actualEffects[operation].blueprints=[emptyId \in {} |-> emptyId] /\ draw=[tag |-> "NoDraw"]
       /\ after=before /\ events={}
       /\ completion=[tag |-> "IdentifyMarkComplete",reference |-> context.currentRef,operation |-> operation,created |-> FALSE,effectId |-> read.effectId,targetSite |-> read.targetSite]
     ELSE
       /\ ~before.turn.formalEnded /\ eventId \in (Nat \ {0}) \ DOMAIN before.history
       /\ LET targetSite==draw.targetSite
              cutoff==before.eventSerial+1
              blueprint==MarkBlueprint1011(context.currentRef.source,IF origin.plan.origin="Rule" THEN "Rule" ELSE origin.parent.kind,targetSite,cutoff,before.turn.id)
              event==[id |-> eventId,kind |-> "MarkDesignated",serial |-> cutoff,turn |-> before.turn.id,targetSite |-> targetSite,effectId |-> effectId,reference |-> context.currentRef,source |-> context.currentRef.source]
          IN /\ MarkDraw1011(before,context,operation,draw,sampler,targetSite)
             /\ context.actualEffects[operation].blueprints=[id \in {effectId} |-> blueprint]
             /\ CreateObservedLingeringEffects910(before.lingering,after.lingering,context,origin,operation,execution,a)
             /\ after=[before EXCEPT !.lingering=after.lingering,!.eventSerial=cutoff,!.history=ReplacementOverlay99(@,[id \in {eventId} |-> event]),
                    !.draws=ReplacementOverlay99(@,[id \in {draw.id} |-> draw]),!.pendingRandomDraws=Without101(@,{draw.id})]
             /\ completion=[tag |-> "IdentifyMarkComplete",reference |-> context.currentRef,operation |-> operation,created |-> TRUE,effectId |-> effectId,targetSite |-> targetSite]
             /\ events={event}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CreateObservedLingeringEffects910, ReplacementOverlay99, blueprint, cutoff, event, targetSite, MarkDraw1011, MarkInstruction1011, MarkRead1011, Without101

IllegalRetireChooser103 · operator

reference-profile · input revision 2 · CC0 1.0

IllegalRetireChooser103(choices,controllers,activePlayer) ==
 LET objects==UNION choices
     players=={controllers[id] : id \in objects}
 IN IF Cardinality(choices)<=1 THEN "NoValue" ELSE IF Cardinality(players)=1 /\ players \subseteq SetupPlayers THEN CHOOSE p \in players : TRUE ELSE activePlayer

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: players, SetupPlayers

InformationClass102 · operator

reference-profile · input revision 2 · CC0 1.0

InformationClass102(viewers) == IF viewers=SetupPlayers THEN "Open" ELSE "Hidden"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

InformationFact102 · operator

reference-profile · input revision 2 · CC0 1.0

InformationFact102(value,viewers,snapshot) ==
 [value |-> value,viewers |-> viewers,snapshot |-> snapshot]

Exact module download · Source bundle and reproduction instructions

LiabilityMarkerCounterDeparture106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerCounterDeparture106(objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) ==
 /\ CheckpointRetirePost103(objects,afterObjects,selected,successors,usedIds,printed,owners,visible)
 /\ LET cards=={id \in selected : objects[id].card#"none"} IN
    IF cards={} THEN BankSpendReturn4(objects,afterObjects,selected,TRUE) /\ afterHistory=beforeHistory /\ events={}
    ELSE RecordMovement8(beforeHistory,afterHistory,batchId,"Retire",cards,"Complete",TRUE,{MovementEvent8(batchId,"Retire",cards)}) /\ events={MovementEvent8(batchId,"Retire",cards)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cards, CheckpointRetirePost103, BankSpendReturn4, MovementEvent8, RecordMovement8

LiabilityMarkerCounterRow106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerCounterRow106 == [DamageCoreCounterRow104 EXCEPT !.kind="LiabilityMarker",!.zone="SideALiabilityMarker",!.placedBy="SideA"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageCoreCounterRow104

LiabilityMarkerFundController106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerFundController106(object,ordinaryController) ==
 IF LiabilityMarkerFundIds106([id \in {1} |-> object])={1} THEN "SideB" ELSE ordinaryController

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiabilityMarkerFundIds106

LiabilityMarkerFundIds106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerFundIds106(objects) ==
 {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ResourceUnit" /\ objects[id].zone="Play" /\ objects[id].host=0 /\ objects[id].resourceUnitLocation="LiabilityMarkerFund"}

Exact module download · Source bundle and reproduction instructions

LiabilityMarkerFundRow106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerFundRow106 == ReplacementOverlay99(DamageCoreCounterRow104,
 [kind |-> "ResourceUnit",zone |-> "Play",resourceUnitLocation |-> "LiabilityMarkerFund",placedBy |-> "SideB"])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, DamageCoreCounterRow104

LiabilityMarkerIds106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerIds106(objects) ==
 {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="LiabilityMarker" /\ objects[id].zone="SideALiabilityMarker" /\ objects[id].host=0}

Exact module download · Source bundle and reproduction instructions

LiabilityMarkerPacket106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerPacket106(context,reference,world,id,cardFacts,packet) ==
 /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates
 /\ LET original==context.templates[id]
        kept==id \in DOMAIN context.actualEffects
        actual==IF kept THEN context.actualEffects[id] ELSE original
    IN /\ original.kind="LiabilityMarker" /\ original.operation \in {"Take","Give","Remove"} /\ original.target="SideA"
       /\ actual.kind=original.kind /\ actual.operation=original.operation /\ actual.target="SideA" /\ actual.actor=original.actor
       /\ actual.actor \in SetupPlayers /\ (actual.operation="Take" => actual.actor="SideA") /\ (actual.operation="Give" => actual.actor="SideB")
       /\ original.baseOrigin=reference.source /\ actual.baseOrigin=reference.source /\ actual.sourceCard=original.sourceCard /\ actual.sourceSHA=original.sourceSHA
       /\ actual.sourceCard \in DOMAIN cardFacts /\ actual.sourceSHA=cardFacts[actual.sourceCard].sourceSHA
       /\ actual.value \in Int
       /\ packet=[contextId |-> context.id,reference |-> reference,effectId |-> id,snapshotId |-> world.id,
             source |-> actual.baseOrigin,sourceCard |-> actual.sourceCard,sourceSHA |-> actual.sourceSHA,operation |-> actual.operation,actor |-> actual.actor,
             amount |-> IF ~kept \/ actual.value<=0 THEN 0 ELSE actual.value]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, actual, kept, original, SetupPlayers

LiabilityMarkerQuantity106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerQuantity106(objects) == Cardinality(LiabilityMarkerIds106(objects))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiabilityMarkerIds106

LiabilityMarkerSpendSources106 · operator

reference-profile · input revision 2 · CC0 1.0

LiabilityMarkerSpendSources106(payment) ==
 CounterPermissionUseSources9(payment,[id \in {1} |-> [source |-> RuleAbilitySource9("ProcedureCode51c5eb4c9e6c"),paymentId |-> payment.id,allowsPayment |-> TRUE,paidCounters |-> payment.fundCounters]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CounterPermissionUseSources9, RuleAbilitySource9

LinkBaseRead107 · operator

reference-profile · input revision 2 · CC0 1.0

LinkBaseRead107(world,cardFacts,read) ==
 /\ world.sideBProfile \in DOMAIN world.objects /\ world.sideBProfile \in DOMAIN world.properties
 /\ LET object==world.objects[world.sideBProfile]
        definition==LinkDefinition107(world,object)
        properties==SideBCharacteristics8(object,world.properties[world.sideBProfile])
    IN /\ object.form="Card" /\ object.kind="Profile" /\ object.zone="Play" /\ object.side="SideB"
       /\ definition \in DOMAIN world.profileLinkFacts /\ definition \in DOMAIN cardFacts
       /\ cardFacts[definition].kind="Profile" /\ cardFacts[definition].side="SideB"
       /\ world.profileLinkFacts[definition].sourceSHA=cardFacts[definition].sourceSHA
       /\ "baseLink" \in DOMAIN properties /\ properties.baseLink \in Int
       /\ read=[tag |-> "CurrentBaseLink",snapshotId |-> world.id,object |-> world.sideBProfile,physical |-> object.card,definition |-> definition,
             sourceSHA |-> cardFacts[definition].sourceSHA,printedBase |-> world.profileLinkFacts[definition].baseLink,value |-> properties.baseLink]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: definition, object, properties

LinkDefinition107 · operator

reference-profile · input revision 2 · CC0 1.0

LinkDefinition107(world,object) == world.definitions[object.card]

Exact module download · Source bundle and reproduction instructions

LinkInstructionSnapshot107 · operator

reference-profile · input revision 2 · CC0 1.0

LinkInstructionSnapshot107(world,cardFacts,base,declarations,read,snapshot) ==
 /\ ReadSideBLink107(world,cardFacts,base,declarations,read)
 /\ snapshot=[tag |-> "CurrentLinkInstructionSnapshot",id |-> world.id,link |-> [player \in {"SideB"} |-> read.value]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReadSideBLink107

LinkedLoadIds109 · operator

reference-profile · input revision 2 · CC0 1.0

LinkedLoadIds109(world,link) ==
 {id \in DOMAIN world.loadHistory : LET h==world.loadHistory[id] IN
   h.tag="CompletedLoad" /\ h.host=link.host /\ h.kind=link.kind /\ h.loadDefinition=link.loadDefinition /\ h.amount>0 /\
   h.reference.source=ObjectAbilitySource9(link.host) /\ h.sourceCard=link.card /\ h.sourceSHA=link.sourceSHA}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, h

LiveMarkIds1011 · operator

reference-profile · input revision 2 · CC0 1.0

LiveMarkIds1011(registry,world) == MarkEffectIds1011(registry) \cap ActiveLingeringIds910(registry,world)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActiveLingeringIds910, MarkEffectIds1011

LoadState109 · operator

reference-profile · input revision 2 · CC0 1.0

LoadState109(world) == [objects |-> world.objects,definitions |-> world.definitions,history |-> world.loadHistory,links |-> world.loadLinks]

Exact module download · Source bundle and reproduction instructions

LoadedCounterToken109 · operator

reference-profile · input revision 2 · CC0 1.0

LoadedCounterToken109(kind,zone,host,actor) ==
 [card |-> "none",form |-> "Counter",kind |-> kind,zone |-> zone,loc |-> host,deployed |-> FALSE,face |-> "Up",front |-> TRUE,
  activated |-> FALSE,host |-> host,placedBy |-> actor,virtual |-> FALSE,objectivePoints |-> 0,marks |-> {}]

Exact module download · Source bundle and reproduction instructions

LoopTrait101 · operator

reference-profile · input revision 2 · CC0 1.0

LoopTrait101(kind,duringTraversal,withdrawTraversalProhibited) ==
 CASE kind="Mandatory" -> "ChooseCount"
   [] kind="Optional" /\ duringTraversal /\ ~withdrawTraversalProhibited -> "SideBWithdrawTraversal"
   [] kind="Optional" /\ duringTraversal /\ withdrawTraversalProhibited -> "SideAContinueTraversal"
   [] OTHER -> "NoRuleIn10.1.6"

Exact module download · Source bundle and reproduction instructions

MarkBalancedSampler1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkBalancedSampler1011(sampler) ==
 /\ sampler.tag="UniformFiniteAtoms" /\ sampler.space#{} /\ IsFiniteSet(sampler.space) /\ DOMAIN sampler.mapping=sampler.space
 /\ {sampler.mapping[atom] : atom \in sampler.space} \subseteq CentralTargetSites4
 /\ sampler.weights=[atom \in sampler.space |-> 1] /\ sampler.totalWeight=Cardinality(sampler.space)
 /\ \A targetSite \in CentralTargetSites4 : 3*Cardinality({atom \in sampler.space : sampler.mapping[atom]=targetSite})=Cardinality(sampler.space)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CentralTargetSites4

MarkBlueprint1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkBlueprint1011(source,originKind,targetSite,cutoff,turn) ==
 [kind |-> "Ordinary",source |-> source,originKind |-> originKind,target |-> 0,value |-> [targetSite |-> targetSite,cutoff |-> cutoff,turn |-> turn],
  baseDuration |-> [kind |-> "Timing",ref |-> TimingRef9("Turn",turn)],durationMode |-> "Specified",durationClass |-> "Turn",choiceKey |-> "GlobalMark",
  lingeringConsumers |-> {},otherConsumers |-> {},definitionId |-> 101101,whenYourTurnBegins |-> FALSE,onlyChoice |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9

MarkConditionalStipulation1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkConditionalStipulation1011(world,a,d,event,rule,receipt) ==
 /\ MarkWorldBound1011(world,world.lingering,a) /\ ConditionalDefinitionValid96(d) /\ d.primaryKind="Trigger" /\ d.triggerRequirements={1}
 /\ ConditionalKey96(d) \in DOMAIN world.markRules /\ rule=world.markRules[ConditionalKey96(d)] /\ rule.definition=d
 /\ rule.card \in DOMAIN world.cardFacts /\ rule.sourceSHA=world.cardFacts[rule.card].sourceSHA /\ rule.role=MarkRole1011(rule.card) /\ rule.role#"Unsupported"
 /\ d.syntax.source.kind="Object" /\ rule.physical \in DOMAIN world.sourceDefinitions /\ world.sourceDefinitions[rule.physical]=rule.card
 /\ IF d.syntax.source.object \in DOMAIN world.objects THEN world.objects[d.syntax.source.object].card=rule.physical ELSE TRUE
 /\ event.id \in DOMAIN world.history /\ event=world.history[event.id].occurrence
 /\ LET row==world.history[event.id]
        mark==row.mark
        kind==CASE rule.role="FirstSuccess" -> "TraversalSuccessful" [] rule.role="FirstTraversalEnd" -> "TraversalEnded" [] OTHER -> "EncounterBarrier"
        matches==HistoricalMark1011(world,mark) /\ event.kind=kind /\ event.actor="SideB" /\
          IF rule.role="EncounterDuringMarkTraversal" THEN event.id \in MarkRelatedEvents1011(world,mark,"EncounterBarrier")
          ELSE FirstMarkEvent1011(world,mark,kind,event.id)
    IN receipt=[tag |-> "ConditionalTriggerStipulations",ability |-> d.syntax.id,source |-> d.syntax.source,occurrence |-> event.id,snapshotId |-> event.snapshot.id,
         results |-> [id \in {1} |-> matches]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionValid96, ConditionalKey96, matches, MarkRole1011, MarkWorldBound1011

MarkDraw1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkDraw1011(world,context,operation,draw,sampler,targetSite) ==
 /\ draw.id \in Nat \ {0} /\ draw.id \in DOMAIN world.pendingRandomDraws /\ draw=world.pendingRandomDraws[draw.id] /\ draw.id \notin DOMAIN world.draws
 /\ draw.tag="UniformMarkDraw" /\ draw.phase="InstructionResolution" /\ draw.snapshotId=world.id /\ draw.reference=context.currentRef /\ draw.operation=operation
 /\ MarkBalancedSampler1011(sampler) /\ draw.sampler=sampler /\ draw.atom \in sampler.space /\ targetSite=sampler.mapping[draw.atom] /\ draw.targetSite=targetSite

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MarkBalancedSampler1011

MarkEffectIds1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkEffectIds1011(registry) == {id \in DOMAIN registry.effects : registry.effects[id].definitionId=101101 /\ registry.effects[id].choiceKey="GlobalMark"}

Exact module download · Source bundle and reproduction instructions

MarkHistoryRead1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkHistoryRead1011(world,a,player,kind,mark,receipt) ==
 /\ MarkRead1011(world,a,player,mark)
 /\ receipt=[tag |-> "CurrentMarkHistory",worldId |-> world.id,effectId |-> mark.effectId,kind |-> kind,events |-> MarkRelatedEvents1011(world,mark,kind),
      first |-> {id \in MarkRelatedEvents1011(world,mark,kind) : FirstMarkEvent1011(world,mark,kind,id)}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FirstMarkEvent1011, MarkRead1011, MarkRelatedEvents1011

MarkInstruction1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkInstruction1011(context,origin,world,operation,cardFacts) ==
 /\ cardFacts=world.cardFacts /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ origin.kind="Instruction" /\ origin.plan.phase="Resolving"
 /\ context.currentRef=InstructionWindowRef93(origin.plan) /\ ConditionalCreationInstruction96(origin.plan,origin.parent,origin.ruleStep)
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \in DOMAIN context.actualEffects /\ operation \in DOMAIN context.templates
 /\ LET e==context.actualEffects[operation] IN
    /\ e.kind="CreateLingering" /\ e.semantic="IdentifyMark" /\ e.actor \in SetupPlayers
    /\ e.sourceCard=context.templates[operation].sourceCard /\ e.sourceSHA=context.templates[operation].sourceSHA
    /\ e.sourceCard \in DOMAIN cardFacts /\ e.sourceSHA=cardFacts[e.sourceCard].sourceSHA /\ e.baseOrigin=context.currentRef.source
    /\ context.currentRef.source.kind="Object"
    /\ IF context.currentRef.source.object \in DOMAIN world.objects THEN world.sourceDefinitions[world.objects[context.currentRef.source.object].card]=e.sourceCard ELSE TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, ConditionalCreationInstruction96, InstructionWindowRef93, e, SetupPlayers

MarkJournalValid1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkJournalValid1011(world) ==
 /\ world.eventSerial \in Nat
 /\ \A id \in DOMAIN world.history : world.history[id].id=id /\ world.history[id].serial \in 1..world.eventSerial
 /\ \A a,b \in DOMAIN world.history : a#b => world.history[a].serial#world.history[b].serial

Exact module download · Source bundle and reproduction instructions

MarkProtectionRelation1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkProtectionRelation1011(world,a,mark,barrierCard,protection,receipt) ==
 /\ MarkRead1011(world,a,"SideB",mark) /\ protection=world.barrierProtection
 /\ receipt=[tag |-> "BarrierProtectingMark",worldId |-> world.id,barrierCard |-> barrierCard,holds |-> mark.present /\ barrierCard \in DOMAIN world.objects /\ world.objects[barrierCard].form="Card" /\ world.objects[barrierCard].kind="Barrier" /\ barrierCard \in DOMAIN protection /\ protection[barrierCard]=mark.targetSite]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MarkRead1011

MarkRead1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkRead1011(world,a,player,read) ==
 /\ player \in SetupPlayers /\ MarkWorldBound1011(world,world.lingering,a)
 /\ ReadActiveLingering910(world.lingering,a,[tag |-> "CurrentActiveLingeringEffects",worldId |-> a.current.id,ids |-> ActiveLingeringIds910(world.lingering,a.current)])
 /\ LET ids==LiveMarkIds1011(world.lingering,a.current) IN
    read=IF ids={} THEN [tag |-> "CurrentGlobalMark",worldId |-> world.id,present |-> FALSE,effectId |-> 0,targetSite |-> "NoValue",cutoff |-> 0,turn |-> world.turn.id]
         ELSE LET id==CHOOSE id \in ids : TRUE
                  value==world.lingering.effects[id].value
              IN [tag |-> "CurrentGlobalMark",worldId |-> world.id,present |-> TRUE,effectId |-> id,targetSite |-> value.targetSite,cutoff |-> value.cutoff,turn |-> value.turn]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActiveLingeringIds910, ReadActiveLingering910, id, ids, value, MarkWorldBound1011, SetupPlayers

MarkRegistryValid1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkRegistryValid1011(registry,world) ==
 /\ Cardinality(LiveMarkIds1011(registry,world))<=1
 /\ \A id \in MarkEffectIds1011(registry) :
      LET e==registry.effects[id] IN
      /\ e.kind="Ordinary" /\ e.choicePolicy="NoValue" /\ e.value.targetSite \in CentralTargetSites4 /\ e.value.cutoff \in Nat \ {0}
      /\ e.value.turn=e.creationTurn /\ e.baseDuration=[kind |-> "Timing",ref |-> TimingRef9("Turn",e.creationTurn)] /\ e.durationClass="Turn"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, e, LiveMarkIds1011, MarkEffectIds1011, CentralTargetSites4

MarkRelatedEvents1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkRelatedEvents1011(world,mark,kind) ==
 IF ~mark.present THEN {} ELSE
 {id \in DOMAIN world.history : LET e==world.history[id] IN e.kind=kind /\ e.targetSite=mark.targetSite /\ e.turn=mark.turn /\ e.serial>mark.cutoff}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: e

MarkRole1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkRole1011(card) ==
 CASE card \in {"Specimen0165","Specimen0259"} -> "FirstSuccess"
   [] card="Specimen0119" -> "FirstTraversalEnd"
   [] card="Specimen0026" -> "EncounterDuringMarkTraversal"
   [] OTHER -> "Unsupported"

Exact module download · Source bundle and reproduction instructions

MarkSpecimen0119Body1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkSpecimen0119Body1011(world,event,receipt) ==
 /\ event.kind="TraversalEnded" /\ event.id \in DOMAIN world.history /\ event=world.history[event.id].occurrence
 /\ LET row==world.history[event.id]
        mark==row.mark
        siteInspections=={id \in MarkRelatedEvents1011(world,mark,"Inspection") : world.history[id].traversalId=row.traversalId /\ world.history[id].serial<=row.serial}
    IN receipt=[tag |-> "Specimen0119InstructionCondition",occurrence |-> event.id,traversalId |-> row.traversalId,holds |-> HistoricalMark1011(world,mark) /\ siteInspections#{}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mark, row, siteInspections, HistoricalMark1011

MarkSpecimen0259Branch1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkSpecimen0259Branch1011(world,event,branch) ==
 /\ event.kind="TraversalSuccessful" /\ event.id \in DOMAIN world.history /\ event=world.history[event.id].occurrence /\ HistoricalMark1011(world,world.history[event.id].mark)
 /\ branch=[tag |-> "Specimen0259InstructionBranch",occurrence |-> event.id,branch |-> IF world.history[event.id].mark.targetSite="SchemaAtom082" THEN "AdditionalCentralAItemInspection" ELSE "InspectionCentralAAfterTraversal"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HistoricalMark1011

MarkTraversalRelation1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkTraversalRelation1011(world,a,mark,receipt) ==
 /\ MarkRead1011(world,a,"SideB",mark)
 /\ receipt=[tag |-> "OngoingTraversalOnMark",worldId |-> world.id,traversalId |-> world.control.traversal.id,holds |-> mark.present /\ DuringTraversal6(world.control.traversal) /\ TimingRef9("SchemaAtom138",world.control.traversal.id) \in world.inside /\ world.control.traversal.attacked=mark.targetSite]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, MarkRead1011, DuringTraversal6

MarkWorldBound1011 · operator

reference-profile · input revision 2 · CC0 1.0

MarkWorldBound1011(world,registry,a) ==
 /\ LifetimeWorldProjection910(world)=a.current /\ world.lingering=registry /\ LifetimeReady910(registry,a)
 /\ MarkRegistryValid1011(registry,a.current) /\ MarkJournalValid1011(world)
 /\ \A id \in LiveMarkIds1011(registry,a.current) :
      LET e==registry.effects[id] IN
      \E event \in DOMAIN world.history :
        /\ world.history[event].kind="MarkDesignated" /\ world.history[event].effectId=id /\ world.history[event].targetSite=e.value.targetSite
        /\ world.history[event].serial=e.value.cutoff /\ world.history[event].turn=e.value.turn
        /\ world.history[event].reference=e.creation[2] /\ world.history[event].source=e.source

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LifetimeReady910, LifetimeWorldProjection910, e, LiveMarkIds1011, MarkJournalValid1011, MarkRegistryValid1011

MergeCheckpointDepartures103 · operator

reference-profile · input revision 2 · CC0 1.0

MergeCheckpointDepartures103(before,added) ==
 [id \in DOMAIN before \cup DOMAIN added |-> IF id \in DOMAIN added THEN added[id] ELSE before[id]]

Exact module download · Source bundle and reproduction instructions

MovableExposureMarkerIds105 · operator

reference-profile · input revision 2 · CC0 1.0

MovableExposureMarkerIds105(objects) == {id \in ExposureMarkerIds105(objects) : ~objects[id].virtual}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExposureMarkerIds105

MovableHostedTokens109 · operator

reference-profile · input revision 2 · CC0 1.0

MovableHostedTokens109(objects,host,kind) ==
 {id \in HostedCounterIds109(objects,host,kind) : BankPhysicalToken4(objects[id])}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostedCounterIds109, BankPhysicalToken4

MovableLiabilityMarkerIds106 · operator

reference-profile · input revision 2 · CC0 1.0

MovableLiabilityMarkerIds106(objects) == {id \in LiabilityMarkerIds106(objects) : ~objects[id].virtual}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiabilityMarkerIds106

MoveDividendObjective1013 · operator

reference-profile · input revision 2 · CC0 1.0

MoveDividendObjective1013(world,next,begin,capture,new,moved,binding,eventId,event) ==
 /\ world.outcome="Playing" /\ CaptureDividendBegin1013(world,begin,world.cardFacts,capture)
 /\ begin.id \in DOMAIN world.dividendCaptures /\ capture=world.dividendCaptures[begin.id] /\ capture.beforeObjects=world.objects
 /\ DividendCleanupSupport1013(world,capture)="SupportedNativeProgressCleanup"
 /\ moved=DividendObjectiveCompletionMap1013(world.objects,capture.oldObject,new)
 /\ CardBatchTransfer8(world.objects,moved,{capture.oldObject},[old \in {capture.oldObject} |-> new],world.usedObjects,"SideAObjectiveCompletion","Up",[old \in {capture.oldObject} |-> 0])
 /\ NormalObjectiveCompletionClaimObjectivePost4(moved[new],"SideA","Scored",TRUE)
 /\ LiabilityMarkerCounterDeparture106(moved,next.objects,capture.physicalProgress,[id \in {} |-> id],world.usedObjects \cup {new},world.printed,world.owners,world.visible,eventId,world.movementHistory,next.movementHistory,{})
 /\ eventId \in (Nat \ {0}) \ world.objectiveCompletionEventIds /\ next.id \in (Nat \ {0}) \ world.usedWorlds
 /\ binding=[tag |-> "DividendObjectiveCompletionBinding",objectiveCompletionId |-> begin.id,oldObject |-> capture.oldObject,newObject |-> new,physical |-> capture.physical,beforeSnapshot |-> world.id,afterSnapshot |-> next.id]
 /\ event=[id |-> eventId,kind |-> "ObjectivePlacementd",actor |-> "SideA",object |-> new,objectiveCompletionId |-> begin.id,binding |-> binding]
 /\ next=[world EXCEPT !.id=next.id,!.objects=next.objects,!.movementHistory=next.movementHistory,!.usedObjects=@ \cup {new},!.usedWorlds=@ \cup {next.id},
       !.requirements=ReplacementOverlay99(Without101(@,{capture.oldObject}),[id \in {new} |-> DividendFacts1013!DividendPrintedFacts1013[capture.sourceCard].requirement]),
       !.consideredProgress=ReplacementOverlay99(Without101(@,{capture.oldObject}),[id \in {new} |-> 0]),!.historicalPhysical=ReplacementOverlay99(@,[id \in {capture.oldObject} |-> capture.physical]),
       !.dividendBindings=ReplacementOverlay99(@,[id \in {begin.id} |-> binding]),!.objectiveCompletionEventIds=@ \cup {eventId},!.objectiveCompletionEvents=ReplacementOverlay99(@,[id \in {eventId} |-> event])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, CaptureDividendBegin1013, DividendCleanupSupport1013, DividendFacts1013!DividendPrintedFacts1013, DividendObjectiveCompletionMap1013, LiabilityMarkerCounterDeparture106, Without101, NormalObjectiveCompletionClaimObjectivePost4, CardBatchTransfer8

NamedReference101 · operator

reference-profile · input revision 2 · CC0 1.0

NamedReference101(source,printedOwnName,referenceName,copyQualifier,objects,currentNames) ==
 IF referenceName=printedOwnName /\ ~copyQualifier THEN {source}
 ELSE {i \in DOMAIN objects \cap DOMAIN currentNames : currentNames[i]=referenceName}

Exact module download · Source bundle and reproduction instructions

NewCheckpoint103 · operator

reference-profile · input revision 2 · CC0 1.0

NewCheckpoint103(id,caller,beginSnapshotId,insideStructures) ==
 [id |-> id,caller |-> caller,beginSnapshotId |-> beginSnapshotId,snapshotId |-> beginSnapshotId,
  inside |-> insideStructures,point |-> "ProcedureCodee605a78f5d5e",owed |-> CheckpointStages103,done |-> {},discharged |-> {},
  recognition |-> [id |-> 0,caller |-> "NoValue"],recognized |-> [emptyId \in {} |-> emptyId],phase |-> "Steps",returned |-> FALSE,
  windowId |-> 0,outcome |-> "Playing",overrideLog |-> <<>>,hostPasses |-> 0,retiredRemotes |-> {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointStages103

NewSabotageOccurrence1012 · operator

reference-profile · input revision 2 · CC0 1.0

NewSabotageOccurrence1012(id,batch,unit,snapshot,beforeSnapshot) ==
 [id |-> id,kind |-> IF unit=0 THEN "CardsRetireed" ELSE "CardRetireed",object |-> unit,actor |-> batch.actor,side |-> "SideA",snapshot |-> snapshot,effectId |-> batch.id,
  movement |-> [tag |-> IF unit=0 THEN "BatchRetire" ELSE "Retire",oldObject |-> unit,newObject |-> IF unit=0 THEN 0 ELSE batch.successors[unit],beforeSnapshot |-> beforeSnapshot],
  scopeKind |-> "Global",scopeDefinition |-> [ability |-> 0,source |-> RuleAbilitySource9("NoValue")],structure |-> NoTimingRef9,step |-> "NoValue",traversal |-> NoTraversal6,siteInspection |-> [traversalId |-> 0,origin |-> "NoValue"],
  batchId |-> batch.id,batch |-> batch,unit |-> unit]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoTimingRef9, RuleAbilitySource9, NoTraversal6

NextChargeAfterCheckpoint1010 · operator

reference-profile · input revision 2 · CC0 1.0

NextChargeAfterCheckpoint1010(beforeAbility,afterAbility,beforePlan,afterPlan,world,cp,ledger,stack,cohort,entry) ==
 /\ cohort.ability=beforeAbility /\ cohort.id=beforeAbility.id /\ cohort.source=beforeAbility.source
 /\ cp.id \in DOMAIN world.instructionCheckpoints /\ world.instructionCheckpoints[cp.id]=cp /\ ledger=world.conditionalLedger
 /\ cp.caller=PlayInstructionCaller97(cohort) /\ CheckpointDrained103(cp,ledger,stack)
 /\ entry.checkpointAndAllNewerChainsComplete
 /\ EnterNextAbilityInstruction93(beforeAbility,afterAbility,beforePlan,afterPlan,entry)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EnterNextAbilityInstruction93, PlayInstructionCaller97, CheckpointDrained103

NormalizeDamageType104 · operator

reference-profile · input revision 2 · CC0 1.0

NormalizeDamageType104(kind) == IF kind="CapacityHarmAlias" THEN "PersistentCapacityHarm" ELSE kind

Exact module download · Source bundle and reproduction instructions

ObserveCheckpointKernel103 · operator

reference-profile · input revision 2 · CC0 1.0

ObserveCheckpointKernel103(frame,beforeRegistry,afterRegistry,beforeLedger,afterLedger,beforeStack,afterStack,
                           beforeSnapshot,afterSnapshot,baseWorld,execution,beforeAuthority,afterAuthority) ==
 /\ CheckpointPrivatePersistentBound103(frame,beforeRegistry,beforeLedger)
 /\ frame.snapshotId=beforeAuthority.current.id
 /\ LifetimeReady910(beforeRegistry,beforeAuthority) /\ PersistentRegistryWorldBound912(beforeRegistry,beforeAuthority.current)
 /\ PersistentConditionalDefinitions912(beforeRegistry,beforeSnapshot.definitions)
 /\ afterAuthority.current=PersistentWorld912(baseWorld,beforeRegistry)
 /\ CommitLifetimeKernelCore910(beforeAuthority,afterAuthority,afterAuthority.current,execution)
 /\ LET local==[afterRegistry EXCEPT !.frontier=beforeRegistry.frontier]
    IN /\ ObserveLingering910(beforeRegistry,local,afterAuthority.current)
       /\ afterRegistry.frontier=LifetimeFrontier910(afterAuthority,Len(afterAuthority.order))
       /\ PersistentRegistryWorldBound912(afterRegistry,afterAuthority.current)
       /\ beforeSnapshot.id=beforeAuthority.current.id /\ afterSnapshot.id=afterAuthority.current.id
       /\ LingeringConditionalWorld910(beforeSnapshot,beforeLedger,beforeAuthority.current)
       /\ LingeringConditionalWorld910(afterSnapshot,beforeLedger,afterAuthority.current)
       /\ afterSnapshot=LingeringConditionalSnapshot910(afterSnapshot,local,beforeLedger,afterAuthority.current)
       /\ PersistentConditionalDefinitions912(local,afterSnapshot.definitions)
       /\ ObserveConditionalActivity96(beforeLedger,beforeLedger,afterLedger,beforeStack,afterStack,beforeSnapshot,afterSnapshot)
       /\ CheckpointCaptured103(frame,afterLedger)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CommitLifetimeKernelCore910, LifetimeFrontier910, LifetimeReady910, LingeringConditionalSnapshot910, LingeringConditionalWorld910, ObserveConditionalActivity96, ObserveLingering910, PersistentConditionalDefinitions912, PersistentRegistryWorldBound912, PersistentWorld912, local, CheckpointCaptured103, CheckpointPrivatePersistentBound103

ObserveCurrentInformation102 · operator

reference-profile · input revision 2 · CC0 1.0

ObserveCurrentInformation102(before,after,facts,fact,player,currentSnapshot) ==
 /\ player \in SetupPlayers /\ fact \in DOMAIN facts /\ facts[fact].snapshot=currentSnapshot
 /\ player \in facts[fact].viewers
 /\ after=Append(before,[tag |-> "AuthoritativeObservation",player |-> player,fact |-> fact,
       value |-> facts[fact].value,snapshot |-> currentSnapshot])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

OpenCheckpointAtSite103 · operator

reference-profile · input revision 2 · CC0 1.0

OpenCheckpointAtSite103(frame,id,site,event,insideStructures,usedCheckpoints) ==
 /\ CheckpointSite103(site,event,insideStructures) /\ id \in (Nat \ {0}) \ usedCheckpoints
 /\ frame=NewCheckpoint103(id,site.caller,site.snapshotId,site.inside)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointSite103, NewCheckpoint103

OpenCheckpointReaction103 · operator

reference-profile · input revision 2 · CC0 1.0

OpenCheckpointReaction103(before,after,ledger,beforeStack,afterStack,site,opening,usedWindows) ==
 /\ DOMAIN before.recognized#{} /\ CheckpointCaptured103(before,ledger)
 /\ CheckpointCompletion103(before,ledger,[id |-> before.snapshotId],opening.completion)
 /\ opening.checkpointId=before.id /\ opening.caller=before.caller
 /\ opening.windowId=CheckpointRecognizedWindow103(before)
 /\ \A id \in DOMAIN before.recognized : before.recognized[id].windowId=opening.windowId
 /\ LET canonicalOpening==[opening EXCEPT !.completion=opening.completion]
        raw==Append(beforeStack,NewPriorityWindow9(opening.windowId,"Reaction",PriorityOpeningSite9(beforeStack,site),
                   before.recognized,opening.group,opening.beginning,opening.instruction,opening.effectRevision))
        pending=={id \in DOMAIN before.recognized : ledger.instances[id].status="Pending"}
    IN /\ OpenPriorityWindow9(beforeStack,raw,opening.windowId,"Reaction",site,before.recognized,canonicalOpening,usedWindows)
       /\ afterStack=ReplaceWindowTop9(raw,[WindowTop9(raw) EXCEPT !.pending=pending,!.lostPending=DOMAIN before.recognized \ pending])
       /\ after=[before EXCEPT !.phase="Reaction",!.windowId=opening.windowId]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenPriorityWindow9, ReplaceWindowTop9, WindowTop9, canonicalOpening, pending, raw, CheckpointCaptured103, CheckpointCompletion103, CheckpointRecognizedWindow103

OpenDividendPlan1013 · operator

reference-profile · input revision 2 · CC0 1.0

OpenDividendPlan1013(world,instance,event,basis,plan) ==
 /\ world.outcome="Playing" /\ instance.status="Resolving" /\ DividendBasis1013(world,instance,event,basis)
 /\ instance.member.id \notin DOMAIN world.dividendBodyAnchors
 /\ plan=[tag |-> "DividendInstructionPlan",instance |-> instance.member.id,reference |-> InstructionWindowRef93(OpenInstruction93(instance.definitionCopy.instructions[1],"Ability",instance.member.id,instance.definition.source,"SideAObjectiveCompletion",1,"NoValue",<<"RepeatedObjectivePlacement">>,FALSE)),
       basis |-> basis,cursor |-> 1,applied |-> {},skipped |-> {},totalPlaced |-> 0,complete |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, OpenInstruction93, DividendBasis1013

OpenSabotage1012 · operator

reference-profile · input revision 2 · CC0 1.0

OpenSabotage1012(id,context,operation,world,packet,frame) ==
 /\ SabotagePacket1012(context,world,operation,packet) /\ SabotageSupport1012(packet)="SupportedResolutionComponent" /\ SabotageZones1012(world)
 /\ id \in (Nat \ {0}) \ world.usedProcedures /\ packet.key \notin world.completedSabotage
 /\ frame=OpenSabotageFrame1012(id,context,operation,world,packet)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenSabotageFrame1012, SabotagePacket1012, SabotageSupport1012, SabotageZones1012

OpenSabotageFrame1012 · operator

reference-profile · input revision 2 · CC0 1.0

OpenSabotageFrame1012(id,context,operation,world,packet) ==
 [tag |-> "SabotageResolution",id |-> id,contextId |-> context.id,operation |-> operation,reference |-> context.currentRef,packet |-> packet,
  scope |-> SabotageScope1012(world),phase |-> "Choose",choiceSealed |-> FALSE,aHandChosen |-> {},aDrawPileCount |-> 0,successors |-> [x \in {} |-> x],complete |-> FALSE,afterWorld |-> 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SabotageScope1012

PayEscalatingResourceContestBoost108 · operator

reference-profile · input revision 2 · CC0 1.0

PayEscalatingResourceContestBoost108(before,after,world,afterObjects,player,amount,selected,transaction,payment,announcement,cardFacts,permissions,usedPayments,
                  successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,movementEvents,spendEvents) ==
 /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="ChooseBoost" /\ before.nextPlayer=player /\ player \in SetupPlayers /\ player \notin before.acted
 /\ usedPayments=world.usedPayments /\ usedIds=world.usedObjects
 /\ amount \in Nat /\ transaction \in (Nat \ {0}) \ usedPayments
 /\ world.resourceUnitCost=[tag |-> "EscalatingResourceContestBoostCostContext",id |-> transaction,escalatingResourceContestId |-> before.id,player |-> player,amount |-> amount,
       snapshotId |-> world.id,source |-> EscalatingResourceContestBoostRule108(player),parent |-> before.caller,status |-> "Paying"]
 /\ permissions=world.escalatingResourceContestSpendPermissions[player]
 /\ \A id \in DOMAIN permissions : EscalatingResourceContestRecurringPermission108(before,world,player,transaction,permissions[id],cardFacts)
 /\ LET fund==IF player="SideB" /\ EscalatingResourceContestDuringTraversal108(world) THEN LiabilityMarkerFundIds106(world.objects) ELSE {}
        hosted==UNION {permissions[id].counters : id \in DOMAIN permissions}
    IN /\ selected \subseteq {id \in (EscalatingResourceContestPoolIds108(world.objects,player) \cup fund \cup hosted) : LiabilityMarkerFundController106(world.objects[id],world.controllers[id])=player} /\ Cardinality(selected)=amount
       /\ selected \subseteq CheckpointPhysicalIds103(world.objects)
 /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,movementEvents)
 /\ payment=[tag |-> "CompletedEscalatingResourceContestBoostCost",id |-> transaction,escalatingResourceContestId |-> before.id,player |-> player,amount |-> amount,
       snapshotId |-> world.id,source |-> EscalatingResourceContestBoostRule108(player),parent |-> before.caller,paidCounterIds |-> selected,complete |-> TRUE]
 /\ announcement=[tag |-> "EscalatingResourceContestBoostChoice",escalatingResourceContestId |-> before.id,player |-> player,mode |-> "Pay",amount |-> amount,viewers |-> SetupPlayers]
 /\ spendEvents=IF amount=0 THEN {} ELSE {[kind |-> "EscalatingResourceContestResourceUnitsSpent",escalatingResourceContestId |-> before.id,player |-> player,amount |-> amount,
       transactionId |-> transaction,escalatingResourceContestSource |-> before.packet.source,beforeSnapshotId |-> world.id]}
 /\ after=[before EXCEPT !.phase="BoostCheckpoint",!.pendingPlayer=player,!.acted=@ \cup {player},!.boosts[player]=[mode |-> "Pay",amount |-> amount,transaction |-> transaction]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: fund, hosted, CheckpointPhysicalIds103, EscalatingResourceContestBoostRule108, EscalatingResourceContestCurrent108, EscalatingResourceContestPoolIds108, EscalatingResourceContestRecurringPermission108, LiabilityMarkerCounterDeparture106, LiabilityMarkerFundController106, SetupPlayers

PayExposureMarkerAction105 · operator

reference-profile · input revision 2 · CC0 1.0

PayExposureMarkerAction105(before,after,stack,world,afterWorld,declarations,afterDeclarations,cardFacts,mods,permissions,selected,payment) ==
 /\ before.phase="Reserved" /\ world.outcome="Playing" /\ Len(stack)>0 /\ OwnActionPhase5(world.turn,before.player)
 /\ WindowTop9(stack).id=before.windowId /\ WindowTop9(stack).busy=before.option /\ WindowTop9(stack).busyTransaction=before.transaction /\ WindowTop9(stack).stage="Resolving"
 /\ CurrentExposureMarkerState105(world,declarations,cardFacts,ExposureMarkerStateView105(world.objects,declarations)) /\ ExposureMarkerActionStatusGate105(before.kind,ExposureMarkerStateView105(world.objects,declarations).hasExposureMarkers)
 /\ ExposureMarkerCostModifiers105(world,before.kind,mods,cardFacts) /\ permissions=world.exposureMarkerSpendPermissions
 /\ \A p \in DOMAIN permissions : ExampleFamily011ExposureMarkerPermission105(world,before.kind,before.transaction,permissions[p],cardFacts)
 /\ selected \subseteq ExposureMarkerResourceUnitEligible105(world,before.player,permissions) /\ Cardinality(selected)=ExposureMarkerResourceUnitCost105(mods)
 /\ world.actionPoints[before.player]>=1 /\ afterWorld.id \in Nat \ {0} /\ afterWorld.id#world.id
 /\ BankSpendReturn4(world.objects,afterWorld.objects,selected,TRUE)
 /\ afterWorld=[world EXCEPT !.id=afterWorld.id,!.objects=afterWorld.objects,!.controllers=Without101(@,selected),
          !.actionPoints[before.player]=@-1,!.spent[before.player]=@+1]
 /\ CurrentExposureMarkerState105(afterWorld,afterDeclarations,cardFacts,ExposureMarkerStateView105(afterWorld.objects,afterDeclarations)) /\ ExposureMarkerActionStatusGate105(before.kind,ExposureMarkerStateView105(afterWorld.objects,afterDeclarations).hasExposureMarkers)
 /\ payment=[tag |-> "BasicExposureMarkerTriggerPayment",id |-> before.transaction,actionId |-> before.id,player |-> before.player,
       beforeSnapshot |-> world.id,afterSnapshot |-> afterWorld.id,actionPoints |-> 1,resourceUnits |-> ExposureMarkerResourceUnitCost105(mods),paidCounterIds |-> selected,complete |-> TRUE]
 /\ LET action==NewAction5(before.id,before.player,ExposureMarkerActionKey105(before.kind)) IN
    /\ ActionStart5(world.turn,before.player,TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1],[kind |-> "SpendResourceUnits",amount |-> ExposureMarkerResourceUnitCost105(mods)]>>,
          TRUE,TRUE,TRUE,before.id,ExposureMarkerActionKey105(before.kind),action)
    /\ after=[before EXCEPT !.phase="BaseCostCheckpoint",!.activationSnapshot=world.id,!.action=action,!.payment=payment]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, action, CurrentExposureMarkerState105, ExampleFamily011ExposureMarkerPermission105, ExposureMarkerActionKey105, ExposureMarkerActionStatusGate105, ExposureMarkerCostModifiers105, ExposureMarkerResourceUnitCost105, ExposureMarkerResourceUnitEligible105, ExposureMarkerStateView105, Without101, BankSpendReturn4, ActionStart5, OwnActionPhase5

PayResourceAdditional105 · operator

reference-profile · input revision 2 · CC0 1.0

PayResourceAdditional105(before,after,world,afterWorld,cardFacts,assignments,successors,usedIds,transaction,eventIds,beforeHistory,afterHistory,events) ==
 /\ before.phase="AdditionalCosts" /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions /\ ResourceAdditionalCosts105(before,world,cardFacts)
 /\ transaction \in Nat \ {0} /\ transaction#before.transaction /\ DOMAIN assignments=DOMAIN before.effectCosts
 /\ \A cost \in DOMAIN assignments : assignments[cost] \subseteq before.effectCosts[cost].eligible /\ Cardinality(assignments[cost])=before.effectCosts[cost].amount
 /\ \A a,b \in DOMAIN assignments : a#b => assignments[a] \cap assignments[b]={}
 /\ DOMAIN eventIds=DOMAIN assignments /\ Cardinality({eventIds[cost] : cost \in DOMAIN eventIds})=Cardinality(DOMAIN eventIds)
 /\ \A cost \in DOMAIN eventIds : eventIds[cost] \in (Nat \ {0}) \ DOMAIN beforeHistory
 /\ LET selected==UNION {assignments[id] : id \in DOMAIN assignments}
        newEvents==[cost \in DOMAIN assignments |-> MovementEvent8(eventIds[cost],"Retire",assignments[cost])]
    IN /\ CardBatchTransfer8(world.objects,afterWorld.objects,selected,successors,usedIds,"SideADiscard","Down",[id \in selected |-> "discard"])
       /\ afterWorld.id \in Nat \ {0} /\ afterWorld.id#world.id
       /\ afterWorld=[world EXCEPT !.id=afterWorld.id,!.objects=afterWorld.objects,
            !.controllers=[id \in (DOMAIN @ \ selected) \cup {successors[old] : old \in selected} |->
                 IF id \in DOMAIN @ \ selected THEN @[id] ELSE "SideA"],!.currentRetireProhibitions=afterWorld.currentRetireProhibitions]
       /\ before.target \notin afterWorld.currentRetireProhibitions
       /\ afterHistory=[id \in DOMAIN beforeHistory \cup {eventIds[cost] : cost \in DOMAIN eventIds} |->
              IF id \in DOMAIN beforeHistory THEN beforeHistory[id] ELSE newEvents[CHOOSE cost \in DOMAIN eventIds : eventIds[cost]=id]]
       /\ \A cost \in DOMAIN assignments : RecordMovement8(beforeHistory,[id \in DOMAIN beforeHistory \cup {eventIds[cost]} |->
               IF id=eventIds[cost] THEN newEvents[cost] ELSE beforeHistory[id]],eventIds[cost],"Retire",assignments[cost],"Complete",TRUE,{newEvents[cost]})
       /\ events={newEvents[cost] : cost \in DOMAIN newEvents}
       /\ after=[before EXCEPT !.phase="AdditionalCostCheckpoint",!.nestedTransaction=transaction]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: newEvents, selected, ResourceAdditionalCosts105, ResourceTargetIds105, CardBatchTransfer8, RecordMovement8

PersistentCapacityLossQuantity104 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentCapacityLossQuantity104(objects) == Cardinality({id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="PersistentCapacityLoss" /\ objects[id].zone="SideBPersistentCapacityLoss" /\ objects[id].host=0})

Exact module download · Source bundle and reproduction instructions

PlayerInformationView102 · operator

reference-profile · input revision 2 · CC0 1.0

PlayerInformationView102(facts,player,currentSnapshot) ==
 [id \in {i \in DOMAIN facts : player \in facts[i].viewers /\ facts[i].snapshot=currentSnapshot} |-> facts[id].value]

Exact module download · Source bundle and reproduction instructions

PrepareExposureMarkerEffect105 · operator

reference-profile · input revision 2 · CC0 1.0

PrepareExposureMarkerEffect105(before,after,world,context,reference,id,cardFacts) ==
 /\ before.phase="Targeted" /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id
 /\ reference.id=before.instruction /\ reference.abilityInstance=before.id /\ reference.source=RuleAbilitySource9(ExposureMarkerActionRule105(before.kind))
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates
 /\ context.templates[id].kind=IF before.kind="RetireResource" THEN "RetireCards" ELSE "RemoveExposureMarkers"
 /\ LET removed==id \notin DOMAIN context.actualEffects
        costs==IF before.kind="RetireResource" /\ ~removed /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions THEN world.additionalResourceCosts ELSE [key \in {} |-> key]
    IN /\ IF removed THEN TRUE ELSE context.actualEffects[id].kind=context.templates[id].kind /\ context.actualEffects[id].targetCard=before.target /\ context.actualEffects[id].actor=before.player /\ context.actualEffects[id].value=1
       /\ (before.kind="RetireResource" /\ ~removed /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions => ResourceKnownCostInventory105(world,before.target,costs,cardFacts))
       /\ after=[before EXCEPT !.effective=[mode |-> IF removed THEN "Removed" ELSE "Kept",reference |-> reference,effectId |-> id],
            !.effectCosts=costs,!.phase=IF DOMAIN costs={} THEN "EffectReady" ELSE "AdditionalCosts"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, RuleAbilitySource9, costs, removed, ExposureMarkerActionRule105, ResourceKnownCostInventory105, ResourceTargetIds105

PrintedLinkObjectIds107 · operator

reference-profile · input revision 2 · CC0 1.0

PrintedLinkObjectIds107(world) ==
 {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].card \in DOMAIN world.definitions /\
    LinkDefinition107(world,world.objects[id]) \in DOMAIN world.linkSymbolFacts}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LinkDefinition107

PublicChoiceFacts102 · operator

reference-profile · input revision 2 · CC0 1.0

PublicChoiceFacts102(actualOpenRememberedChoices,snapshot) ==
 [id \in DOMAIN actualOpenRememberedChoices |-> InformationFact102(actualOpenRememberedChoices[id],SetupPlayers,snapshot)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InformationFact102, SetupPlayers

PublishBidOccurrence1014 · operator

reference-profile · input revision 2 · CC0 1.0

PublishBidOccurrence1014(world,event,definition,card,priorEvents,occurrence,cardFacts) ==
 /\ cardFacts=world.cardFacts /\ BidPublished1014(event,world) /\ card \in DOMAIN cardFacts /\ BidObserverRule1014(card)#"UnsupportedObserver"
 /\ priorEvents=[id \in {id \in DOMAIN world.bidEvents : world.bidEvents[id].serial<event.serial} |-> world.bidEvents[id]]
 /\ definition.syntax.source.object \in DOMAIN world.objects /\ LinkDefinition107(world,world.objects[definition.syntax.source.object])=card
 /\ ConditionalDefinitionValid96(definition) /\ definition.primaryKind="Trigger" /\ definition.trigger.kinds={"BidsRevealedAndPaid"}
 /\ definition.triggerRequirements={} /\ BidObserverCondition1014(BidObserverRule1014(card),event,priorEvents,cardFacts)
 /\ occurrence.kind="BidsRevealedAndPaid" /\ occurrence.effectId=event.id /\ occurrence.snapshot=event.snapshot /\ occurrence.bidId=event.bidId
 /\ occurrence.amounts=event.amounts /\ occurrence.result=event.result /\ occurrence.scopeKind="Ability" /\ occurrence.scopeDefinition=ConditionalKey96(definition)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionValid96, ConditionalKey96, BidObserverCondition1014, BidObserverRule1014, BidPublished1014, LinkDefinition107

PublishDividendPlan1013 · operator

reference-profile · input revision 2 · CC0 1.0

PublishDividendPlan1013(before,next,instance,event,basis,plan) ==
 /\ OpenDividendPlan1013(before,instance,event,basis,plan)
 /\ next=[before EXCEPT !.dividendBodyAnchors=ReplacementOverlay99(@,[id \in {plan.instance} |-> [basis |-> basis,reference |-> plan.reference]])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, OpenDividendPlan1013

PublishSabotageOccurrences1012 · operator

reference-profile · input revision 2 · CC0 1.0

PublishSabotageOccurrences1012(world,batch,allocation,snapshot,beforeSnapshot,occurrences) ==
 /\ batch.id \in DOMAIN world.sabotageEvents /\ batch=world.sabotageEvents[batch.id] /\ batch.objects#{}
 /\ snapshot.id=world.id /\ snapshot.objects=world.objects /\ batch.afterSnapshot=world.id /\ beforeSnapshot.id=batch.beforeSnapshot
 /\ DOMAIN allocation={0} \cup batch.objects /\ {allocation[unit] : unit \in DOMAIN allocation} \subseteq (Nat \ {0}) \ world.usedOccurrenceIds
 /\ Cardinality({allocation[unit] : unit \in DOMAIN allocation})=Cardinality(DOMAIN allocation)
 /\ occurrences=[id \in {allocation[unit] : unit \in DOMAIN allocation} |-> LET unit==CHOOSE unit \in DOMAIN allocation : allocation[unit]=id
       IN NewSabotageOccurrence1012(id,batch,unit,snapshot,beforeSnapshot)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: unit, NewSabotageOccurrence1012

PurgeClusterIds101 · operator

reference-profile · input revision 2 · CC0 1.0

PurgeClusterIds101(objects) ==
 {i \in DOMAIN objects : objects[i].form="Counter" /\ objects[i].kind="SchemaAtom180" /\ ~objects[i].virtual /\
    objects[i].host \in DOMAIN objects /\ objects[objects[i].host].form="Card"}

Exact module download · Source bundle and reproduction instructions

PurgeClusterOriginalProjectionPost101 · operator

reference-profile · input revision 2 · CC0 1.0

PurgeClusterOriginalProjectionPost101(objects,afterObjects,returnedToBank,revertedAndRetireed) ==
 LET plan==PurgeClusterPlan101(objects)
 IN /\ returnedToBank=plan.bank /\ revertedAndRetireed=plan.revertAndRetire
    /\ DOMAIN afterObjects=DOMAIN objects \ plan.targets
    /\ \A i \in DOMAIN afterObjects : afterObjects[i]=objects[i]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: plan

PurgeClusterPlan101 · operator

reference-profile · input revision 2 · CC0 1.0

PurgeClusterPlan101(objects) ==
 LET targets==PurgeClusterIds101(objects)
 IN [targets |-> targets,
     bank |-> {i \in targets : objects[i].card="none"},
     revertAndRetire |-> {i \in targets : objects[i].card#"none"}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: targets

RandomDamageChoices104 · operator

reference-profile · input revision 2 · CC0 1.0

RandomDamageChoices104(population,amount) == {selected \in SUBSET population : Cardinality(selected)=amount}

Exact module download · Source bundle and reproduction instructions

ReadDividendExampleFamily052Requirement1013 · operator

reference-profile · input revision 2 · CC0 1.0

ReadDividendExampleFamily052Requirement1013(world,objective,read) ==
 /\ objective \in DOMAIN world.objects /\ world.objects[objective].form="Card" /\ world.objects[objective].kind="Objective"
 /\ world.requirementProfile="PrintedAndExampleFamily052Only"
 /\ LET card==world.definitions[world.objects[objective].card]
        sources=={id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].kind="Attachment" /\ world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.objects[id].activated /\ world.objects[id].face="Up" /\
          world.definitions[world.objects[id].card]="Specimen0208" /\ world.objects[id].area="Root" /\ world.objects[id].targetSite=world.objects[objective].targetSite /\ world.objects[objective].deployed /\ world.objects[objective].area="Root"}
    IN /\ DividendFact1013(card,world.cardFacts)
       /\ read=[tag |-> "CurrentExampleFamily052ObjectiveRequirement",snapshotId |-> world.id,object |-> objective,sourceIds |-> sources,sourceSHA |-> world.cardFacts["Specimen0208"].sourceSHA,
            value |-> DividendFacts1013!DividendPrintedFacts1013[card].requirement-Cardinality(sources)]
       /\ world.requirements[objective]=read.value

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: card, sources, DividendFact1013, DividendFacts1013!DividendPrintedFacts1013

ReadEmpty109 · operator

reference-profile · input revision 2 · CC0 1.0

ReadEmpty109(world,cardFacts,link,read) ==
 /\ EmptyLink109(world,cardFacts,link)
 /\ read=[tag |-> "CurrentLinkedEmpty",snapshotId |-> world.id,linkId |-> link.id,host |-> link.host,physical |-> link.physical,
       kind |-> link.kind,loadDefinition |-> link.loadDefinition,linkedLoads |-> LinkedLoadIds109(world,link),
       effectiveCounterIds |-> HostedCounterIds109(world.objects,link.host,link.kind),
       empty |-> LinkedLoadIds109(world,link)#{} /\ HostedCounterIds109(world.objects,link.host,link.kind)={}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyLink109, HostedCounterIds109, LinkedLoadIds109

ReadSabotageDiscardSite1012 · operator

reference-profile · input revision 2 · CC0 1.0

ReadSabotageDiscardSite1012(frame,world,viewer,currentVisibleIds,read) ==
 /\ viewer \in SetupPlayers /\ currentVisibleIds=world.currentLookIds[viewer] /\ frame.packet.key \in world.completedSabotage /\ frame.id \in world.usedProcedures
 /\ frame.complete /\ frame.phase="Complete" /\ frame.choiceSealed /\ frame.afterWorld=world.id
 /\ LET moved=={frame.successors[id] : id \in DOMAIN frame.successors}
    IN /\ moved \subseteq DOMAIN world.objects /\ \A id \in moved : world.objects[id].zone="SideADiscard" /\ world.objects[id].face="Down"
       /\ read=[tag |-> "SabotageArchiveLook",viewer |-> viewer,snapshotId |-> world.id,
            visible |-> DiscardSiteVisibleCards4(moved,[id \in moved |-> world.objects[id].face],viewer,currentVisibleIds)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: moved, DiscardSiteVisibleCards4, SetupPlayers

ReadSideBLink107 · operator

reference-profile · input revision 2 · CC0 1.0

ReadSideBLink107(world,cardFacts,base,declarations,read) ==
 /\ LinkBaseRead107(world,cardFacts,base) /\ CurrentLinkDeclarations107(world,cardFacts,declarations)
 /\ read=[tag |-> "CurrentSideBLink",snapshotId |-> world.id,profile |-> base.object,base |-> base.value,
       contributions |-> [id \in DOMAIN declarations |-> declarations[id].projection.value],
       value |-> base.value+SumMap([id \in DOMAIN declarations |-> declarations[id].projection.value])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CurrentLinkDeclarations107, LinkBaseRead107, SumMap

ReceivePriorityAfterCheckpoint103 · operator

reference-profile · input revision 2 · CC0 1.0

ReceivePriorityAfterCheckpoint103(frame,ledger,beforeStack,afterStack,receipt) ==
 /\ CheckpointDrained103(frame,ledger,beforeStack) /\ receipt.id=frame.id
 /\ CheckpointPriorityWithConditionals96(ledger,beforeStack,afterStack,receipt)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriorityWithConditionals96, CheckpointDrained103

RecognizeCheckpoint103 · operator

reference-profile · input revision 2 · CC0 1.0

RecognizeCheckpoint103(before,after,beforeLedger,afterLedger,beforeStack,afterStack,x) ==
 /\ CheckpointAt103(before,"ProcedureCodee605a78f5d5e") /\ x.cp.id=before.id /\ x.cp.caller=before.caller
 /\ x.cp.beginSnapshot.id=before.beginSnapshotId /\ x.cp.processingSnapshot.id=before.snapshotId
 /\ CASE x.route="Persistent" ->
          ProcessPersistentCheckpoint912(x.registry,beforeLedger,afterLedger,beforeStack,afterStack,x.definitions,x.lexemes,x.cp,
            x.conditions,x.allocation,x.bindings,x.departures,x.holds,x.scope,x.usedWindows,x.cardFacts,x.world,x.authority)
      [] x.route="Ordinary" ->
          ProcessConditionalCheckpoint99(beforeLedger,afterLedger,beforeStack,afterStack,x.definitions,x.lexemes,x.cp,
            x.conditions,x.allocation,x.bindings,x.departures,x.holds,x.usedWindows,x.cardFacts)
      [] OTHER -> FALSE
 /\ LET advanced==[after EXCEPT !.recognition=before.recognition,!.recognized=before.recognized]
    IN /\ CheckpointStageAdvance103(before,advanced,"ProcedureCodee605a78f5d5e",before.snapshotId)
       /\ after=[advanced EXCEPT !.recognition=x.cp,!.recognized=CheckpointMemberMap103(afterLedger,before.id)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProcessConditionalCheckpoint99, ProcessPersistentCheckpoint912, advanced, CheckpointAt103, CheckpointMemberMap103, CheckpointStageAdvance103

RecordBidGuess1014 · operator

reference-profile · input revision 2 · CC0 1.0

RecordBidGuess1014(before,after,world,player,guess,continuation) ==
 /\ BidCurrent1014(before,world) /\ before.phase="WaitingReveal" /\ before.packet.participants={"SideB"} /\ player="SideA" /\ before.guess="NoValue"
 /\ "Selection" \in before.generalStages /\ guess \in {"Even","Odd"} /\ continuation=world.bidContinuations[before.id]
 /\ continuation.tag="AuthorizedBidGuess" /\ continuation.bidId=before.id /\ continuation.instance=before.caller.abilityInstance /\ continuation.player=player /\ continuation.snapshotId=world.id
 /\ after=[before EXCEPT !.guess=guess]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidCurrent1014

RecordHostDeparture103 · operator

reference-profile · input revision 2 · CC0 1.0

RecordHostDeparture103(beforeHistory,afterHistory,eventId,beforeObjects,afterObjects,source,sourceAfter,hostedSuccessors) ==
 /\ eventId \in Nat \ {0} /\ <<"Movement",eventId>> \notin DOMAIN beforeHistory /\ source \in DOMAIN beforeObjects
 /\ sourceAfter \in DOMAIN afterObjects /\ afterObjects[sourceAfter].card=beforeObjects[source].card
 /\ LET hosted=={id \in DOMAIN beforeObjects : beforeObjects[id].host=source}
        current=={IF id \in DOMAIN hostedSuccessors THEN hostedSuccessors[id] ELSE id : id \in hosted}
        objectiveCompletionLeft==beforeObjects[source].form="Card" /\ beforeObjects[source].kind="Objective" /\
                   beforeObjects[source].zone \in SetupObjectiveZones /\ afterObjects[sourceAfter].zone \notin SetupObjectiveZones
        uninstalled==beforeObjects[source].form="Card" /\ beforeObjects[source].deployed /\ ~afterObjects[sourceAfter].deployed
    IN /\ DOMAIN hostedSuccessors \subseteq hosted
       /\ \A id \in DOMAIN hostedSuccessors : hostedSuccessors[id] \in DOMAIN afterObjects /\
            afterObjects[hostedSuccessors[id]].card=beforeObjects[id].card /\ hostedSuccessors[id]#id /\ id \notin DOMAIN afterObjects
       /\ objectiveCompletionLeft \/ uninstalled
       /\ afterHistory=[id \in DOMAIN beforeHistory \cup {<<"Movement",eventId>>} |-> IF id= <<"Movement",eventId>>
            THEN [source |-> source,objectiveCompletionLeft |-> objectiveCompletionLeft,uninstalled |-> uninstalled,hostRemoved |-> uninstalled \/ objectiveCompletionLeft,children |-> current] ELSE beforeHistory[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: current, hosted, objectiveCompletionLeft, uninstalled

RemoveLiabilityMarker106 · operator

reference-profile · input revision 2 · CC0 1.0

RemoveLiabilityMarker106(context,reference,world,id,cardFacts,packet,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) ==
 /\ LiabilityMarkerPacket106(context,reference,world,id,cardFacts,packet) /\ packet.operation="Remove"
 /\ selected \subseteq MovableLiabilityMarkerIds106(world.objects)
 /\ Cardinality(selected)=IF packet.amount<=Cardinality(MovableLiabilityMarkerIds106(world.objects)) THEN packet.amount ELSE Cardinality(MovableLiabilityMarkerIds106(world.objects))
 /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiabilityMarkerCounterDeparture106, LiabilityMarkerPacket106, MovableLiabilityMarkerIds106

ReserveExposureMarkerAction105 · operator

reference-profile · input revision 2 · CC0 1.0

ReserveExposureMarkerAction105(beforeStack,afterStack,world,declarations,cardFacts,state,kind,option,legality,actionId,usedActions,frame) ==
 /\ kind \in {"RetireResource","RemoveExposureMarker"} /\ CurrentExposureMarkerState105(world,declarations,cardFacts,state)
 /\ ExposureMarkerActionStatusGate105(kind,state.hasExposureMarkers) /\ OwnActionPhase5(world.turn,ExposureMarkerActionActor105(kind)) /\ world.outcome="Playing"
 /\ actionId \in (Nat \ {0}) \ usedActions /\ Len(beforeStack)>0
 /\ LET w==WindowTop9(beforeStack) IN
    /\ w.kind="NeutralValue00001" /\ WindowSiteAllowed9("NeutralValue00001",w.site)
    /\ w.site=TurnPrioritySite9(world.turn,world.step,world.phaseId,world.actionPoints[ExposureMarkerActionActor105(kind)],[turn |-> world.turn,step |-> world.step])
    /\ \A i \in 1..Len(beforeStack) : beforeStack[i].kind="NeutralValue00001" => beforeStack[i].busy.id=0
    /\ option.kind="NeutralValue00001" /\ option.controller=ExposureMarkerActionActor105(kind) /\ option.source=RuleAbilitySource9(ExposureMarkerActionRule105(kind))
    /\ option.target=0 /\ option.newStructures={}
    /\ BeginPriorityOption9(beforeStack,afterStack,option,world.objects,legality,[id \in {} |-> id])
    /\ frame=[id |-> actionId,kind |-> kind,player |-> ExposureMarkerActionActor105(kind),windowId |-> w.id,option |-> option,transaction |-> legality.transactionId,
         activationSnapshot |-> 0,phase |-> "Reserved",action |-> [id |-> 0],target |-> 0,instruction |-> 0,effective |-> [mode |-> "NoValue"],
         nestedTransaction |-> 0,effectCosts |-> [id \in {} |-> id],payment |-> [complete |-> FALSE]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginPriorityOption9, RuleAbilitySource9, TurnPrioritySite9, WindowSiteAllowed9, w, CurrentExposureMarkerState105, ExposureMarkerActionActor105, ExposureMarkerActionRule105, ExposureMarkerActionStatusGate105, OwnActionPhase5

ResolveCharge1010 · operator

reference-profile · input revision 2 · CC0 1.0

ResolveCharge1010(context,world,id,cardFacts,admission,spec,afterObjects,afterHistory,afterCompleted,added,eventId,completion,events) ==
 /\ ChargePacket1010(context,world,id,cardFacts,admission,spec)
 /\ ChargeAdmissionKey1010(context,id) \notin world.completedCharges /\ eventId \in (Nat \ {0}) \ world.chargeEventIds
 /\ LET targets==CurrentChargeTargets1010(world,admission,spec)
    IN /\ Cardinality(DOMAIN added)=Cardinality(targets)
       /\ {added[i].host : i \in DOMAIN added}=targets
       /\ \A target \in targets : Cardinality({i \in DOMAIN added : added[i].host=target})=1
       /\ \A i \in DOMAIN added : added[i]=LoadedCounterToken109("Power",world.objects[added[i].host].zone,added[i].host,spec.actor)
       /\ BankMintProjection4(world.objects,afterObjects,added,Cardinality(targets),"Power",world.usedObjects,BankDefaultSource4("Place",FALSE,[kind |-> "NoValue"]),TRUE,TRUE)
       /\ afterHistory=world.loadHistory /\ afterCompleted=world.completedCharges \cup {ChargeAdmissionKey1010(context,id)}
       /\ completion=[tag |-> "ChargeInstructionComplete",id |-> eventId,reference |-> context.currentRef,admission |-> ChargeAdmissionKey1010(context,id),charged |-> targets,complete |-> TRUE]
       /\ events={[tag |-> "PowerCounterPlacedByCharge",instruction |-> context.currentRef,host |-> target,counter |-> CHOOSE i \in DOMAIN added : added[i].host=target,
             source |-> context.currentRef.source,snapshotId |-> world.id] : target \in targets}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: targets, ChargeAdmissionKey1010, ChargePacket1010, LoadedCounterToken109, BankDefaultSource4, BankMintProjection4

ResolveDamageBatch104 · operator

reference-profile · input revision 2 · CC0 1.0

ResolveDamageBatch104(before,after,objects,afterObjects,successors,usedIds,owners,addedCore,beforeHistory,afterHistory,batchId,events) ==
 /\ before.phase="ReadyToRetire" /\ before.outcome="Playing" /\ objects=before.beforeObjects
 /\ before.packet.amount<=Cardinality(before.bHand) /\ Cardinality(before.selected)=before.packet.amount
 /\ LET cardsAfter==DamageOwnerMoveMap104(
           DamageOwnerMoveMap104(objects,{id \in before.selected : owners[objects[id].card]="SideB"},
             [id \in {i \in before.selected : owners[objects[i].card]="SideB"} |-> successors[id]],"SideB"),
           {id \in before.selected : owners[objects[id].card]="SideA"},
             [id \in {i \in before.selected : owners[objects[i].card]="SideA"} |-> successors[id]],"SideA")
        fresh=={successors[id] : id \in before.selected}
        movementEvents=={MovementEvent8(batchId,"Retire",before.selected)}
        damageEvent==DamageSufferedEvent104(before,batchId,successors)
    IN /\ DamageCardBatchTransfer104(objects,cardsAfter,before.selected,successors,usedIds,owners)
       /\ DamageCoreCounters104(before.packet,cardsAfter,afterObjects,addedCore,usedIds \cup fresh)
       /\ RecordMovement8(beforeHistory,afterHistory,batchId,"Retire",before.selected,"Complete",TRUE,movementEvents)
       /\ events=movementEvents \cup {damageEvent}
       /\ after=[before EXCEPT !.phase="Complete",!.finalObjects=afterObjects,
            !.completion=[batchId |-> batchId,damageEvent |-> damageEvent,movementEvent |-> MovementEvent8(batchId,"Retire",before.selected)]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cardsAfter, damageEvent, fresh, movementEvents, DamageCardBatchTransfer104, DamageCoreCounters104, MovementEvent8, RecordMovement8

ResolveExposureMarkerAction105 · operator

reference-profile · input revision 2 · CC0 1.0

ResolveExposureMarkerAction105(before,after,world,afterObjects,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,beforeDepartures,afterDepartures,events) ==
 /\ before.phase="EffectReady" /\ before.action.status="Effects" /\ world.outcome="Playing"
 /\ LET blocked==IF before.kind="RetireResource" THEN world.currentRetireProhibitions ELSE world.currentExposureMarkerRemovalProhibitions
        due==IF before.effective.mode="Kept" /\ before.target \in ExposureMarkerActionTargets105(before,world) /\ before.target \notin blocked THEN {before.target} ELSE {}
        cards=={id \in due : world.objects[id].card#"none"}
    IN /\ CheckpointRetirePost103(world.objects,afterObjects,due,successors,usedIds,printed,owners,visible)
       /\ IF cards={} THEN
            /\ BankSpendReturn4(world.objects,afterObjects,due,TRUE) /\ afterHistory=beforeHistory /\ afterDepartures=beforeDepartures
          ELSE
            /\ RecordMovement8(beforeHistory,afterHistory,batchId,"Retire",cards,"Complete",TRUE,{MovementEvent8(batchId,"Retire",cards)})
            /\ IF before.kind="RetireResource" THEN RecordHostDeparture103(beforeDepartures,afterDepartures,batchId,world.objects,afterObjects,before.target,successors[before.target],[id \in {} |-> id])
               ELSE afterDepartures=beforeDepartures
       /\ events=(IF cards={} THEN {} ELSE {MovementEvent8(batchId,"Retire",cards)}) \cup
            (IF before.kind="RemoveExposureMarker" /\ due#{} THEN {[tag |-> "ExposureMarkerRemoved",actionId |-> before.id,player |-> "SideB",counter |-> before.target]} ELSE {})
       /\ after=[before EXCEPT !.phase="EffectCheckpoint"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cards, due, CheckpointRetirePost103, RecordHostDeparture103, BankSpendReturn4, MovementEvent8, RecordMovement8

ResolveMandatoryLoop101 · operator

reference-profile · input revision 2 · CC0 1.0

ResolveMandatoryLoop101(frame,afterFrame,beforeGame,afterGame,count,witness,Iteration(_,_)) ==
 /\ frame.kind="Mandatory" /\ frame.phase="Detected" /\ frame.resolver \in SetupPlayers
 /\ count \in Nat /\ Len(witness)=count+1
 /\ witness[1]=beforeGame /\ witness[count+1]=afterGame
 /\ \A i \in 1..count : Iteration(witness[i],witness[i+1])
 /\ afterFrame=[frame EXCEPT !.phase="Ended",!.iterations=count]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

ResolveOptionalTraversalLoop101 · operator

reference-profile · input revision 2 · CC0 1.0

ResolveOptionalTraversalLoop101(frame,afterFrame,withdrawTraversalProhibited,actor,actualTraversalDisposition) ==
 /\ frame.kind="Optional" /\ frame.phase="Detected" /\ frame.traversal \in Nat \ {0}
 /\ IF withdrawTraversalProhibited THEN actor="SideA" /\ actualTraversalDisposition="Continue"
    ELSE actor="SideB" /\ actualTraversalDisposition="WithdrawTraversal"
 /\ afterFrame=[frame EXCEPT !.phase="Ended",!.disposition=actualTraversalDisposition]

Exact module download · Source bundle and reproduction instructions

ResolveSabotage1012 · operator

reference-profile · input revision 2 · CC0 1.0

ResolveSabotage1012(before,after,context,operation,world,next,packet,successors,afterId,eventId,eventMap,completion) ==
 /\ SabotageFrameBound1012(before,context,operation,world,packet) /\ before.phase="ReadyRetire" /\ before.choiceSealed
 /\ before.aHandChosen \subseteq world.aHand /\ before.aDrawPileCount=SabotageTotal1012(world,packet.amount)-Cardinality(before.aHandChosen)
 /\ before.aDrawPileCount \in 0..Len(world.aDrawPile) /\ Cardinality(before.aHandChosen)<=SabotageTotal1012(world,packet.amount)
 /\ afterId \in (Nat \ {0}) \ world.usedWorlds /\ eventId \in (Nat \ {0}) \ world.eventIds
 /\ LET selected==SabotageSelected1012(before,world)
        event==SabotageRetireEvent1012(eventId,before,world,afterId,successors)
    IN /\ next.objects=SabotageRetireMap1012(world.objects,successors)
       /\ CardBatchTransfer8(world.objects,next.objects,selected,successors,world.usedObjects,"SideADiscard","Down",[id \in selected |-> 0])
       /\ eventMap=IF selected={} THEN [id \in {} |-> id] ELSE [id \in {eventId} |-> event]
       /\ next=[world EXCEPT !.id=afterId,!.objects=next.objects,!.aHand=@ \ before.aHandChosen,!.aDrawPile=SubSeq(@,before.aDrawPileCount+1,Len(@)),
             !.owners=ReplacementOverlay99(Without101(@,selected),[id \in {successors[old] : old \in selected} |-> world.owners[CHOOSE old \in selected : successors[old]=id]]),
             !.usedObjects=@ \cup {successors[old] : old \in selected},!.usedProcedures=@ \cup {before.id},!.usedWorlds=@ \cup {afterId},
             !.completedSabotage=@ \cup {packet.key},!.eventIds=@ \cup DOMAIN eventMap,!.sabotageEvents=ReplacementOverlay99(@,eventMap)]
       /\ SabotageZones1012(next)
       /\ after=[before EXCEPT !.phase="Complete",!.successors=successors,!.complete=TRUE,!.afterWorld=afterId]
       /\ completion=[tag |-> "SabotageBodyComplete",reference |-> before.reference,operation |-> operation,snapshotId |-> afterId,frameId |-> before.id,
             actor |-> "SideA",trashed |-> selected,events |-> DOMAIN eventMap,complete |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, event, selected, SabotageFrameBound1012, SabotageRetireMap1012, SabotageTotal1012, SabotageZones1012, Without101, CardBatchTransfer8

ResourceAdditionalCosts105 · operator

reference-profile · input revision 2 · CC0 1.0

ResourceAdditionalCosts105(frame,world,cardFacts) ==
 /\ frame.effectCosts=world.additionalResourceCosts /\ DOMAIN frame.effectCosts#{}
 /\ \A id \in DOMAIN frame.effectCosts :
       LET c==frame.effectCosts[id] IN
       /\ c.snapshotId=world.id /\ c.actionId=frame.id /\ c.target=frame.target /\ c.kind="RetireCentralA" /\ c.amount=1
       /\ ExposureMarkerSourceBound105(world,c.source,c.sourceObject,c.sourceSHA,cardFacts)
       /\ c.eligible \subseteq {card \in DOMAIN world.objects : world.objects[card].form="Card" /\ world.objects[card].zone="SideAHand" /\ card \notin world.currentRetireProhibitions}
       /\ (c.sourceObject.card="Specimen0212" => "SchemaAtom044" \in world.subtypes[frame.target])
       /\ (c.sourceObject.card="Specimen0136" => c.source.object=frame.target /\ ThreatFlagGate93(<<[category |-> "AbilityFlag",subtype |-> "Threat",value |-> 3]>>,world.points))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ThreatFlagGate93, c, ExposureMarkerSourceBound105

ResourceKnownCostInventory105 · operator

reference-profile · input revision 2 · CC0 1.0

ResourceKnownCostInventory105(world,target,costs,cardFacts) ==
 LET required==ResourceKnownCostSources105(world,target,cardFacts)
     observed=={costs[id].source.object : id \in {id \in DOMAIN costs : costs[id].source.object \in DOMAIN world.objects /\
          world.objects[costs[id].source.object].card \in {"Specimen0212","Specimen0136"}}}
 IN /\ observed=required
    /\ \A source \in required : Cardinality({id \in DOMAIN costs : costs[id].source=ObjectAbilitySource9(source)})=1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, observed, required

ResourceKnownCostSources105 · operator

reference-profile · input revision 2 · CC0 1.0

ResourceKnownCostSources105(world,target,cardFacts) ==
 {source \in world.activeSources \cap DOMAIN world.objects :
   DefaultActive(world.objects[source],world.started,cardFacts) /\
   ((world.objects[source].card="Specimen0212" /\ "SchemaAtom044" \in world.subtypes[target]) \/
    (world.objects[source].card="Specimen0136" /\ source=target /\
       ThreatFlagGate93(<<[category |-> "AbilityFlag",subtype |-> "Threat",value |-> 3]>>,world.points)))}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ThreatFlagGate93, DefaultActive

ResourceTargetIds105 · operator

reference-profile · input revision 2 · CC0 1.0

ResourceTargetIds105(world) ==
 {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].zone="Play" /\ world.objects[id].deployed /\
     BasicCardTarget5("SideA","RetireResource",world.objects[id].kind,world.objects[id].zone,world.objects[id].deployed) /\ world.owners[world.objects[id].card]="SideB"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasicCardTarget5

ResourceUnitPoolFact102 · operator

reference-profile · input revision 2 · CC0 1.0

ResourceUnitPoolFact102(player,objects,snapshot) ==
 InformationFact102(Cardinality({i \in DOMAIN objects : objects[i].form="Counter" /\ objects[i].kind="ResourceUnit" /\
      objects[i].zone=player \o "ResourceUnits"}),SetupPlayers,snapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InformationFact102, SetupPlayers

RestoreDiscardConversions103 · operator

reference-profile · input revision 2 · CC0 1.0

RestoreDiscardConversions103(objects,afterObjects,conversions,afterConversions,printed) ==
 LET due=={id \in DOMAIN objects \cap DOMAIN conversions : objects[id].zone \in {"SideADiscard","SideBDiscard"} /\ objects[id].card#"none"}
 IN /\ \A id \in due : ConversionValid101(conversions[id]) /\ conversions[id].card=objects[id].card
    /\ afterObjects=[id \in DOMAIN objects |-> IF id \in due THEN [objects[id] EXCEPT
          !.form="Card",!.kind=printed[objects[id].card].kind,!.properties=printed[objects[id].card],!.host=0,!.deployed=FALSE]
        ELSE objects[id]]
    /\ afterConversions=Without101(conversions,due)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: due, ConversionValid101, Without101

ResumeConditionalInstructionAfterCheckpoint103 · operator

reference-profile · input revision 2 · CC0 1.0

ResumeConditionalInstructionAfterCheckpoint103(frame,ledger,stack,before,after,receipt) ==
 /\ CheckpointDrained103(frame,ledger,stack) /\ receipt.id=frame.id
 /\ ConditionalInstructionCheckpoint96(ledger,stack,before,after,receipt)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalInstructionCheckpoint96, CheckpointDrained103

ResumePaidAfterCheckpoint103 · operator

reference-profile · input revision 2 · CC0 1.0

ResumePaidAfterCheckpoint103(frame,ledger,stack,before,after,objects,transits,receipt) ==
 /\ CheckpointDrained103(frame,ledger,stack) /\ receipt.id=frame.id
 /\ PaidCheckpointWithConditionals96(ledger,stack,before,after,objects,transits,receipt)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidCheckpointWithConditionals96, CheckpointDrained103

ReturnBid1014 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnBid1014(before,after,completion,caller) ==
 /\ completion.tag="BiddingInstructionComplete" /\ completion.result=before.result
 /\ before.complete /\ ~before.returned /\ caller=before.revealCaller /\ completion.bidId=before.id /\ completion.caller=caller /\ completion.paid
 /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

ReturnCheckpointAfterReaction103 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnCheckpointAfterReaction103(before,after,ledger,beforeStack,afterStack,caller) ==
 /\ before.phase="Reaction" /\ ~before.returned /\ caller=before.caller
 /\ CheckpointCaptured103(before,ledger) /\ DOMAIN before.recognized#{}
 /\ ConditionalCheckpointDrained96(ledger,beforeStack,before.id)
 /\ Len(beforeStack)>0 /\ WindowTop9(beforeStack).id=before.windowId
 /\ DOMAIN WindowTop9(beforeStack).members=DOMAIN before.recognized
 /\ \A id \in DOMAIN before.recognized : WindowTop9(beforeStack).members[id]=before.recognized[id]
 /\ PopClosedPriorityWindow9(beforeStack,afterStack)
 /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalCheckpointDrained96, PopClosedPriorityWindow9, WindowTop9, CheckpointCaptured103

ReturnCheckpointWithoutReaction103 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnCheckpointWithoutReaction103(before,after,ledger,world,completion,caller) ==
 /\ CheckpointCompletion103(before,ledger,world,completion) /\ DOMAIN before.recognized={}
 /\ caller=before.caller /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointCompletion103

ReturnEscalatingResourceContest108 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnEscalatingResourceContest108(before,after,world,completion) ==
 /\ before.id \in DOMAIN world.escalatingResourceContestFrames /\ world.escalatingResourceContestFrames[before.id]=before /\ before.phase="Complete" /\ before.complete /\ ~before.returned
 /\ completion=[tag |-> "OwnedEscalatingResourceContestProcedureReturn",escalatingResourceContestId |-> before.id,instance |-> before.instance,caller |-> before.caller,
       operation |-> before.packet.effectId,resultEvent |-> before.resultEvent,complete |-> TRUE,unprocessedCheckpointRequests |-> {}]
 /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

ReturnExposureMarkerAction105 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnExposureMarkerAction105(frame,beforeStack,afterStack,receipt) ==
 /\ frame.phase="Complete" /\ frame.action.status="Complete" /\ Len(beforeStack)>0
 /\ WindowTop9(beforeStack).id=frame.windowId /\ WindowTop9(beforeStack).busy=frame.option /\ WindowTop9(beforeStack).busyTransaction=frame.transaction
 /\ CompletePriorityOption9(beforeStack,afterStack,receipt)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOption9, WindowTop9

ReturnLiabilityMarkerFund106 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnLiabilityMarkerFund106(before,after,world,afterObjects,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) ==
 /\ world.traversal=before.traversal /\ world.outcome="Playing"
 /\ LiabilityMarkerFundIds106(world.objects) \subseteq CheckpointPhysicalIds103(world.objects)
 /\ ReturnLiabilityMarkerFund6(before,after,Cardinality(LiabilityMarkerFundIds106(world.objects)),Cardinality(LiabilityMarkerFundIds106(afterObjects)),0,Cardinality(LiabilityMarkerFundIds106(world.objects)))
 /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,LiabilityMarkerFundIds106(world.objects),successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPhysicalIds103, LiabilityMarkerCounterDeparture106, LiabilityMarkerFundIds106, ReturnLiabilityMarkerFund6

RevealBids1014 · operator

reference-profile · input revision 2 · CC0 1.0

RevealBids1014(before,after,world,cardFacts,transactions,continuation) ==
 /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase \in {"RevealDue","WaitingReveal"} /\ DOMAIN before.selections=before.packet.participants
 /\ BidRevealSupport1014(before,world,cardFacts)="OrdinaryFullPayment"
 /\ continuation=world.bidContinuations[before.id] /\ continuation.tag="AuthorizedBidReveal" /\ continuation.bidId=before.id
 /\ continuation.instance=before.caller.abilityInstance /\ continuation.snapshotId=world.id /\ continuation.source=before.caller.source
 /\ (before.phase="RevealDue" => continuation.instruction=before.caller)
 /\ (before.phase="WaitingReveal" => "Selection" \in before.generalStages /\ continuation.instruction#before.caller)
 /\ (before.packet.sourceCard \in {"Specimen0191","Specimen0200"} => before.guess#"NoValue" /\ "Guess" \in before.generalStages)
 /\ DOMAIN transactions=before.packet.participants /\ \A p \in DOMAIN transactions : transactions[p] \in (Nat \ {0}) \ BidReservedCosts1014(world)
 /\ \A p,q \in DOMAIN transactions : p#q => transactions[p]#transactions[q]
 /\ after=[before EXCEPT !.phase="ChoosePayment",!.revealed=before.packet.participants,!.paymentWorld=world.id,!.paymentScope=BidPaymentScope1014(world),
      !.transactions=transactions,!.revealCaller=continuation.instruction,!.costs=[p \in before.packet.participants |-> BidNestedCost1014([before EXCEPT !.revealCaller=continuation.instruction],world,p,transactions[p])]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BidCurrent1014, BidNestedCost1014, BidPaymentScope1014, BidReservedCosts1014, BidRevealSupport1014

RewriteCheckpointOrder103 · operator

reference-profile · input revision 2 · CC0 1.0

RewriteCheckpointOrder103(before,after,a,execution,compiledExceptions) ==
 /\ before.phase="Steps" /\ ~before.returned /\ a.id \in DOMAIN compiledExceptions /\ compiledExceptions[a.id]=a
 /\ a.checkpointId=before.id /\ a.snapshotId=before.snapshotId /\ a.rule="CheckpointOrder"
 /\ a.directContradiction /\ ~a.prohibited /\ a.source.kind="Object" /\ a.source.object \in Nat \ {0}
 /\ execution.tag="ActualCheckpointCardOverride" /\ execution.id=a.executionId /\ execution.source=a.source
 /\ execution.instruction=a.instruction /\ execution.checkpointId=before.id /\ execution.snapshotId=before.snapshotId /\ execution.resolved
 /\ a.beforeOwed=before.owed /\ a.discharged \subseteq SetupRange(before.owed)
 /\ a.discharged \subseteq a.explicitlyReplacedObligations
 /\ SetupRange(a.afterOwed)=SetupRange(before.owed) \ a.discharged
 /\ Len(a.afterOwed)=Cardinality(SetupRange(a.afterOwed))
 /\ after=[before EXCEPT !.owed=a.afterOwed,!.discharged=@ \cup a.discharged,!.overrideLog=Append(@,a),
       !.point=IF a.afterOwed = <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE a.afterOwed[1],!.phase=IF a.afterOwed = <<>> THEN "Completed" ELSE "Steps"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange

SabotageFrameBound1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageFrameBound1012(frame,context,operation,world,packet) ==
 /\ SabotagePacket1012(context,world,operation,packet) /\ SabotageSupport1012(packet)="SupportedResolutionComponent" /\ SabotageZones1012(world)
 /\ frame.tag="SabotageResolution" /\ frame.id \in (Nat \ {0}) \ world.usedProcedures /\ ~frame.complete
 /\ frame.contextId=context.id /\ frame.operation=operation /\ frame.reference=context.currentRef /\ frame.packet=packet /\ frame.scope=SabotageScope1012(world)
 /\ packet.key \notin world.completedSabotage

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SabotagePacket1012, SabotageScope1012, SabotageSupport1012, SabotageZones1012

SabotageKey1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageKey1012(context,operation) == <<context.id,context.currentRef,operation>>

Exact module download · Source bundle and reproduction instructions

SabotageObserverRole1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageObserverRole1012(card) ==
 CASE card="Specimen0024" -> [actor |-> "SideA",scope |-> "CentralABatch"]
   [] card \in {"Specimen0072","Specimen0110","Specimen0041"} -> [actor |-> "SideB",scope |-> "SideACard"]
   [] OTHER -> [actor |-> "NoValue",scope |-> "Unsupported"]

Exact module download · Source bundle and reproduction instructions

SabotageOmitted1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageOmitted1012(context,operation,world,afterObjects,afterCentralA,afterADrawPile,events) ==
 /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.id \in DOMAIN world.expectedInstructions /\ context=world.expectedInstructions[context.id]
 /\ operation \in DOMAIN context.templates /\ context.templates[operation].kind="SchemaAtom139"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \notin DOMAIN context.actualEffects
 /\ afterObjects=world.objects /\ afterCentralA=world.aHand /\ afterADrawPile=world.aDrawPile /\ events={}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99

SabotagePacket1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotagePacket1012(context,world,operation,packet) ==
 /\ world.outcome="Playing" /\ context.phase="Resolving" /\ context.currentWorld=world.id
 /\ context.id \in DOMAIN world.expectedInstructions /\ context=world.expectedInstructions[context.id]
 /\ ExpectedEffectsValid99(context.state.effects) /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \in DOMAIN context.actualEffects /\ operation \in DOMAIN context.templates
 /\ SabotageKey1012(context,operation) \in DOMAIN world.sabotagePackets /\ packet=world.sabotagePackets[SabotageKey1012(context,operation)]
 /\ LET e==context.actualEffects[operation] IN
    /\ e.id=operation /\ e.kind="SchemaAtom139" /\ context.templates[operation].kind="SchemaAtom139" /\ e.value \in Int
    /\ e.actor="SideA" /\ e.abilityController="SideB" /\ e.baseOrigin=context.currentRef.source
    /\ e.sourceCard \in SabotageSources1012 /\ e.sourceCard=context.templates[operation].sourceCard /\ e.sourceSHA=context.templates[operation].sourceSHA
    /\ e.sourceCard \in DOMAIN world.cardFacts /\ e.sourceSHA=world.cardFacts[e.sourceCard].sourceSHA
    /\ packet=[tag |-> "CurrentSabotagePacket",key |-> SabotageKey1012(context,operation),reference |-> context.currentRef,snapshotId |-> world.id,
         sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA,amount |-> e.value,actor |-> "SideA",abilityController |-> "SideB",sourcePhysical |-> packet.sourcePhysical,
         choicePolicy |-> packet.choicePolicy,trashProfile |-> packet.trashProfile]
    /\ context.currentRef.source.kind="Object" /\ packet.sourcePhysical \in DOMAIN world.sourceDefinitions /\ world.sourceDefinitions[packet.sourcePhysical]=e.sourceCard
    /\ IF context.currentRef.source.object \in DOMAIN world.objects THEN world.objects[context.currentRef.source.object].card=packet.sourcePhysical
       ELSE context.currentRef.source.object \in DOMAIN world.historicalPhysical /\ world.historicalPhysical[context.currentRef.source.object]=packet.sourcePhysical

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, ExpectedEffectsValid99, e, SabotageKey1012, SabotageSources1012

SabotagePublicSummary1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotagePublicSummary1012(event) ==
 [tag |-> "SabotageRetireSummary",actor |-> event.actor,aHandCount |-> Cardinality(event.fromCentralA),aDrawPileCount |-> Len(event.fromADrawPile),destination |-> "SchemaAtom018",face |-> "Down"]

Exact module download · Source bundle and reproduction instructions

SabotageRetireEvent1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageRetireEvent1012(id,frame,world,afterId,successors) ==
 [id |-> id,kind |-> "CardsRetireed",actor |-> "SideA",abilityController |-> frame.packet.abilityController,source |-> frame.reference.source,
  sourceCard |-> frame.packet.sourceCard,sourceSHA |-> frame.packet.sourceSHA,reference |-> frame.reference,operation |-> frame.operation,
  objects |-> SabotageSelected1012(frame,world),fromCentralA |-> frame.aHandChosen,fromADrawPile |-> SubSeq(world.aDrawPile,1,frame.aDrawPileCount),successors |-> successors,
  beforeSnapshot |-> world.id,afterSnapshot |-> afterId,destination |-> "SideADiscard",face |-> "Down",simultaneous |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SabotageSelected1012

SabotageRetireMap1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageRetireMap1012(objects,successors) ==
 ReplacementOverlay99(Without101(objects,DOMAIN successors),[new \in {successors[old] : old \in DOMAIN successors} |->
   [objects[CHOOSE old \in DOMAIN successors : successors[old]=new] EXCEPT !.zone="SideADiscard",!.face="Down",!.loc=0,!.host=0,!.deployed=FALSE,!.activated=FALSE,!.marks={}]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReplacementOverlay99, Without101

SabotageScope1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageScope1012(world) ==
 [id |-> world.id,objects |-> world.objects,aHand |-> world.aHand,aDrawPile |-> world.aDrawPile,usedObjects |-> world.usedObjects,owners |-> world.owners,known |-> world.sideAKnowledge]

Exact module download · Source bundle and reproduction instructions

SabotageSelected1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageSelected1012(frame,world) == frame.aHandChosen \cup SetupRange(SubSeq(world.aDrawPile,1,frame.aDrawPileCount))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange

SabotageSources1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageSources1012 == {"Specimen0159","Specimen0242","Specimen0025","Specimen0083","Specimen0041","Specimen0141","Specimen0048"}

Exact module download · Source bundle and reproduction instructions

SabotageSupport1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageSupport1012(packet) ==
 CASE packet.choicePolicy#"InternalResolutionChoice" -> "RequiresTargetTimingAdapter"
   [] packet.trashProfile#"OrdinaryUnreplaced" -> "RequiresOwningRetireAdapter"
   [] OTHER -> "SupportedResolutionComponent"

Exact module download · Source bundle and reproduction instructions

SabotageTotal1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageTotal1012(world,amount) == MinOf(MaxOf(0,amount),Cardinality(world.aHand)+Len(world.aDrawPile))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, MinOf

SabotageTriggerStipulation1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageTriggerStipulation1012(world,d,event,rule,receipt) ==
 /\ ConditionalDefinitionValid96(d) /\ d.primaryKind="Trigger" /\ d.triggerRequirements={1}
 /\ ConditionalKey96(d) \in DOMAIN world.trashRules /\ rule=world.trashRules[ConditionalKey96(d)] /\ rule.definition=d
 /\ rule.card \in DOMAIN world.cardFacts /\ rule.sourceSHA=world.cardFacts[rule.card].sourceSHA /\ rule.role=SabotageObserverRole1012(rule.card) /\ rule.role.scope#"Unsupported"
 /\ d.syntax.source.kind="Object" /\ d.syntax.source.object \in DOMAIN world.objects
 /\ world.sourceDefinitions[world.objects[d.syntax.source.object].card]=rule.card
 /\ event.id \in DOMAIN world.sabotageOccurrences /\ event=world.sabotageOccurrences[event.id]
 /\ event.batchId \in DOMAIN world.sabotageEvents /\ event.batch=world.sabotageEvents[event.batchId] /\ event.batch.id=event.batchId
 /\ (event.unit=0 \/ event.unit \in event.batch.objects)
 /\ event.kind=(IF event.unit=0 THEN "CardsRetireed" ELSE "CardRetireed") /\ event.object=event.unit
 /\ event.actor=event.batch.actor /\ event.batch.objects#{} /\ event.batch.actor="SideA"
 /\ LET matched==event.actor=rule.role.actor /\ (IF rule.role.scope="CentralABatch" THEN event.unit=0 /\ event.batch.fromCentralA#{} ELSE event.unit \in event.batch.objects)
    IN receipt=[tag |-> "ConditionalTriggerStipulations",ability |-> d.syntax.id,source |-> d.syntax.source,occurrence |-> event.id,snapshotId |-> event.snapshot.id,results |-> [part \in {1} |-> matched]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionValid96, ConditionalKey96, matched, SabotageObserverRole1012

SabotageZones1012 · operator

reference-profile · input revision 2 · CC0 1.0

SabotageZones1012(world) ==
 /\ DeckObjectOrder8(world.objects,"SideA",world.aDrawPile)
 /\ world.aHand={id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].zone="SideAHand"}
 /\ world.aHand \cap SetupRange(world.aDrawPile)={}
 /\ DOMAIN world.objects \subseteq world.usedObjects /\ DOMAIN world.owners=DOMAIN world.objects
 /\ \A id \in world.aHand \cup SetupRange(world.aDrawPile) : world.objects[id].side="SideA" /\ world.owners[id]="SideA" /\ ~world.objects[id].deployed /\ world.objects[id].host=0

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckObjectOrder8, SetupRange

SelectDamageNext104 · operator

reference-profile · input revision 2 · CC0 1.0

SelectDamageNext104(before,after,objects,card,actor,receipt) ==
 /\ before.phase="SelectingSequentially" /\ before.outcome="Playing" /\ objects=before.beforeObjects
 /\ card \in before.bHand \ before.selected
 /\ LET index==Len(before.selectionOrder)+1
        slot==before.policy.slots[index]
        selected==before.selected \cup {card}
    IN /\ index<=before.packet.amount /\ actor=slot.actor
       /\ IF slot.mode="Random" THEN DamageRandomReceipt104(before.packet,before.bHand \ before.selected,1,{card},actor,receipt)
          ELSE receipt=[tag |-> "ActualAuthorizedDamageChoice",packet |-> before.packet.key,reference |-> before.packet.reference,
                 authorityId |-> before.policy.id,index |-> index,card |-> card,actor |-> actor]
       /\ after=[before EXCEPT !.selected=selected,!.selectionOrder=Append(@,card),!.selections=Append(@,receipt),
            !.phase=IF Cardinality(selected)=before.packet.amount THEN "ReadyToRetire" ELSE "SelectingSequentially"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: index, selected, slot, DamageRandomReceipt104

SelectDamageRandomBatch104 · operator

reference-profile · input revision 2 · CC0 1.0

SelectDamageRandomBatch104(before,after,objects,selected,actor,receipt) ==
 /\ before.phase="Selecting" /\ before.outcome="Playing" /\ objects=before.beforeObjects /\ before.selected={}
 /\ DamageRandomReceipt104(before.packet,before.bHand,before.packet.amount,selected,actor,receipt)
 /\ after=[before EXCEPT !.selected=selected,!.selections= <<receipt>>,!.phase="ReadyToRetire"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DamageRandomReceipt104

SelectSecretBid1014 · operator

reference-profile · input revision 2 · CC0 1.0

SelectSecretBid1014(before,after,world,player,amount,cardFacts) ==
 /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase="Selecting" /\ player \in before.packet.participants \ DOMAIN before.selections
 /\ (IF before.packet.rangeMode="AnyAffordable" THEN amount \in Nat ELSE amount \in before.packet.allowed[player]) /\ BidPaymentPlans1014(world,player,amount,cardFacts)#{}
 /\ LET selections==ReplacementOverlay99(before.selections,[p \in {player} |-> amount]) IN
    after=[before EXCEPT !.selections=selections,!.phase=IF DOMAIN selections=before.packet.participants THEN IF before.packet.reveal="Immediate" THEN "RevealDue" ELSE "WaitingReveal" ELSE "Selecting"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: selections, BidCurrent1014, BidPaymentPlans1014

SideAMeatDamage104 · operator

reference-profile · input revision 2 · CC0 1.0

SideAMeatDamage104(packet) == packet.responsible="SideA" /\ packet.damageType="HarmClassB"

Exact module download · Source bundle and reproduction instructions

SideASabotageView1012 · operator

reference-profile · input revision 2 · CC0 1.0

SideASabotageView1012(world,packet) ==
 [tag |-> "SideASabotageDecisionView",actor |-> "SideA",amount |-> packet.amount,
  aHand |-> [id \in HandVisibleCards4(world.aHand,"SideA","SideA",{}) |-> world.objects[id].card],aDrawPileCount |-> DeckCount4(world.aDrawPile),previousKnowledge |-> world.sideAKnowledge]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckCount4, HandVisibleCards4

SkipDividendRemainder1013 · operator

reference-profile · input revision 2 · CC0 1.0

SkipDividendRemainder1013(before,after,world) ==
 /\ world.outcome="Playing" /\ DividendPlanBound1013(world,before) /\ ~before.complete /\ DividendTargetStatus1013(world,before) \in {"ReferencedObjectGone","UnhostableReferencedObject"}
 /\ after=[before EXCEPT !.skipped=@ \cup (before.cursor..before.basis.repetitions),!.cursor=before.basis.repetitions+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DividendPlanBound1013, DividendTargetStatus1013

SkipResourceAdditional105 · operator

reference-profile · input revision 2 · CC0 1.0

SkipResourceAdditional105(before,after,world,reason) ==
 /\ before.phase="AdditionalCosts" /\ reason \in {"Declined","Unpayable"} /\ world.outcome="Playing"
 /\ after=[before EXCEPT !.phase="EffectReady",!.effective.mode="Removed"]

Exact module download · Source bundle and reproduction instructions

SpendLiabilityMarkerFund106 · operator

reference-profile · input revision 2 · CC0 1.0

SpendLiabilityMarkerFund106(world,afterObjects,cost,selected,payment,usedPayments,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) ==
 /\ world.outcome="Playing" /\ DuringTraversal6(world.traversal) /\ TimingRef9("SchemaAtom138",world.traversal.id) \in world.inside
 /\ cost=world.resourceUnitCost /\ cost.tag="ResourceUnitCostContext" /\ cost.status="Paying" /\ cost.snapshotId=world.id
 /\ cost.traversalId=world.traversal.id /\ cost.player="SideB" /\ cost.amount \in Nat /\ cost.id \in (Nat \ {0}) \ usedPayments
 /\ selected \subseteq (LiabilityMarkerFundIds106(world.objects) \cup BaseSideBPoolIds106(world.objects))
 /\ selected \subseteq CheckpointPhysicalIds103(world.objects) /\ Cardinality(selected)=cost.amount
 /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events)
 /\ payment=[tag |-> "CompletedResourceUnitMethod",id |-> cost.id,source |-> cost.source,player |-> "SideB",traversalId |-> world.traversal.id,
       snapshotId |-> world.id,amount |-> cost.amount,paidCounterIds |-> selected,fundCounters |-> selected \cap LiabilityMarkerFundIds106(world.objects),complete |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, BaseSideBPoolIds106, CheckpointPhysicalIds103, LiabilityMarkerCounterDeparture106, LiabilityMarkerFundIds106, DuringTraversal6

TakeExposureMarkers105 · operator

reference-profile · input revision 2 · CC0 1.0

TakeExposureMarkers105(context,reference,world,id,afterObjects,added,usedIds,event) ==
 /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing"
 /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects
 /\ LET effect==context.actualEffects[id] IN
    /\ effect.kind="ExposureMarkers" /\ effect.value \in Nat \ {0} /\ effect.actor \in SetupPlayers /\ effect.baseOrigin=reference.source
    /\ DOMAIN added \subseteq (Nat \ {0}) \ usedIds /\ \A token \in DOMAIN added : added[token]=ExposureMarkerCounterRow105
    /\ BankMintProjection4(world.objects,afterObjects,added,effect.value,"ExposureMarker",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE)
    /\ event=[tag |-> "ExposureMarkersTaken",contextId |-> context.id,reference |-> reference,effectId |-> id,source |-> effect.baseOrigin,actor |-> effect.actor,
         player |-> "SideB",amount |-> effect.value,counters |-> DOMAIN added]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualExpectedEffects99, effect, ExposureMarkerCounterRow105, BankMintProjection4, SetupPlayers

TakeLiabilityMarker106 · operator

reference-profile · input revision 2 · CC0 1.0

TakeLiabilityMarker106(context,reference,world,id,cardFacts,packet,afterObjects,added,usedIds,events) ==
 /\ LiabilityMarkerPacket106(context,reference,world,id,cardFacts,packet) /\ packet.operation \in {"Take","Give"}
 /\ \A token \in DOMAIN added : added[token]=LiabilityMarkerCounterRow106
 /\ BankMintProjection4(world.objects,afterObjects,added,packet.amount,"LiabilityMarker",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE)
 /\ events=IF packet.amount=0 THEN {} ELSE {[tag |-> "LiabilityMarkerTaken",player |-> "SideA",actor |-> packet.actor,packet |-> packet,
       counters |-> DOMAIN added,amount |-> packet.amount]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LiabilityMarkerCounterRow106, LiabilityMarkerPacket106, BankMintProjection4

UniqueActivationPlan101 · operator

reference-profile · input revision 2 · CC0 1.0

UniqueActivationPlan101(objects,names,unique,beforeActive,afterActive,newlyActive) ==
 LET applicable == newlyActive \in DOMAIN objects /\ newlyActive \in DOMAIN names /\
                   newlyActive \in unique /\ newlyActive \notin beforeActive /\ newlyActive \in afterActive
     cohort == IF newlyActive \in DOMAIN names
               THEN {i \in ((afterActive \ beforeActive) \cap DOMAIN objects \cap DOMAIN names) : names[i]=names[newlyActive]}
               ELSE {}
     disposition == IF ~applicable THEN "NotApplicable"
                    ELSE IF cohort={newlyActive} THEN "Supported" ELSE "UnsupportedSimultaneousActivation"
 IN [valid |-> disposition="Supported",disposition |-> disposition,
     targets |-> IF disposition="Supported"
                 THEN {i \in (afterActive \cap DOMAIN objects \cap DOMAIN names) \ {newlyActive} : names[i]=names[newlyActive]} ELSE {},
     timing |-> "NextCheckpoint",preventable |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: disposition

UniqueActivationRetire101 · operator

reference-profile · input revision 2 · CC0 1.0

UniqueActivationRetire101(plan,actuallyRetireed,actualCheckpointStage,preventionApplied) ==
 /\ plan.valid /\ actualCheckpointStage="ProcedureCodefe50c31480ea"
 /\ actuallyRetireed=plan.targets /\ ~preventionApplied

Exact module download · Source bundle and reproduction instructions

Without101 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

ZoneCountFact102 · operator

reference-profile · input revision 2 · CC0 1.0

ZoneCountFact102(zone,objects,snapshot) ==
 InformationFact102(Cardinality({i \in DOMAIN objects : objects[i].form="Card" /\ objects[i].zone=zone}),SetupPlayers,snapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InformationFact102, SetupPlayers