OperationContracts

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.

prefix · operator

reference-profile · input revision 2 · CC0 1.0

prefix == DeckArrangePrefix8(deck,before.amount)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckArrangePrefix8

sources · operator

reference-profile · input revision 2 · CC0 1.0

sources == SubIds6(prefix)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: prefix, SubIds6

renew · operator

reference-profile · input revision 2 · CC0 1.0

renew == objects[before.object].zone # "Play"

Exact module download · Source bundle and reproduction instructions

prefixes · operator

reference-profile · input revision 2 · CC0 1.0

prefixes == DrawPrefixes8(before,decks)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawPrefixes8

sources · operator

reference-profile · input revision 2 · CC0 1.0

sources == DrawSources8(before,decks)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawSources8

renew · operator

reference-profile · input revision 2 · CC0 1.0

renew == objects[before.object].zone # "Play"

Exact module download · Source bundle and reproduction instructions

kind · operator

reference-profile · input revision 2 · CC0 1.0

kind == DeployEffectiveKind8(objects[f.object],f.face)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployEffectiveKind8

eligible · operator

reference-profile · input revision 2 · CC0 1.0

eligible == {i \in DOMAIN frames : ~frames[i].complete /\ frames[i].stage # "ProcedureCodec4ba55e330f8" /\ frames[i].destination.targetSite # "NoValue"}

Exact module download · Source bundle and reproduction instructions

f · operator

reference-profile · input revision 2 · CC0 1.0

f == CHOOSE id \in eligible : frames[id].object = object

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: eligible

card · operator

reference-profile · input revision 2 · CC0 1.0

card == objects[f.object]

Exact module download · Source bundle and reproduction instructions

old · operator

reference-profile · input revision 2 · CC0 1.0

old == CHOOSE s \in sources : successors[s] = id

Exact module download · Source bundle and reproduction instructions

player · operator

reference-profile · input revision 2 · CC0 1.0

player == CHOOSE p \in b.participants : objects[old].zone = p \o "Deck"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old

disposition · operator

reference-profile · input revision 2 · CC0 1.0

disposition == PlayCleanupDisposition8(before,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayCleanupDisposition8

LAMBDA · operator

reference-profile · input revision 2 · CC0 1.0

LAMBDA id : id \notin chosen

Exact module download · Source bundle and reproduction instructions

hosted · operator

reference-profile · input revision 2 · CC0 1.0

hosted == {id \in DOMAIN objects : objects[id].host = objective}

Exact module download · Source bundle and reproduction instructions

present · operator

reference-profile · input revision 2 · CC0 1.0

present == objective \in DOMAIN objects

Exact module download · Source bundle and reproduction instructions

validObjective · operator

reference-profile · input revision 2 · CC0 1.0

validObjective == IF present THEN objects[objective].form = "Card" /\ objects[objective].kind = "Objective" /\
                      objects[objective].zone \in SetupObjectiveZones ELSE FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: present, SetupObjectiveZones

next · operator

reference-profile · input revision 2 · CC0 1.0

next == ({id \in DOMAIN objects : objects[id].host \in frontier} \ visited) \ frontier

Exact module download · Source bundle and reproduction instructions

old · operator

reference-profile · input revision 2 · CC0 1.0

old == CHOOSE s \in sources : successors[s] = id

Exact module download · Source bundle and reproduction instructions

group · operator

reference-profile · input revision 2 · CC0 1.0

group == AsideGroupIds8(objects,transits,before.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AsideGroupIds8

group · operator

reference-profile · input revision 2 · CC0 1.0

group == AsideGroupIds8(objects,transits,before.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AsideGroupIds8

available · operator

reference-profile · input revision 2 · CC0 1.0

available == SearchZoneIds8(objects,f.zone)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchZoneIds8

legal · operator

reference-profile · input revision 2 · CC0 1.0

legal == SearchLegalFindSelections8(f,objects,actualCriteriaMatches,actualFeasibleSelections)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchLegalFindSelections8

o · operator

reference-profile · input revision 2 · CC0 1.0

o == afterObjects[successors[id]]

Exact module download · Source bundle and reproduction instructions

owner · operator

reference-profile · input revision 2 · CC0 1.0

owner == IF before.zone = "SideADeck" THEN "SideA" ELSE "SideB"

Exact module download · Source bundle and reproduction instructions

sources · operator

reference-profile · input revision 2 · CC0 1.0

sources == SubIds6(deck)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SubIds6

ownOrigin · operator

reference-profile · input revision 2 · CC0 1.0

ownOrigin == objects[incoming].zone = "SetAside" /\ incoming \in DOMAIN transits

Exact module download · Source bundle and reproduction instructions

target · operator

reference-profile · input revision 2 · CC0 1.0

target == transits[outgoing]

Exact module download · Source bundle and reproduction instructions

barrierCard · operator

reference-profile · input revision 2 · CC0 1.0

barrierCard == afterObjects[actualCurrentBarrierSuccessor]

Exact module download · Source bundle and reproduction instructions

other · operator

reference-profile · input revision 2 · CC0 1.0

other == IF id = a THEN b ELSE a

Exact module download · Source bundle and reproduction instructions

all · operator

reference-profile · input revision 2 · CC0 1.0

all == familyA \cup familyB

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: familyA, familyB

familyA · operator

reference-profile · input revision 2 · CC0 1.0

familyA == {a} \cup HostDescendants8(objects,a)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostDescendants8

familyB · operator

reference-profile · input revision 2 · CC0 1.0

familyB == {b} \cup HostDescendants8(objects,b)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostDescendants8

location · operator

reference-profile · input revision 2 · CC0 1.0

location == IF id = root THEN CardLocation8(objects[other])
                            ELSE [CardLocation8(row) EXCEPT !.zone = objects[other].zone,
                                    !.host = successors[row.host],!.loc = <<"Host",successors[row.host]>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: other, root, row, CardLocation8

other · operator

reference-profile · input revision 2 · CC0 1.0

other == IF root = a THEN b ELSE a

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: root

root · operator

reference-profile · input revision 2 · CC0 1.0

root == IF id \in familyA THEN a ELSE b

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: familyA

row · operator

reference-profile · input revision 2 · CC0 1.0

row == objects[id]

Exact module download · Source bundle and reproduction instructions

other · operator

reference-profile · input revision 2 · CC0 1.0

other == IF id = a THEN b ELSE a

Exact module download · Source bundle and reproduction instructions

renew · operator

reference-profile · input revision 2 · CC0 1.0

renew == SwapRenewalRequired8(objects[id],objects[other],actualArrivals[id].destinationHidden)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: other, SwapRenewalRequired8

entering · operator

reference-profile · input revision 2 · CC0 1.0

entering == {id \in {a,b} : afterObjects[successors[id]].zone = "SetAside"}

Exact module download · Source bundle and reproduction instructions

incoming · operator

reference-profile · input revision 2 · CC0 1.0

incoming == CHOOSE s \in entering : successors[s] = id

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: entering

outgoing · operator

reference-profile · input revision 2 · CC0 1.0

outgoing == IF incoming = a THEN b ELSE a

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: incoming

ActivatePlayedCard8 · operator

reference-profile · input revision 2 · CC0 1.0

ActivatePlayedCard8(before,after) ==
 /\ before.stage = "ProcedureCodecbf6b11f0ae0" /\ ~before.complete
 /\ after = [before EXCEPT !.stage = "ProcedureCode7647b901fcb1",!.activationReached = TRUE]

Exact module download · Source bundle and reproduction instructions

ActivationCacheValid8 · operator

reference-profile · input revision 2 · CC0 1.0

ActivationCacheValid8(o) == o.activated = (ActivationStatus8(o) = "ItemActivated")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivationStatus8

ActivationPermission8 · operator

reference-profile · input revision 2 · CC0 1.0

ActivationPermission8(object,o,context) ==
 /\ ItemActivatable8(o)
 /\ CASE context.route = "CardEffect" -> context.effectAuthorizes
      [] context.route = "Paid" ->
          /\ context.open /\ context.kind = "Paid" /\ context.priority = "SideA"
          /\ IF o.kind = "Barrier" THEN context.step = "ProcedureCode3a6daf593ad4" /\ context.approachedBarrier = object
             ELSE context.nonBarrierActivationAllowed
      [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemActivatable8

ActivationStatus8 · operator

reference-profile · input revision 2 · CC0 1.0

ActivationStatus8(o) ==
 IF o.form # "Card" \/ o.side # "SideA" \/ ~o.deployed \/ o.zone # "Play" THEN "Neither"
 ELSE IF o.face = "Down" /\ o.kind \in {"Objective","Facility","Attachment","Barrier"} THEN "Dormant"
 ELSE IF o.face = "Up" /\ o.kind \in {"Facility","Attachment","Barrier"} THEN "ItemActivated" ELSE "Neither"

Exact module download · Source bundle and reproduction instructions

ArrangeWord8 · operator

reference-profile · input revision 2 · CC0 1.0

ArrangeWord8(word) == word \in {"Arrange","Rearrange"}

Exact module download · Source bundle and reproduction instructions

ArrangementInstructionCheckpointAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

ArrangementInstructionCheckpointAllowed8(frame,actualContainingInstructionResolved) ==
 frame.complete /\ actualContainingInstructionResolved

Exact module download · Source bundle and reproduction instructions

AsideGroupIds8 · operator

reference-profile · input revision 2 · CC0 1.0

AsideGroupIds8(objects,transits,effectId) ==
 {id \in DOMAIN objects \cap DOMAIN transits :
    objects[id].form = "Card" /\ objects[id].zone = "SetAside" /\ transits[id].effect = effectId}

Exact module download · Source bundle and reproduction instructions

BeginDeckArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

BeginDeckArrangement8(before,after,objects,afterObjects,deck,afterDeck,transits,afterTransits,
                      successors,usedIds,actualCompoundInstructionNeedsAside) ==
 /\ before.stage = "Start" /\ ~before.complete /\ before.id \in Nat \ {0}
 /\ before.actor \in SetupPlayers /\ before.owner \in SetupPlayers /\ before.amount \in Nat
 /\ DeckObjectOrder8(objects,before.owner,deck) /\ SetAsideTrackingValid4(objects,transits)
 /\ LET prefix == DeckArrangePrefix8(deck,before.amount)
        sources == SubIds6(prefix)
    IN /\ Cardinality(sources) >= 2 \/ actualCompoundInstructionNeedsAside
       /\ CardBatchTransfer8(objects,afterObjects,sources,successors,usedIds,"SetAside","Down",
            [id \in sources |-> "SetAside"])
       /\ afterDeck = SubSeq(deck,Len(prefix)+1,Len(deck))
       /\ RegisterAsideBatch8(transits,afterTransits,objects,sources,successors,before.id,before.ability)
       /\ after = [before EXCEPT !.stage = "OtherEffects",!.originalIds = sources,!.originalCount = Len(prefix)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTrackingValid4, prefix, sources, CardBatchTransfer8, DeckObjectOrder8, RegisterAsideBatch8, SetupPlayers

BeginDeploy8 · operator

reference-profile · input revision 2 · CC0 1.0

BeginDeploy8(before,after,objects,afterObjects,newObject,usedIds,actualDeployAuthorized,
               actualSpecialDeployAuthorized,actualSpecifiedDestinationResolvable) ==
 /\ before.stage = "ProcedureCodec4ba55e330f8" /\ ~before.complete /\ before.id \in Nat \ {0}
 /\ before.object \in DOMAIN objects /\ ~objects[before.object].deployed
 /\ actualDeployAuthorized /\ actualSpecifiedDestinationResolvable
 /\ DeployTypeAllowed8(objects[before.object],before.actor,before.face,actualSpecialDeployAuthorized)
 /\ LET renew == objects[before.object].zone # "Play"
    IN /\ IF renew THEN newObject \in Nat \ {0} /\ newObject \notin usedIds \cup DOMAIN objects ELSE newObject = before.object
       /\ afterObjects = [id \in (DOMAIN objects \ {before.object}) \cup {newObject} |->
            IF id=newObject THEN DeployStagingRow8(objects[before.object],before.face,renew) ELSE objects[id]]
       /\ after = [before EXCEPT !.object = newObject,!.stage = "ProcedureCode6eba7e0bfa75"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: renew, DeployStagingRow8, DeployTypeAllowed8

BeginDrawBatch8 · operator

reference-profile · input revision 2 · CC0 1.0

BeginDrawBatch8(before,after,objects,afterObjects,decks,afterDecks,transits,afterTransits,successors,usedIds,events) ==
 /\ DrawBatchValid8(before) /\ before.stage = "SetAside" /\ before.countsReady
 /\ \E p \in before.participants : before.effective[p] > 0
 /\ DrawDeckoutWinner8(before,decks) = "NoValue"
 /\ DOMAIN decks = SetupPlayers /\ \A p \in SetupPlayers : DeckObjectOrder8(objects,p,decks[p])
 /\ SetAsideTrackingValid4(objects,transits)
 /\ LET prefixes == DrawPrefixes8(before,decks)
        sources == DrawSources8(before,decks)
    IN /\ CardBatchTransfer8(objects,afterObjects,sources,successors,usedIds,"SetAside","Down",[id \in sources |-> "SetAside"])
       /\ afterDecks = [p \in SetupPlayers |-> IF p \in before.participants
            THEN SubSeq(decks[p],Len(prefixes[p])+1,Len(decks[p])) ELSE decks[p]]
       /\ afterTransits = DrawAsideTransits8(transits,objects,sources,successors,before)
       /\ after = [before EXCEPT !.stage = "Checkpoint",
            !.initialDrawn = [p \in before.participants |-> {successors[id] : id \in SubIds6(prefixes[p])}],
            !.actualCounts = [p \in before.participants |-> Len(prefixes[p])]]
       /\ events = DrawStartEvents8(after)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTrackingValid4, prefixes, sources, CardBatchTransfer8, DeckObjectOrder8, DrawAsideTransits8, DrawBatchValid8, DrawDeckoutWinner8, DrawStartEvents8, SetupPlayers, SubIds6

BeginPlay8 · operator

reference-profile · input revision 2 · CC0 1.0

BeginPlay8(before,after,objects,afterObjects,newObject,usedIds,actualPlayAuthorized) ==
 /\ before.stage = "ProcedureCodebfd1895de2c0" /\ ~before.complete /\ before.id \in Nat \ {0}
 /\ before.object \in DOMAIN objects /\ actualPlayAuthorized
 /\ PlayTypeAllowed8(objects[before.object],before.actor) /\ ~objects[before.object].deployed
 /\ LET renew == objects[before.object].zone # "Play"
    IN /\ IF renew THEN newObject \in Nat \ {0} /\ newObject \notin usedIds \cup DOMAIN objects ELSE newObject = before.object
       /\ afterObjects = [id \in (DOMAIN objects \ {before.object}) \cup {newObject} |->
            IF id = newObject THEN PlayedPlacementRow8(objects[before.object],renew) ELSE objects[id]]
       /\ after = [before EXCEPT !.object = newObject,!.stage = "ProcedureCode0f076861472c",
            !.kind = objects[before.object].kind,!.subtypes = objects[before.object].subtypes]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: renew, PlayTypeAllowed8, PlayedPlacementRow8

CancelActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

CancelActivation8(before,after,actualActivationInstructionWithoutActivationzingComplete,events) ==
 /\ ~before.complete /\ actualActivationInstructionWithoutActivationzingComplete
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "NotItemActivated"]
 /\ events = {}

Exact module download · Source bundle and reproduction instructions

CardBatchTransfer8 · operator

reference-profile · input revision 2 · CC0 1.0

CardBatchTransfer8(beforeObjects,afterObjects,sources,successors,usedIds,destination,face,destinationLocs) ==
 /\ sources \subseteq DOMAIN beforeObjects /\ DOMAIN beforeObjects \subseteq usedIds
 /\ FreshSuccessors8(sources,successors,usedIds) /\ DOMAIN destinationLocs = sources
 /\ DOMAIN afterObjects = (DOMAIN beforeObjects \ sources) \cup {successors[id] : id \in sources}
 /\ \A id \in DOMAIN beforeObjects \ sources : afterObjects[id] = beforeObjects[id]
 /\ \A id \in sources :
      /\ beforeObjects[id].form = "Card" /\ beforeObjects[id].host = 0
      /\ afterObjects[successors[id]].form = "Card"
      /\ afterObjects[successors[id]].card = beforeObjects[id].card
      /\ afterObjects[successors[id]].side = beforeObjects[id].side
      /\ afterObjects[successors[id]].zone = destination /\ afterObjects[successors[id]].loc = destinationLocs[id]
      /\ afterObjects[successors[id]].face = face /\ ~afterObjects[successors[id]].deployed
      /\ ~afterObjects[successors[id]].activated /\ afterObjects[successors[id]].host = 0
      /\ afterObjects[successors[id]].marks = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FreshSuccessors8

CardLocation8 · operator

reference-profile · input revision 2 · CC0 1.0

CardLocation8(o) ==
 [zone |-> o.zone,loc |-> o.loc,area |-> o.area,targetSite |-> o.targetSite,
  targetSiteKind |-> o.targetSiteKind,position |-> o.position,host |-> o.host]

Exact module download · Source bundle and reproduction instructions

CardMovements8 · operator

reference-profile · input revision 2 · CC0 1.0

CardMovements8 == {"Arrange","Draw","Forfeit","Deploy","Play","Search","ObjectiveCompletion","ClaimObjective","Swap","Retire"}

Exact module download · Source bundle and reproduction instructions

ChooseDrawAmount8 · operator

reference-profile · input revision 2 · CC0 1.0

ChooseDrawAmount8(before,after,player,amount,actualAllowedAmounts) ==
 /\ DrawBatchValid8(before) /\ before.stage = "Decisions" /\ before.nextChoice \in 1..Len(before.order)
 /\ player = before.order[before.nextChoice] /\ amount \in Nat /\ amount \in actualAllowedAmounts[player]
 /\ after = [before EXCEPT !.amounts[player] = amount,!.nextChoice = @+1,
      !.stage = IF before.nextChoice = Len(before.order) THEN "SetAside" ELSE "Decisions"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawBatchValid8

CompletePlay8 · operator

reference-profile · input revision 2 · CC0 1.0

CompletePlay8(before,after) ==
 /\ before.stage = "ProcedureCode03de9212dc90" /\ ~before.complete
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE]

Exact module download · Source bundle and reproduction instructions

CompleteZeroDraw8 · operator

reference-profile · input revision 2 · CC0 1.0

CompleteZeroDraw8(before,after,events) ==
 /\ DrawBatchValid8(before) /\ before.stage = "SetAside" /\ before.countsReady
 /\ \A p \in before.participants : before.effective[p] = 0
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE] /\ events = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawBatchValid8

ComposeArrangementSwap8 · operator

reference-profile · input revision 2 · CC0 1.0

ComposeArrangementSwap8(before,after,objects,afterObjects,a,b,occurrenceId,usedOccurrenceIds,
                        actualDestinationChecks,checkpointSerial,afterCheckpointSerial,pending,afterPending,events) ==
 /\ SwapDeployedCards8(objects,afterObjects,a,b,actualDestinationChecks,occurrenceId,usedOccurrenceIds,events)
 /\ SwapArrangingBarrier8(before,after,objects,afterObjects,a,b,occurrenceId,TRUE,
      checkpointSerial,afterCheckpointSerial,pending,afterPending,events)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SwapArrangingBarrier8, SwapDeployedCards8

ComposeSwapBarrierPosition8 · operator

reference-profile · input revision 2 · CC0 1.0

ComposeSwapBarrierPosition8(layout,afterLayout,position,incoming,otherPosition,actualSwapCompleted) ==
 SwapIntoPosition6(layout,afterLayout,position,incoming,otherPosition,actualSwapCompleted)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SwapIntoPosition6

CreatePlayRetention8 · operator

reference-profile · input revision 2 · CC0 1.0

CreatePlayRetention8(beforeEffects,afterEffects,frame,actualReceipt) ==
 /\ actualReceipt.id \in Nat \ {0} /\ actualReceipt.id \notin DOMAIN beforeEffects
 /\ actualReceipt.playId = frame.id /\ actualReceipt.source = frame.object
 /\ actualReceipt.created /\ actualReceipt.expiryEffect # "NoValue"
 /\ afterEffects = [id \in DOMAIN beforeEffects \cup {actualReceipt.id} |->
      IF id = actualReceipt.id THEN actualReceipt ELSE beforeEffects[id]]

Exact module download · Source bundle and reproduction instructions

Deactivation8 · operator

reference-profile · input revision 2 · CC0 1.0

Deactivation8(objects,afterObjects,object,actualCardEffectAuthorizes,events) ==
 /\ object \in DOMAIN objects /\ ActivationStatus8(objects[object]) = "ItemActivated" /\ actualCardEffectAuthorizes
 /\ afterObjects = [objects EXCEPT ![object].face = "Down",![object].activated = FALSE]
 /\ events = {[tag |-> "Deactivation",object |-> object]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivationStatus8

DeckArrangeEffectiveViewers8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckArrangeEffectiveViewers8(frame,objects,transits,object,ordinaryViewers) ==
 IF ~frame.complete /\ frame.stage = "OtherEffects" /\ object \in AsideGroupIds8(objects,transits,frame.id)
 THEN (ordinaryViewers \ (IF frame.owner # frame.actor THEN {frame.owner} ELSE {})) \cup {frame.actor}
 ELSE ordinaryViewers

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AsideGroupIds8

DeckArrangeMayLook8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckArrangeMayLook8(frame,viewer) ==
 ~frame.complete /\ frame.stage = "OtherEffects" /\ viewer = frame.actor

Exact module download · Source bundle and reproduction instructions

DeckArrangeOtherEffects8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckArrangeOtherEffects8(frame,objects,transits,actedOnIds,declaredOriginalPositions) ==
 frame.stage = "OtherEffects" /\ ~frame.complete /\ SetAsideTrackingValid4(objects,transits) /\
 actedOnIds \subseteq AsideGroupIds8(objects,transits,frame.id) /\ declaredOriginalPositions = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTrackingValid4, AsideGroupIds8

DeckArrangePrefix8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckArrangePrefix8(deck,amount) == SubSeq(deck,1,TopCardCount8(deck,amount))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TopCardCount8

DeckArrangementPublicAction8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckArrangementPublicAction8(kind,destination,actualPublicProfile,privateOriginalPosition) ==
 [kind |-> kind,destination |-> destination,profile |-> actualPublicProfile]

Exact module download · Source bundle and reproduction instructions

DeckArrangementPublicSummary8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckArrangementPublicSummary8(frame) ==
 [actor |-> frame.actor,owner |-> frame.owner,count |-> frame.originalCount]

Exact module download · Source bundle and reproduction instructions

DeckObjectOrder8 · operator

reference-profile · input revision 2 · CC0 1.0

DeckObjectOrder8(objects,owner,deck) ==
 SubIds6(deck) = {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].zone = owner \o "Deck"} /\
 Len(deck) = Cardinality(SubIds6(deck))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SubIds6

DeclareDeployBarrierPosition8 · operator

reference-profile · input revision 2 · CC0 1.0

DeclareDeployBarrierPosition8(before,after,layout,afterLayout,gap,mode,anchor,rememberedLocation) ==
 /\ before.stage = "ProcedureCode6eba7e0bfa75" /\ after.stage = "ProcedureCode61973f2a75d8" /\ after.id = before.id
 /\ after.destination.area = "Protecting"
 /\ DeclareBarrierPosition6(DeployPositionBase8(layout,after.destination,after.newAuxiliarySite),afterLayout,
      after.destination.position,after.destination.targetSite,gap,mode,anchor,rememberedLocation,before.id,"ProcedureCode6eba7e0bfa75")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployPositionBase8, DeclareBarrierPosition6

DeclareDeployDestination8 · operator

reference-profile · input revision 2 · CC0 1.0

DeclareDeployDestination8(before,after,objects,destination,newAuxiliarySite,targetSites,usedTargetSiteIds,
                           actualHostAllowed,actualSpecifiedDestinationValid,allowedUpgradeTargetSites,activeAuxiliarySiteLimits) ==
 /\ before.stage = "ProcedureCode6eba7e0bfa75" /\ ~before.complete /\ before.object \in DOMAIN objects
 /\ DeployDestinationAllowed8(objects[before.object],before.actor,before.face,destination,newAuxiliarySite,
      targetSites,usedTargetSiteIds,objects,actualHostAllowed,actualSpecifiedDestinationValid,allowedUpgradeTargetSites,activeAuxiliarySiteLimits)
 /\ after = [before EXCEPT !.destination = destination,!.newAuxiliarySite = newAuxiliarySite,!.stage = "ProcedureCode61973f2a75d8"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployDestinationAllowed8

DeployAndActivationChoiceAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployAndActivationChoiceAllowed8(mode,actualDeployPossible,actualActivationPossible,declinesActivationAdditionalCost) ==
 mode \in {"NoValue","Normal","IfAble"} /\ actualDeployPossible /\ (mode # "IfAble" \/ (actualActivationPossible /\ ~declinesActivationAdditionalCost))

Exact module download · Source bundle and reproduction instructions

DeployAtDestination8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployAtDestination8(before,after,objects,afterObjects,targetSites,afterTargetSites,usedTargetSiteIds,activeAuxiliarySiteLimits,
                       actualAllLocationAndCapacityRestrictionsSatisfied) ==
 /\ before.stage = "ProcedureCode0f76bcc2eb00" /\ ~before.complete /\ before.object \in DOMAIN objects
 /\ ~objects[before.object].deployed /\ actualAllLocationAndCapacityRestrictionsSatisfied
 /\ IF before.newAuxiliarySite THEN NewAuxiliarySiteDeclaration4(targetSites,afterTargetSites,before.destination.targetSite,usedTargetSiteIds,
             before.destination,TRUE,activeAuxiliarySiteLimits)
    ELSE afterTargetSites = targetSites /\ (before.actor = "SideB" \/ before.destination.host # 0 \/ before.destination.targetSite \in DOMAIN targetSites)
 /\ afterObjects = [objects EXCEPT ![before.object] =
      [WithCardLocation8(objects[before.object],before.destination) EXCEPT !.deployed = TRUE,
       !.activated = objects[before.object].form="Card" /\ before.actor="SideA" /\ before.face="Up" /\
                     objects[before.object].kind \in {"Facility","Attachment","Barrier"}]]
 /\ after = [before EXCEPT !.stage = "ProcedureCode4585e6a51427"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewAuxiliarySiteDeclaration4, WithCardLocation8

DeployBeginEvent8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployBeginEvent8(f) == [tag |-> "Deployed",object |-> f.object,deployId |-> f.id,actor |-> f.actor,face |-> f.face]

Exact module download · Source bundle and reproduction instructions

DeployCardDefaultActive8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployCardDefaultActive8(frame,o) ==
 IF ~frame.complete /\ frame.stage # "ProcedureCode4585e6a51427" THEN FALSE
 ELSE o.form="Card" /\ o.face="Up" /\ o.deployed /\ (o.side="SideB" \/ o.activated)

Exact module download · Source bundle and reproduction instructions

DeployDestinationAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployDestinationAllowed8(o,actor,face,destination,newAuxiliarySite,targetSites,usedTargetSiteIds,objects,
                           actualHostAllowed,actualSpecifiedDestinationValid,allowedUpgradeTargetSites,activeAuxiliarySiteLimits) ==
 /\ actualSpecifiedDestinationValid /\ destination.zone = "Play"
 /\ IF destination.host # 0 THEN
      ~newAuxiliarySite /\ actualHostAllowed /\ destination.host \in DOMAIN objects /\ objects[destination.host].zone = "Play" /\ destination.area = "Hosted"
    ELSE IF actor = "SideB" THEN destination.area = "SideBRig" /\ destination.targetSite = "NoValue" /\ ~newAuxiliarySite
    ELSE /\ destination.area \in {"Root","Protecting"}
         /\ IF newAuxiliarySite THEN
              destination.targetSiteKind = "SchemaAtom132" /\ destination.targetSite \notin usedTargetSiteIds \cup DOMAIN targetSites \cup {"NoValue"} /\
              \A limit \in activeAuxiliarySiteLimits : Cardinality(AuxiliarySiteTargetSiteIds4(targetSites))+1 <= limit
            ELSE destination.targetSite \in DOMAIN targetSites /\ destination.targetSiteKind = targetSites[destination.targetSite].kind
         /\ TargetSiteDeployDestinationGate4(actor,o.kind,destination,TRUE,
              o.kind # "Attachment" \/ destination.targetSite \in allowedUpgradeTargetSites)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AuxiliarySiteTargetSiteIds4, TargetSiteDeployDestinationGate4

DeployEffectiveKind8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployEffectiveKind8(o,face) == IF o.side = "SideB" /\ face = "Down" THEN "Facedown" ELSE o.kind

Exact module download · Source bundle and reproduction instructions

DeployInherentPart8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployInherentPart8(card,face,objects,destination,x) ==
 IF card.form = "Counter" \/ (card.side="SideB" /\ face="Down") THEN [applicable |-> TRUE,exists |-> FALSE,amount |-> 0]
 ELSE IF card.kind="Barrier" THEN InherentDeployCost(card,Cardinality(DeployedProtectingBarrier8(objects,destination.targetSite)))
 ELSE InherentDeployCost([card EXCEPT !.deployCost = IF card.deployX THEN x ELSE @],0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InherentDeployCost, DeployedProtectingBarrier8

DeployLikeEligible8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployLikeEligible8(f,objects,effectiveTypes,controllers) ==
 LET kind == DeployEffectiveKind8(objects[f.object],f.face)
 IN IF f.actor = "SideA" /\ f.destination.area = "Root" /\ kind \in {"Objective","Facility","Attachment"}
    THEN {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].deployed /\ objects[id].zone = "Play" /\
            objects[id].area = "Root" /\ objects[id].targetSite = f.destination.targetSite}
    ELSE IF f.actor = "SideA" /\ f.destination.area = "Protecting" /\ kind="Barrier" THEN DeployedProtectingBarrier8(objects,f.destination.targetSite)
    ELSE IF f.actor="SideB" /\ kind="Technique" THEN
           {id \in DeployedTechniqueIds(objects,effectiveTypes) : controllers[id] = "SideB"}
    ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: kind, DeployedProtectingBarrier8, DeployedTechniqueIds

DeployPendingProjection8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployPendingProjection8(frames,currentOrPastObjects) ==
 LET eligible == {i \in DOMAIN frames : ~frames[i].complete /\ frames[i].stage # "ProcedureCodec4ba55e330f8" /\ frames[i].destination.targetSite # "NoValue"}
 IN [object \in {frames[id].object : id \in eligible} |->
     LET f == CHOOSE id \in eligible : frames[id].object = object
     IN [form |-> currentOrPastObjects[object].form,kind |-> currentOrPastObjects[object].kind,
         subtypes |-> currentOrPastObjects[object].subtypes,destination |-> frames[f].destination]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: eligible, f

DeployPositionBase8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployPositionBase8(layout,destination,newAuxiliarySite) ==
 IF newAuxiliarySite /\ destination.targetSite \notin DOMAIN layout.orders
 THEN [layout EXCEPT !.orders = [s \in DOMAIN @ \cup {destination.targetSite} |-> IF s=destination.targetSite THEN <<>> ELSE layout.orders[s]]]
 ELSE layout

Exact module download · Source bundle and reproduction instructions

DeployPublicLayout8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployPublicLayout8(kind) ==
 [orientation |-> IF kind="Barrier" THEN "Horizontal" ELSE "Vertical",
  rootTypeShown |-> FALSE]

Exact module download · Source bundle and reproduction instructions

DeployRequiredRootRetire8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployRequiredRootRetire8(f,objects) ==
 LET card == objects[f.object]
 IN IF f.actor="SideA" /\ f.destination.area="Root" THEN
      (IF card.kind \in {"Objective","Facility"} THEN ObjectiveFacilityRootOccupants(objects,f.destination.targetSite) ELSE {}) \cup
      (IF "SchemaAtom130" \in card.subtypes THEN DeployedRootRegions(objects,f.destination.targetSite) ELSE {})
    ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: card, DeployedRootRegions, ObjectiveFacilityRootOccupants

DeployRetireArrivalFace8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployRetireArrivalFace8(beforeCard,afterCard) ==
 beforeCard.side = "SideA" /\ afterCard.zone = "SideADiscard" /\ afterCard.face = beforeCard.face

Exact module download · Source bundle and reproduction instructions

DeployRevealRequired8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployRevealRequired8(hasOtherRequirements,actuallyOtherwiseVerified,failedDeployAndActivation) ==
 (hasOtherRequirements /\ ~actuallyOtherwiseVerified) \/ failedDeployAndActivation

Exact module download · Source bundle and reproduction instructions

DeployStagingRow8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployStagingRow8(o,face,renew) ==
 [o EXCEPT !.zone = "Play",!.loc = "DeployStaging",!.area = "Staging",!.targetSite = "NoValue",!.targetSiteKind = "NoValue",
           !.position = "NoValue",!.host = 0,!.deployed = FALSE,!.activated = FALSE,!.face = face,
           !.marks = IF renew THEN {} ELSE @]

Exact module download · Source bundle and reproduction instructions

DeploySteps8 · operator

reference-profile · input revision 2 · CC0 1.0

DeploySteps8 == {"ProcedureCodec4ba55e330f8","ProcedureCode6eba7e0bfa75","ProcedureCode61973f2a75d8","ProcedureCode1ff52d705816","CostBarrier","ProcedureCode0f76bcc2eb00","ProcedureCode4585e6a51427","Complete"}

Exact module download · Source bundle and reproduction instructions

DeployTypeAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployTypeAllowed8(o,actor,face,actualSpecialDeployAuthorized) ==
 /\ actor \in SetupPlayers /\ face \in {"Up","Down"}
 /\ IF o.form = "Counter" THEN actualSpecialDeployAuthorized
    ELSE /\ o.form = "Card" /\ o.side = actor
         /\ IF actor = "SideA" THEN o.kind \in {"Objective","Facility","Barrier","Attachment"} /\ (face="Down" \/ actualSpecialDeployAuthorized)
            ELSE IF face="Down" THEN actualSpecialDeployAuthorized ELSE o.kind \in {"Equipment","Technique","Support"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

DeployedBarrier8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployedBarrier8(o) == o.form = "Card" /\ o.side = "SideA" /\ o.kind = "Barrier" /\ o.zone = "Play" /\ o.deployed

Exact module download · Source bundle and reproduction instructions

DeployedProtectingBarrier8 · operator

reference-profile · input revision 2 · CC0 1.0

DeployedProtectingBarrier8(objects,targetSite) ==
 {id \in DOMAIN objects : DeployedBarrier8(objects[id]) /\ objects[id].host = 0 /\ objects[id].area = "Protecting" /\ objects[id].targetSite = targetSite}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployedBarrier8

DirectRelocationPlan8 · operator

reference-profile · input revision 2 · CC0 1.0

DirectRelocationPlan8(verb,owner,directedZone) ==
 [valid |-> verb \in DirectRelocations8 /\ owner \in SetupPlayers /\
       (verb \in {"Add","Move"} => directedZone \in ZoneInstances4),
  destination |-> CASE verb \in {"Add","Move"} -> directedZone
                    [] verb = "Discard" -> owner \o "Discard"
                    [] verb = "SetAside" -> "SetAside"
                    [] verb = "RemoveFromGame" -> "Removed" [] OTHER -> "NoValue",
  namedMovement |-> "NoValue"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ZoneInstances4, DirectRelocations8, SetupPlayers

DirectRelocations8 · operator

reference-profile · input revision 2 · CC0 1.0

DirectRelocations8 == {"Add","Move","Discard","SetAside","RemoveFromGame"}

Exact module download · Source bundle and reproduction instructions

DrainActivationCostCheckpoint8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainActivationCostCheckpoint8(before,after,actualTransactionId,normalCostCheckpointAndReactionsComplete) ==
 /\ before.stage = "CostCheckpoint" /\ ~before.complete /\ before.transaction # 0
 /\ actualTransactionId = before.transaction /\ normalCostCheckpointAndReactionsComplete
 /\ after = [before EXCEPT !.stage = "TurnFaceUp"]

Exact module download · Source bundle and reproduction instructions

DrainDeployCostBarrier8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainDeployCostBarrier8(before,after,actualTransactionId,actualCostCheckpointId,actualNormalCostReactionsComplete) ==
 /\ before.stage = "CostBarrier" /\ ~before.complete /\ before.transaction = actualTransactionId
 /\ actualNormalCostReactionsComplete
 /\ IF before.checkpointRequired THEN actualCostCheckpointId \in Nat \ {0} ELSE actualCostCheckpointId = 0
 /\ after = [before EXCEPT !.stage = "ProcedureCode0f76bcc2eb00"]

Exact module download · Source bundle and reproduction instructions

DrainPlayCostBarrier8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainPlayCostBarrier8(before,after,actualTransactionId,actualCostCheckpointId,actualNormalCostReactionsComplete) ==
 /\ before.stage = "CostBarrier" /\ ~before.complete /\ before.transaction = actualTransactionId
 /\ actualNormalCostReactionsComplete
 /\ IF before.checkpointRequired THEN actualCostCheckpointId \in Nat \ {0} ELSE actualCostCheckpointId = 0
 /\ after = [before EXCEPT !.stage = "ProcedureCodecbf6b11f0ae0"]

Exact module download · Source bundle and reproduction instructions

DrawAsideTransits8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawAsideTransits8(beforeTransits,objects,sources,successors,b) ==
 [id \in (DOMAIN beforeTransits \ sources) \cup {successors[s] : s \in sources} |->
   IF id \in {successors[s] : s \in sources} THEN
     LET old == CHOOSE s \in sources : successors[s] = id
         player == CHOOSE p \in b.participants : objects[old].zone = p \o "Deck"
     IN [object |-> id,originZone |-> objects[old].zone,originLocation |-> objects[old].loc,
         effect |-> b.id,ability |-> b.ability,protected |-> FALSE,cleanupStage |-> "ProcedureCode96bfa1b6a970",drawPlayer |-> player]
   ELSE beforeTransits[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: old, player

DrawBatchValid8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawBatchValid8(b) ==
 /\ b.id \in Nat \ {0} /\ b.participants \subseteq SetupPlayers /\ b.participants # {}
 /\ DOMAIN b.amounts = b.participants /\ DOMAIN b.effective = b.participants
 /\ SubIds6(b.order) = b.participants /\ Len(b.order) = Cardinality(b.participants)
 /\ b.nextChoice \in 1..(Len(b.order)+1)
 /\ \A p \in b.participants : b.amounts[p] \in Nat /\ b.effective[p] \in Nat
 /\ b.stage \in {"Decisions","SetAside","Checkpoint","DrawReactions","Return","Complete"}
 /\ b.complete = (b.stage = "Complete") /\ (b.returned => b.complete)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, SubIds6

DrawChoiceOrder8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawChoiceOrder8(active,participants) ==
 (IF active \in participants THEN <<active>> ELSE <<>>) \o
 (IF TurnOtherPlayer5(active) \in participants THEN <<TurnOtherPlayer5(active)>> ELSE <<>>)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnOtherPlayer5

DrawDeckoutWinner8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawDeckoutWinner8(b,decks) ==
 IF "SideA" \in b.participants THEN IF b.effective["SideA"] > Len(decks["SideA"]) THEN "SideB" ELSE "NoValue" ELSE "NoValue"

Exact module download · Source bundle and reproduction instructions

DrawGroupsValid8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawGroupsValid8(b,objects,transits) ==
 /\ SetAsideTrackingValid4(objects,transits)
 /\ \A id \in AsideGroupIds8(objects,transits,b.id) :
      "drawPlayer" \in DOMAIN transits[id] /\ transits[id].drawPlayer \in b.participants /\ transits[id].ability = b.ability

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTrackingValid4, AsideGroupIds8

DrawHandTransfer8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawHandTransfer8(objects,afterObjects,sources,successors,usedIds,cardData) ==
 /\ sources \subseteq DOMAIN objects /\ DOMAIN objects \subseteq usedIds
 /\ FreshSuccessors8(sources,successors,usedIds)
 /\ DOMAIN afterObjects = (DOMAIN objects \ sources) \cup {successors[id] : id \in sources}
 /\ \A id \in DOMAIN objects \ sources : afterObjects[id] = objects[id]
 /\ \A id \in sources :
      /\ objects[id].form = "Card" /\ objects[id].zone = "SetAside"
      /\ cardData[objects[id].card].owner \in SetupPlayers
      /\ afterObjects[successors[id]].form = "Card" /\ afterObjects[successors[id]].card = objects[id].card
      /\ afterObjects[successors[id]].side = objects[id].side
      /\ afterObjects[successors[id]].zone = cardData[objects[id].card].owner \o "Hand"
      /\ afterObjects[successors[id]].loc = cardData[objects[id].card].owner \o "Hand"
      /\ afterObjects[successors[id]].face = "Down" /\ ~afterObjects[successors[id]].deployed
      /\ ~afterObjects[successors[id]].activated /\ afterObjects[successors[id]].host = 0
      /\ afterObjects[successors[id]].marks = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FreshSuccessors8, SetupPlayers

DrawLookGrant8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawLookGrant8(b,objects,transits,controllers,viewer,object) ==
 b.stage \in {"Checkpoint","DrawReactions","Return"} /\ ~b.complete /\
 object \in AsideGroupIds8(objects,transits,b.id) /\ object \in DOMAIN controllers /\ controllers[object] = viewer

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AsideGroupIds8

DrawPrefixes8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawPrefixes8(b,decks) == [p \in b.participants |-> DeckArrangePrefix8(decks[p],b.effective[p])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckArrangePrefix8

DrawSources8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawSources8(b,decks) == UNION {SubIds6(DrawPrefixes8(b,decks)[p]) : p \in b.participants}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawPrefixes8, SubIds6

DrawSpecificAbilitySees8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawSpecificAbilitySees8(b,objects,transits,object,actualAbility) ==
 b.stage = "DrawReactions" /\ ~b.complete /\ actualAbility.triggerRefersDrawn /\
 actualAbility.batchId = b.id /\ object \in DrawnIds8(b,objects,transits,actualAbility.player)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawnIds8

DrawStartEvents8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawStartEvents8(b) ==
 {[tag |-> "CardsDrawn",batchId |-> b.id,player |-> p,objects |-> b.initialDrawn[p],count |-> b.actualCounts[p]] :
    p \in {q \in b.participants : b.actualCounts[q] > 0}}

Exact module download · Source bundle and reproduction instructions

DrawTransitObservation8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawTransitObservation8(transit,actualAbilityRefersToDrawn,phase,destination) ==
 IF actualAbilityRefersToDrawn THEN [visible |-> TRUE,fromZone |-> IF phase="Enter" THEN transit.originZone ELSE "SetAside",
                                    toZone |-> IF phase="Enter" THEN "SetAside" ELSE destination]
 ELSE IF phase="Enter" THEN [visible |-> FALSE,fromZone |-> "NoValue",toZone |-> "NoValue"]
 ELSE [visible |-> TRUE,fromZone |-> transit.originZone,toZone |-> destination]

Exact module download · Source bundle and reproduction instructions

DrawnIds8 · operator

reference-profile · input revision 2 · CC0 1.0

DrawnIds8(b,objects,transits,player) ==
 {id \in AsideGroupIds8(objects,transits,b.id) : transits[id].drawPlayer = player}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AsideGroupIds8

ExchangeDeployedLocations8 · operator

reference-profile · input revision 2 · CC0 1.0

ExchangeDeployedLocations8(objects,a,b) ==
 [id \in DOMAIN objects |-> IF id=a THEN WithCardLocation8(objects[a],CardLocation8(objects[b]))
   ELSE IF id=b THEN WithCardLocation8(objects[b],CardLocation8(objects[a])) ELSE objects[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardLocation8, WithCardLocation8

FinishActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishActivation8(before,after,objects,afterObjects,actualInstructionStillLegal,events) ==
 /\ before.stage = "TurnFaceUp" /\ ~before.complete /\ before.object \in DOMAIN objects
 /\ ItemActivatable8(objects[before.object]) /\ actualInstructionStillLegal
 /\ afterObjects = [objects EXCEPT ![before.object].face = "Up",![before.object].activated = TRUE]
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "ItemActivated"]
 /\ events = {[tag |-> "Activation",object |-> before.object,activationId |-> before.id]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemActivatable8

FinishBarrierArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishBarrierArrangement8(before,after,actualArrangementResolved,events) ==
 /\ before.stage = "Swaps" /\ ~before.complete /\ actualArrangementResolved
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE]
 /\ events = IF SmallArrangement8(before.targets) THEN {} ELSE {MovementEvent8(before.id,"Arrange",before.targets)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MovementEvent8, SmallArrangement8

FinishDeploy8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishDeploy8(before,after,objects,events) ==
 /\ before.stage = "ProcedureCode4585e6a51427" /\ ~before.complete /\ before.object \in DOMAIN objects /\ objects[before.object].deployed
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.deployedOccurred = TRUE]
 /\ events = {DeployBeginEvent8(before)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployBeginEvent8

FinishDeployActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishDeployActivation8(before,after,actualActivationFrame) ==
 /\ before.complete /\ before.activationStarted /\ ~before.activationProcessed /\ actualActivationFrame.complete /\ actualActivationFrame.returned
 /\ actualActivationFrame.object = before.object /\ actualActivationFrame.caller = <<"DeployAndActivation",before.id>>
 /\ after = [before EXCEPT !.activationProcessed = TRUE,!.activationPerformed = actualActivationFrame.result = "ItemActivated"]

Exact module download · Source bundle and reproduction instructions

FinishDeployLikeRetire8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishDeployLikeRetire8(before,after,objects,chosen,actuallyRetireed,effectiveTypes,controllers,capacityAfter(_),actualRetireProcedureComplete) ==
 /\ before.stage = "ProcedureCode61973f2a75d8" /\ ~before.complete /\ before.object \in DOMAIN objects /\ actualRetireProcedureComplete
 /\ chosen \subseteq DeployLikeEligible8(before,objects,effectiveTypes,controllers) /\ actuallyRetireed \subseteq chosen
 /\ DeployRequiredRootRetire8(before,objects) \subseteq actuallyRetireed
 /\ IF before.actor="SideB" /\ DeployEffectiveKind8(objects[before.object],before.face)="Technique"
    THEN TechniqueDeployCapacityChoice(DeployedTechniqueIds(objects,effectiveTypes),before.object,actuallyRetireed,capacityAfter)
    ELSE TRUE
 /\ after = [before EXCEPT !.stage = "ProcedureCode1ff52d705816"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployEffectiveKind8, DeployLikeEligible8, DeployRequiredRootRetire8, DeployedTechniqueIds, TechniqueDeployCapacityChoice

FinishDeployWithoutDeployment8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishDeployWithoutDeployment8(before,after,actualFailureDispositionAndReservationsComplete) ==
 /\ ~before.complete /\ actualFailureDispositionAndReservationsComplete
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE,!.verificationDone = TRUE,
                           !.activationProcessed = TRUE,!.activationPerformed = FALSE,!.deployedOccurred = FALSE]

Exact module download · Source bundle and reproduction instructions

FinishDrawReactions8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishDrawReactions8(before,after,actualAllDrawReactionsAndChildrenComplete) ==
 /\ before.stage = "DrawReactions" /\ ~before.complete /\ actualAllDrawReactionsAndChildrenComplete
 /\ after = [before EXCEPT !.stage = "Return"]

Exact module download · Source bundle and reproduction instructions

FinishPlayAbilities8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishPlayAbilities8(before,after,actualCompletionReceipt) ==
 /\ before.stage = "ProcedureCode3d7f756d78f7" /\ ~before.complete
 /\ PlayAbilitiesCompletion8(before,actualCompletionReceipt)
 /\ after = [before EXCEPT !.stage = "ProcedureCodee977e478b45b"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayAbilitiesCompletion8

FinishPlayCleanup8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishPlayCleanup8(before,after,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval,
                  actualCleanupReceipt,effects,afterEffects,actualRetentionReceipt) ==
 /\ before.stage = "ProcedureCodee977e478b45b" /\ ~before.complete
 /\ actualCleanupReceipt.playId = before.id /\ actualCleanupReceipt.object = before.object
 /\ LET disposition == PlayCleanupDisposition8(before,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval)
    IN /\ actualCleanupReceipt.disposition = disposition
       /\ IF disposition = "Retire" THEN
            /\ PlayedResolutionRetireDue(objects[before.object],TRUE,FALSE,FALSE)
            /\ actualCleanupReceipt.trashInstructionComplete
          ELSE TRUE
       /\ IF disposition = "RetainSelf" THEN CreatePlayRetention8(effects,afterEffects,before,actualRetentionReceipt)
          ELSE afterEffects = effects
 /\ after = [before EXCEPT !.stage = "ProcedureCodec610fc738935"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: disposition, CreatePlayRetention8, PlayedResolutionRetireDue

FinishSearchChoice8 · operator

reference-profile · input revision 2 · CC0 1.0

FinishSearchChoice8(before,after,objects,afterObjects,chosen,successors,usedIds,
                    actualCriteriaMatches,actualFeasibleSelections,actualAllowedCounts,
                    actualFindMovementReceipt,deck,afterDeck,transits,afterTransits) ==
 /\ before.stage = "Searching" /\ ~before.complete /\ before.id \in Nat \ {0} /\ before.actor \in SetupPlayers
 /\ SearchChoiceAllowed8(before,objects,chosen,actualCriteriaMatches,actualFeasibleSelections,actualAllowedCounts)
 /\ actualFindMovementReceipt.searchId = before.id /\ actualFindMovementReceipt.ability = before.ability
 /\ actualFindMovementReceipt.sources = chosen /\ actualFindMovementReceipt.successors = successors
 /\ actualFindMovementReceipt.complete
 /\ SearchFoundRows8(objects,afterObjects,chosen,successors,usedIds)
 /\ IF SearchDeck8(before) THEN
      /\ DeckObjectOrder8(objects,IF before.zone = "SideADeck" THEN "SideA" ELSE "SideB",deck)
      /\ afterDeck = SelectSeq(deck,LAMBDA id : id \notin chosen)
    ELSE afterDeck = deck
 /\ RegisterAsideBatch8(transits,afterTransits,objects,chosen,successors,before.id,before.ability)
 /\ after = [before EXCEPT !.complete = TRUE,!.foundCount = Cardinality(chosen),
      !.stage = IF SearchDeck8(before) THEN "Shuffle" ELSE "Conditions"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LAMBDA, DeckObjectOrder8, RegisterAsideBatch8, SearchChoiceAllowed8, SearchDeck8, SearchFoundRows8, SetupPlayers

ForfeitHostedCleanup8 · operator

reference-profile · input revision 2 · CC0 1.0

ForfeitHostedCleanup8(plan,actuallyRetireedSourceIds,actualProtectedTransits,owningAbility) ==
 /\ plan.valid /\ plan.trashNow \subseteq actuallyRetireedSourceIds
 /\ plan.cleanupLater \cap actuallyRetireedSourceIds = {}
 /\ plan.cleanupLater \subseteq DOMAIN actualProtectedTransits
 /\ \A id \in plan.cleanupLater :
      actualProtectedTransits[id].protected /\ actualProtectedTransits[id].ability = owningAbility /\
      actualProtectedTransits[id].cleanupStage = "ProcedureCode76ca53ad9dd0" /\ actualProtectedTransits[id].object \in Nat \ {0}

Exact module download · Source bundle and reproduction instructions

ForfeitObjectiveCompletionMembership8 · operator

reference-profile · input revision 2 · CC0 1.0

ForfeitObjectiveCompletionMembership8(beforeIds,afterIds,objective) ==
 objective \in beforeIds /\ afterIds = beforeIds \ {objective}

Exact module download · Source bundle and reproduction instructions

ForfeitObjectivePost8 · operator

reference-profile · input revision 2 · CC0 1.0

ForfeitObjectivePost8(beforeObjects,afterObjects,oldObjective,newObject,usedObjectIds) ==
 /\ oldObjective \in DOMAIN beforeObjects
 /\ beforeObjects[oldObjective].form = "Card" /\ beforeObjects[oldObjective].kind = "Objective"
 /\ beforeObjects[oldObjective].zone \in SetupObjectiveZones
 /\ newObject \in Nat \ {0} /\ newObject \notin usedObjectIds /\ newObject \notin DOMAIN beforeObjects
 /\ oldObjective \notin DOMAIN afterObjects /\ newObject \in DOMAIN afterObjects
 /\ afterObjects[newObject].form = "Card" /\ afterObjects[newObject].card = beforeObjects[oldObjective].card
 /\ afterObjects[newObject].zone = "Removed" /\ ~afterObjects[newObject].deployed /\ afterObjects[newObject].host = 0

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupObjectiveZones

ForfeitPlan8 · operator

reference-profile · input revision 2 · CC0 1.0

ForfeitPlan8(objects,objective,actualProtectedHostedSourceIds) ==
 LET present == objective \in DOMAIN objects
     validObjective == IF present THEN objects[objective].form = "Card" /\ objects[objective].kind = "Objective" /\
                      objects[objective].zone \in SetupObjectiveZones ELSE FALSE
     hosted == {id \in DOMAIN objects : objects[id].host = objective}
 IN [valid |-> validObjective /\ actualProtectedHostedSourceIds \subseteq hosted,
     destination |-> "Removed",removeFromObjectiveArea |-> {objective},
     trashNow |-> hosted \ actualProtectedHostedSourceIds,
     cleanupLater |-> actualProtectedHostedSourceIds,cleanupStage |-> "ProcedureCode76ca53ad9dd0"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: hosted, validObjective

FreshSuccessors8 · operator

reference-profile · input revision 2 · CC0 1.0

FreshSuccessors8(sources,successors,usedIds) ==
 /\ DOMAIN successors = sources
 /\ {successors[id] : id \in sources} \subseteq (Nat \ {0}) \ usedIds
 /\ Cardinality({successors[id] : id \in sources}) = Cardinality(sources)

Exact module download · Source bundle and reproduction instructions

HostDescendants8 · operator

reference-profile · input revision 2 · CC0 1.0

HostDescendants8(objects,root) ==
 HostDescendantsStep8(objects,{id \in DOMAIN objects : objects[id].host = root},{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostDescendantsStep8

HostDescendantsStep8 · operator

reference-profile · input revision 2 · CC0 1.0

HostDescendantsStep8(objects,frontier,visited) ==
 IF frontier = {} THEN visited
 ELSE LET next == ({id \in DOMAIN objects : objects[id].host \in frontier} \ visited) \ frontier
      IN HostDescendantsStep8(objects,next,visited \cup frontier)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: next, HostDescendantsStep8

ItemActivatable8 · operator

reference-profile · input revision 2 · CC0 1.0

ItemActivatable8(o) == ActivationStatus8(o) = "Dormant" /\ o.kind # "Objective"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivationStatus8

LockDrawCounts8 · operator

reference-profile · input revision 2 · CC0 1.0

LockDrawCounts8(before,after,actualEffectiveAmounts,actualDrawModifiersResolved) ==
 /\ DrawBatchValid8(before) /\ before.stage = "SetAside" /\ ~before.countsReady
 /\ actualDrawModifiersResolved /\ DOMAIN actualEffectiveAmounts = before.participants
 /\ \A p \in before.participants : actualEffectiveAmounts[p] \in Nat
 /\ after = [before EXCEPT !.effective = actualEffectiveAmounts,!.countsReady = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawBatchValid8

MarkSearchConditions8 · operator

reference-profile · input revision 2 · CC0 1.0

MarkSearchConditions8(before,after,actualPendingReceipt,events) ==
 /\ before.stage = "Conditions" /\ before.complete /\ ~before.conditionsMarked
 /\ (SearchDeck8(before) => before.shuffled)
 /\ actualPendingReceipt.searchId = before.id /\ actualPendingReceipt.allRequiredMarked
 /\ after = [before EXCEPT !.stage = "Resume",!.conditionsMarked = TRUE]
 /\ events = {[tag |-> "Searched",searchId |-> before.id,actor |-> before.actor,zone |-> before.zone,foundCount |-> before.foundCount]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchDeck8

MeetPlayResolvedConditions8 · operator

reference-profile · input revision 2 · CC0 1.0

MeetPlayResolvedConditions8(before,after,events) ==
 /\ before.stage = "ProcedureCodec610fc738935" /\ ~before.complete
 /\ after = [before EXCEPT !.stage = "ProcedureCode03de9212dc90"]
 /\ events = {[tag |-> "PlayResolved",object |-> before.object,kind |-> before.kind,actor |-> before.actor,playId |-> before.id]}

Exact module download · Source bundle and reproduction instructions

MeetPlayedConditions8 · operator

reference-profile · input revision 2 · CC0 1.0

MeetPlayedConditions8(before,after,events) ==
 /\ before.stage = "ProcedureCode7647b901fcb1" /\ before.activationReached /\ ~before.complete
 /\ after = [before EXCEPT !.stage = "ProcedureCodebddd9a1a600b"]
 /\ events = {PlayedCondition8(before)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayedCondition8

MeetSwapDeployConditions8 · operator

reference-profile · input revision 2 · CC0 1.0

MeetSwapDeployConditions8(before,after,actualCheckpointSerial,actualNormalConditionsProcessing,events) ==
 /\ ~before.met /\ actualCheckpointSerial = before.createdSerial+1 /\ actualNormalConditionsProcessing
 /\ after = [before EXCEPT !.met = TRUE]
 /\ events = {[tag |-> "Uninstalled",object |-> id,swapId |-> before.swapId] : id \in before.uninstalled} \cup
             {[tag |-> "Deployed",object |-> id,swapId |-> before.swapId] : id \in before.deployed}

Exact module download · Source bundle and reproduction instructions

MovementDispositions8 · operator

reference-profile · input revision 2 · CC0 1.0

MovementDispositions8 == {"Complete","ModifiedEffects","ReplacedByName","Prevented","Impossible","NoEffect"}

Exact module download · Source bundle and reproduction instructions

MovementEvent8 · operator

reference-profile · input revision 2 · CC0 1.0

MovementEvent8(occurrenceId,kind,originalObjects) ==
 [tag |-> "Movement",occurrenceId |-> occurrenceId,kind |-> kind,originalObjects |-> originalObjects]

Exact module download · Source bundle and reproduction instructions

MovementOccurred8 · operator

reference-profile · input revision 2 · CC0 1.0

MovementOccurred8(kind,disposition,actualInstructionResolved) ==
 kind \in CardMovements8 /\ actualInstructionResolved /\ disposition \in {"Complete","ModifiedEffects"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardMovements8

MovementRuleBlock8 · operator

reference-profile · input revision 2 · CC0 1.0

MovementRuleBlock8(kind) ==
 CASE kind = "Arrange" -> "ProcedureCode00dc1c832c18" [] kind = "Draw" -> "ProcedureCode163c820d9576"
   [] kind = "Forfeit" -> "ProcedureCode4cb5f79f70e8" [] kind = "Deploy" -> "ProcedureCodecc6f2aa507f6"
   [] kind = "Play" -> "ProcedureCode6dc50a2fd3ef" [] kind = "Search" -> "ProcedureCode8719c8b9d63c"
   [] kind \in {"ObjectiveCompletion","ClaimObjective"} -> "ProcedureCode3d7a51acc5cb" [] kind = "Swap" -> "ProcedureCode01037eaa1fce"
   [] kind = "Retire" -> "ProcedureCodea93d4fa2a792" [] OTHER -> "NoValue"

Exact module download · Source bundle and reproduction instructions

NextDeployInBatch8 · operator

reference-profile · input revision 2 · CC0 1.0

NextDeployInBatch8(beforeIndex,afterIndex,previous,actualPreviousSeparateInstructionAndCheckpointComplete) ==
 previous.returned /\ actualPreviousSeparateInstructionAndCheckpointComplete /\ beforeIndex \in Nat \ {0} /\ afterIndex = beforeIndex+1

Exact module download · Source bundle and reproduction instructions

NextPlayInBatch8 · operator

reference-profile · input revision 2 · CC0 1.0

NextPlayInBatch8(index,nextIndex,previous,actualPreviousSeparateInstructionComplete) ==
 /\ index \in Nat \ {0} /\ previous.returned /\ actualPreviousSeparateInstructionComplete /\ nextIndex = index+1

Exact module download · Source bundle and reproduction instructions

NoDeployDestination8 · operator

reference-profile · input revision 2 · CC0 1.0

NoDeployDestination8 ==
 [zone |-> "Play",loc |-> "NoValue",area |-> "NoValue",targetSite |-> "NoValue",targetSiteKind |-> "NoValue",position |-> "NoValue",host |-> 0]

Exact module download · Source bundle and reproduction instructions

NoOpDeckArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

NoOpDeckArrangement8(before,after,objects,deck,actualCompoundInstructionNeedsAside,events) ==
 /\ before.stage = "Start" /\ ~before.complete /\ before.amount \in Nat
 /\ DeckObjectOrder8(objects,before.owner,deck) /\ ~actualCompoundInstructionNeedsAside
 /\ Len(DeckArrangePrefix8(deck,before.amount)) <= 1
 /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE]
 /\ events = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckArrangePrefix8, DeckObjectOrder8

ObjectiveAreaObjectSwap8 · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveAreaObjectSwap8(objects,a,b) ==
 /\ {a,b} \subseteq DOMAIN objects /\ a # b
 /\ objects[a].kind = "Objective" /\ objects[b].kind = "Objective"
 /\ objects[a].zone \in SetupObjectiveZones /\ objects[b].zone \in SetupObjectiveZones /\ objects[a].zone # objects[b].zone

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupObjectiveZones

OccupyDeployBarrierPosition8 · operator

reference-profile · input revision 2 · CC0 1.0

OccupyDeployBarrierPosition8(before,after,layout,afterLayout,actualDeployAuthorized) ==
 before.stage = "ProcedureCode0f76bcc2eb00" /\ after.stage = "ProcedureCode4585e6a51427" /\ before.id = after.id /\
 OccupyDeclaredPosition6(layout,afterLayout,before.destination.position,before.id,before.object,"ProcedureCode0f76bcc2eb00",actualDeployAuthorized)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OccupyDeclaredPosition6

OpenActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenActivation8(id,object,caller) ==
 [id |-> id,object |-> object,caller |-> caller,stage |-> "Pay",transaction |-> 0,
  complete |-> FALSE,returned |-> FALSE,result |-> "NoValue"]

Exact module download · Source bundle and reproduction instructions

OpenBarrierArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenBarrierArrangement8(id,targets) ==
 [id |-> id,targets |-> targets,stage |-> "Swaps",complete |-> FALSE,swapEvents |-> {}]

Exact module download · Source bundle and reproduction instructions

OpenDeckArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenDeckArrangement8(id,actor,owner,amount,ability) ==
 [id |-> id,actor |-> actor,owner |-> owner,amount |-> amount,ability |-> ability,
  stage |-> "Start",complete |-> FALSE,originalIds |-> {},originalCount |-> 0]

Exact module download · Source bundle and reproduction instructions

OpenDeploy8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenDeploy8(id,object,actor,face,caller,activationMode) ==
 [id |-> id,sourceObject |-> object,object |-> object,actor |-> actor,face |-> face,caller |-> caller,
  activationMode |-> activationMode,stage |-> "ProcedureCodec4ba55e330f8",destination |-> NoDeployDestination8,newAuxiliarySite |-> FALSE,
  transaction |-> 0,checkpointRequired |-> FALSE,x |-> [exists |-> FALSE,amount |-> 0],
  complete |-> FALSE,deployedOccurred |-> FALSE,activationStarted |-> FALSE,activationProcessed |-> FALSE,activationPerformed |-> FALSE,
  verificationDone |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoDeployDestination8

OpenDrawBatch8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenDrawBatch8(id,participants,amounts,optional,active,ability,caller) ==
 [id |-> id,participants |-> participants,amounts |-> amounts,
  effective |-> [p \in participants |-> 0],countsReady |-> FALSE,
  order |-> DrawChoiceOrder8(active,participants),nextChoice |-> 1,
  ability |-> ability,caller |-> caller,stage |-> IF optional THEN "Decisions" ELSE "SetAside",
  checkpointId |-> 0,reactionId |-> 0,initialDrawn |-> [p \in participants |-> {}],
  actualCounts |-> [p \in participants |-> 0],complete |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrawChoiceOrder8

OpenDrawReactions8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenDrawReactions8(before,after,actualCheckpointId,actualReactionWindowId,actualNormalCheckpointProcessed) ==
 /\ before.stage = "Checkpoint" /\ ~before.complete /\ actualNormalCheckpointProcessed
 /\ actualCheckpointId \in Nat \ {0} /\ actualReactionWindowId \in Nat
 /\ after = [before EXCEPT !.stage = "DrawReactions",!.checkpointId = actualCheckpointId,!.reactionId = actualReactionWindowId]

Exact module download · Source bundle and reproduction instructions

OpenPlay8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenPlay8(id,object,actor,caller) ==
 [id |-> id,object |-> object,actor |-> actor,caller |-> caller,stage |-> "ProcedureCodebfd1895de2c0",
  kind |-> "NoValue",subtypes |-> {},activationReached |-> FALSE,transaction |-> 0,
  checkpointRequired |-> FALSE,x |-> [exists |-> FALSE,amount |-> 0],
  complete |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

OpenPlayAbilities8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenPlayAbilities8(before,after,actualCheckpointId,actualCheckpointAndReactionsComplete) ==
 /\ before.stage = "ProcedureCodebddd9a1a600b" /\ ~before.complete
 /\ actualCheckpointId \in Nat \ {0} /\ actualCheckpointAndReactionsComplete
 /\ after = [before EXCEPT !.stage = "ProcedureCode3d7f756d78f7"]

Exact module download · Source bundle and reproduction instructions

OpenSearch8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenSearch8(id,actor,zone,amount,hasCriteria,followup,ability,caller) ==
 [id |-> id,actor |-> actor,zone |-> zone,amount |-> amount,hasCriteria |-> hasCriteria,
  followup |-> followup,ability |-> ability,caller |-> caller,stage |-> "Searching",
  foundCount |-> 0,complete |-> FALSE,shuffled |-> FALSE,conditionsMarked |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

OpenSwapCheckpoint8 · operator

reference-profile · input revision 2 · CC0 1.0

OpenSwapCheckpoint8(swapId,objects,afterObjects,a,b,successors,checkpointSerial) ==
 [swapId |-> swapId,createdSerial |-> checkpointSerial,met |-> FALSE,
  uninstalled |-> {id \in {a,b} : objects[id].deployed /\ ~afterObjects[successors[id]].deployed},
  deployed |-> {successors[id] : id \in {i \in {a,b} : ~objects[i].deployed /\ afterObjects[successors[i]].deployed}}]

Exact module download · Source bundle and reproduction instructions

PayActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

PayActivation8(before,after,objects,context,actualAllApplicableCostsPaid,actualTransactionId) ==
 /\ before.stage = "Pay" /\ ~before.complete /\ before.object \in DOMAIN objects
 /\ before.id \in Nat \ {0}
 /\ ActivationPermission8(before.object,objects[before.object],context)
 /\ actualAllApplicableCostsPaid /\ actualTransactionId \in Nat \ {0}
 /\ after = [before EXCEPT !.stage = "CostCheckpoint",!.transaction = actualTransactionId]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivationPermission8

PayDeployStep8 · operator

reference-profile · input revision 2 · CC0 1.0

PayDeployStep8(before,after,objects,actualTransaction,actualX,actualXLegal) ==
 /\ before.stage = "ProcedureCode1ff52d705816" /\ ~before.complete /\ before.object \in DOMAIN objects
 /\ actualTransaction.id \in Nat \ {0} /\ actualTransaction.procedureId = before.id /\ actualTransaction.object = before.object
 /\ actualTransaction.allPaid /\ actualX \in Nat /\ actualXLegal
 /\ actualTransaction.basePart = DeployInherentPart8(objects[before.object],before.face,objects,before.destination,actualX)
 /\ (actualTransaction.basePart.exists /\ ~actualTransaction.deployCostIgnored) => actualTransaction.paidSomething
 /\ actualTransaction.checkpointRequired = actualTransaction.paidSomething
 /\ after = [before EXCEPT !.stage = "CostBarrier",!.transaction = actualTransaction.id,
      !.checkpointRequired = actualTransaction.checkpointRequired,
      !.x = [exists |-> objects[before.object].deployX /\ DeployEffectiveKind8(objects[before.object],before.face) \in {"Equipment","Technique","Support"},
             amount |-> IF objects[before.object].deployX /\ DeployEffectiveKind8(objects[before.object],before.face) \in {"Equipment","Technique","Support"} THEN actualX ELSE 0]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployEffectiveKind8, DeployInherentPart8

PayPlayStep8 · operator

reference-profile · input revision 2 · CC0 1.0

PayPlayStep8(before,after,objects,actualTransaction,actualIgnorePlayCostAuthorized,actualX,actualXLegal) ==
 /\ before.stage = "ProcedureCode0f076861472c" /\ ~before.complete /\ before.object \in DOMAIN objects
 /\ actualTransaction.id \in Nat \ {0} /\ actualTransaction.procedureId = before.id
 /\ actualTransaction.object = before.object /\ actualTransaction.allPaid
 /\ actualX \in Nat /\ actualXLegal
 /\ actualTransaction.basePart = PlayInherentPart8(objects[before.object],actualX)
 /\ actualTransaction.playCostIgnored => actualIgnorePlayCostAuthorized
 /\ ~actualTransaction.playCostIgnored => actualTransaction.paidSomething
 /\ actualTransaction.checkpointRequired = actualTransaction.paidSomething
 /\ after = [before EXCEPT !.stage = "CostBarrier",!.transaction = actualTransaction.id,
      !.checkpointRequired = actualTransaction.checkpointRequired,
      !.x = [exists |-> objects[before.object].playX,amount |-> IF objects[before.object].playX THEN actualX ELSE 0]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayInherentPart8

PlayAbilitiesCompletion8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayAbilitiesCompletion8(f,receipt) ==
 /\ receipt.playId = f.id /\ receipt.object = f.object /\ receipt.allPlayAbilitiesResolved
 /\ receipt.ownedTimingIds \subseteq receipt.returnedTimingIds /\ receipt.ownEndTriggersResolved

Exact module download · Source bundle and reproduction instructions

PlayCleanupDisposition8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayCleanupDisposition8(f,objects,actualSelfRetentionText,actualNestedAfterResolveRemoval) ==
 IF f.object \notin DOMAIN objects THEN "LeftPlay"
 ELSE IF objects[f.object].zone # "Play" THEN "LeftPlay"
 ELSE IF objects[f.object].form = "Counter" \/ objects[f.object].host # 0 THEN "ConvertedOrHosted"
 ELSE IF actualSelfRetentionText THEN "RetainSelf"
 ELSE IF actualNestedAfterResolveRemoval THEN "NestedRemoval"
 ELSE "Retire"

Exact module download · Source bundle and reproduction instructions

PlayEffectiveCardActivity8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayEffectiveCardActivity8(frame,object,o,ordinaryCardActivity) ==
 IF object = frame.object /\ ~frame.returned
 THEN PlayedCardActive(o,frame.activationReached) ELSE ordinaryCardActivity

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayedCardActive

PlayInherentPart8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayInherentPart8(o,x) ==
 InherentPlayCost([o EXCEPT !.playCost = IF o.playX THEN x ELSE @])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InherentPlayCost

PlayTypeAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayTypeAllowed8(o,actor) ==
 o.form = "Card" /\ o.side = actor /\
 ((actor = "SideA" /\ o.kind = "Plan") \/ (actor = "SideB" /\ o.kind = "Action"))

Exact module download · Source bundle and reproduction instructions

PlayedCondition8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayedCondition8(f) ==
 [tag |-> "Played",object |-> f.object,kind |-> f.kind,subtypes |-> f.subtypes,actor |-> f.actor,playId |-> f.id]

Exact module download · Source bundle and reproduction instructions

PlayedPlacementRow8 · operator

reference-profile · input revision 2 · CC0 1.0

PlayedPlacementRow8(o,renew) ==
 [WithCardLocation8(o,[NoDeployDestination8 EXCEPT !.loc = "Played",!.area = "Played"]) EXCEPT
    !.deployed = FALSE,!.face = "Up",!.activated = FALSE,!.marks = IF renew THEN {} ELSE @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoDeployDestination8, WithCardLocation8

PublicSideBOrigins8 · operator

reference-profile · input revision 2 · CC0 1.0

PublicSideBOrigins8(objects,origins,actualPublicEventHistory) ==
 [id \in {i \in DOMAIN objects : SideBFacedown8(objects[i])} |->
    [method |-> origins[id].method,serial |-> origins[id].serial,ability |-> origins[id].ability,
     previousFaceupProfile |-> IF origins[id].method = "TurnedFacedown"
       THEN actualPublicEventHistory[origins[id].eventId].previousFaceupProfile
       ELSE [known |-> FALSE,card |-> "Hidden"]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBFacedown8

RecordMovement8 · operator

reference-profile · input revision 2 · CC0 1.0

RecordMovement8(beforeHistory,afterHistory,occurrenceId,kind,originalObjects,disposition,actualInstructionResolved,events) ==
 /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin DOMAIN beforeHistory
 /\ kind \in CardMovements8 /\ disposition \in MovementDispositions8 /\ actualInstructionResolved
 /\ IF MovementOccurred8(kind,disposition,actualInstructionResolved) THEN
      /\ afterHistory = [id \in DOMAIN beforeHistory \cup {occurrenceId} |-> IF id = occurrenceId
           THEN MovementEvent8(occurrenceId,kind,originalObjects) ELSE beforeHistory[id]]
      /\ events = {MovementEvent8(occurrenceId,kind,originalObjects)}
    ELSE afterHistory = beforeHistory /\ events = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardMovements8, MovementDispositions8, MovementEvent8, MovementOccurred8

RecordSideBFaceOrigin8 · operator

reference-profile · input revision 2 · CC0 1.0

RecordSideBFaceOrigin8(before,after,object,method,serial,ability,actualFacedownEvent) ==
 /\ SideBOriginEventValid8(object,method,serial,ability,actualFacedownEvent)
 /\ IF object \in DOMAIN before THEN serial > before[object].serial ELSE TRUE
 /\ after = [id \in DOMAIN before \cup {object} |-> IF id = object
       THEN [method |-> method,serial |-> serial,ability |-> ability,eventId |-> actualFacedownEvent.id] ELSE before[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBOriginEventValid8

RegisterAsideBatch8 · operator

reference-profile · input revision 2 · CC0 1.0

RegisterAsideBatch8(beforeTransits,afterTransits,beforeObjects,sources,successors,effectId,ability) ==
 afterTransits = [id \in (DOMAIN beforeTransits \ sources) \cup {successors[s] : s \in sources} |->
    IF id \in {successors[s] : s \in sources} THEN
      LET old == CHOOSE s \in sources : successors[s] = id
      IN SetAsideTransit4(id,beforeObjects[old].zone,beforeObjects[old].loc,effectId,ability,FALSE,FALSE)
    ELSE beforeTransits[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTransit4, old

ResumeSearchAbility8 · operator

reference-profile · input revision 2 · CC0 1.0

ResumeSearchAbility8(before,after,caller) ==
 /\ before.stage = "Resume" /\ before.complete /\ before.conditionsMarked /\ ~before.returned
 /\ (SearchDeck8(before) => before.shuffled) /\ caller = before.caller
 /\ after = [before EXCEPT !.stage = "Resumed",!.returned = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchDeck8

ReturnActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnActivation8(before,after,actualInstructionAndEndingReactionsComplete,caller) ==
 /\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualInstructionAndEndingReactionsComplete
 /\ after = [before EXCEPT !.returned = TRUE]

Exact module download · Source bundle and reproduction instructions

ReturnDeckArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnDeckArrangement8(before,after,objects,afterObjects,deck,afterDeck,transits,afterTransits,
                       order,successors,usedIds,actualOtherEffectsComplete) ==
 /\ before.stage = "OtherEffects" /\ ~before.complete /\ actualOtherEffectsComplete
 /\ DeckObjectOrder8(objects,before.owner,deck) /\ SetAsideTrackingValid4(objects,transits)
 /\ LET group == AsideGroupIds8(objects,transits,before.id)
    IN /\ SubIds6(order) = group /\ Len(order) = Cardinality(group)
       /\ CardBatchTransfer8(objects,afterObjects,group,successors,usedIds,before.owner \o "Deck","Down",
            [id \in group |-> <<"Deck",before.id,PositionIndex6(order,id)>>])
       /\ afterDeck = [i \in 1..Len(order) |-> successors[order[i]]] \o deck
       /\ afterTransits = [id \in DOMAIN transits \ group |-> transits[id]]
       /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTrackingValid4, group, CardBatchTransfer8, DeckObjectOrder8, PositionIndex6, SubIds6

ReturnDeployToCaller8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnDeployToCaller8(before,after,actualWholeInstructionAndCheckpointReactionsComplete,caller) ==
 /\ before.complete /\ before.verificationDone /\ ~before.returned /\ caller = before.caller
 /\ (before.activationMode = "NoValue" \/ before.activationProcessed) /\ actualWholeInstructionAndCheckpointReactionsComplete
 /\ after = [before EXCEPT !.returned = TRUE]

Exact module download · Source bundle and reproduction instructions

ReturnDrawToCaller8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnDrawToCaller8(before,after,actualProcedureEndCheckpointAndReactionsComplete,caller) ==
 /\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualProcedureEndCheckpointAndReactionsComplete
 /\ after = [before EXCEPT !.returned = TRUE]

Exact module download · Source bundle and reproduction instructions

ReturnDrawnCards8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnDrawnCards8(before,after,objects,afterObjects,transits,afterTransits,successors,usedIds,cardData,events) ==
 /\ before.stage = "Return" /\ ~before.complete /\ DrawGroupsValid8(before,objects,transits)
 /\ LET group == AsideGroupIds8(objects,transits,before.id)
    IN /\ DrawHandTransfer8(objects,afterObjects,group,successors,usedIds,cardData)
       /\ afterTransits = [id \in DOMAIN transits \ group |-> transits[id]]
       /\ after = [before EXCEPT !.stage = "Complete",!.complete = TRUE]
       /\ events = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: group, DrawGroupsValid8, DrawHandTransfer8

ReturnPlayToCaller8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnPlayToCaller8(before,after,actualSeparateInstructionAndEndingReactionsComplete,caller) ==
 /\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualSeparateInstructionAndEndingReactionsComplete
 /\ after = [before EXCEPT !.returned = TRUE]

Exact module download · Source bundle and reproduction instructions

SearchChainReactionsAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchChainReactionsAllowed8(f) == f.complete /\ f.conditionsMarked /\ (SearchDeck8(f) => f.shuffled)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchDeck8

SearchChoiceAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchChoiceAllowed8(f,objects,chosen,actualCriteriaMatches,actualFeasibleSelections,actualAllowedCounts) ==
 LET available == SearchZoneIds8(objects,f.zone)
     legal == SearchLegalFindSelections8(f,objects,actualCriteriaMatches,actualFeasibleSelections)
 IN /\ f.amount \in Nat /\ f.followup \in {"NoValue","Deploy","Play"}
    /\ (~f.hasCriteria => available \subseteq actualCriteriaMatches)
    /\ chosen \in legal
    /\ IF ~f.hasCriteria THEN Cardinality(chosen) = SearchMaximumFeasibleCount8(legal)
       ELSE (Cardinality(chosen) \in actualAllowedCounts \/ (SearchDeck8(f) /\ chosen = {}))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: available, legal, SearchDeck8, SearchMaximumFeasibleCount8

SearchDeck8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchDeck8(f) == f.zone \in {"SideADeck","SideBDeck"}

Exact module download · Source bundle and reproduction instructions

SearchFoundActionAllowed8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchFoundActionAllowed8(f) ==
 f.returned /\ f.stage = "Resumed" /\ f.conditionsMarked /\ (SearchDeck8(f) => f.shuffled)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchDeck8

SearchFoundRows8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchFoundRows8(beforeObjects,afterObjects,chosen,successors,usedIds) ==
 /\ chosen \subseteq DOMAIN beforeObjects /\ DOMAIN beforeObjects \subseteq usedIds
 /\ FreshSuccessors8(chosen,successors,usedIds)
 /\ chosen \cap DOMAIN afterObjects = {}
 /\ {successors[id] : id \in chosen} \subseteq DOMAIN afterObjects
 /\ \A id \in chosen :
      LET o == afterObjects[successors[id]]
      IN /\ o.form = "Card" /\ o.card = beforeObjects[id].card /\ o.side = beforeObjects[id].side
         /\ o.zone = "SetAside" /\ o.face = "Down" /\ ~o.deployed /\ ~o.activated /\ o.host = 0 /\ o.marks = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: o, FreshSuccessors8

SearchLegalFindSelections8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchLegalFindSelections8(f,objects,actualCriteriaMatches,actualFeasibleSelections) ==
 {selection \in SUBSET SearchZoneIds8(objects,f.zone) :
    selection \subseteq actualCriteriaMatches /\ Cardinality(selection) <= f.amount /\
    (f.followup = "NoValue" \/ selection = {} \/ selection \in actualFeasibleSelections)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchZoneIds8

SearchLookGrant8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchLookGrant8(f,viewer,object,objects) ==
 f.stage = "Searching" /\ ~f.complete /\ viewer = f.actor /\ object \in SearchZoneIds8(objects,f.zone)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchZoneIds8

SearchMaximumFeasibleCount8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchMaximumFeasibleCount8(selections) ==
 CHOOSE count \in {Cardinality(selection) : selection \in selections} :
    \A selection \in selections : Cardinality(selection) <= count

Exact module download · Source bundle and reproduction instructions

SearchRemainingEffectsContinue8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchRemainingEffectsContinue8(f) == SearchFoundActionAllowed8(f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchFoundActionAllowed8

SearchRevealFound8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchRevealFound8(f,objects,transits,object,actualAbilityInstructsReveal,actualRevealReceipt) ==
 /\ SearchRevealRequired8(f,actualAbilityInstructsReveal)
 /\ object \in AsideGroupIds8(objects,transits,f.id)
 /\ actualRevealReceipt.performed /\ actualRevealReceipt.object = object /\ actualRevealReceipt.searchId = f.id

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AsideGroupIds8, SearchRevealRequired8

SearchRevealRequired8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchRevealRequired8(f,actualAbilityInstructsReveal) ==
 SearchFoundActionAllowed8(f) /\ actualAbilityInstructsReveal

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SearchFoundActionAllowed8

SearchShuffle8 · operator

reference-profile · input revision 2 · CC0 1.0

SearchShuffle8(before,after,objects,afterObjects,deck,afterDeck,oldOrder,successors,usedIds,
               actualShuffleReceipt,transits,afterTransits) ==
 /\ before.stage = "Shuffle" /\ before.complete /\ SearchDeck8(before) /\ ~before.shuffled
 /\ actualShuffleReceipt.searchId = before.id /\ actualShuffleReceipt.zone = before.zone /\ actualShuffleReceipt.performed
 /\ LET owner == IF before.zone = "SideADeck" THEN "SideA" ELSE "SideB"
        sources == SubIds6(deck)
    IN /\ DeckObjectOrder8(objects,owner,deck)
       /\ Len(oldOrder) = Len(deck) /\ SubIds6(oldOrder) = sources
       /\ CardBatchTransfer8(objects,afterObjects,sources,successors,usedIds,before.zone,"Down",
            [id \in sources |-> <<before.zone,PositionIndex6(oldOrder,id)>>])
       /\ afterDeck = [i \in 1..Len(oldOrder) |-> successors[oldOrder[i]]]
       /\ DeckObjectOrder8(afterObjects,owner,afterDeck)
       /\ DeckSearchCompletion4([i \in 1..Len(deck) |-> objects[deck[i]].card],
            [i \in 1..Len(afterDeck) |-> afterObjects[afterDeck[i]].card],actualShuffleReceipt.performed)
 /\ afterTransits = transits
 /\ after = [before EXCEPT !.stage = "Conditions",!.shuffled = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckSearchCompletion4, owner, sources, CardBatchTransfer8, DeckObjectOrder8, SearchDeck8, PositionIndex6, SubIds6

SearchZoneIds8 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

SideBAbilityActivity8 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAbilityActivity8(o,otherwiseActive) == ~SideBFacedown8(o) /\ otherwiseActive

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBFacedown8

SideBBDiscardPileFacePost8 · operator

reference-profile · input revision 2 · CC0 1.0

SideBBDiscardPileFacePost8(o) ==
 (o.form = "Card" /\ o.side = "SideB" /\ o.zone = "SideBDiscard") => o.face = "Up"

Exact module download · Source bundle and reproduction instructions

SideBCharacteristics8 · operator

reference-profile · input revision 2 · CC0 1.0

SideBCharacteristics8(o,normalCharacteristics) ==
 IF SideBFacedown8(o) THEN [key \in {} |-> key] ELSE normalCharacteristics

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBFacedown8

SideBFacedown8 · operator

reference-profile · input revision 2 · CC0 1.0

SideBFacedown8(o) ==
 o.form = "Card" /\ o.side = "SideB" /\ o.zone = "Play" /\ o.deployed /\ o.face = "Down"

Exact module download · Source bundle and reproduction instructions

SideBOriginEventValid8 · operator

reference-profile · input revision 2 · CC0 1.0

SideBOriginEventValid8(object,method,serial,ability,event) ==
 /\ method \in {"DeployedFacedown","TurnedFacedown"} /\ serial \in Nat \ {0}
 /\ event.id \in Nat \ {0} /\ event.object = object /\ event.serial = serial /\ event.ability = ability
 /\ IF method = "DeployedFacedown"
    THEN event.tag = "Deployed" /\ event.face = "Down" /\ ~event.previousFaceupProfile.known
    ELSE event.tag = "TurnFacedown" /\ event.previousFaceupProfile.known

Exact module download · Source bundle and reproduction instructions

SideBOriginsComplete8 · operator

reference-profile · input revision 2 · CC0 1.0

SideBOriginsComplete8(objects,origins,actualPublicEventHistory) ==
 /\ {id \in DOMAIN objects : SideBFacedown8(objects[id])} \subseteq DOMAIN origins
 /\ \A id \in {i \in DOMAIN objects : SideBFacedown8(objects[i])} :
      /\ origins[id].eventId \in DOMAIN actualPublicEventHistory
      /\ actualPublicEventHistory[origins[id].eventId].id = origins[id].eventId
      /\ SideBOriginEventValid8(id,origins[id].method,origins[id].serial,origins[id].ability,
           actualPublicEventHistory[origins[id].eventId])
      /\ \A e \in DOMAIN actualPublicEventHistory :
           actualPublicEventHistory[e].object = id => actualPublicEventHistory[e].serial <= origins[id].serial

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBFacedown8, SideBOriginEventValid8

SmallArrangement8 · operator

reference-profile · input revision 2 · CC0 1.0

SmallArrangement8(ids) == Cardinality(ids) <= 1

Exact module download · Source bundle and reproduction instructions

StartDeployActivation8 · operator

reference-profile · input revision 2 · CC0 1.0

StartDeployActivation8(before,after,request) ==
 /\ before.complete /\ before.deployedOccurred /\ before.activationMode \in {"Normal","IfAble"} /\ ~before.activationStarted
 /\ after = [before EXCEPT !.activationStarted = TRUE]
 /\ request = [kind |-> "Activation",object |-> before.object,caller |-> <<"DeployAndActivation",before.id>>]

Exact module download · Source bundle and reproduction instructions

SwapArrangingBarrier8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapArrangingBarrier8(before,after,objects,afterObjects,a,b,occurrenceId,actualNormalSwapAllowed,
                   checkpointSerial,afterCheckpointSerial,pending,afterPending,events) ==
 /\ before.stage = "Swaps" /\ ~before.complete /\ ~SmallArrangement8(before.targets)
 /\ a \in before.targets \cap DOMAIN objects /\ b \in before.targets \cap DOMAIN objects /\ a # b
 /\ DeployedBarrier8(objects[a]) /\ DeployedBarrier8(objects[b]) /\ actualNormalSwapAllowed
 /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin before.swapEvents
 /\ afterObjects = ExchangeDeployedLocations8(objects,a,b)
 /\ checkpointSerial = afterCheckpointSerial /\ pending = afterPending
 /\ after = [before EXCEPT !.swapEvents = @ \cup {occurrenceId}]
 /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployedBarrier8, ExchangeDeployedLocations8, MovementEvent8, SmallArrangement8

SwapAsideTransit8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapAsideTransit8(incoming,outgoing,successor,objects,transits) ==
 LET ownOrigin == objects[incoming].zone = "SetAside" /\ incoming \in DOMAIN transits
     target == transits[outgoing]
 IN [key \in DOMAIN target |->
      CASE key = "object" -> successor
        [] key = "originZone" -> IF ownOrigin THEN transits[incoming].originZone ELSE objects[incoming].zone
        [] key = "originLocation" -> IF ownOrigin THEN transits[incoming].originLocation ELSE objects[incoming].loc
        [] OTHER -> target[key]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ownOrigin, target

SwapBarrierTraversalPlan8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapBarrierTraversalPlan8(traversal,afterObjects,actualCurrentBarrierSuccessor) ==
 LET barrierCard == afterObjects[actualCurrentBarrierSuccessor]
 IN BarrierChangeTraversalPlan6(traversal,IF traversal.phase = "Encounter" /\ ~barrierCard.deployed THEN "Uninstall" ELSE "Swap",barrierCard.position,barrierCard.targetSite)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: barrierCard, BarrierChangeTraversalPlan6

SwapDeployedBarrierTraversalPlan8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapDeployedBarrierTraversalPlan8(traversal,newPosition,newTargetSite) == BarrierChangeTraversalPlan6(traversal,"Swap",newPosition,newTargetSite)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BarrierChangeTraversalPlan6

SwapDeployedCards8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapDeployedCards8(objects,afterObjects,a,b,actualDestinationChecks,occurrenceId,usedOccurrenceIds,events) ==
 /\ SwapLegal8(objects,a,b,actualDestinationChecks) /\ objects[a].deployed /\ objects[b].deployed
 /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin usedOccurrenceIds
 /\ afterObjects = ExchangeDeployedLocations8(objects,a,b)
 /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExchangeDeployedLocations8, MovementEvent8, SwapLegal8

SwapHostedRetireDue8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapHostedRetireDue8(objects,a,b) ==
 IF objects[a].zone = objects[b].zone \/ ObjectiveAreaObjectSwap8(objects,a,b) THEN {}
 ELSE HostDescendants8(objects,a) \cup HostDescendants8(objects,b)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostDescendants8, ObjectiveAreaObjectSwap8

SwapLegal8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapLegal8(objects,a,b,actualDestinationChecks) ==
 /\ a # b /\ {a,b} \subseteq DOMAIN objects
 /\ objects[a].form = "Card" /\ objects[b].form = "Card"
 /\ DOMAIN actualDestinationChecks = {a,b}
 /\ \A id \in {a,b} :
      LET other == IF id = a THEN b ELSE a
      IN /\ actualDestinationChecks[id].destination = CardLocation8(objects[other])
         /\ actualDestinationChecks[id].gameRulesHold /\ actualDestinationChecks[id].cardAbilitiesHold

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: other, CardLocation8

SwapNoLegalExchange8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapNoLegalExchange8(actualLegalPairs,objects,afterObjects,events) ==
 actualLegalPairs = {} /\ afterObjects = objects /\ events = {}

Exact module download · Source bundle and reproduction instructions

SwapObjectiveFamilies8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapObjectiveFamilies8(objects,afterObjects,a,b,successors,usedIds,actualDestinationChecks,
                    occurrenceId,usedOccurrenceIds,events) ==
 /\ SwapLegal8(objects,a,b,actualDestinationChecks) /\ ObjectiveAreaObjectSwap8(objects,a,b)
 /\ LET familyA == {a} \cup HostDescendants8(objects,a)
        familyB == {b} \cup HostDescendants8(objects,b)
        all == familyA \cup familyB
    IN /\ familyA \cap familyB = {} /\ DOMAIN objects \subseteq usedIds
       /\ FreshSuccessors8(all,successors,usedIds)
       /\ DOMAIN afterObjects = (DOMAIN objects \ all) \cup {successors[id] : id \in all}
       /\ \A id \in DOMAIN objects \ all : afterObjects[id] = objects[id]
       /\ \A id \in all :
            LET root == IF id \in familyA THEN a ELSE b
                other == IF root = a THEN b ELSE a
                row == objects[id]
                location == IF id = root THEN CardLocation8(objects[other])
                            ELSE [CardLocation8(row) EXCEPT !.zone = objects[other].zone,
                                    !.host = successors[row.host],!.loc = <<"Host",successors[row.host]>>]
            IN afterObjects[successors[id]] = [WithCardLocation8(row,location) EXCEPT
                 !.marks = {},!.deployed = FALSE,!.activated = FALSE]
 /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin usedOccurrenceIds
 /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: all, familyA, familyB, location, row, FreshSuccessors8, MovementEvent8, ObjectiveAreaObjectSwap8, SwapLegal8, WithCardLocation8

SwapOtherCards8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapOtherCards8(objects,afterObjects,a,b,successors,usedIds,actualDestinationChecks,actualArrivals,
                actualMovementReceipt,pendingRetire,afterPendingRetire,occurrenceId,usedOccurrenceIds,events) ==
 /\ SwapLegal8(objects,a,b,actualDestinationChecks)
 /\ ~(objects[a].deployed /\ objects[b].deployed) /\ ~ObjectiveAreaObjectSwap8(objects,a,b)
 /\ DOMAIN successors = {a,b} /\ DOMAIN actualArrivals = {a,b}
 /\ Cardinality({successors[a],successors[b]}) = 2 /\ DOMAIN objects \subseteq usedIds
 /\ actualMovementReceipt.complete /\ actualMovementReceipt.sources = {a,b}
 /\ actualMovementReceipt.successors = successors
 /\ ~actualMovementReceipt.deployProcedurePerformed /\ ~actualMovementReceipt.deployCostPaid /\ ~actualMovementReceipt.likeCardsRetireed
 /\ \A id \in {a,b} :
      LET other == IF id = a THEN b ELSE a
          renew == SwapRenewalRequired8(objects[id],objects[other],actualArrivals[id].destinationHidden)
      IN /\ actualArrivals[id].source = id
         /\ IF renew THEN successors[id] \in (Nat \ {0}) \ usedIds ELSE successors[id] = id
         /\ successors[id] \in DOMAIN afterObjects
         /\ SwapTargetPost8(objects[id],objects[other],afterObjects[successors[id]],renew,actualArrivals[id])
 /\ DOMAIN afterObjects = (DOMAIN objects \ {a,b}) \cup {successors[a],successors[b]}
 /\ \A id \in DOMAIN objects \ {a,b} : afterObjects[id] = objects[id]
 /\ afterPendingRetire = pendingRetire \cup SwapHostedRetireDue8(objects,a,b)
 /\ occurrenceId \in Nat \ {0} /\ occurrenceId \notin usedOccurrenceIds
 /\ events = {MovementEvent8(occurrenceId,"Swap",{a,b})}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: other, renew, MovementEvent8, ObjectiveAreaObjectSwap8, SwapHostedRetireDue8, SwapLegal8, SwapTargetPost8

SwapRenewalRequired8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapRenewalRequired8(source,destination,actualDestinationHidden) ==
 source.zone # destination.zone \/ actualDestinationHidden

Exact module download · Source bundle and reproduction instructions

SwapTargetPost8 · operator

reference-profile · input revision 2 · CC0 1.0

SwapTargetPost8(source,destination,result,renew,actualArrival) ==
 /\ actualArrival.complete /\ actualArrival.row = result
 /\ actualArrival.destination = CardLocation8(destination)
 /\ result.form = "Card" /\ result.card = source.card /\ result.side = source.side
 /\ CardLocation8(result) = CardLocation8(destination) /\ result.deployed = destination.deployed
 /\ ActivationCacheValid8(result)
 /\ result.marks = IF renew THEN {} ELSE source.marks
 /\ IF source.zone # destination.zone THEN
      /\ IF actualArrival.faceExceptionAuthorized THEN TRUE
         ELSE CASE destination.zone = "SideADiscard" -> result.face = IF actualArrival.sideBCouldSee THEN "Up" ELSE "Down"
              [] destination.zone = "SideBDiscard" -> result.face = "Up"
              [] ZoneType4(destination.zone) \in {"Deck","Hand"} -> result.face = "Down"
              [] destination.zone \in SetupObjectiveZones -> result.face = "Up"
              [] destination.zone = "Play" -> result.face = IF source.side = "SideA" THEN "Down" ELSE "Up"
              [] destination.zone = "SetAside" -> result.face = destination.face
              [] OTHER -> TRUE
    ELSE TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ZoneType4, ActivationCacheValid8, CardLocation8, SetupObjectiveZones

TopCardCount8 · operator

reference-profile · input revision 2 · CC0 1.0

TopCardCount8(deck,amount) == IF amount < Len(deck) THEN amount ELSE Len(deck)

Exact module download · Source bundle and reproduction instructions

TransferSwapAsideGroups8 · operator

reference-profile · input revision 2 · CC0 1.0

TransferSwapAsideGroups8(objects,afterObjects,transits,afterTransits,a,b,successors) ==
 /\ DOMAIN successors = {a,b} /\ SetAsideTrackingValid4(objects,transits)
 /\ {successors[a],successors[b]} \subseteq DOMAIN afterObjects
 /\ LET entering == {id \in {a,b} : afterObjects[successors[id]].zone = "SetAside"}
    IN /\ \A id \in entering : (IF id = a THEN b ELSE a) \in DOMAIN transits
       /\ afterTransits = [id \in (DOMAIN transits \ {a,b}) \cup {successors[s] : s \in entering} |->
            IF id \in {successors[s] : s \in entering} THEN
              LET incoming == CHOOSE s \in entering : successors[s] = id
                  outgoing == IF incoming = a THEN b ELSE a
              IN SwapAsideTransit8(incoming,outgoing,id,objects,transits)
            ELSE transits[id]]
 /\ SetAsideTrackingValid4(afterObjects,afterTransits)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetAsideTrackingValid4, entering, incoming, outgoing, SwapAsideTransit8

TurnSideBFace8 · operator

reference-profile · input revision 2 · CC0 1.0

TurnSideBFace8(objects,afterObjects,object,face,actualCardEffectAuthorizes,events) ==
 /\ object \in DOMAIN objects /\ objects[object].form = "Card" /\ objects[object].side = "SideB"
 /\ objects[object].deployed /\ objects[object].zone = "Play"
 /\ face \in {"Up","Down"} /\ objects[object].face # face /\ actualCardEffectAuthorizes
 /\ afterObjects = [objects EXCEPT ![object].face = face,![object].activated = FALSE]
 /\ events = {[tag |-> IF face = "Down" THEN "TurnFacedown" ELSE "TurnFaceup",object |-> object]}

Exact module download · Source bundle and reproduction instructions

UninstallationOccurred8 · operator

reference-profile · input revision 2 · CC0 1.0

UninstallationOccurred8(beforeCard,afterCard) == beforeCard.deployed /\ ~afterCard.deployed

Exact module download · Source bundle and reproduction instructions

UninstalledEvent8 · operator

reference-profile · input revision 2 · CC0 1.0

UninstalledEvent8(object) == [tag |-> "Uninstalled",object |-> object]

Exact module download · Source bundle and reproduction instructions

VerifyDeployedCard8 · operator

reference-profile · input revision 2 · CC0 1.0

VerifyDeployedCard8(before,after,hasOtherRequirements,actuallyOtherwiseVerified,actualRevealReceipt) ==
 /\ before.complete /\ ~before.verificationDone /\ (before.activationMode = "NoValue" \/ before.activationProcessed)
 /\ DeployRevealRequired8(hasOtherRequirements,actuallyOtherwiseVerified,before.activationMode # "NoValue" /\ ~before.activationPerformed) =>
      actualRevealReceipt.performed /\ actualRevealReceipt.object = before.object /\ actualRevealReceipt.afterDeployment
 /\ after = [before EXCEPT !.verificationDone = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployRevealRequired8

WithCardLocation8 · operator

reference-profile · input revision 2 · CC0 1.0

WithCardLocation8(o,l) ==
 [o EXCEPT !.zone = l.zone,!.loc = l.loc,!.area = l.area,!.targetSite = l.targetSite,
           !.targetSiteKind = l.targetSiteKind,!.position = l.position,!.host = l.host]

Exact module download · Source bundle and reproduction instructions