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

TypeContracts

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.

eligible · operator

reference-profile · input revision 2 · CC0 1.0

eligible == ConsoleCandidates(objects,controllers,active,subtypes,player)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConsoleCandidates

valid · operator

reference-profile · input revision 2 · CC0 1.0

valid == ConsoleActivationHistoryValid(eligible,history)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: eligible, ConsoleActivationHistoryValid

relevant · operator

reference-profile · input revision 2 · CC0 1.0

relevant == SelectSeq(history,LAMBDA id : id \in eligible)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LAMBDA

LAMBDA · operator

reference-profile · input revision 2 · CC0 1.0

LAMBDA id : id \in eligible

Exact module download · Source bundle and reproduction instructions

absent · operator

reference-profile · input revision 2 · CC0 1.0

absent == [exists |-> FALSE,amount |-> 0]

Exact module download · Source bundle and reproduction instructions

applies · operator

reference-profile · input revision 2 · CC0 1.0

applies == c.kind = "Profile" /\ c.front /\ context = "Deckbuilding"

Exact module download · Source bundle and reproduction instructions

ids · operator

reference-profile · input revision 2 · CC0 1.0

ids == ActiveProfileObjects(objects,side,cardData)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActiveProfileObjects

after · operator

reference-profile · input revision 2 · CC0 1.0

after == candidateAfter(trashed)

Exact module download · Source bundle and reproduction instructions

ActiveProfileObjects · operator

reference-profile · input revision 2 · CC0 1.0

ActiveProfileObjects(objects, side, cardData) ==
    {id \in DOMAIN objects :
        objects[id].form = "Card" /\ objects[id].kind = "Profile" /\
        cardData[objects[id].card].side = side /\
        DefaultActive(objects[id],TRUE,cardData)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive

AddBarrierResponseCardBoost · operator

reference-profile · input revision 2 · CC0 1.0

AddBarrierResponseCardBoost(before, after, effectId, boost) ==
    /\ effectId \notin DOMAIN before
    /\ after = [id \in DOMAIN before \cup {effectId} |->
                   IF id = effectId THEN boost ELSE before[id]]

Exact module download · Source bundle and reproduction instructions

AnotherCurrentPlayed · operator

reference-profile · input revision 2 · CC0 1.0

AnotherCurrentPlayed(sourceId, event) ==
    /\ event.tag = "Played" /\ event.object # sourceId
    /\ event.kind \in {"Plan","Action"} /\ "SchemaAtom048" \in event.subtypes

Exact module download · Source bundle and reproduction instructions

BarrierDeployResourceUnitCost · operator

reference-profile · input revision 2 · CC0 1.0

BarrierDeployResourceUnitCost(otherBarrierOrder) ==
    InherentDeployCost([kind |-> "Barrier"],Len(otherBarrierOrder))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InherentDeployCost

BarrierDeployTypeLocation · operator

reference-profile · input revision 2 · CC0 1.0

BarrierDeployTypeLocation(actor, kind, destination) ==
    /\ actor = "SideA" /\ kind = "Barrier"
    /\ destination.zone = "Play" /\ destination.area = "Protecting"
    /\ destination.targetSiteKind \in {"SchemaAtom033","SchemaAtom132"}

Exact module download · Source bundle and reproduction instructions

BarrierDeploymentPost · operator

reference-profile · input revision 2 · CC0 1.0

BarrierDeploymentPost(o) ==
    /\ o.form = "Card" /\ o.kind = "Barrier" /\ o.zone = "Play"
    /\ o.deployed /\ o.face = "Down" /\ ~o.activated

Exact module download · Source bundle and reproduction instructions

BarrierInstructionOwnerKindValid · operator

reference-profile · input revision 2 · CC0 1.0

BarrierInstructionOwnerKindValid(kind, barrierInstructions) == Len(barrierInstructions) = 0 \/ kind = "Barrier"

Exact module download · Source bundle and reproduction instructions

BarrierNormalItemInspectionDeploymentGate · operator

reference-profile · input revision 2 · CC0 1.0

BarrierNormalItemInspectionDeploymentGate(o) ==
    o.form = "Card" /\ o.kind = "Barrier" /\ ~o.deployed

Exact module download · Source bundle and reproduction instructions

BarrierProtectionLayout · operator

reference-profile · input revision 2 · CC0 1.0

BarrierProtectionLayout == [orientation |-> "Horizontal",order |-> "InnermostToOutermost",
                        outermost |-> "FurthestFromTargetSite"]

Exact module download · Source bundle and reproduction instructions

BarrierResponseCardBoost · operator

reference-profile · input revision 2 · CC0 1.0

BarrierResponseCardBoost(targetId, amount, encounterId, hasExplicit, explicitDuration) ==
    [target |-> targetId,amount |-> amount,encounter |-> encounterId,
     hasExplicit |-> hasExplicit,explicit |-> explicitDuration]

Exact module download · Source bundle and reproduction instructions

BarrierResponseCardBoostCheckpointStep · operator

reference-profile · input revision 2 · CC0 1.0

BarrierResponseCardBoostCheckpointStep(before, after, liveEncounters, durationAlive(_), stage) ==
    /\ stage = "ProcedureCode88eda145024f"
    /\ after = BarrierResponseCardBoostsAfterCheckpoint(before,liveEncounters,durationAlive)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BarrierResponseCardBoostsAfterCheckpoint

BarrierResponseCardBoostTotal · operator

reference-profile · input revision 2 · CC0 1.0

BarrierResponseCardBoostTotal(boosts, targetId, liveObjectIds) ==
    IF targetId \notin liveObjectIds THEN 0
    ELSE SumMap([id \in DOMAIN boosts |->
        IF boosts[id].target = targetId THEN boosts[id].amount ELSE 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

BarrierResponseCardBoostUnexpired · operator

reference-profile · input revision 2 · CC0 1.0

BarrierResponseCardBoostUnexpired(boost, liveEncounters, durationAlive(_)) ==
    (boost.encounter # 0 /\ boost.encounter \in liveEncounters) \/
    (boost.hasExplicit /\ durationAlive(boost.explicit))

Exact module download · Source bundle and reproduction instructions

BarrierResponseCardBoostsAfterCheckpoint · operator

reference-profile · input revision 2 · CC0 1.0

BarrierResponseCardBoostsAfterCheckpoint(before, liveEncounters, durationAlive(_)) ==
    [id \in {e \in DOMAIN before : BarrierResponseCardBoostUnexpired(before[e],liveEncounters,durationAlive)}
     |-> before[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BarrierResponseCardBoostUnexpired

BarrierResponseCardTechnique · operator

reference-profile · input revision 2 · CC0 1.0

BarrierResponseCardTechnique(o, subtypes) ==
    o.form = "Card" /\ o.kind = "Technique" /\ "SchemaAtom086" \in subtypes

Exact module download · Source bundle and reproduction instructions

BarrierTermRefersToType · operator

reference-profile · input revision 2 · CC0 1.0

BarrierTermRefersToType(term) == term \in {"barrierCard","piece of barrier"}

Exact module download · Source bundle and reproduction instructions

BarrierTraversalStrengthScope · operator

reference-profile · input revision 2 · CC0 1.0

BarrierTraversalStrengthScope(traversalId, encounterId, checkpointSerial) ==
    IF traversalId # 0 THEN [scope |-> "SchemaAtom138",token |-> traversalId]
    ELSE IF encounterId # 0 THEN [scope |-> "Encounter",token |-> encounterId]
    ELSE [scope |-> "Checkpoint",token |-> checkpointSerial+1]

Exact module download · Source bundle and reproduction instructions

CentralRootCardTypeValid · operator

reference-profile · input revision 2 · CC0 1.0

CentralRootCardTypeValid(o) ==
    (o.form = "Card" /\ o.deployed /\ o.zone = "Play" /\
     o.area = "Root" /\ o.targetSiteKind = "SchemaAtom033") => o.kind = "Attachment"

Exact module download · Source bundle and reproduction instructions

ConditionCounterPost · operator

reference-profile · input revision 2 · CC0 1.0

ConditionCounterPost(sourceCard, o) ==
    /\ o.card = sourceCard /\ o.form = "Counter" /\ o.kind = "SchemaAtom043"
    /\ o.deployed /\ o.zone = "Play"

Exact module download · Source bundle and reproduction instructions

ConditionEventSelfDeployGate · operator

reference-profile · input revision 2 · CC0 1.0

ConditionEventSelfDeployGate(o, route, ownAbilityAuthorized) ==
    /\ o.form = "Card" /\ o.kind = "Action" /\ "SchemaAtom043" \in o.subtypes
    /\ route = "OwnConversion" /\ ownAbilityAuthorized

Exact module download · Source bundle and reproduction instructions

ConditionOperationSelfDeployGate · operator

reference-profile · input revision 2 · CC0 1.0

ConditionOperationSelfDeployGate(o, route, ownAbilityAuthorized) ==
    /\ o.form = "Card" /\ o.kind = "Plan" /\ "SchemaAtom043" \in o.subtypes
    /\ route = "OwnConversion" /\ ownAbilityAuthorized

Exact module download · Source bundle and reproduction instructions

ConsoleActivationHistoryValid · operator

reference-profile · input revision 2 · CC0 1.0

ConsoleActivationHistoryValid(eligible, history) == eligible \subseteq SetupRange(history)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange

ConsoleCandidates · operator

reference-profile · input revision 2 · CC0 1.0

ConsoleCandidates(objects, controllers, active, subtypes, player) ==
    {id \in DOMAIN objects :
        objects[id].form = "Card" /\ objects[id].kind = "Equipment" /\
        objects[id].deployed /\ controllers[id] = player /\ active[id] /\
        "SchemaAtom045" \in subtypes[id]}

Exact module download · Source bundle and reproduction instructions

ConsoleCorrection · operator

reference-profile · input revision 2 · CC0 1.0

ConsoleCorrection(objects, controllers, active, subtypes, history, player) ==
    LET eligible == ConsoleCandidates(objects,controllers,active,subtypes,player)
        valid == ConsoleActivationHistoryValid(eligible,history)
    IN [valid |-> valid,preventable |-> FALSE,checkpointStage |-> "ProcedureCodefe50c31480ea",
        trash |-> IF valid THEN eligible \ LatestActiveConsole(eligible,history) ELSE {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: eligible, valid, LatestActiveConsole

ConsolePrintedDeclarationValid · operator

reference-profile · input revision 2 · CC0 1.0

ConsolePrintedDeclarationValid(c) ==
    "SchemaAtom045" \in c.printedSubtypes => c.printedConsoleLimit = 1

Exact module download · Source bundle and reproduction instructions

DeployedRootRegions · operator

reference-profile · input revision 2 · CC0 1.0

DeployedRootRegions(objects, targetSite) ==
    {id \in DOMAIN objects :
        objects[id].form = "Card" /\ objects[id].kind # "Barrier" /\
        "SchemaAtom130" \in objects[id].subtypes /\ objects[id].deployed /\
        objects[id].zone = "Play" /\ objects[id].area = "Root" /\ objects[id].targetSite = targetSite}

Exact module download · Source bundle and reproduction instructions

DeployedTechniqueIds · operator

reference-profile · input revision 2 · CC0 1.0

DeployedTechniqueIds(objects, effectiveTypes) ==
    {id \in DOMAIN objects :
        objects[id].form = "Card" /\ objects[id].deployed /\ "Technique" \in effectiveTypes[id]}

Exact module download · Source bundle and reproduction instructions

DeployingRootRegions · operator

reference-profile · input revision 2 · CC0 1.0

DeployingRootRegions(deploying, targetSite) ==
    {id \in DOMAIN deploying :
        deploying[id].form = "Card" /\ deploying[id].kind # "Barrier" /\
        "SchemaAtom130" \in deploying[id].subtypes /\
        deploying[id].destination.zone = "Play" /\ deploying[id].destination.area = "Root" /\
        deploying[id].destination.targetSite = targetSite}

Exact module download · Source bundle and reproduction instructions

EquipmentTermRefersToType · operator

reference-profile · input revision 2 · CC0 1.0

EquipmentTermRefersToType(term) == term \in {"equipment","piece of equipment"}

Exact module download · Source bundle and reproduction instructions

EventCurrentExpires · operator

reference-profile · input revision 2 · CC0 1.0

EventCurrentExpires(sourceId, event) ==
    AnotherCurrentPlayed(sourceId,event) \/ event.tag = "ObjectivePlacementd"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AnotherCurrentPlayed

EventPlayTypeAllowed · operator

reference-profile · input revision 2 · CC0 1.0

EventPlayTypeAllowed(actor, kind) == actor = "SideB" /\ kind = "Action"

Exact module download · Source bundle and reproduction instructions

EventRetentionAfterEvent · operator

reference-profile · input revision 2 · CC0 1.0

EventRetentionAfterEvent(before, sourceId, event, objects) ==
    ExpirePlayedRetention([before EXCEPT !.inPlay = PlayedSourceInPlay(sourceId,objects)],
        before.mode = "SchemaAtom048" /\ EventCurrentExpires(sourceId,event),
        PlayedRetireSourceApplicable(sourceId,objects))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EventCurrentExpires, ExpirePlayedRetention, PlayedRetireSourceApplicable, PlayedSourceInPlay

ExampleItemARegionDeclaration · operator

reference-profile · input revision 2 · CC0 1.0

ExampleItemARegionDeclaration(c) ==
    /\ c.kind = "Facility" /\ CanonicalName(c) = <<"Example Item A">>
    /\ "SchemaAtom130" \in c.printedSubtypes /\ c.printedRegionLimit = 1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanonicalName

ExampleItemBConditionDeclaration · operator

reference-profile · input revision 2 · CC0 1.0

ExampleItemBConditionDeclaration(c) ==
    /\ c.kind = "Action" /\ CanonicalName(c) = <<"Example Item B">>
    /\ "SchemaAtom043" \in c.printedSubtypes

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanonicalName

ExpirePlayedRetention · operator

reference-profile · input revision 2 · CC0 1.0

ExpirePlayedRetention(before, shouldExpire, sourceApplicable) ==
    IF before.live /\ shouldExpire
    THEN [before EXCEPT !.live = FALSE,!.pendingRetire = sourceApplicable] ELSE before

Exact module download · Source bundle and reproduction instructions

FacilityActivationStep · operator

reference-profile · input revision 2 · CC0 1.0

FacilityActivationStep(before, after, actor, paidWindow, costsComplete, activationAllowedByRules) ==
    /\ actor = "SideA" /\ before.form = "Card" /\ before.kind = "Facility"
    /\ before.deployed /\ before.zone = "Play"
    /\ before.face = "Down" /\ ~before.activated
    /\ paidWindow /\ costsComplete /\ activationAllowedByRules
    /\ after = [before EXCEPT !.face = "Up",!.activated = TRUE]

Exact module download · Source bundle and reproduction instructions

FacilityDeployTypeLocation · operator

reference-profile · input revision 2 · CC0 1.0

FacilityDeployTypeLocation(actor, kind, destination) ==
    /\ actor = "SideA" /\ kind = "Facility"
    /\ destination.zone = "Play" /\ destination.area = "Root"
    /\ destination.targetSiteKind = "SchemaAtom132"

Exact module download · Source bundle and reproduction instructions

FacilityDeploymentPost · operator

reference-profile · input revision 2 · CC0 1.0

FacilityDeploymentPost(o) ==
    /\ o.form = "Card" /\ o.kind = "Facility" /\ o.zone = "Play"
    /\ o.deployed /\ o.face = "Down" /\ ~o.activated

Exact module download · Source bundle and reproduction instructions

InterfaceAbilityLocalGate · operator

reference-profile · input revision 2 · CC0 1.0

InterfaceAbilityLocalGate(actor, source, sourceSubtypes, ability, context,
                          sourceStrength, barrierStrength, barrierSubtypes, targets) ==
    /\ actor = "SideB" /\ ability.isInterface /\ ability.presentActive
    /\ context.encounterActive /\ context.step = "ProcedureCode8b3260c0010f"
    /\ context.barrierForm = "Card" /\ context.barrierKind = "Barrier"
    /\ InterfaceTargetsAllowed(targets,context.barrierId,context.barrierInstructions)
    /\ InterfaceSubtypeMatches(ability.restriction,barrierSubtypes)
    /\ IF BarrierResponseCardTechnique(source,sourceSubtypes)
       THEN sourceStrength.exists /\ barrierStrength.exists /\
            StrengthThresholdMet(sourceStrength.amount,barrierStrength.amount)
       ELSE TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StrengthThresholdMet, BarrierResponseCardTechnique, InterfaceSubtypeMatches, InterfaceTargetsAllowed

InterfaceFlagValid · operator

reference-profile · input revision 2 · CC0 1.0

InterfaceFlagValid(ability) ==
    /\ ability.isInterface \in BOOLEAN
    /\ ability.interfaceFlag = IF ability.isInterface THEN "Interface" ELSE "NoValue"

Exact module download · Source bundle and reproduction instructions

InterfaceSubtypeMatches · operator

reference-profile · input revision 2 · CC0 1.0

InterfaceSubtypeMatches(restriction, barrierSubtypes) ==
    ~restriction.present \/ restriction.name \in barrierSubtypes

Exact module download · Source bundle and reproduction instructions

InterfaceTargetsAllowed · operator

reference-profile · input revision 2 · CC0 1.0

InterfaceTargetsAllowed(targets, barrierId, barrierInstructionIds) ==
    \A t \in targets :
        (t.kind = "Card" /\ t.object = barrierId) \/
        (t.kind = "BarrierInstruction" /\ t.object = barrierId /\ t.barrierInstruction \in barrierInstructionIds)

Exact module download · Source bundle and reproduction instructions

ItemInspectionRetireCostOpportunity · operator

reference-profile · input revision 2 · CC0 1.0

ItemInspectionRetireCostOpportunity(actor, o, accessing, effectiveRetirePart) ==
    /\ actor = "SideB" /\ o.form = "Card" /\ accessing
    /\ o.zone # "SideADiscard"
    /\ effectiveRetirePart.exists

Exact module download · Source bundle and reproduction instructions

LatestActiveConsole · operator

reference-profile · input revision 2 · CC0 1.0

LatestActiveConsole(eligible, history) ==
    LET relevant == SelectSeq(history,LAMBDA id : id \in eligible)
    IN IF eligible = {} THEN {} ELSE {relevant[Len(relevant)]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: relevant

ObjectiveAbilityActive · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveAbilityActive(o, abilityPresent, gameStarted, cardData,
                    printedFaceupDeploy, sideBObjectiveAreaTextActive, objectiveCompletionClaimObjectiveException) ==
    /\ o.form = "Card" /\ o.kind = "Objective"
    /\ TextAbilityActive(abilityPresent,ObjectiveCardActive(o,gameStarted,cardData),
          (o.deployed /\ o.zone = "Play" /\ printedFaceupDeploy) \/
          (o.zone = "SideBObjectiveCompletion" /\ sideBObjectiveAreaTextActive) \/ objectiveCompletionClaimObjectiveException)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TextAbilityActive, ObjectiveCardActive

ObjectiveActivationStatus · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveActivationStatus(o) ==
    IF o.form = "Card" /\ o.kind = "Objective" /\ o.deployed /\ o.face = "Down"
    THEN "Dormant" ELSE "Neither"

Exact module download · Source bundle and reproduction instructions

ObjectiveCanActivation · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveCanActivation(o) == FALSE

Exact module download · Source bundle and reproduction instructions

ObjectiveCardActive · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveCardActive(o, gameStarted, cardData) ==
    o.form = "Card" /\ o.kind = "Objective" /\ DefaultActive(o,gameStarted,cardData)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive

ObjectiveCharacteristicSlotsValid · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveCharacteristicSlotsValid(c) ==
    ProgressMetadataValid(c) /\ ObjectivePointsMetadataValid(c)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectivePointsMetadataValid, ProgressMetadataValid

ObjectiveDeployTypeLocation · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveDeployTypeLocation(actor, kind, destination) ==
    /\ actor = "SideA" /\ kind = "Objective"
    /\ destination.zone = "Play" /\ destination.area = "Root"
    /\ destination.targetSiteKind = "SchemaAtom132"

Exact module download · Source bundle and reproduction instructions

ObjectiveFacilityRootLimit · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveFacilityRootLimit(objects, targetSite) ==
    Cardinality(ObjectiveFacilityRootOccupants(objects,targetSite)) <= 1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveFacilityRootOccupants

ObjectiveFacilityRootOccupants · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveFacilityRootOccupants(objects, targetSite) ==
    {id \in DOMAIN objects :
        objects[id].form = "Card" /\ objects[id].deployed /\
        objects[id].zone = "Play" /\ objects[id].area = "Root" /\
        objects[id].targetSite = targetSite /\ objects[id].kind \in {"Objective","Facility"}}

Exact module download · Source bundle and reproduction instructions

ObjectivePointsInObjectiveArea · operator

reference-profile · input revision 2 · CC0 1.0

ObjectivePointsInObjectiveArea(o, area, effectivePoints) ==
    IF area \in {"SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ o.zone = area /\
       o.form = "Card" /\ o.kind = "Objective" THEN effectivePoints ELSE 0

Exact module download · Source bundle and reproduction instructions

ObjectiveProgressEligible · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveProgressEligible(o) == o.form = "Card" /\ o.kind = "Objective" /\ o.deployed

Exact module download · Source bundle and reproduction instructions

OperationCurrentExpires · operator

reference-profile · input revision 2 · CC0 1.0

OperationCurrentExpires(sourceId, event) ==
    AnotherCurrentPlayed(sourceId,event) \/ event.tag = "ObjectiveClaimedObjective"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AnotherCurrentPlayed

OperationPlayTypeAllowed · operator

reference-profile · input revision 2 · CC0 1.0

OperationPlayTypeAllowed(actor, kind) == actor = "SideA" /\ kind = "Plan"

Exact module download · Source bundle and reproduction instructions

OperationRetentionAfterEvent · operator

reference-profile · input revision 2 · CC0 1.0

OperationRetentionAfterEvent(before, sourceId, event, objects) ==
    ExpirePlayedRetention([before EXCEPT !.inPlay = PlayedSourceInPlay(sourceId,objects)],
        CASE before.mode = "SchemaAtom048" -> OperationCurrentExpires(sourceId,event)
          [] before.mode = "SchemaAtom099" -> Specimen0133Expires(before.expiresSideATurn,event)
          [] OTHER -> FALSE,PlayedRetireSourceApplicable(sourceId,objects))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExpirePlayedRetention, OperationCurrentExpires, PlayedRetireSourceApplicable, PlayedSourceInPlay, Specimen0133Expires

PlayedCardActive · operator

reference-profile · input revision 2 · CC0 1.0

PlayedCardActive(o, activationReached) ==
    /\ o.form = "Card" /\ o.kind \in {"Plan","Action"}
    /\ o.zone = "Play" /\ o.face = "Up" /\ activationReached

Exact module download · Source bundle and reproduction instructions

PlayedResolutionRetireDue · operator

reference-profile · input revision 2 · CC0 1.0

PlayedResolutionRetireDue(o, abilitiesFullyResolved, holdLive, nestedRemovalPending) ==
    /\ PlayedSourceRetireEligible(o) /\ abilitiesFullyResolved
    /\ ~holdLive /\ ~nestedRemovalPending

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayedSourceRetireEligible

PlayedRetention · operator

reference-profile · input revision 2 · CC0 1.0

PlayedRetention(mode, sideATurn) ==
    [mode |-> mode,live |-> mode # "NoValue",inPlay |-> TRUE,
     pendingRetire |-> FALSE,expiresSideATurn |-> sideATurn+1]

Exact module download · Source bundle and reproduction instructions

PlayedRetireSourceApplicable · operator

reference-profile · input revision 2 · CC0 1.0

PlayedRetireSourceApplicable(sourceId, objects) ==
    IF sourceId \in DOMAIN objects THEN PlayedSourceRetireEligible(objects[sourceId]) ELSE FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayedSourceRetireEligible

PlayedSourceInPlay · operator

reference-profile · input revision 2 · CC0 1.0

PlayedSourceInPlay(sourceId, objects) ==
    IF sourceId \in DOMAIN objects THEN objects[sourceId].zone = "Play" ELSE FALSE

Exact module download · Source bundle and reproduction instructions

PlayedSourceRetireEligible · operator

reference-profile · input revision 2 · CC0 1.0

PlayedSourceRetireEligible(o) ==
    /\ o.form = "Card" /\ o.kind \in {"Plan","Action"}
    /\ o.zone = "Play" /\ o.host = 0

Exact module download · Source bundle and reproduction instructions

PlayedTypeNotDeployed · operator

reference-profile · input revision 2 · CC0 1.0

PlayedTypeNotDeployed(o) ==
    (o.form = "Card" /\ o.kind \in {"Plan","Action"}) => ~o.deployed

Exact module download · Source bundle and reproduction instructions

PrintedBarrierResponseCardInterfacesValid · operator

reference-profile · input revision 2 · CC0 1.0

PrintedBarrierResponseCardInterfacesValid(c, printedAbilities) ==
    c.printedBarrierResponseCard => \E i \in 1..Len(printedAbilities) : printedAbilities[i].isInterface

Exact module download · Source bundle and reproduction instructions

ProfileDeckValues · operator

reference-profile · input revision 2 · CC0 1.0

ProfileDeckValues(c, context, resolvedMinX, resolvedLimitX) ==
    LET applies == c.kind = "Profile" /\ c.front /\ context = "Deckbuilding"
        absent == [exists |-> FALSE,amount |-> 0]
    IN [applicable |-> applies,
        minimum |-> IF applies THEN MinimumDeckPart(c,resolvedMinX) ELSE absent,
        importBudget |-> IF applies THEN ImportCostLimitPart(c,resolvedLimitX) ELSE absent]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ImportCostLimitPart, MinimumDeckPart, absent, applies

ProfileFaceActive · operator

reference-profile · input revision 2 · CC0 1.0

ProfileFaceActive(o, faceIsFront, gameStarted, cardData) ==
    /\ o.kind = "Profile" /\ o.front = faceIsFront
    /\ DefaultActive(o,gameStarted,cardData)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive

ProfileFaceValuesValid · operator

reference-profile · input revision 2 · CC0 1.0

ProfileFaceValuesValid(c) ==
    /\ MinimumDeckMetadataValid(c) /\ ImportCostLimitMetadataValid(c)
    /\ BaseLinkMetadataValid(c)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BaseLinkMetadataValid, ImportCostLimitMetadataValid, MinimumDeckMetadataValid

ProfileObjectValid · operator

reference-profile · input revision 2 · CC0 1.0

ProfileObjectValid(o) ==
    (o.form = "Card" /\ o.kind = "Profile") => ~o.deployed

Exact module download · Source bundle and reproduction instructions

ProfileTargetSiteSpecimen0139 · operator

reference-profile · input revision 2 · CC0 1.0

ProfileTargetSiteSpecimen0139(o, cardData) ==
    IF o.form = "Card" /\ o.kind = "Profile" /\ o.zone = "Play" /\
       cardData[o.card].side = "SideA" THEN "SchemaAtom082" ELSE "NoValue"

Exact module download · Source bundle and reproduction instructions

ProtectingCardTypeValid · operator

reference-profile · input revision 2 · CC0 1.0

ProtectingCardTypeValid(o) ==
    (o.form = "Card" /\ o.deployed /\ o.area = "Protecting") => o.kind = "Barrier"

Exact module download · Source bundle and reproduction instructions

RegionMoveSwapGate · operator

reference-profile · input revision 2 · CC0 1.0

RegionMoveSwapGate(afterObjects, afterDeploying, targetSiteIds) ==
    \A targetSite \in targetSiteIds : RegionRootLimit(afterObjects,afterDeploying,targetSite)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RegionRootLimit

RegionPrintedDeclarationValid · operator

reference-profile · input revision 2 · CC0 1.0

RegionPrintedDeclarationValid(c) ==
    "SchemaAtom130" \in c.printedSubtypes => c.printedRegionLimit = 1

Exact module download · Source bundle and reproduction instructions

RegionReplacementRetireSatisfied · operator

reference-profile · input revision 2 · CC0 1.0

RegionReplacementRetireSatisfied(required, actuallyRetireed) == required \subseteq actuallyRetireed

Exact module download · Source bundle and reproduction instructions

RegionRequiredOldRetire · operator

reference-profile · input revision 2 · CC0 1.0

RegionRequiredOldRetire(objects, newId, newCard, destination) ==
    IF newCard.form = "Card" /\ newCard.kind # "Barrier" /\ "SchemaAtom130" \in newCard.subtypes /\
       destination.zone = "Play" /\ destination.area = "Root"
    THEN DeployedRootRegions(objects,destination.targetSite) \ {newId} ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployedRootRegions

RegionRootLimit · operator

reference-profile · input revision 2 · CC0 1.0

RegionRootLimit(objects, deploying, targetSite) ==
    Cardinality(DeployedRootRegions(objects,targetSite) \cup DeployingRootRegions(deploying,targetSite)) <= 1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployedRootRegions, DeployingRootRegions

ResourceRetireBasicActionLocalGate · operator

reference-profile · input revision 2 · CC0 1.0

ResourceRetireBasicActionLocalGate(actor, target, effectiveTypes, context,
                                 effectiveExposureMarkerCount, costsComplete, actionAllowedByRules) ==
    /\ actor = "SideA" /\ context.turn = "SideA" /\ context.phase = "NeutralValue00001"
    /\ context.basicActionAvailable /\ SideBHasExposureMarkersForResourceAction(effectiveExposureMarkerCount)
    /\ target.form = "Card" /\ target.deployed /\ target.zone = "Play"
    /\ "Support" \in effectiveTypes
    /\ costsComplete /\ actionAllowedByRules

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBHasExposureMarkersForResourceAction

ResourceRetireBasicCost · operator

reference-profile · input revision 2 · CC0 1.0

ResourceRetireBasicCost == [actionPoints |-> 1,resourceUnits |-> 2]

Exact module download · Source bundle and reproduction instructions

RetentionCheckpointStep · operator

reference-profile · input revision 2 · CC0 1.0

RetentionCheckpointStep(before, after, sourceId, objects, checkpointStage) ==
    /\ before.pendingRetire /\ checkpointStage = "ProcedureCode88eda145024f"
    /\ after = [before EXCEPT !.live = FALSE,!.pendingRetire = FALSE,
          !.inPlay = IF PlayedRetireSourceApplicable(sourceId,objects) THEN FALSE
                     ELSE PlayedSourceInPlay(sourceId,objects)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayedRetireSourceApplicable, PlayedSourceInPlay

RetentionReactionGate · operator

reference-profile · input revision 2 · CC0 1.0

RetentionReactionGate(retentions, objects) ==
    \A id \in DOMAIN retentions :
        ~retentions[id].pendingRetire \/ ~PlayedRetireSourceApplicable(id,objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayedRetireSourceApplicable

SideAHasInherentDeployCost · operator

reference-profile · input revision 2 · CC0 1.0

SideAHasInherentDeployCost(kind) == kind = "Barrier"

Exact module download · Source bundle and reproduction instructions

SideAHasPlayCost · operator

reference-profile · input revision 2 · CC0 1.0

SideAHasPlayCost(kind) == kind = "Plan"

Exact module download · Source bundle and reproduction instructions

SideBHasExposureMarkersForResourceAction · operator

reference-profile · input revision 2 · CC0 1.0

SideBHasExposureMarkersForResourceAction(effectiveExposureMarkerCount) ==
    effectiveExposureMarkerCount \in Nat /\ effectiveExposureMarkerCount > 0

Exact module download · Source bundle and reproduction instructions

SideBHasPlayCost · operator

reference-profile · input revision 2 · CC0 1.0

SideBHasPlayCost(kind) == kind = "Action"

Exact module download · Source bundle and reproduction instructions

SideBPaidDeployPost · operator

reference-profile · input revision 2 · CC0 1.0

SideBPaidDeployPost(o, actor, expectedKind, costsComplete, deployAllowedByRules) ==
    /\ actor = "SideB" /\ expectedKind \in {"Equipment","Technique","Support"}
    /\ o.form = "Card" /\ o.kind = expectedKind /\ o.zone = "Play"
    /\ o.deployed /\ o.face = "Up" /\ ~o.activated
    /\ costsComplete /\ deployAllowedByRules

Exact module download · Source bundle and reproduction instructions

Specimen0133Expires · operator

reference-profile · input revision 2 · CC0 1.0

Specimen0133Expires(expiresSideATurn, event) ==
    event.tag = "TurnBegins" /\ event.actor = "SideA" /\ event.sideATurn >= expiresSideATurn

Exact module download · Source bundle and reproduction instructions

StandardBarrierActivationStep · operator

reference-profile · input revision 2 · CC0 1.0

StandardBarrierActivationStep(before, after, objectId, actor, context, costsComplete, activationAllowedByRules) ==
    /\ actor = "SideA" /\ before.form = "Card" /\ before.kind = "Barrier"
    /\ before.deployed /\ before.zone = "Play" /\ before.face = "Down" /\ ~before.activated
    /\ context.inTraversal /\ context.window = "ProcedureCode3a6daf593ad4" /\ context.approachedObject = objectId
    /\ costsComplete /\ activationAllowedByRules
    /\ after = [before EXCEPT !.face = "Up",!.activated = TRUE]

Exact module download · Source bundle and reproduction instructions

StandardBarrierInsertion · operator

reference-profile · input revision 2 · CC0 1.0

StandardBarrierInsertion(beforeOrder, afterOrder, newId) ==
    /\ newId \notin SetupRange(beforeOrder)
    /\ afterOrder = Append(beforeOrder,newId)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange

StandardEquipmentCountAllowed · operator

reference-profile · input revision 2 · CC0 1.0

StandardEquipmentCountAllowed(count) == count \in Nat

Exact module download · Source bundle and reproduction instructions

StandardResourceCountAllowed · operator

reference-profile · input revision 2 · CC0 1.0

StandardResourceCountAllowed(count) == count \in Nat

Exact module download · Source bundle and reproduction instructions

StandardUpgradeCountAllowed · operator

reference-profile · input revision 2 · CC0 1.0

StandardUpgradeCountAllowed(count) == count \in Nat

Exact module download · Source bundle and reproduction instructions

StartingProfilesValid · operator

reference-profile · input revision 2 · CC0 1.0

StartingProfilesValid(objects, cardData) ==
    /\ \A id \in DOMAIN objects : ProfileObjectValid(objects[id])
    /\ \A side \in SetupPlayers :
        LET ids == ActiveProfileObjects(objects,side,cardData)
        IN /\ Cardinality(ids) = 1
           /\ \A id \in ids :
                objects[id].front /\ cardData[objects[id].card].owner = side

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, ids, ProfileObjectValid

StrengthScopeAlive · operator

reference-profile · input revision 2 · CC0 1.0

StrengthScopeAlive(binding, liveTraversalIds, liveEncounterIds, checkpointSerial) ==
    CASE binding.scope = "SchemaAtom138" -> binding.token \in liveTraversalIds
      [] binding.scope = "Encounter" -> binding.token \in liveEncounterIds
      [] binding.scope = "Checkpoint" -> checkpointSerial < binding.token

Exact module download · Source bundle and reproduction instructions

TechniqueCapacityArithmeticFits · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityArithmeticFits(demand, limit) == SumMap(demand) <= limit

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

TechniqueCapacityCandidateLegal · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityCandidateLegal(candidate) ==
    /\ DOMAIN candidate.demand = candidate.techniqueIds
    /\ TechniqueCapacityLegal(candidate.demand,candidate.limit,candidate.allocationFits)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TechniqueCapacityLegal

TechniqueCapacityCheckpointChoice · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityCheckpointChoice(deployedIds, trashed, candidateAfter(_)) ==
    /\ ~TechniqueCapacityCandidateLegal(candidateAfter({}))
    /\ trashed \subseteq deployedIds /\ trashed # {}
    /\ TechniqueCapacityCandidateLegal(candidateAfter(trashed))
    /\ \A id \in trashed : ~TechniqueCapacityCandidateLegal(candidateAfter(trashed \ {id}))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TechniqueCapacityCandidateLegal

TechniqueCapacityDemand · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityDemand(objects, effectiveTypes, effectiveCapacity) ==
    [id \in DeployedTechniqueIds(objects,effectiveTypes) |->
        IF effectiveCapacity[id].exists THEN effectiveCapacity[id].amount ELSE 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployedTechniqueIds

TechniqueCapacityLegal · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityLegal(demand, limit, allocationFits) ==
    TechniqueCapacityArithmeticFits(demand,limit) /\ allocationFits

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TechniqueCapacityArithmeticFits

TechniqueCapacityRepairTiming · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityRepairTiming(cause) ==
    IF cause = "DeployingTechnique" THEN "DuringDeploy" ELSE "NextCheckpoint10.3.1e"

Exact module download · Source bundle and reproduction instructions

TechniqueDeployCapacityChoice · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueDeployCapacityChoice(existingIds, newId, trashed, candidateAfter(_)) ==
    /\ newId \notin existingIds /\ trashed \subseteq existingIds
    /\ LET after == candidateAfter(trashed)
       IN /\ newId \in after.techniqueIds /\ trashed \intersect after.techniqueIds = {}
          /\ TechniqueCapacityCandidateLegal(after)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, TechniqueCapacityCandidateLegal

TechniqueResourceUnitAndCapacity · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueResourceUnitAndCapacity(c, paymentX, increases, reductions, resourceUnitWaived, capacityX) ==
    [resourceUnitCost |-> IF resourceUnitWaived THEN 0
                    ELSE ModifiedCost(CardResourceUnitCost(c,"Deploy",0,TRUE,paymentX).amount,
                                      increases,reductions),
     capacity |-> CapacityCostPart(c,capacityX)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ModifiedCost, CapacityCostPart, CardResourceUnitCost

TechniqueStrengthMetadataValid · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueStrengthMetadataValid(c) ==
    /\ c.kind = "Technique" /\ StrengthMetadataValid(c) /\ SubtypeFlagsConsistent(c)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StrengthMetadataValid, SubtypeFlagsConsistent

UpgradeActivationStep · operator

reference-profile · input revision 2 · CC0 1.0

UpgradeActivationStep(before, after, actor, paidWindow, costsComplete, activationAllowedByRules) ==
    /\ actor = "SideA" /\ before.form = "Card" /\ before.kind = "Attachment"
    /\ before.deployed /\ before.zone = "Play" /\ before.face = "Down" /\ ~before.activated
    /\ paidWindow /\ costsComplete /\ activationAllowedByRules
    /\ after = [before EXCEPT !.face = "Up",!.activated = TRUE]

Exact module download · Source bundle and reproduction instructions

UpgradeDeployTypeLocation · operator

reference-profile · input revision 2 · CC0 1.0

UpgradeDeployTypeLocation(actor, kind, destination) ==
    /\ actor = "SideA" /\ kind = "Attachment" /\ destination.zone = "Play"
    /\ destination.area = "Root" /\ destination.targetSiteKind \in {"SchemaAtom033","SchemaAtom132"}

Exact module download · Source bundle and reproduction instructions

UpgradeDeploymentPost · operator

reference-profile · input revision 2 · CC0 1.0

UpgradeDeploymentPost(o) ==
    /\ o.form = "Card" /\ o.kind = "Attachment" /\ o.zone = "Play"
    /\ o.deployed /\ o.face = "Down" /\ ~o.activated

Exact module download · Source bundle and reproduction instructions