----------------------------- MODULE TypeContracts ----------------------------- EXTENDS SchemaContracts ProfileObjectValid(o) == (o.form = "Card" /\ o.kind = "Profile") => ~o.deployed ProfileFaceActive(o, faceIsFront, gameStarted, cardData) == /\ o.kind = "Profile" /\ o.front = faceIsFront /\ DefaultActive(o,gameStarted,cardData) 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)} 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 ProfileFaceValuesValid(c) == /\ MinimumDeckMetadataValid(c) /\ ImportCostLimitMetadataValid(c) /\ BaseLinkMetadataValid(c) 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] ProfileTargetSiteSpecimen0139(o, cardData) == IF o.form = "Card" /\ o.kind = "Profile" /\ o.zone = "Play" /\ cardData[o.card].side = "SideA" THEN "SchemaAtom082" ELSE "NoValue" ObjectiveDeployTypeLocation(actor, kind, destination) == /\ actor = "SideA" /\ kind = "Objective" /\ destination.zone = "Play" /\ destination.area = "Root" /\ destination.targetSiteKind = "SchemaAtom132" 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"}} ObjectiveFacilityRootLimit(objects, targetSite) == Cardinality(ObjectiveFacilityRootOccupants(objects,targetSite)) <= 1 ObjectiveCharacteristicSlotsValid(c) == ProgressMetadataValid(c) /\ ObjectivePointsMetadataValid(c) ObjectivePointsInObjectiveArea(o, area, effectivePoints) == IF area \in {"SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ o.zone = area /\ o.form = "Card" /\ o.kind = "Objective" THEN effectivePoints ELSE 0 ObjectiveCanActivation(o) == FALSE ObjectiveActivationStatus(o) == IF o.form = "Card" /\ o.kind = "Objective" /\ o.deployed /\ o.face = "Down" THEN "Dormant" ELSE "Neither" ObjectiveCardActive(o, gameStarted, cardData) == o.form = "Card" /\ o.kind = "Objective" /\ DefaultActive(o,gameStarted,cardData) 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) ObjectiveProgressEligible(o) == o.form = "Card" /\ o.kind = "Objective" /\ o.deployed FacilityDeployTypeLocation(actor, kind, destination) == /\ actor = "SideA" /\ kind = "Facility" /\ destination.zone = "Play" /\ destination.area = "Root" /\ destination.targetSiteKind = "SchemaAtom132" FacilityDeploymentPost(o) == /\ o.form = "Card" /\ o.kind = "Facility" /\ o.zone = "Play" /\ o.deployed /\ o.face = "Down" /\ ~o.activated 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] ItemInspectionRetireCostOpportunity(actor, o, accessing, effectiveRetirePart) == /\ actor = "SideB" /\ o.form = "Card" /\ accessing /\ o.zone # "SideADiscard" /\ effectiveRetirePart.exists ExampleItemARegionDeclaration(c) == /\ c.kind = "Facility" /\ CanonicalName(c) = <<"Example Item A">> /\ "SchemaAtom130" \in c.printedSubtypes /\ c.printedRegionLimit = 1 BarrierTermRefersToType(term) == term \in {"barrierCard","piece of barrier"} BarrierDeployTypeLocation(actor, kind, destination) == /\ actor = "SideA" /\ kind = "Barrier" /\ destination.zone = "Play" /\ destination.area = "Protecting" /\ destination.targetSiteKind \in {"SchemaAtom033","SchemaAtom132"} ProtectingCardTypeValid(o) == (o.form = "Card" /\ o.deployed /\ o.area = "Protecting") => o.kind = "Barrier" StandardBarrierInsertion(beforeOrder, afterOrder, newId) == /\ newId \notin SetupRange(beforeOrder) /\ afterOrder = Append(beforeOrder,newId) BarrierProtectionLayout == [orientation |-> "Horizontal",order |-> "InnermostToOutermost", outermost |-> "FurthestFromTargetSite"] BarrierDeploymentPost(o) == /\ o.form = "Card" /\ o.kind = "Barrier" /\ o.zone = "Play" /\ o.deployed /\ o.face = "Down" /\ ~o.activated 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] SideAHasInherentDeployCost(kind) == kind = "Barrier" BarrierDeployResourceUnitCost(otherBarrierOrder) == InherentDeployCost([kind |-> "Barrier"],Len(otherBarrierOrder)) BarrierNormalItemInspectionDeploymentGate(o) == o.form = "Card" /\ o.kind = "Barrier" /\ ~o.deployed BarrierInstructionOwnerKindValid(kind, barrierInstructions) == Len(barrierInstructions) = 0 \/ kind = "Barrier" 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] 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 OperationPlayTypeAllowed(actor, kind) == actor = "SideA" /\ kind = "Plan" PlayedTypeNotDeployed(o) == (o.form = "Card" /\ o.kind \in {"Plan","Action"}) => ~o.deployed PlayedCardActive(o, activationReached) == /\ o.form = "Card" /\ o.kind \in {"Plan","Action"} /\ o.zone = "Play" /\ o.face = "Up" /\ activationReached PlayedSourceRetireEligible(o) == /\ o.form = "Card" /\ o.kind \in {"Plan","Action"} /\ o.zone = "Play" /\ o.host = 0 PlayedResolutionRetireDue(o, abilitiesFullyResolved, holdLive, nestedRemovalPending) == /\ PlayedSourceRetireEligible(o) /\ abilitiesFullyResolved /\ ~holdLive /\ ~nestedRemovalPending ConditionOperationSelfDeployGate(o, route, ownAbilityAuthorized) == /\ o.form = "Card" /\ o.kind = "Plan" /\ "SchemaAtom043" \in o.subtypes /\ route = "OwnConversion" /\ ownAbilityAuthorized ConditionCounterPost(sourceCard, o) == /\ o.card = sourceCard /\ o.form = "Counter" /\ o.kind = "SchemaAtom043" /\ o.deployed /\ o.zone = "Play" AnotherCurrentPlayed(sourceId, event) == /\ event.tag = "Played" /\ event.object # sourceId /\ event.kind \in {"Plan","Action"} /\ "SchemaAtom048" \in event.subtypes OperationCurrentExpires(sourceId, event) == AnotherCurrentPlayed(sourceId,event) \/ event.tag = "ObjectiveClaimedObjective" Specimen0133Expires(expiresSideATurn, event) == event.tag = "TurnBegins" /\ event.actor = "SideA" /\ event.sideATurn >= expiresSideATurn PlayedRetention(mode, sideATurn) == [mode |-> mode,live |-> mode # "NoValue",inPlay |-> TRUE, pendingRetire |-> FALSE,expiresSideATurn |-> sideATurn+1] PlayedSourceInPlay(sourceId, objects) == IF sourceId \in DOMAIN objects THEN objects[sourceId].zone = "Play" ELSE FALSE PlayedRetireSourceApplicable(sourceId, objects) == IF sourceId \in DOMAIN objects THEN PlayedSourceRetireEligible(objects[sourceId]) ELSE FALSE ExpirePlayedRetention(before, shouldExpire, sourceApplicable) == IF before.live /\ shouldExpire THEN [before EXCEPT !.live = FALSE,!.pendingRetire = sourceApplicable] ELSE before 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)) 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)] RetentionReactionGate(retentions, objects) == \A id \in DOMAIN retentions : ~retentions[id].pendingRetire \/ ~PlayedRetireSourceApplicable(id,objects) SideAHasPlayCost(kind) == kind = "Plan" UpgradeDeployTypeLocation(actor, kind, destination) == /\ actor = "SideA" /\ kind = "Attachment" /\ destination.zone = "Play" /\ destination.area = "Root" /\ destination.targetSiteKind \in {"SchemaAtom033","SchemaAtom132"} CentralRootCardTypeValid(o) == (o.form = "Card" /\ o.deployed /\ o.zone = "Play" /\ o.area = "Root" /\ o.targetSiteKind = "SchemaAtom033") => o.kind = "Attachment" StandardUpgradeCountAllowed(count) == count \in Nat UpgradeDeploymentPost(o) == /\ o.form = "Card" /\ o.kind = "Attachment" /\ o.zone = "Play" /\ o.deployed /\ o.face = "Down" /\ ~o.activated 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] RegionPrintedDeclarationValid(c) == "SchemaAtom130" \in c.printedSubtypes => c.printedRegionLimit = 1 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} 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} RegionRootLimit(objects, deploying, targetSite) == Cardinality(DeployedRootRegions(objects,targetSite) \cup DeployingRootRegions(deploying,targetSite)) <= 1 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 {} RegionReplacementRetireSatisfied(required, actuallyRetireed) == required \subseteq actuallyRetireed RegionMoveSwapGate(afterObjects, afterDeploying, targetSiteIds) == \A targetSite \in targetSiteIds : RegionRootLimit(afterObjects,afterDeploying,targetSite) EventPlayTypeAllowed(actor, kind) == actor = "SideB" /\ kind = "Action" SideBHasPlayCost(kind) == kind = "Action" ExampleItemBConditionDeclaration(c) == /\ c.kind = "Action" /\ CanonicalName(c) = <<"Example Item B">> /\ "SchemaAtom043" \in c.printedSubtypes ConditionEventSelfDeployGate(o, route, ownAbilityAuthorized) == /\ o.form = "Card" /\ o.kind = "Action" /\ "SchemaAtom043" \in o.subtypes /\ route = "OwnConversion" /\ ownAbilityAuthorized EventCurrentExpires(sourceId, event) == AnotherCurrentPlayed(sourceId,event) \/ event.tag = "ObjectivePlacementd" EventRetentionAfterEvent(before, sourceId, event, objects) == ExpirePlayedRetention([before EXCEPT !.inPlay = PlayedSourceInPlay(sourceId,objects)], before.mode = "SchemaAtom048" /\ EventCurrentExpires(sourceId,event), PlayedRetireSourceApplicable(sourceId,objects)) EquipmentTermRefersToType(term) == term \in {"equipment","piece of equipment"} 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 StandardEquipmentCountAllowed(count) == count \in Nat ConsolePrintedDeclarationValid(c) == "SchemaAtom045" \in c.printedSubtypes => c.printedConsoleLimit = 1 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]} ConsoleActivationHistoryValid(eligible, history) == eligible \subseteq SetupRange(history) LatestActiveConsole(eligible, history) == LET relevant == SelectSeq(history,LAMBDA id : id \in eligible) IN IF eligible = {} THEN {} ELSE {relevant[Len(relevant)]} 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 {}] DeployedTechniqueIds(objects, effectiveTypes) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].deployed /\ "Technique" \in effectiveTypes[id]} TechniqueCapacityDemand(objects, effectiveTypes, effectiveCapacity) == [id \in DeployedTechniqueIds(objects,effectiveTypes) |-> IF effectiveCapacity[id].exists THEN effectiveCapacity[id].amount ELSE 0] TechniqueCapacityArithmeticFits(demand, limit) == SumMap(demand) <= limit TechniqueCapacityLegal(demand, limit, allocationFits) == TechniqueCapacityArithmeticFits(demand,limit) /\ allocationFits TechniqueCapacityCandidateLegal(candidate) == /\ DOMAIN candidate.demand = candidate.techniqueIds /\ TechniqueCapacityLegal(candidate.demand,candidate.limit,candidate.allocationFits) 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) TechniqueCapacityCheckpointChoice(deployedIds, trashed, candidateAfter(_)) == /\ ~TechniqueCapacityCandidateLegal(candidateAfter({})) /\ trashed \subseteq deployedIds /\ trashed # {} /\ TechniqueCapacityCandidateLegal(candidateAfter(trashed)) /\ \A id \in trashed : ~TechniqueCapacityCandidateLegal(candidateAfter(trashed \ {id})) TechniqueCapacityRepairTiming(cause) == IF cause = "DeployingTechnique" THEN "DuringDeploy" ELSE "NextCheckpoint10.3.1e" 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)] TechniqueStrengthMetadataValid(c) == /\ c.kind = "Technique" /\ StrengthMetadataValid(c) /\ SubtypeFlagsConsistent(c) BarrierResponseCardTechnique(o, subtypes) == o.form = "Card" /\ o.kind = "Technique" /\ "SchemaAtom086" \in subtypes PrintedBarrierResponseCardInterfacesValid(c, printedAbilities) == c.printedBarrierResponseCard => \E i \in 1..Len(printedAbilities) : printedAbilities[i].isInterface InterfaceFlagValid(ability) == /\ ability.isInterface \in BOOLEAN /\ ability.interfaceFlag = IF ability.isInterface THEN "Interface" ELSE "NoValue" InterfaceTargetsAllowed(targets, barrierId, barrierInstructionIds) == \A t \in targets : (t.kind = "Card" /\ t.object = barrierId) \/ (t.kind = "BarrierInstruction" /\ t.object = barrierId /\ t.barrierInstruction \in barrierInstructionIds) InterfaceSubtypeMatches(restriction, barrierSubtypes) == ~restriction.present \/ restriction.name \in barrierSubtypes 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 BarrierResponseCardBoost(targetId, amount, encounterId, hasExplicit, explicitDuration) == [target |-> targetId,amount |-> amount,encounter |-> encounterId, hasExplicit |-> hasExplicit,explicit |-> explicitDuration] AddBarrierResponseCardBoost(before, after, effectId, boost) == /\ effectId \notin DOMAIN before /\ after = [id \in DOMAIN before \cup {effectId} |-> IF id = effectId THEN boost ELSE before[id]] BarrierResponseCardBoostUnexpired(boost, liveEncounters, durationAlive(_)) == (boost.encounter # 0 /\ boost.encounter \in liveEncounters) \/ (boost.hasExplicit /\ durationAlive(boost.explicit)) BarrierResponseCardBoostsAfterCheckpoint(before, liveEncounters, durationAlive(_)) == [id \in {e \in DOMAIN before : BarrierResponseCardBoostUnexpired(before[e],liveEncounters,durationAlive)} |-> before[id]] BarrierResponseCardBoostCheckpointStep(before, after, liveEncounters, durationAlive(_), stage) == /\ stage = "ProcedureCode88eda145024f" /\ after = BarrierResponseCardBoostsAfterCheckpoint(before,liveEncounters,durationAlive) 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]) StandardResourceCountAllowed(count) == count \in Nat SideBHasExposureMarkersForResourceAction(effectiveExposureMarkerCount) == effectiveExposureMarkerCount \in Nat /\ effectiveExposureMarkerCount > 0 ResourceRetireBasicCost == [actionPoints |-> 1,resourceUnits |-> 2] 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 =============================================================================