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

TurnContracts

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.

next · operator

reference-profile · input revision 2 · CC0 1.0

next == SideANextStep5(before.step,before.decision)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideANextStep5

kind · operator

reference-profile · input revision 2 · CC0 1.0

kind == CASE step = "ProcedureCode3557d050aec7" -> "AllotActionPoints"
               [] step \in {"ProcedureCode36065334a34a","ProcedureCoded6fbcb09dd4f","ProcedureCode438597bede05"} -> "PaidWindow"
               [] step = "ProcedureCode599a3c2d7264" -> "Refill"
               [] step = "ProcedureCode824821d07be7" -> "TurnBegins"
               [] step = "ProcedureCode59141ee1a13b" -> "MandatoryDraw"
               [] step = "ProcedureCode0e20572a4bab" -> "NeutralValue00001"
               [] step = "ProcedureCodeb6035cb98279" -> "Loop"
               [] step = "ProcedureCode042aa78ff256" -> "ActionPhaseEnds"
               [] step = "ProcedureCode93af477f9d95" -> "DiscardStep"
               [] step = "ProcedureCode4e363e6bb7cf" -> "LoseUnspentActionPoints"
               [] step = "ProcedureCodea107cee5c079" -> "TurnEnds"
               [] step = "ProcedureCode72a65676fb11" -> "Handoff" [] OTHER -> "PhaseComplete"

Exact module download · Source bundle and reproduction instructions

phase · operator

reference-profile · input revision 2 · CC0 1.0

phase == CASE step \in SetupRange(SubSeq(SideASteps5,1,6)) -> "Draw"
                [] step \in SetupRange(SubSeq(SideASteps5,7,11)) -> "NeutralValue00001"
                [] OTHER -> "Discard"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange, SideASteps5

next · operator

reference-profile · input revision 2 · CC0 1.0

next == SideBNextStep5(before.step,before.decision)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBNextStep5

kind · operator

reference-profile · input revision 2 · CC0 1.0

kind == CASE step = "ProcedureCode81ed7b3ac00d" -> "AllotActionPoints"
               [] step \in {"ProcedureCodef53fc09e15ad","ProcedureCode484be3e50aa9","ProcedureCode13c5f7239eb2"} -> "PaidWindow"
               [] step = "ProcedureCoded05d55b14bf9" -> "Refill"
               [] step = "ProcedureCodebb587f61a951" -> "TurnBegins"
               [] step = "ProcedureCode989abc27e0c6" -> "NeutralValue00001"
               [] step = "ProcedureCodea439ce381bba" -> "Loop"
               [] step = "ProcedureCodeb6952d25a4da" -> "ActionPhaseEnds"
               [] step = "ProcedureCode593c4a6fb4f5" -> "DiscardStep"
               [] step = "ProcedureCodede325c329e93" -> "LoseUnspentActionPoints"
               [] step = "ProcedureCode8f113080e47f" -> "TurnEnds"
               [] step = "ProcedureCode49c3ccade13b" -> "Handoff" [] OTHER -> "PhaseComplete"

Exact module download · Source bundle and reproduction instructions

phase · operator

reference-profile · input revision 2 · CC0 1.0

phase == IF step \in SetupRange(SubSeq(SideBSteps5,1,9)) THEN "NeutralValue00001" ELSE "Discard"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange, SideBSteps5

ActionComplete5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionComplete5(before,after,allRemainingActionEffectsResolved) ==
    /\ before.status = "Effects" /\ before.nested = "NoValue"
    /\ allRemainingActionEffectsResolved
    /\ after = [before EXCEPT !.status = "Complete"]

Exact module download · Source bundle and reproduction instructions

ActionCompletionReactionStep5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionCompletionReactionStep5(player) ==
    IF player = "SideA" THEN "After5.6.2b" ELSE "After5.7.1f"

Exact module download · Source bundle and reproduction instructions

ActionEffectsBegin5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionEffectsBegin5(before,after,costCheckpointAndReactionsDrained) ==
    /\ before.status = "CostReactions" /\ costCheckpointAndReactionsDrained
    /\ after = [before EXCEPT !.status = "Effects"]

Exact module download · Source bundle and reproduction instructions

ActionNestedBegin5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionNestedBegin5(before,after,actualNestedStructureId) ==
    /\ before.status = "Effects" /\ before.nested = "NoValue"
    /\ actualNestedStructureId # "NoValue"
    /\ after = [before EXCEPT !.status = "Nested",!.nested = actualNestedStructureId]

Exact module download · Source bundle and reproduction instructions

ActionNestedReturn5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionNestedReturn5(before,after,completedStructureId,actualStructureComplete) ==
    /\ before.status = "Nested" /\ actualStructureComplete
    /\ completedStructureId = before.nested
    /\ after = [before EXCEPT !.status = "Effects",!.nested = "NoValue"]

Exact module download · Source bundle and reproduction instructions

ActionPhaseDecision5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionPhaseDecision5(turn,ending,actionPoints,actualDecisionStep,precedingProceduresDrained) ==
    IF ActionPhaseMayTakeAction5(turn,ending,turn.owner) /\ actualDecisionStep
       /\ precedingProceduresDrained
    THEN IF actionPoints > 0 THEN "MustTakeAction" ELSE "ProceedToFormalEnd"
    ELSE "Unavailable"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseMayTakeAction5

ActionPhaseEndCheckpoint5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionPhaseEndCheckpoint5(before,after,actualNormalCheckpointCompleted) ==
    /\ before.ending /\ before.step = "EndingCheckpoint" /\ before.checkpointDue
    /\ actualNormalCheckpointCompleted
    /\ after = [before EXCEPT !.step = "EndingReactions",!.checkpointDue = FALSE]

Exact module download · Source bundle and reproduction instructions

ActionPhaseEndDrain5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionPhaseEndDrain5(before,after,allEndingReactionWindowsDrained) ==
    /\ before.ending /\ before.step = "EndingReactions" /\ ~before.checkpointDue
    /\ allEndingReactionWindowsDrained
    /\ after = [before EXCEPT !.turn.phase = "Discard",!.ending = FALSE,!.step = "DiscardStep"]

Exact module download · Source bundle and reproduction instructions

ActionPhaseEndEvent5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionPhaseEndEvent5(turn) ==
    [tag |-> "ActionPhaseEnds",actor |-> turn.owner,turnId |-> turn.id]

Exact module download · Source bundle and reproduction instructions

ActionPhaseEndOutsidePhase5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionPhaseEndOutsidePhase5(before,after,player,events) ==
    ~OwnActionPhase5(before.turn,player) /\ after = before /\ events = {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OwnActionPhase5

ActionPhaseMayTakeAction5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionPhaseMayTakeAction5(turn,ending,player) == OwnActionPhase5(turn,player) /\ ~ending

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OwnActionPhase5

ActionReadyToContinue5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionReadyToContinue5(action) == action.status = "Complete"

Exact module download · Source bundle and reproduction instructions

ActionStart5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionStart5(turn,player,paidAbility,cost,actualActionWindow,allCostsPaid,
             noResolvingAction,actionId,key,after) ==
    /\ OwnActionPhase5(turn,player) /\ IsAction5(paidAbility,cost)
    /\ actualActionWindow /\ allCostsPaid /\ noResolvingAction
    /\ after = NewAction5(actionId,player,key)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IsAction5, NewAction5, OwnActionPhase5

ActionVoluntaryOption5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionVoluntaryOption5(action,option,actualNestedPriorityOptions) ==
    /\ action.status = "Nested" /\ action.nested # "NoValue"
    /\ option \in {"PaidAbility","Activation","ObjectiveCompletion"} /\ option \in actualNestedPriorityOptions

Exact module download · Source bundle and reproduction instructions

AllDifferentActions5 · operator

reference-profile · input revision 2 · CC0 1.0

AllDifferentActions5(keys) ==
    \A i,j \in 1..Len(keys): i # j => keys[i] # keys[j]

Exact module download · Source bundle and reproduction instructions

AllSameActions5 · operator

reference-profile · input revision 2 · CC0 1.0

AllSameActions5(keys) == Len(keys) > 0 /\ \A i \in 1..Len(keys): keys[i] = keys[1]

Exact module download · Source bundle and reproduction instructions

BasicAction5 · operator

reference-profile · input revision 2 · CC0 1.0

BasicAction5(player, id) ==
    [actionPoints |-> IF id = "Purge" THEN 3 ELSE 1,
     resourceUnits |-> CASE id = "AddProgress" -> 1
                   [] id \in {"RetireResource","RemoveExposureMarker"} -> 2 [] OTHER -> 0,
     effect |-> CASE id = "GainResourceUnit" -> "GainResourceUnit" [] id = "Draw" -> "Draw"
                  [] id = "Deploy" -> "Deploy" [] id = "Play" -> "Play"
                  [] id = "AddProgress" -> "AddProgress" [] id = "RetireResource" -> "Retire"
                  [] id = "Purge" -> "PurgeCluster" [] id = "SchemaAtom138" -> "SchemaAtom138"
                  [] OTHER -> "RemoveExposureMarker",
     quantity |-> IF id = "Purge" THEN "AllClusterCounters" ELSE 1,
     sourceZone |-> IF id \in {"Deploy","Play"} THEN
                       IF player = "SideA" THEN "SchemaAtom082" ELSE "BHand"
                    ELSE "NoValue",
     types |-> CASE id = "Deploy" /\ player = "SideA" -> {"Objective","Facility","Attachment","Barrier"}
                 [] id = "Deploy" -> {"Technique","Support","Equipment"}
                 [] id = "Play" -> IF player = "SideA" THEN {"Plan"} ELSE {"Action"}
                 [] id = "RetireResource" -> {"Support"} [] OTHER -> {},
     deployedTarget |-> id \in {"AddProgress","RetireResource"},
     needsHasExposureMarkers |-> id \in {"RetireResource","RemoveExposureMarker"}]

Exact module download · Source bundle and reproduction instructions

BasicActionIds5 · operator

reference-profile · input revision 2 · CC0 1.0

BasicActionIds5(player) ==
    IF player = "SideA" THEN
       {"GainResourceUnit","Draw","Deploy","Play","AddProgress","RetireResource","Purge"}
    ELSE {"GainResourceUnit","Draw","Deploy","Play","SchemaAtom138","RemoveExposureMarker"}

Exact module download · Source bundle and reproduction instructions

BasicActionKey5 · operator

reference-profile · input revision 2 · CC0 1.0

BasicActionKey5(player,id) == <<"Basic",player,id>>

Exact module download · Source bundle and reproduction instructions

BasicActionLocalGate5 · operator

reference-profile · input revision 2 · CC0 1.0

BasicActionLocalGate5(player,id,sideBHasExposureMarkers) ==
    /\ player \in SetupPlayers /\ id \in BasicActionIds5(player)
    /\ (BasicAction5(player,id).needsHasExposureMarkers => sideBHasExposureMarkers)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, BasicAction5, BasicActionIds5

BasicCardTarget5 · operator

reference-profile · input revision 2 · CC0 1.0

BasicCardTarget5(player,id,cardType,zone,deployed) ==
    /\ id \in BasicActionIds5(player)
    /\ (BasicAction5(player,id).types # {} => cardType \in BasicAction5(player,id).types)
    /\ (BasicAction5(player,id).sourceZone # "NoValue" =>
          zone = BasicAction5(player,id).sourceZone)
    /\ (BasicAction5(player,id).deployedTarget => deployed)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasicAction5, BasicActionIds5

CardActionKey5 · operator

reference-profile · input revision 2 · CC0 1.0

CardActionKey5(sourceObject,abilityNode) == <<"Card",sourceObject,abilityNode>>

Exact module download · Source bundle and reproduction instructions

DirectedActionOutsidePhase5 · operator

reference-profile · input revision 2 · CC0 1.0

DirectedActionOutsidePhase5(turn,player,before,after) ==
    ~OwnActionPhase5(turn,player) /\ after = before

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OwnActionPhase5

DiscardBatchEvent5 · operator

reference-profile · input revision 2 · CC0 1.0

DiscardBatchEvent5(player,selected) ==
    [tag |-> "Discard",actor |-> player,cards |-> selected,simultaneous |-> TRUE]

Exact module download · Source bundle and reproduction instructions

DiscardStep5 · operator

reference-profile · input revision 2 · CC0 1.0

DiscardStep5(turn,before,after,atActualDiscardBoundary,skipDiscardStep,
             effectiveMaximum,selected,handChecked,winCondition,events) ==
    /\ TurnFrameValid5(turn) /\ turn.phase = "Discard" /\ ~turn.formalEnded
    /\ atActualDiscardBoundary
    /\ IF skipDiscardStep THEN
          /\ after = before /\ selected = {} /\ ~handChecked
          /\ winCondition = "NoValue" /\ events = {}
       ELSE
          /\ handChecked
          /\ IF SideBHandHarmElimination4(turn.owner,effectiveMaximum,TRUE) THEN
                /\ after = before /\ selected = {} /\ winCondition = "SideA"
                /\ events = {}
             ELSE
                /\ winCondition = "NoValue" /\ selected \subseteq before.hand
                                                                              
                                                                                
                /\ Cardinality(selected) =
                     MinOf(Cardinality(before.hand),
                           HandDiscardDemand4(before.hand,effectiveMaximum,TRUE))
                /\ selected \subseteq DOMAIN before.faces
                /\ after = [before EXCEPT !.hand = @ \ selected,
                     !.discard = @ \cup selected,
                     !.faces = [c \in DOMAIN @ |-> IF c \in selected
                                  THEN DiscardArrivalFace4(turn.owner,
                                         IF turn.owner = "SideA" THEN "SideAHand" ELSE "SideBHand",
                                         "Discard",FALSE)
                                  ELSE before.faces[c]]]
                /\ events = IF selected = {} THEN {} ELSE {DiscardBatchEvent5(turn.owner,selected)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinOf, DiscardArrivalFace4, HandDiscardDemand4, SideBHandHarmElimination4, DiscardBatchEvent5, TurnFrameValid5

DiscardStepId5 · operator

reference-profile · input revision 2 · CC0 1.0

DiscardStepId5(player) == IF player = "SideA" THEN "ProcedureCode93af477f9d95" ELSE "ProcedureCode593c4a6fb4f5"

Exact module download · Source bundle and reproduction instructions

DuringPlayersTurn5 · operator

reference-profile · input revision 2 · CC0 1.0

DuringPlayersTurn5(t, player) == t.owner = player

Exact module download · Source bundle and reproduction instructions

ForceActionPhaseEnd5 · operator

reference-profile · input revision 2 · CC0 1.0

ForceActionPhaseEnd5(before,after,player,actualAuthorizedEndInstruction,events) ==
    /\ actualAuthorizedEndInstruction
    /\ OwnActionPhase5(before.turn,player) /\ ~before.ending
    /\ events = {ActionPhaseEndEvent5(before.turn)}
    /\ after = [before EXCEPT
         !.ending = TRUE,!.step = "EndingCheckpoint",!.remainingSteps = <<>>,
         !.openWindows = {},!.priority = "none",
         !.pending = {a \in @: before.pendingWindow[a] \notin before.openWindows},
         !.completedActions = @ \cup before.resolvingActions,
         !.completedAbilities = @ \cup before.resolvingAbilities,
         !.resolvingActions = {},!.resolvingAbilities = {},!.checkpointDue = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseEndEvent5, OwnActionPhase5

GainAllottedActionPoints5 · operator

reference-profile · input revision 2 · CC0 1.0

GainAllottedActionPoints5(before,after,player,effectiveAllotment) ==
    /\ player \in SetupPlayers /\ effectiveAllotment \in Int
    /\ after = [before EXCEPT ![player] = @+effectiveAllotment]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

HasDrawPhase5 · operator

reference-profile · input revision 2 · CC0 1.0

HasDrawPhase5(player) == player = "SideA"

Exact module download · Source bundle and reproduction instructions

IsAction5 · operator

reference-profile · input revision 2 · CC0 1.0

IsAction5(paidAbility, triggerCost) ==
    paidAbility /\ Len(triggerCost) > 0 /\ triggerCost[1].kind = "SpendActionPoints"

Exact module download · Source bundle and reproduction instructions

LoseUnspentActionPoints5 · operator

reference-profile · input revision 2 · CC0 1.0

LoseUnspentActionPoints5(before,after,player) ==
    player \in SetupPlayers /\ after = [before EXCEPT ![player] = IF @ > 0 THEN 0 ELSE @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

MandatoryDrawContext5 · operator

reference-profile · input revision 2 · CC0 1.0

MandatoryDrawContext5(turn,atActualMandatoryDrawStep) ==
    TurnFrameValid5(turn) /\ turn.owner = "SideA" /\ turn.phase = "Draw"
    /\ ~turn.formalEnded /\ atActualMandatoryDrawStep

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnFrameValid5

MandatoryDrawEvent5 · operator

reference-profile · input revision 2 · CC0 1.0

MandatoryDrawEvent5 ==
    [tag |-> "Draw",actor |-> "SideA",mandatory |-> TRUE,action |-> FALSE,amount |-> 1]

Exact module download · Source bundle and reproduction instructions

MaximumHandSize5 · operator

reference-profile · input revision 2 · CC0 1.0

MaximumHandSize5(player,persistentCapacityLoss,effectiveOtherAdjustment) ==
    StandardMaximumHandSize4 + effectiveOtherAdjustment -
      IF player = "SideB" THEN persistentCapacityLoss ELSE 0

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StandardMaximumHandSize4

NewAction5 · operator

reference-profile · input revision 2 · CC0 1.0

NewAction5(actionId,player,key) ==
    [id |-> actionId,owner |-> player,key |-> key,status |-> "CostReactions",nested |-> "NoValue"]

Exact module download · Source bundle and reproduction instructions

NextTurnPhase5 · operator

reference-profile · input revision 2 · CC0 1.0

NextTurnPhase5(owner, phase) ==
    CASE owner = "SideA" /\ phase = "Draw" -> "NeutralValue00001"
      [] phase = "NeutralValue00001" -> "Discard" [] OTHER -> "NoValue"

Exact module download · Source bundle and reproduction instructions

NoBetweenTurns5 · operator

reference-profile · input revision 2 · CC0 1.0

NoBetweenTurns5(gameStarted, turn) == gameStarted => TurnFrameValid5(turn)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnFrameValid5

OpenSideAProcedure5 · operator

reference-profile · input revision 2 · CC0 1.0

OpenSideAProcedure5(turn) ==
    [turn |-> turn,step |-> "ProcedureCode3557d050aec7",decision |-> "NoValue",phaseEndMet |-> FALSE]

Exact module download · Source bundle and reproduction instructions

OpenSideBProcedure5 · operator

reference-profile · input revision 2 · CC0 1.0

OpenSideBProcedure5(turn) ==
    [turn |-> turn,step |-> "ProcedureCode81ed7b3ac00d",decision |-> "NoValue",phaseEndMet |-> FALSE]

Exact module download · Source bundle and reproduction instructions

OpenTurn5 · operator

reference-profile · input revision 2 · CC0 1.0

OpenTurn5(player, turnId, begunCounts) ==
    [owner |-> player,phase |-> TurnPhases5(player)[1],id |-> turnId,
     formalBegun |-> FALSE,formalEnded |-> FALSE,begunCounts |-> begunCounts]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnPhases5

OwnActionPhase5 · operator

reference-profile · input revision 2 · CC0 1.0

OwnActionPhase5(turn, player) ==
    TurnFrameValid5(turn) /\ turn.owner = player /\ turn.phase = "NeutralValue00001" /\ ~turn.formalEnded

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnFrameValid5

PersistentCapacityLossAccrual5 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentCapacityLossAccrual5(before,after,suffered) ==
    before \in Nat /\ suffered \in Nat /\ after = before+suffered

Exact module download · Source bundle and reproduction instructions

RecurringRefill5 · operator

reference-profile · input revision 2 · CC0 1.0

RecurringRefill5(beforeCount,afterCount,effectiveRecurring,activeControlledByTurnPlayer) ==
    /\ activeControlledByTurnPlayer /\ beforeCount \in Nat /\ effectiveRecurring \in Int
    /\ afterCount = beforeCount+MaxOf(0,effectiveRecurring-beforeCount)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf

SideAActionPhaseEndAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAActionPhaseEndAtStep5(before,after,events) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCode042aa78ff256" /\ ~before.phaseEndMet
    /\ events = {ActionPhaseEndEvent5(before.turn)}
    /\ after = [before EXCEPT !.phaseEndMet = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseEndEvent5, SideAProcedureValid5

SideAAllotmentAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAllotmentAtStep5(f,before,after,effectiveAllotment) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode3557d050aec7" /\
    GainAllottedActionPoints5(before,after,"SideA",effectiveAllotment)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: GainAllottedActionPoints5, SideAProcedureValid5

SideADefaultAllotment5 · operator

reference-profile · input revision 2 · CC0 1.0

SideADefaultAllotment5 == 3

Exact module download · Source bundle and reproduction instructions

SideADiscardAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideADiscardAtStep5(f,before,after,skip,maximum,selected,checked,winCondition,events) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode93af477f9d95" /\
    DiscardStep5(f.turn,before,after,TRUE,skip,maximum,selected,checked,winCondition,events)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DiscardStep5, SideAProcedureValid5

SideAFormalBeginAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAFormalBeginAtStep5(before,after,events) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCode824821d07be7"
    /\ TurnFormalBegin5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAProcedureValid5, TurnFormalBegin5

SideAFormalEndAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAFormalEndAtStep5(before,after,events) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCodea107cee5c079"
    /\ TurnFormalEnd5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAProcedureValid5, TurnFormalEnd5

SideALatchDecision5 · operator

reference-profile · input revision 2 · CC0 1.0

SideALatchDecision5(before,after,actualUnspentActionPoints,precedingWindowAndReactionsDrained) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCode0e20572a4bab"
    /\ before.decision = "NoValue" /\ ~before.phaseEndMet
    /\ ActionPhaseDecision5(before.turn,FALSE,actualUnspentActionPoints,TRUE,
                          precedingWindowAndReactionsDrained) # "Unavailable"
    /\ after = [before EXCEPT !.decision = IF actualUnspentActionPoints > 0 THEN "NeutralValue00001" ELSE "End"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseDecision5, SideAProcedureValid5

SideALoseActionPointsAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideALoseActionPointsAtStep5(f,before,after) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode4e363e6bb7cf" /\ LoseUnspentActionPoints5(before,after,"SideA")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LoseUnspentActionPoints5, SideAProcedureValid5

SideAMandatoryDrawAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAMandatoryDrawAtStep5(f,before,after,normalDrawApplies,winCondition,events) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode59141ee1a13b" /\
    UnmodifiedMandatoryDraw5(f.turn,before,after,TRUE,normalDrawApplies,winCondition,events)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAProcedureValid5, UnmodifiedMandatoryDraw5

SideANextStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideANextStep5(step,decision) ==
    CASE step = "ProcedureCode0e20572a4bab" -> IF decision = "NeutralValue00001" THEN "ProcedureCodeb6035cb98279" ELSE "ProcedureCode042aa78ff256"
      [] step = "ProcedureCodeb6035cb98279" -> "ProcedureCoded6fbcb09dd4f"
      [] step = "ProcedureCode72a65676fb11" -> "ProcedureCode81ed7b3ac00d"
      [] OTHER -> SideASteps5[(CHOOSE i \in 1..Len(SideASteps5): SideASteps5[i] = step)+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideASteps5

SideAProcedureValid5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAProcedureValid5(f) ==
    TurnFrameValid5(f.turn) /\ f.turn.owner = "SideA" /\ f.step \in SetupRange(SideASteps5)
    /\ f.turn.phase = SideAStepInfo5(f.step).phase
    /\ f.decision \in {"NoValue","NeutralValue00001","End"} /\ f.phaseEndMet \in BOOLEAN

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange, SideAStepInfo5, SideASteps5, TurnFrameValid5

SideARefillAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideARefillAtStep5(f,before,after,effectiveRecurring,activeControlledBySideA) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode599a3c2d7264" /\
    RecurringRefill5(before,after,effectiveRecurring,activeControlledBySideA)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RecurringRefill5, SideAProcedureValid5

SideAStepAdvance5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAStepAdvance5(before,after,actualStepIncludingReactionsComplete) ==
    /\ SideAProcedureValid5(before) /\ actualStepIncludingReactionsComplete
    /\ (before.step = "ProcedureCode0e20572a4bab" => before.decision \in {"NeutralValue00001","End"})
    /\ (before.step = "ProcedureCode824821d07be7" => before.turn.formalBegun)
    /\ (before.step = "ProcedureCode042aa78ff256" => before.phaseEndMet)
    /\ (before.step = "ProcedureCodea107cee5c079" => before.turn.formalEnded)
    /\ IF before.step = "ProcedureCode72a65676fb11" THEN
          /\ TurnHandoff5(before.turn,after.turn,TRUE,{})
          /\ after = [before EXCEPT !.turn = OpenTurn5("SideB",before.turn.id+1,before.turn.begunCounts),
                       !.step = "ProcedureCode81ed7b3ac00d",!.decision = "NoValue",!.phaseEndMet = FALSE]
       ELSE
          LET next == SideANextStep5(before.step,before.decision)
          IN after = [before EXCEPT !.step = next,!.turn.phase = SideAStepInfo5(next).phase,!.decision = "NoValue"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: next, OpenTurn5, SideAProcedureValid5, SideAStepInfo5, TurnHandoff5

SideAStepInfo5 · operator

reference-profile · input revision 2 · CC0 1.0

SideAStepInfo5(step) ==
 LET phase == CASE step \in SetupRange(SubSeq(SideASteps5,1,6)) -> "Draw"
                [] step \in SetupRange(SubSeq(SideASteps5,7,11)) -> "NeutralValue00001"
                [] OTHER -> "Discard"
     kind == CASE step = "ProcedureCode3557d050aec7" -> "AllotActionPoints"
               [] step \in {"ProcedureCode36065334a34a","ProcedureCoded6fbcb09dd4f","ProcedureCode438597bede05"} -> "PaidWindow"
               [] step = "ProcedureCode599a3c2d7264" -> "Refill"
               [] step = "ProcedureCode824821d07be7" -> "TurnBegins"
               [] step = "ProcedureCode59141ee1a13b" -> "MandatoryDraw"
               [] step = "ProcedureCode0e20572a4bab" -> "NeutralValue00001"
               [] step = "ProcedureCodeb6035cb98279" -> "Loop"
               [] step = "ProcedureCode042aa78ff256" -> "ActionPhaseEnds"
               [] step = "ProcedureCode93af477f9d95" -> "DiscardStep"
               [] step = "ProcedureCode4e363e6bb7cf" -> "LoseUnspentActionPoints"
               [] step = "ProcedureCodea107cee5c079" -> "TurnEnds"
               [] step = "ProcedureCode72a65676fb11" -> "Handoff" [] OTHER -> "PhaseComplete"
 IN TurnStepDescriptor5(kind,phase,step \in {"ProcedureCode36065334a34a","ProcedureCoded6fbcb09dd4f"})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: kind, phase, TurnStepDescriptor5

SideASteps5 · operator

reference-profile · input revision 2 · CC0 1.0

SideASteps5 ==
    <<"ProcedureCode3557d050aec7","ProcedureCode36065334a34a","ProcedureCode599a3c2d7264","ProcedureCode824821d07be7","ProcedureCode59141ee1a13b","ProcedureCodedab8b83ddbcc",
      "ProcedureCoded6fbcb09dd4f","ProcedureCode0e20572a4bab","ProcedureCodeb6035cb98279","ProcedureCode042aa78ff256","ProcedureCode79efdf0ee977",
      "ProcedureCode93af477f9d95","ProcedureCode438597bede05","ProcedureCode4e363e6bb7cf","ProcedureCodea107cee5c079","ProcedureCode72a65676fb11">>

Exact module download · Source bundle and reproduction instructions

SideBActionPhaseEndAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBActionPhaseEndAtStep5(before,after,events) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCodeb6952d25a4da" /\ ~before.phaseEndMet
    /\ events = {ActionPhaseEndEvent5(before.turn)}
    /\ after = [before EXCEPT !.phaseEndMet = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseEndEvent5, SideBProcedureValid5

SideBAllotmentAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAllotmentAtStep5(f,before,after,effectiveAllotment) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCode81ed7b3ac00d" /\
    GainAllottedActionPoints5(before,after,"SideB",effectiveAllotment)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: GainAllottedActionPoints5, SideBProcedureValid5

SideBDefaultAllotment5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBDefaultAllotment5 == 4

Exact module download · Source bundle and reproduction instructions

SideBDiscardAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBDiscardAtStep5(f,before,after,skip,maximum,selected,checked,winCondition,events) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCode593c4a6fb4f5" /\
    DiscardStep5(f.turn,before,after,TRUE,skip,maximum,selected,checked,winCondition,events)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DiscardStep5, SideBProcedureValid5

SideBFormalBeginAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBFormalBeginAtStep5(before,after,events) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCodebb587f61a951"
    /\ TurnFormalBegin5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBProcedureValid5, TurnFormalBegin5

SideBFormalEndAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBFormalEndAtStep5(before,after,events) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCode8f113080e47f"
    /\ TurnFormalEnd5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBProcedureValid5, TurnFormalEnd5

SideBLatchDecision5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBLatchDecision5(before,after,actualUnspentActionPoints,precedingWindowAndReactionsDrained) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCode989abc27e0c6"
    /\ before.decision = "NoValue" /\ ~before.phaseEndMet
    /\ ActionPhaseDecision5(before.turn,FALSE,actualUnspentActionPoints,TRUE,
                          precedingWindowAndReactionsDrained) # "Unavailable"
    /\ after = [before EXCEPT !.decision = IF actualUnspentActionPoints > 0 THEN "NeutralValue00001" ELSE "End"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseDecision5, SideBProcedureValid5

SideBLoseActionPointsAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBLoseActionPointsAtStep5(f,before,after) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCodede325c329e93" /\ LoseUnspentActionPoints5(before,after,"SideB")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LoseUnspentActionPoints5, SideBProcedureValid5

SideBNextStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBNextStep5(step,decision) ==
    CASE step = "ProcedureCode989abc27e0c6" -> IF decision = "NeutralValue00001" THEN "ProcedureCodea439ce381bba" ELSE "ProcedureCodeb6952d25a4da"
      [] step = "ProcedureCodea439ce381bba" -> "ProcedureCode484be3e50aa9"
      [] step = "ProcedureCode49c3ccade13b" -> "ProcedureCode3557d050aec7"
      [] OTHER -> SideBSteps5[(CHOOSE i \in 1..Len(SideBSteps5): SideBSteps5[i] = step)+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBSteps5

SideBProcedureValid5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBProcedureValid5(f) ==
    TurnFrameValid5(f.turn) /\ f.turn.owner = "SideB" /\ f.step \in SetupRange(SideBSteps5)
    /\ f.turn.phase = SideBStepInfo5(f.step).phase
    /\ f.decision \in {"NoValue","NeutralValue00001","End"} /\ f.phaseEndMet \in BOOLEAN

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupRange, SideBStepInfo5, SideBSteps5, TurnFrameValid5

SideBRefillAtStep5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBRefillAtStep5(f,before,after,effectiveRecurring,activeControlledBySideB) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCoded05d55b14bf9" /\
    RecurringRefill5(before,after,effectiveRecurring,activeControlledBySideB)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RecurringRefill5, SideBProcedureValid5

SideBStepAdvance5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBStepAdvance5(before,after,actualStepIncludingReactionsComplete) ==
    /\ SideBProcedureValid5(before) /\ actualStepIncludingReactionsComplete
    /\ (before.step = "ProcedureCode989abc27e0c6" => before.decision \in {"NeutralValue00001","End"})
    /\ (before.step = "ProcedureCodebb587f61a951" => before.turn.formalBegun)
    /\ (before.step = "ProcedureCodeb6952d25a4da" => before.phaseEndMet)
    /\ (before.step = "ProcedureCode8f113080e47f" => before.turn.formalEnded)
    /\ IF before.step = "ProcedureCode49c3ccade13b" THEN
          /\ TurnHandoff5(before.turn,after.turn,TRUE,{})
          /\ after = [before EXCEPT !.turn = OpenTurn5("SideA",before.turn.id+1,before.turn.begunCounts),
                       !.step = "ProcedureCode3557d050aec7",!.decision = "NoValue",!.phaseEndMet = FALSE]
       ELSE
          LET next == SideBNextStep5(before.step,before.decision)
          IN after = [before EXCEPT !.step = next,!.turn.phase = SideBStepInfo5(next).phase,!.decision = "NoValue"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: next, OpenTurn5, SideBProcedureValid5, SideBStepInfo5, TurnHandoff5

SideBStepInfo5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBStepInfo5(step) ==
 LET phase == IF step \in SetupRange(SubSeq(SideBSteps5,1,9)) THEN "NeutralValue00001" ELSE "Discard"
     kind == CASE step = "ProcedureCode81ed7b3ac00d" -> "AllotActionPoints"
               [] step \in {"ProcedureCodef53fc09e15ad","ProcedureCode484be3e50aa9","ProcedureCode13c5f7239eb2"} -> "PaidWindow"
               [] step = "ProcedureCoded05d55b14bf9" -> "Refill"
               [] step = "ProcedureCodebb587f61a951" -> "TurnBegins"
               [] step = "ProcedureCode989abc27e0c6" -> "NeutralValue00001"
               [] step = "ProcedureCodea439ce381bba" -> "Loop"
               [] step = "ProcedureCodeb6952d25a4da" -> "ActionPhaseEnds"
               [] step = "ProcedureCode593c4a6fb4f5" -> "DiscardStep"
               [] step = "ProcedureCodede325c329e93" -> "LoseUnspentActionPoints"
               [] step = "ProcedureCode8f113080e47f" -> "TurnEnds"
               [] step = "ProcedureCode49c3ccade13b" -> "Handoff" [] OTHER -> "PhaseComplete"
 IN TurnStepDescriptor5(kind,phase,FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: kind, phase, TurnStepDescriptor5

SideBSteps5 · operator

reference-profile · input revision 2 · CC0 1.0

SideBSteps5 ==
    <<"ProcedureCode81ed7b3ac00d","ProcedureCodef53fc09e15ad","ProcedureCoded05d55b14bf9","ProcedureCodebb587f61a951","ProcedureCode484be3e50aa9","ProcedureCode989abc27e0c6","ProcedureCodea439ce381bba","ProcedureCodeb6952d25a4da","ProcedureCoded3bf6d016bb1",
      "ProcedureCode593c4a6fb4f5","ProcedureCode13c5f7239eb2","ProcedureCodede325c329e93","ProcedureCode8f113080e47f","ProcedureCode49c3ccade13b">>

Exact module download · Source bundle and reproduction instructions

TurnActivePlayer5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnActivePlayer5(t) == t.owner

Exact module download · Source bundle and reproduction instructions

TurnBeginEvent5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnBeginEvent5(t) ==
    [tag |-> "TurnBegins",actor |-> t.owner,turnId |-> t.id,
     sideATurn |-> t.begunCounts["SideA"] + IF t.owner = "SideA" THEN 1 ELSE 0]

Exact module download · Source bundle and reproduction instructions

TurnEndEvents5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnEndEvents5(t) ==
    {[tag |-> tag,actor |-> t.owner,turnId |-> t.id,
      sideATurn |-> t.begunCounts["SideA"]] : tag \in {"TurnEnds","DiscardPhaseEnds"}}

Exact module download · Source bundle and reproduction instructions

TurnFirstPriority5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnFirstPriority5(t) == t.owner

Exact module download · Source bundle and reproduction instructions

TurnFormalBegin5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnFormalBegin5(before, after, atActualFormalBeginStep, events) ==
    /\ TurnFrameValid5(before) /\ ~before.formalBegun /\ ~before.formalEnded
    /\ atActualFormalBeginStep /\ events = {TurnBeginEvent5(before)}
    /\ after = [before EXCEPT !.formalBegun = TRUE,!.begunCounts[before.owner] = @+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnBeginEvent5, TurnFrameValid5

TurnFormalEnd5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnFormalEnd5(before, after, atActualFormalEndStep, events) ==
    /\ TurnFrameValid5(before) /\ before.phase = "Discard" /\ ~before.formalEnded
    /\ atActualFormalEndStep /\ events = TurnEndEvents5(before)
    /\ after = [before EXCEPT !.formalEnded = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnEndEvents5, TurnFrameValid5

TurnFrameValid5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnFrameValid5(t) ==
    /\ t.owner \in SetupPlayers /\ t.phase \in SetupRange(TurnPhases5(t.owner))
    /\ t.id \in Nat \ {0} /\ t.formalBegun \in BOOLEAN /\ t.formalEnded \in BOOLEAN
    /\ t.begunCounts \in [SetupPlayers -> Nat]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, SetupRange, TurnPhases5

TurnHandoff5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnHandoff5(before, after, oldTurnProcedureComplete, events) ==
    /\ TurnFrameValid5(before) /\ before.phase = "Discard" /\ before.formalEnded
    /\ oldTurnProcedureComplete /\ events = {}
    /\ after = OpenTurn5(TurnOtherPlayer5(before.owner),before.id+1,before.begunCounts)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenTurn5, TurnFrameValid5, TurnOtherPlayer5

TurnOtherPlayer5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnOtherPlayer5(player) == IF player = "SideA" THEN "SideB" ELSE "SideA"

Exact module download · Source bundle and reproduction instructions

TurnPhaseAdvance5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnPhaseAdvance5(before, after, actualPhaseProcedureComplete) ==
    /\ TurnFrameValid5(before) /\ ~before.formalEnded /\ actualPhaseProcedureComplete
    /\ NextTurnPhase5(before.owner,before.phase) # "NoValue"
    /\ after = [before EXCEPT !.phase = NextTurnPhase5(before.owner,before.phase)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NextTurnPhase5, TurnFrameValid5

TurnPhases5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnPhases5(player) ==
    IF player = "SideA" THEN <<"Draw","NeutralValue00001","Discard">> ELSE <<"NeutralValue00001","Discard">>

Exact module download · Source bundle and reproduction instructions

TurnStepDescriptor5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnStepDescriptor5(kind,phase,objectiveCompletionWindow) ==
    [kind |-> kind,phase |-> phase,
     options |-> IF kind = "PaidWindow" THEN
                   IF objectiveCompletionWindow THEN {"PaidAbility","Activation","ObjectiveCompletion"} ELSE {"PaidAbility","Activation"}
                 ELSE {},
     activationNonBarrierOnly |-> kind = "PaidWindow"]

Exact module download · Source bundle and reproduction instructions

UnmodifiedMandatoryDraw5 · operator

reference-profile · input revision 2 · CC0 1.0

UnmodifiedMandatoryDraw5(turn,before,after,atActualMandatoryDrawStep,
                        normalDrawProcedureApplies,winner,events) ==
    /\ MandatoryDrawContext5(turn,atActualMandatoryDrawStep)
    /\ normalDrawProcedureApplies /\ DeckSequenceValid4(before.deck)
    /\ SetupRange(before.deck) \intersect before.hand = {}
    /\ IF before.deck = <<>> THEN
          /\ winner = RequiredEmptyDeckWinner4("SideA",before.deck,TRUE,TRUE)
          /\ after = before /\ events = {}
       ELSE
          /\ winner = "NoValue" /\ events = {MandatoryDrawEvent5}
          /\ after = [before EXCEPT !.deck = Tail(@),!.hand = @ \cup {before.deck[1]}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeckSequenceValid4, RequiredEmptyDeckWinner4, SetupRange, MandatoryDrawContext5, MandatoryDrawEvent5

WithBasicEffect5 · operator

reference-profile · input revision 2 · CC0 1.0

WithBasicEffect5(actionKind,actionId,occurrenceActionId,actualEffect,queriedEffect) ==
    actionKind = "Basic" /\ actionId = occurrenceActionId /\ actualEffect = queriedEffect

Exact module download · Source bundle and reproduction instructions