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

TypeChecksMC

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.

This model/fact module also contains 88 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

BarrierChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

BarrierChecks3 ==
    LET dest == [zone |-> "Play",area |-> "Protecting",targetSiteKind |-> "SchemaAtom033"]
        barrierCard == [card |-> "barrierCard",form |-> "Card",kind |-> "Barrier",deployed |-> TRUE,
                zone |-> "Play",face |-> "Down",activated |-> FALSE,area |-> "Protecting"]
        activated == [barrierCard EXCEPT !.face = "Up",!.activated = TRUE]
        context == [inTraversal |-> TRUE,window |-> "ProcedureCode3a6daf593ad4",approachedObject |-> 7]
        data == [barrierCard |-> [kind |-> "Barrier",side |-> "SideA"]]
        traversalScope == BarrierTraversalStrengthScope(10,20,3)
        encounterScope == BarrierTraversalStrengthScope(0,20,3)
        checkpointScope == BarrierTraversalStrengthScope(0,0,3)
    IN /\ BarrierTermRefersToType("barrierCard") /\ BarrierTermRefersToType("piece of barrier")
       /\ BarrierDeployTypeLocation("SideA","Barrier",dest)
       /\ BarrierDeployTypeLocation("SideA","Barrier",[dest EXCEPT !.targetSiteKind = "SchemaAtom132"])
       /\ ~BarrierDeployTypeLocation("SideA","Barrier",[dest EXCEPT !.area = "Root"])
       /\ ~BarrierDeployTypeLocation("SideA","Facility",dest)
       /\ ProtectingCardTypeValid(barrierCard)
       /\ ~ProtectingCardTypeValid([barrierCard EXCEPT !.kind = "Attachment"])
       /\ StandardBarrierInsertion(<<1,2>>,<<1,2,3>>,3)
       /\ StandardBarrierInsertion(<<>>,<<3>>,3)
       /\ ~StandardBarrierInsertion(<<1,2>>,<<3,1,2>>,3)
       /\ ~StandardBarrierInsertion(<<1,2>>,<<1,2,2>>,2)
       /\ BarrierDeploymentPost(barrierCard) /\ ~DefaultActive(barrierCard,TRUE,data)
       /\ StandardBarrierActivationStep(barrierCard,activated,7,"SideA",context,TRUE,TRUE)
       /\ DefaultActive(activated,TRUE,data)
       /\ ~StandardBarrierActivationStep(barrierCard,activated,8,"SideA",context,TRUE,TRUE)
       /\ ~StandardBarrierActivationStep(barrierCard,activated,7,"SideA",[context EXCEPT !.inTraversal = FALSE],TRUE,TRUE)
       /\ ~StandardBarrierActivationStep(barrierCard,activated,7,"SideA",[context EXCEPT !.window = "ProcedureCode8b3260c0010f"],TRUE,TRUE)
       /\ ~StandardBarrierActivationStep(barrierCard,activated,7,"SideA",context,FALSE,TRUE)
       /\ {k \in SetupSideAKinds : SideAHasInherentDeployCost(k)} = {"Barrier"}
       /\ BarrierDeployResourceUnitCost(<<>>).amount = 0 /\ BarrierDeployResourceUnitCost(<<1,2,3>>).amount = 3
       /\ StrengthThresholdMet(-1,-1) /\ ~StrengthThresholdMet(-2,-1)
       /\ ~BarrierNormalItemInspectionDeploymentGate(barrierCard)
       /\ BarrierNormalItemInspectionDeploymentGate([barrierCard EXCEPT !.deployed = FALSE,!.zone = "SideAHand"])
       /\ ~ItemInspectionRetireCostOpportunity("SideB",barrierCard,FALSE,[exists |-> TRUE,amount |-> 0])
       /\ ItemInspectionRetireCostOpportunity("SideB",[barrierCard EXCEPT !.zone = "SideAHand",!.deployed = FALSE],TRUE,
                                     [exists |-> TRUE,amount |-> 0])
       /\ ~ItemInspectionRetireCostOpportunity("SideB",barrierCard,TRUE,[exists |-> FALSE,amount |-> 0])
       /\ BarrierInstructionOwnerKindValid("Barrier",<<>>) /\ BarrierInstructionOwnerKindValid("Barrier",<<1,2>>)
       /\ ~BarrierInstructionOwnerKindValid("Technique",<<1>>)
       /\ traversalScope = [scope |-> "SchemaAtom138",token |-> 10]
       /\ encounterScope = [scope |-> "Encounter",token |-> 20]
       /\ StrengthScopeAlive(traversalScope,{10},{20},3)
       /\ StrengthScopeAlive(traversalScope,{10},{},3)
       /\ ~StrengthScopeAlive(traversalScope,{11},{21},3)
       /\ StrengthScopeAlive(encounterScope,{}, {20},3)
       /\ ~StrengthScopeAlive(encounterScope,{}, {21},3)
       /\ StrengthScopeAlive(checkpointScope,{}, {},3)
       /\ ~StrengthScopeAlive(checkpointScope,{11},{21},4)
       /\ BarrierProtectionLayout.orientation = "Horizontal"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StrengthThresholdMet, DefaultActive, SetupSideAKinds, BarrierDeployResourceUnitCost, BarrierDeployTypeLocation, BarrierDeploymentPost, BarrierInstructionOwnerKindValid, BarrierNormalItemInspectionDeploymentGate, BarrierProtectionLayout, BarrierTermRefersToType, BarrierTraversalStrengthScope, ItemInspectionRetireCostOpportunity, ProtectingCardTypeValid, SideAHasInherentDeployCost, StandardBarrierActivationStep, StandardBarrierInsertion, StrengthScopeAlive

Block3Assertions · operator

reference-profile · input revision 2 · CC0 1.0

Block3Assertions == CASE block3 = 1 -> ProfileChecks3
 [] block3 = 2 -> ObjectiveChecks3
 [] block3 = 3 -> FacilityChecks3
 [] block3 = 4 -> BarrierChecks3
 [] block3 = 5 -> OperationChecks3
 [] block3 = 6 -> UpgradeChecks3
 [] block3 = 7 -> EventChecks3
 [] block3 = 8 -> EquipmentChecks3
 [] block3 = 9 -> TechniqueChecks3
 [] block3 = 10 -> ResourceChecks3

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BarrierChecks3, EquipmentChecks3, EventChecks3, FacilityChecks3, ObjectiveChecks3, OperationChecks3, ProfileChecks3, ResourceChecks3, TechniqueChecks3, UpgradeChecks3, block3

CapacityFixtureAfter3 · operator

reference-profile · input revision 2 · CC0 1.0

CapacityFixtureAfter3(trashed) ==
    [techniqueIds |-> DOMAIN CapacityFixtureDemand3 \ trashed,
     demand |-> [id \in DOMAIN CapacityFixtureDemand3 \ trashed |-> CapacityFixtureDemand3[id]],
     limit |-> 2,allocationFits |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CapacityFixtureDemand3

CapacityFixtureDemand3 · operator

reference-profile · input revision 2 · CC0 1.0

CapacityFixtureDemand3 == [id \in 1..3 |-> IF id = 3 THEN 0 ELSE 2]

Exact module download · Source bundle and reproduction instructions

DeployFitsWithoutRetire3 · operator

reference-profile · input revision 2 · CC0 1.0

DeployFitsWithoutRetire3(trashed) == [DeployFixtureAfter3(trashed) EXCEPT !.limit = 5]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DeployFixtureAfter3

DeployFixtureAfter3 · operator

reference-profile · input revision 2 · CC0 1.0

DeployFixtureAfter3(trashed) ==
    LET ids == ({1,2} \ trashed) \cup {3}
    IN [techniqueIds |-> ids,demand |-> [id \in ids |-> IF id = 3 THEN 1 ELSE 2],
        limit |-> 4,allocationFits |-> TRUE]

Exact module download · Source bundle and reproduction instructions

EquipmentChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

EquipmentChecks3 ==
    LET equipment == [card |-> "h",form |-> "Card",kind |-> "Equipment",
                     zone |-> "Play",deployed |-> TRUE,face |-> "Up",activated |-> FALSE]
        data == [h |-> [kind |-> "Equipment",side |-> "SideB"]]
        objects == [id \in 1..6 |-> IF id = 4 THEN [equipment EXCEPT !.kind = "Technique"] ELSE equipment]
        controllers == [id \in 1..6 |-> IF id = 5 THEN "SideA" ELSE "SideB"]
        active == [id \in 1..6 |-> id # 3]
        subtypes == [id \in 1..6 |-> IF id = 6 THEN {} ELSE {"SchemaAtom045"}]
        history == <<1,2,1,5,6>>
        correction == ConsoleCorrection(objects,controllers,active,subtypes,history,"SideB")
        deck == [id \in 1..6 |-> [equipment EXCEPT !.zone = "SideBDeck",!.deployed = FALSE]]
    IN /\ EquipmentTermRefersToType("equipment") /\ EquipmentTermRefersToType("piece of equipment")
       /\ SideBPaidDeployPost(equipment,"SideB","Equipment",TRUE,TRUE)
       /\ DefaultActive(equipment,TRUE,data)
       /\ ~SideBPaidDeployPost(equipment,"SideA","Equipment",TRUE,TRUE)
       /\ ~SideBPaidDeployPost(equipment,"SideB","Equipment",FALSE,TRUE)
       /\ ~SideBPaidDeployPost(equipment,"SideB","Equipment",TRUE,FALSE)
       /\ ~SideBPaidDeployPost([equipment EXCEPT !.face = "Down"],"SideB","Equipment",TRUE,TRUE)
       /\ StandardEquipmentCountAllowed(0) /\ StandardEquipmentCountAllowed(1000000)
       /\ ConsolePrintedDeclarationValid([printedSubtypes |-> {"SchemaAtom045"},printedConsoleLimit |-> 1])
       /\ ~ConsolePrintedDeclarationValid([printedSubtypes |-> {"SchemaAtom045"},printedConsoleLimit |-> 2])
       /\ ConsoleCandidates(objects,controllers,active,subtypes,"SideB") = {1,2}
       /\ ConsoleCandidates(objects,controllers,active,subtypes,"SideA") = {5}
       /\ LatestActiveConsole({1,2},history) = {1}
       /\ LatestActiveConsole({1,2},<<1,2>>) = {2}
       /\ correction.valid /\ correction.trash = {2} /\ ~correction.preventable
       /\ correction.checkpointStage = "ProcedureCodefe50c31480ea"
       /\ ConsoleCorrection(objects,controllers,active,subtypes,<<1,5>>,"SideB").valid = FALSE
       /\ ConsoleCorrection(objects,controllers,active,subtypes,history,"SideA").trash = {}
       /\ ConsoleCorrection(deck,controllers,[id \in 1..6 |-> FALSE],subtypes,<<>>,"SideB").trash = {}
       /\ ConsoleCorrection(deck,controllers,[id \in 1..6 |-> FALSE],subtypes,<<>>,"SideB").valid
       /\ ConsoleCandidates([objects EXCEPT ![2].deployed = FALSE],controllers,active,subtypes,"SideB") = {1}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive, ConsoleCandidates, ConsoleCorrection, ConsolePrintedDeclarationValid, EquipmentTermRefersToType, LatestActiveConsole, SideBPaidDeployPost, StandardEquipmentCountAllowed

EventChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

EventChecks3 ==
    LET ev == [card |-> "ev",form |-> "Card",kind |-> "Action",zone |-> "Play",
               deployed |-> FALSE,face |-> "Up",host |-> 0,subtypes |-> {"SchemaAtom043"}]
        sources == [id \in {7} |-> ev]
        empty == [id \in {} |-> ev]
        current == PlayedRetention("SchemaAtom048",5)
        scored == PlayEvent3("ObjectivePlacementd",0,"Objective",{},"SideA",5)
        played == PlayEvent3("Played",8,"Plan",{"SchemaAtom048"},"SideA",5)
        expired == EventRetentionAfterEvent(current,7,scored,sources)
        cleanup == [expired EXCEPT !.inPlay = FALSE,!.pendingRetire = FALSE]
        counter == [ev EXCEPT !.form = "Counter",!.kind = "SchemaAtom043",!.deployed = TRUE]
        lam == [kind |-> "Action",canonicalTitle |-> "Example Item B",printedSubtypes |-> {"SchemaAtom043"}]
    IN /\ EventPlayTypeAllowed("SideB","Action")
       /\ ~EventPlayTypeAllowed("SideA","Action")
       /\ ~EventPlayTypeAllowed("SideB","Support")
       /\ {k \in SetupSideBKinds : SideBHasPlayCost(k)} = {"Action"}
       /\ PlayedTypeNotDeployed(ev) /\ ~PlayedTypeNotDeployed([ev EXCEPT !.deployed = TRUE])
       /\ ~PlayedCardActive(ev,FALSE) /\ PlayedCardActive(ev,TRUE)
       /\ PlayedResolutionRetireDue(ev,TRUE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue(ev,FALSE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue(ev,TRUE,TRUE,FALSE)
       /\ ~PlayedResolutionRetireDue([ev EXCEPT !.zone = "Removed"],TRUE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue(counter,TRUE,FALSE,FALSE)
       /\ ExampleItemBConditionDeclaration(lam)
       /\ ~ExampleItemBConditionDeclaration([lam EXCEPT !.printedSubtypes = {}])
       /\ ConditionEventSelfDeployGate(ev,"OwnConversion",TRUE)
       /\ ~ConditionEventSelfDeployGate(ev,"DeployEffect",TRUE)
       /\ ~ConditionEventSelfDeployGate(ev,"OwnConversion",FALSE)
       /\ ConditionCounterPost("ev",counter)
       /\ EventCurrentExpires(7,scored)
       /\ ~EventCurrentExpires(7,[scored EXCEPT !.tag = "ObjectiveClaimedObjective"])
       /\ EventCurrentExpires(7,played)
       /\ ~EventCurrentExpires(7,[played EXCEPT !.object = 7])
       /\ ~EventCurrentExpires(7,[played EXCEPT !.subtypes = {}])
       /\ expired.pendingRetire /\ expired.inPlay
       /\ RetentionCheckpointStep(expired,cleanup,7,sources,"ProcedureCode88eda145024f")
       /\ ~RetentionReactionGate([id \in {7} |-> expired],sources)
       /\ RetentionReactionGate([id \in {7} |-> cleanup],empty)
       /\ ~EventRetentionAfterEvent(current,7,scored,empty).pendingRetire
       /\ ~EventRetentionAfterEvent(current,7,scored,[id \in {7} |-> counter]).pendingRetire

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupSideBKinds, PlayEvent3, ConditionCounterPost, ConditionEventSelfDeployGate, EventCurrentExpires, EventPlayTypeAllowed, EventRetentionAfterEvent, ExampleItemBConditionDeclaration, PlayedCardActive, PlayedResolutionRetireDue, PlayedRetention, PlayedTypeNotDeployed, RetentionCheckpointStep, RetentionReactionGate, SideBHasPlayCost

FacilityChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

FacilityChecks3 ==
    LET dest == [zone |-> "Play",area |-> "Root",targetSiteKind |-> "SchemaAtom132"]
        facility == [card |-> "facility",form |-> "Card",kind |-> "Facility",deployed |-> TRUE,
                  zone |-> "Play",face |-> "Down",activated |-> FALSE]
        activated == [facility EXCEPT !.face = "Up",!.activated = TRUE]
        data == [facility |-> [kind |-> "Facility",side |-> "SideA"]]
        zero == [exists |-> TRUE,amount |-> 0]
        noCost == [exists |-> FALSE,amount |-> 0]
        liberty == [kind |-> "Facility",canonicalTitle |-> "Example Item A",
                    printedSubtypes |-> {"SchemaAtom130"},printedRegionLimit |-> 1]
    IN /\ FacilityDeployTypeLocation("SideA","Facility",dest)
       /\ ~FacilityDeployTypeLocation("SideB","Facility",dest)
       /\ ~FacilityDeployTypeLocation("SideA","Facility",[dest EXCEPT !.targetSiteKind = "SchemaAtom033"])
       /\ ~FacilityDeployTypeLocation("SideA","Facility",[dest EXCEPT !.area = "Protecting"])
       /\ FacilityDeploymentPost(facility) /\ ~DefaultActive(facility,TRUE,data)
       /\ ~FacilityDeploymentPost(activated)
       /\ FacilityActivationStep(facility,activated,"SideA",TRUE,TRUE,TRUE)
       /\ DefaultActive(activated,TRUE,data)
       /\ ~FacilityActivationStep(facility,activated,"SideA",FALSE,TRUE,TRUE)
       /\ ~FacilityActivationStep(facility,activated,"SideA",TRUE,FALSE,TRUE)
       /\ ~FacilityActivationStep(facility,activated,"SideA",TRUE,TRUE,FALSE)
       /\ ~FacilityActivationStep(facility,activated,"SideB",TRUE,TRUE,TRUE)
       /\ ~FacilityActivationStep([facility EXCEPT !.deployed = FALSE],activated,"SideA",TRUE,TRUE,TRUE)
       /\ ~FacilityActivationStep(facility,[activated EXCEPT !.zone = "SideAObjectiveCompletion"],"SideA",TRUE,TRUE,TRUE)
       /\ ItemInspectionRetireCostOpportunity("SideB",facility,TRUE,zero)
       /\ ~ItemInspectionRetireCostOpportunity("SideB",[facility EXCEPT !.zone = "SideADiscard",!.deployed = FALSE],TRUE,zero)
       /\ ItemInspectionRetireCostOpportunity("SideB",[facility EXCEPT !.zone = "SideAHand",!.deployed = FALSE],TRUE,zero)
       /\ ~ItemInspectionRetireCostOpportunity("SideB",facility,FALSE,zero)
       /\ ~ItemInspectionRetireCostOpportunity("SideB",facility,TRUE,noCost)
       /\ ~ItemInspectionRetireCostOpportunity("SideA",facility,TRUE,zero)
       /\ ExampleItemARegionDeclaration(liberty)
       /\ ~ExampleItemARegionDeclaration([liberty EXCEPT !.printedSubtypes = {}])
       /\ ~ExampleItemARegionDeclaration([liberty EXCEPT !.printedRegionLimit = 2])
       /\ ~ObjectiveFacilityRootLimit([id \in {1,2} |->
            RootObject3(IF id = 1 THEN "Facility" ELSE "Objective","r1","Root")],"r1")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive, RootObject3, ExampleItemARegionDeclaration, FacilityActivationStep, FacilityDeployTypeLocation, FacilityDeploymentPost, ItemInspectionRetireCostOpportunity, ObjectiveFacilityRootLimit

Init3 · operator

reference-profile · input revision 2 · CC0 1.0

Init3 == block3 \in 1..10

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block3

Next3 · operator

reference-profile · input revision 2 · CC0 1.0

Next3 == UNCHANGED block3

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block3

NoExplicitDuration3 · operator

reference-profile · input revision 2 · CC0 1.0

NoExplicitDuration3(duration) == FALSE

Exact module download · Source bundle and reproduction instructions

ObjectiveChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveChecks3 ==
    LET auxiliarySite == [zone |-> "Play",area |-> "Root",targetSiteKind |-> "SchemaAtom132"]
        objective == ObjectiveObject3
        root == [id \in {1,2} |-> IF id = 1 THEN RootObject3("Objective","r1","Root")
                                 ELSE RootObject3("Attachment","r1","Root")]
        scored == [objective EXCEPT !.deployed = FALSE,!.zone = "SideAObjectiveCompletion",!.face = "Up"]
        faceup == [objective EXCEPT !.face = "Up"]
        meta == [kind |-> "Objective",progressRequirement |-> NumberPart(TRUE,3),
                 objectivePoints |-> NumberPart(TRUE,-1)]
    IN /\ ObjectiveDeployTypeLocation("SideA","Objective",auxiliarySite)
       /\ ~ObjectiveDeployTypeLocation("SideB","Objective",auxiliarySite)
       /\ ~ObjectiveDeployTypeLocation("SideA","Objective",[auxiliarySite EXCEPT !.targetSiteKind = "SchemaAtom033"])
       /\ ~ObjectiveDeployTypeLocation("SideA","Objective",[auxiliarySite EXCEPT !.area = "Protecting"])
       /\ ObjectiveFacilityRootLimit(root,"r1")
       /\ ~ObjectiveFacilityRootLimit([root EXCEPT ![2].kind = "Facility"],"r1")
       /\ ObjectiveFacilityRootLimit([root EXCEPT ![2].kind = "Facility",![2].targetSite = "r2"],"r1")
       /\ ObjectiveFacilityRootLimit([root EXCEPT ![2].kind = "Facility",![2].deployed = FALSE],"r1")
       /\ ObjectiveFacilityRootLimit([root EXCEPT ![2].kind = "Facility",![2].area = "CentralCards"],"r1")
       /\ ObjectiveCharacteristicSlotsValid(meta)
       /\ ~ObjectiveCharacteristicSlotsValid([meta EXCEPT !.kind = "Facility"])
       /\ ProgressThresholdMet(3,3) /\ ~ProgressThresholdMet(2,3)
       /\ ObjectivePointsInObjectiveArea(scored,"SideAObjectiveCompletion",-1) = -1
       /\ ObjectivePointsInObjectiveArea(scored,"SideBObjectiveCompletion",7) = 0
       /\ ObjectivePointsInObjectiveArea(objective,"Play",7) = 0
       /\ ObjectivePointsInObjectiveArea([scored EXCEPT !.form = "Counter"],"SideAObjectiveCompletion",7) = 0
       /\ ~ObjectiveCanActivation(objective) /\ ~ObjectiveCanActivation(faceup)
       /\ ObjectiveActivationStatus(objective) = "Dormant" /\ ObjectiveActivationStatus(faceup) = "Neither"
       /\ ~ObjectiveCardActive(objective,TRUE,ObjectiveData3)
       /\ ~ObjectiveCardActive(faceup,TRUE,ObjectiveData3)
       /\ ObjectiveCardActive(scored,TRUE,ObjectiveData3)
       /\ ~ObjectiveCardActive([scored EXCEPT !.zone = "SideBObjectiveCompletion"],TRUE,ObjectiveData3)
       /\ ~ObjectiveAbilityActive(faceup,TRUE,TRUE,ObjectiveData3,FALSE,FALSE,FALSE)
       /\ ObjectiveAbilityActive(faceup,TRUE,TRUE,ObjectiveData3,TRUE,FALSE,FALSE)
       /\ ObjectiveAbilityActive(objective,TRUE,TRUE,ObjectiveData3,TRUE,FALSE,FALSE)
       /\ ~ObjectiveAbilityActive(objective,TRUE,TRUE,ObjectiveData3,FALSE,FALSE,FALSE)
       /\ ObjectiveAbilityActive([scored EXCEPT !.zone = "SideBObjectiveCompletion"],TRUE,TRUE,ObjectiveData3,FALSE,TRUE,FALSE)
       /\ ObjectiveAbilityActive(objective,TRUE,TRUE,ObjectiveData3,FALSE,FALSE,TRUE)
       /\ ~ObjectiveAbilityActive(objective,FALSE,TRUE,ObjectiveData3,FALSE,FALSE,TRUE)
       /\ ObjectiveProgressEligible(objective) /\ ObjectiveProgressEligible(faceup)
       /\ ~ObjectiveProgressEligible(scored)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NumberPart, ProgressThresholdMet, ObjectiveData3, ObjectiveObject3, RootObject3, ObjectiveAbilityActive, ObjectiveActivationStatus, ObjectiveCanActivation, ObjectiveCardActive, ObjectiveCharacteristicSlotsValid, ObjectiveDeployTypeLocation, ObjectiveFacilityRootLimit, ObjectivePointsInObjectiveArea, ObjectiveProgressEligible

ObjectiveData3 · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveData3 == [objective |-> [side |-> "SideA",kind |-> "Objective"]]

Exact module download · Source bundle and reproduction instructions

ObjectiveObject3 · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveObject3 ==
    [card |-> "objective",form |-> "Card",kind |-> "Objective",deployed |-> TRUE,
     zone |-> "Play",face |-> "Down",activated |-> FALSE]

Exact module download · Source bundle and reproduction instructions

OmittedNewDemand3 · operator

reference-profile · input revision 2 · CC0 1.0

OmittedNewDemand3(trashed) ==
    [techniqueIds |-> {3},demand |-> [id \in {} |-> 0],limit |-> 4,allocationFits |-> TRUE]

Exact module download · Source bundle and reproduction instructions

OnlyEmptyAfterRetire3 · operator

reference-profile · input revision 2 · CC0 1.0

OnlyEmptyAfterRetire3(trashed) ==
    [techniqueIds |-> {1} \ trashed,demand |-> [id \in {1} \ trashed |-> 2],
     limit |-> 2,allocationFits |-> 1 \in trashed]

Exact module download · Source bundle and reproduction instructions

OperationChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

OperationChecks3 ==
    LET op == [card |-> "op",form |-> "Card",kind |-> "Plan",zone |-> "Play",
               deployed |-> FALSE,face |-> "Up",host |-> 0,subtypes |-> {"SchemaAtom043"}]
        sources == [id \in {1} |-> op]
        emptySources == [id \in {} |-> op]
        current == PlayedRetention("SchemaAtom048",5)
        Specimen0133 == PlayedRetention("SchemaAtom099",5)
        played == PlayEvent3("Played",2,"Action",{"SchemaAtom048"},"SideB",5)
        claimedObjective == PlayEvent3("ObjectiveClaimedObjective",0,"Objective",{},"SideB",5)
        sideATurn == PlayEvent3("TurnBegins",0,"Profile",{},"SideA",6)
        expired == OperationRetentionAfterEvent(current,1,played,sources)
        cleanup == [expired EXCEPT !.inPlay = FALSE,!.pendingRetire = FALSE]
        counter == [op EXCEPT !.form = "Counter",!.kind = "SchemaAtom043",!.deployed = TRUE]
    IN /\ OperationPlayTypeAllowed("SideA","Plan")
       /\ ~OperationPlayTypeAllowed("SideB","Plan")
       /\ ~OperationPlayTypeAllowed("SideA","Facility")
       /\ PlayedTypeNotDeployed(op)
       /\ ~PlayedTypeNotDeployed([op EXCEPT !.deployed = TRUE])
       /\ PlayedTypeNotDeployed(counter)
       /\ ~PlayedCardActive(op,FALSE) /\ PlayedCardActive(op,TRUE)
       /\ PlayedResolutionRetireDue(op,TRUE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue(op,FALSE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue(op,TRUE,TRUE,FALSE)
       /\ ~PlayedResolutionRetireDue(op,TRUE,FALSE,TRUE)
       /\ ~PlayedResolutionRetireDue([op EXCEPT !.zone = "Removed"],TRUE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue([op EXCEPT !.host = 9],TRUE,FALSE,FALSE)
       /\ ~PlayedResolutionRetireDue(counter,TRUE,FALSE,FALSE)
       /\ ConditionOperationSelfDeployGate(op,"OwnConversion",TRUE)
       /\ ~ConditionOperationSelfDeployGate(op,"DeployEffect",TRUE)
       /\ ~ConditionOperationSelfDeployGate(op,"OwnConversion",FALSE)
       /\ ConditionCounterPost("op",counter)
       /\ AnotherCurrentPlayed(1,played) /\ ~AnotherCurrentPlayed(2,played)
       /\ ~AnotherCurrentPlayed(1,[played EXCEPT !.subtypes = {}])
       /\ OperationCurrentExpires(1,claimedObjective)
       /\ ~OperationCurrentExpires(1,[claimedObjective EXCEPT !.tag = "ObjectivePlacementd"])
       /\ expired.pendingRetire /\ expired.inPlay /\ ~expired.live
       /\ OperationRetentionAfterEvent(current,1,[played EXCEPT !.object = 1],sources) = current
       /\ OperationRetentionAfterEvent(Specimen0133,1,sideATurn,sources).pendingRetire
       /\ ~OperationRetentionAfterEvent(Specimen0133,1,[sideATurn EXCEPT !.actor = "SideB"],sources).pendingRetire
       /\ ~OperationRetentionAfterEvent(Specimen0133,1,[sideATurn EXCEPT !.sideATurn = 5],sources).pendingRetire
       /\ ~OperationRetentionAfterEvent(PlayedRetention("NoValue",5),1,played,sources).pendingRetire
       /\ RetentionCheckpointStep(expired,cleanup,1,sources,"ProcedureCode88eda145024f")
       /\ ~RetentionCheckpointStep(expired,cleanup,1,sources,"BeforeCheckpoint")
       /\ ~RetentionReactionGate([id \in {1} |-> expired],sources)
       /\ RetentionReactionGate([id \in {1} |-> cleanup],emptySources)
       /\ RetentionReactionGate([id \in {1} |-> expired],emptySources)
       /\ RetentionCheckpointStep(expired,cleanup,1,emptySources,"ProcedureCode88eda145024f")
       /\ RetentionCheckpointStep([expired EXCEPT !.inPlay = FALSE],cleanup,
                                  1,emptySources,"ProcedureCode88eda145024f")
       /\ ~OperationRetentionAfterEvent(current,1,played,emptySources).pendingRetire
       /\ ~OperationRetentionAfterEvent(current,1,played,[id \in {1} |-> counter]).pendingRetire
       /\ ~OperationRetentionAfterEvent(current,1,played,[id \in {1} |-> [op EXCEPT !.host = 9]]).pendingRetire
       /\ RetentionReactionGate([id \in {1} |-> expired],[id \in {1} |-> counter])
       /\ RetentionCheckpointStep(expired,[expired EXCEPT !.live = FALSE,!.pendingRetire = FALSE],
                                  1,[id \in {1} |-> counter],"ProcedureCode88eda145024f")
       /\ RetentionCheckpointStep(expired,cleanup,1,
             [id \in {1} |-> [op EXCEPT !.zone = "SideAHand"]],"ProcedureCode88eda145024f")
       /\ RetentionReactionGate([id \in {1} |-> expired],[id \in {2} |-> op])
       /\ RetentionCheckpointStep(expired,cleanup,1,[id \in {2} |-> op],"ProcedureCode88eda145024f")
       /\ {k \in SetupSideAKinds : SideAHasPlayCost(k)} = {"Plan"}
       /\ ItemInspectionRetireCostOpportunity("SideB",[op EXCEPT !.zone = "SideAHand"],TRUE,
                                     [exists |-> TRUE,amount |-> 0])
       /\ ~ItemInspectionRetireCostOpportunity("SideB",op,TRUE,[exists |-> FALSE,amount |-> 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupSideAKinds, PlayEvent3, AnotherCurrentPlayed, ConditionCounterPost, ConditionOperationSelfDeployGate, ItemInspectionRetireCostOpportunity, OperationCurrentExpires, OperationPlayTypeAllowed, OperationRetentionAfterEvent, PlayedCardActive, PlayedResolutionRetireDue, PlayedRetention, PlayedTypeNotDeployed, RetentionCheckpointStep, RetentionReactionGate, SideAHasPlayCost

PlayEvent3 · operator

reference-profile · input revision 2 · CC0 1.0

PlayEvent3(tag, object, kind, subtypes, actor, sideATurn) ==
    [tag |-> tag,object |-> object,kind |-> kind,subtypes |-> subtypes,
     actor |-> actor,sideATurn |-> sideATurn]

Exact module download · Source bundle and reproduction instructions

ProfileChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

ProfileChecks3 ==
    LET sideA == ProfileObject3("sideA")
        sideB == ProfileObject3("sideB")
        objects == [id \in {1,2} |-> IF id = 1 THEN sideA ELSE sideB]
        back == [ProfileFace3 EXCEPT !.front = FALSE,
                 !.minDeckSize = NoNumber,!.importBudget = NoNumber]
    IN /\ StartingProfilesValid(objects,ProfileData3)
       /\ ~StartingProfilesValid([id \in {1} |-> sideA],ProfileData3)
       /\ ~StartingProfilesValid([id \in {1,2,3} |->
            IF id = 1 THEN sideA ELSE IF id = 2 THEN sideB ELSE ProfileObject3("other")],ProfileData3)
       /\ ~StartingProfilesValid([objects EXCEPT ![2].deployed = TRUE],ProfileData3)
       /\ ~StartingProfilesValid([objects EXCEPT ![2].front = FALSE],ProfileData3)
       /\ ProfileFaceActive(sideB,TRUE,TRUE,ProfileData3)
       /\ ~ProfileFaceActive(sideB,FALSE,TRUE,ProfileData3)
       /\ ProfileFaceActive([sideB EXCEPT !.front = FALSE],FALSE,TRUE,ProfileData3)
       /\ ~ProfileFaceActive([sideB EXCEPT !.front = FALSE],TRUE,TRUE,ProfileData3)
       /\ ~ProfileFaceActive(sideB,TRUE,FALSE,ProfileData3)
       /\ ProfileObjectValid([sideB EXCEPT !.form = "Counter",!.deployed = TRUE])
       /\ ProfileFaceValuesValid(ProfileFace3) /\ ProfileFaceValuesValid(back)
       /\ ~ProfileFaceValuesValid([back EXCEPT !.minDeckSize = NumberPart(TRUE,45)])
       /\ ~ProfileFaceValuesValid([ProfileFace3 EXCEPT !.side = "SideA"])
       /\ ProfileDeckValues(ProfileFace3,"Deckbuilding",0,0).minimum.amount = 45
       /\ ProfileDeckValues(ProfileFace3,"Deckbuilding",0,0).importBudget.amount = 15
       /\ ~ProfileDeckValues(back,"Deckbuilding",0,0).applicable
       /\ ~ProfileDeckValues(ProfileFace3,"SchemaAtom076",0,0).applicable
       /\ ~ProfileDeckValues(ProfileFace3,"SchemaAtom076",0,0).minimum.exists
       /\ BaseLinkPart(ProfileFace3,0) = [exists |-> TRUE,amount |-> 0]
       /\ ProfileTargetSiteSpecimen0139(sideA,ProfileData3) = "SchemaAtom082"
       /\ ProfileTargetSiteSpecimen0139(sideB,ProfileData3) = "NoValue"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BaseLinkPart, NoNumber, NumberPart, ProfileData3, ProfileFace3, ProfileObject3, ProfileDeckValues, ProfileFaceActive, ProfileFaceValuesValid, ProfileObjectValid, ProfileTargetSiteSpecimen0139, StartingProfilesValid

ProfileData3 · operator

reference-profile · input revision 2 · CC0 1.0

ProfileData3 ==
    [c \in {"sideA","sideB","other"} |->
        [kind |-> "Profile",side |-> IF c = "sideA" THEN "SideA" ELSE "SideB",
         owner |-> IF c = "sideA" THEN "SideA" ELSE "SideB"]]

Exact module download · Source bundle and reproduction instructions

ProfileFace3 · operator

reference-profile · input revision 2 · CC0 1.0

ProfileFace3 ==
    [kind |-> "Profile",side |-> "SideB",front |-> TRUE,
     minDeckSize |-> NumberPart(TRUE,45),importBudget |-> NumberPart(TRUE,15),
     baseLink |-> NumberPart(TRUE,0)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NumberPart

ProfileObject3 · operator

reference-profile · input revision 2 · CC0 1.0

ProfileObject3(card) ==
    [card |-> card,form |-> "Card",kind |-> "Profile",zone |-> "Play",
     deployed |-> FALSE,face |-> "Up",front |-> TRUE,activated |-> FALSE]

Exact module download · Source bundle and reproduction instructions

ResourceChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

ResourceChecks3 ==
    LET resource == [card |-> "r",form |-> "Card",kind |-> "Support",
                     zone |-> "Play",deployed |-> TRUE,face |-> "Up",activated |-> FALSE]
        data == [r |-> [kind |-> "Support",side |-> "SideB"]]
        context == [turn |-> "SideA",phase |-> "NeutralValue00001",basicActionAvailable |-> TRUE]
        types == {"Support"}
    IN /\ SideBPaidDeployPost(resource,"SideB","Support",TRUE,TRUE)
       /\ DefaultActive(resource,TRUE,data)
       /\ ~SideBPaidDeployPost(resource,"SideA","Support",TRUE,TRUE)
       /\ ~SideBPaidDeployPost(resource,"SideB","Equipment",TRUE,TRUE)
       /\ ~SideBPaidDeployPost(resource,"SideB","Support",FALSE,TRUE)
       /\ ~SideBPaidDeployPost(resource,"SideB","Support",TRUE,FALSE)
       /\ ~SideBPaidDeployPost([resource EXCEPT !.face = "Down"],"SideB","Support",TRUE,TRUE)
       /\ ~SideBPaidDeployPost([resource EXCEPT !.zone = "SideBDiscard"],"SideB","Support",TRUE,TRUE)
       /\ StandardResourceCountAllowed(0) /\ StandardResourceCountAllowed(1000000)
       /\ ~StandardResourceCountAllowed(-1)
       /\ ~SideBHasExposureMarkersForResourceAction(0)
       /\ SideBHasExposureMarkersForResourceAction(1) /\ SideBHasExposureMarkersForResourceAction(3)
       /\ ResourceRetireBasicCost = [actionPoints |-> 1,resourceUnits |-> 2]
       /\ ResourceRetireBasicActionLocalGate("SideA",resource,types,context,1,TRUE,TRUE)
       /\ ResourceRetireBasicActionLocalGate("SideA",resource,types,context,3,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideB",resource,types,context,1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,types,[context EXCEPT !.turn = "SideB"],1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,types,[context EXCEPT !.phase = "Discard"],1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,types,[context EXCEPT !.basicActionAvailable = FALSE],1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,types,context,0,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",[resource EXCEPT !.deployed = FALSE],types,context,1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",[resource EXCEPT !.form = "Counter"],types,context,1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",[resource EXCEPT !.zone = "SideBDiscard"],types,context,1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,{},context,1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,{"Technique"},context,1,TRUE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,types,context,1,FALSE,TRUE)
       /\ ~ResourceRetireBasicActionLocalGate("SideA",resource,types,context,1,TRUE,FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive, ResourceRetireBasicActionLocalGate, ResourceRetireBasicCost, SideBHasExposureMarkersForResourceAction, SideBPaidDeployPost, StandardResourceCountAllowed

RootObject3 · operator

reference-profile · input revision 2 · CC0 1.0

RootObject3(kind, targetSite, area) ==
    [form |-> "Card",kind |-> kind,deployed |-> TRUE,zone |-> "Play",
     targetSite |-> targetSite,area |-> area]

Exact module download · Source bundle and reproduction instructions

Spec3 · operator

reference-profile · input revision 2 · CC0 1.0

Spec3 == Init3 /\ [][Next3]_block3

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Init3, Next3, block3

TechniqueChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueChecks3 ==
    LET technique == [card |-> "p",form |-> "Card",kind |-> "Technique",deployed |-> TRUE,
                    zone |-> "Play",face |-> "Up",activated |-> FALSE]
        objects == [id \in {1,2} |-> technique]
        types == [id \in {1,2} |-> {"Technique"}]
        capacity == [id \in {1,2} |-> [exists |-> TRUE,amount |-> 2]]
        data == [p |-> [kind |-> "Technique",side |-> "SideB"]]
        printed == [kind |-> "Technique",printedBarrierResponseCard |-> TRUE,printedAlliance |-> FALSE,
                    printedSubtypes |-> {"SchemaAtom086","SchemaAtom073"},strength |-> NumberPart(TRUE,0),
                    capacityCost |-> NumberPart(TRUE,2),playCost |-> NoNumber,
                    deployCost |-> NumberPart(TRUE,3),activationCost |-> NoNumber]
        ability == [isInterface |-> TRUE,interfaceFlag |-> "Interface",presentActive |-> TRUE,
                    restriction |-> [present |-> TRUE,name |-> "SchemaSymbol001"]]
        context == [encounterActive |-> TRUE,step |-> "ProcedureCode8b3260c0010f",barrierId |-> 9,
                    barrierForm |-> "Card",barrierKind |-> "Barrier",barrierInstructions |-> {1,2}]
        cardTarget == [kind |-> "Card",object |-> 9,barrierInstruction |-> 0]
        subTarget == [kind |-> "BarrierInstruction",object |-> 9,barrierInstruction |-> 1]
        strength == [exists |-> TRUE,amount |-> 3]
        absent == [exists |-> FALSE,amount |-> 0]
        noneDuration == [scope |-> "NoValue",token |-> 0]
        traversalDuration == [scope |-> "SchemaAtom138",token |-> 10]
        emptyBoosts == [id \in {} |-> id]
        implicit == BarrierResponseCardBoost(1,1,20,FALSE,noneDuration)
        explicit == BarrierResponseCardBoost(1,2,20,TRUE,traversalDuration)
        outside == BarrierResponseCardBoost(1,1,0,FALSE,noneDuration)
        boosts == [id \in {1,2} |-> IF id = 1 THEN implicit ELSE explicit]
        afterEncounter == BarrierResponseCardBoostsAfterCheckpoint(boosts,{},Traversal10Duration3)
    IN /\ SideBPaidDeployPost(technique,"SideB","Technique",TRUE,TRUE)
       /\ DefaultActive(technique,TRUE,data)
       /\ TechniqueCapacityDemand(objects,types,capacity) = [id \in {1,2} |-> 2]
       /\ SumMap(TechniqueCapacityDemand([objects EXCEPT ![1].deployed = FALSE],types,capacity)) = 2
       /\ SumMap(TechniqueCapacityDemand(objects,[types EXCEPT ![1] = {}],capacity)) = 2
       /\ SumMap(TechniqueCapacityDemand(objects,types,[capacity EXCEPT ![1].amount = -1])) = 1
       /\ TechniqueCapacityArithmeticFits([one |-> -1,two |-> 2],1)
       /\ ~TechniqueCapacityLegal([one |-> 2],2,FALSE)
       /\ ~CapacityFits([restrictedDemand |-> 2],[one |-> 2],[restrictedDemand |-> {}])
       /\ TechniqueDeployCapacityChoice({1,2},3,{1},DeployFixtureAfter3)
       /\ ~TechniqueDeployCapacityChoice({1,2},3,{},DeployFixtureAfter3)
       /\ ~TechniqueDeployCapacityChoice({1,2},3,{3},DeployFixtureAfter3)
       /\ ~TechniqueDeployCapacityChoice({1,2},3,{},OmittedNewDemand3)
       /\ ~TechniqueDeployCapacityChoice({1,2},3,{99},DeployFitsWithoutRetire3)
       /\ TechniqueCapacityCheckpointChoice({1,2,3},{1},CapacityFixtureAfter3)
       /\ ~TechniqueCapacityCheckpointChoice({1,2,3},{1,3},CapacityFixtureAfter3)
       /\ ~TechniqueCapacityCheckpointChoice({1,2,3},{1,2},CapacityFixtureAfter3)
       /\ TechniqueCapacityCheckpointChoice({1},{1},OnlyEmptyAfterRetire3)
       /\ TechniqueCapacityRepairTiming("DeployingTechnique") = "DuringDeploy"
       /\ TechniqueCapacityRepairTiming("LimitDecreased") = "NextCheckpoint10.3.1e"
       /\ TechniqueCapacityRepairTiming("DemandIncreased") = "NextCheckpoint10.3.1e"
       /\ TechniqueResourceUnitAndCapacity(printed,0,<<>>,<<3>>,FALSE,0).resourceUnitCost = 0
       /\ TechniqueResourceUnitAndCapacity(printed,0,<<>>,<<3>>,FALSE,0).capacity.amount = 2
       /\ TechniqueResourceUnitAndCapacity(printed,0,<<>>,<<>>,TRUE,0).capacity.amount = 2
       /\ TechniqueStrengthMetadataValid(printed)
       /\ TechniqueStrengthMetadataValid([printed EXCEPT !.printedBarrierResponseCard = FALSE,
              !.printedSubtypes = {},!.strength = NoNumber])
       /\ StrengthLayout([printed EXCEPT !.printedBarrierResponseCard = FALSE,!.strength = NoNumber]).icon = "SchemaAtom052"
       /\ StrengthPart(printed,0) = [exists |-> TRUE,amount |-> 0]
       /\ PrintedBarrierResponseCardInterfacesValid(printed,<<ability>>)
       /\ ~PrintedBarrierResponseCardInterfacesValid(printed,<<>>)
       /\ InterfaceFlagValid(ability)
       /\ ~InterfaceFlagValid([ability EXCEPT !.interfaceFlag = "NoValue"])
       /\ InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom086"},ability,context,
                                    strength,strength,{"SchemaSymbol001"},{cardTarget,subTarget})
       /\ ~InterfaceAbilityLocalGate("SideA",technique,{"SchemaAtom086"},ability,context,
                                    strength,strength,{"SchemaSymbol001"},{cardTarget})
       /\ ~InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom086"},ability,
              [context EXCEPT !.step = "ProcedureCode3a6daf593ad4"],strength,strength,{"SchemaSymbol001"},{cardTarget})
       /\ ~InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom086"},ability,context,
              [strength EXCEPT !.amount = 2],strength,{"SchemaSymbol001"},{cardTarget})
       /\ ~InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom086"},ability,context,
                                    absent,strength,{"SchemaSymbol001"},{cardTarget})
       /\ ~InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom086"},ability,context,
                                    strength,strength,{"Sentry"},{cardTarget})
       /\ InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom086"},
              [ability EXCEPT !.restriction = [present |-> FALSE,name |-> ""]],context,
              strength,strength,{"Sentry"},{cardTarget})
       /\ InterfaceAbilityLocalGate("SideB",technique,{"SchemaAtom180"},ability,context,
                                    absent,strength,{"SchemaSymbol001"},{subTarget})
       /\ ~InterfaceTargetsAllowed({[cardTarget EXCEPT !.object = 8]},9,{1,2})
       /\ ~InterfaceTargetsAllowed({[subTarget EXCEPT !.barrierInstruction = 3]},9,{1,2})
       /\ AddBarrierResponseCardBoost(emptyBoosts,[id \in {1} |-> implicit],1,implicit)
       /\ ~AddBarrierResponseCardBoost(boosts,boosts,1,implicit)
       /\ BarrierResponseCardBoostUnexpired(implicit,{20},NoExplicitDuration3)
       /\ ~BarrierResponseCardBoostUnexpired(implicit,{21},NoExplicitDuration3)
       /\ BarrierResponseCardBoostUnexpired(explicit,{},Traversal10Duration3)
       /\ BarrierResponseCardBoostUnexpired(explicit,{20},NoExplicitDuration3)
       /\ ~BarrierResponseCardBoostUnexpired(explicit,{},NoExplicitDuration3)
       /\ DOMAIN afterEncounter = {2}
       /\ BarrierResponseCardBoostTotal(boosts,1,{1}) = 3
       /\ BarrierResponseCardBoostTotal(afterEncounter,1,{1}) = 2
       /\ BarrierResponseCardBoostsAfterCheckpoint(afterEncounter,{},NoExplicitDuration3) = emptyBoosts
       /\ BarrierResponseCardBoostTotal([id \in {1} |-> outside],1,{1}) = 1
       /\ BarrierResponseCardBoostsAfterCheckpoint([id \in {1} |-> outside],{},NoExplicitDuration3) = emptyBoosts
       /\ BarrierResponseCardBoostUnexpired(BarrierResponseCardBoost(1,1,0,TRUE,traversalDuration),{},Traversal10Duration3)
       /\ BarrierResponseCardBoostUnexpired(BarrierResponseCardBoost(1,1,20,TRUE,[scope |-> "SchemaAtom138",token |-> 0]),
                                   {20},Traversal10Duration3)
       /\ ~BarrierResponseCardBoostUnexpired(BarrierResponseCardBoost(1,1,20,TRUE,[scope |-> "SchemaAtom138",token |-> 0]),
                                    {},Traversal10Duration3)
       /\ BarrierResponseCardBoostCheckpointStep(boosts,afterEncounter,{},Traversal10Duration3,"ProcedureCode88eda145024f")
       /\ ~BarrierResponseCardBoostCheckpointStep(boosts,afterEncounter,{},Traversal10Duration3,"EncounterEnds")
       /\ BarrierResponseCardBoostTotal(boosts,1,{2}) = 0 /\ BarrierResponseCardBoostTotal(boosts,2,{2}) = 0
       /\ \A implicitAlive,explicitAlive \in BOOLEAN :
            BarrierResponseCardBoostUnexpired(
                BarrierResponseCardBoost(1,1,IF implicitAlive THEN 20 ELSE 0,explicitAlive,traversalDuration),
                {20},Traversal10Duration3) = (implicitAlive \/ explicitAlive)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CapacityFits, SumMap, NoNumber, NumberPart, StrengthLayout, StrengthPart, DefaultActive, CapacityFixtureAfter3, DeployFitsWithoutRetire3, DeployFixtureAfter3, NoExplicitDuration3, OmittedNewDemand3, OnlyEmptyAfterRetire3, Traversal10Duration3, AddBarrierResponseCardBoost, BarrierResponseCardBoost, BarrierResponseCardBoostCheckpointStep, BarrierResponseCardBoostTotal, BarrierResponseCardBoostUnexpired, BarrierResponseCardBoostsAfterCheckpoint, InterfaceAbilityLocalGate, InterfaceFlagValid, InterfaceTargetsAllowed, PrintedBarrierResponseCardInterfacesValid, SideBPaidDeployPost, TechniqueCapacityArithmeticFits, TechniqueCapacityCheckpointChoice, TechniqueCapacityDemand, TechniqueCapacityLegal, TechniqueCapacityRepairTiming, TechniqueDeployCapacityChoice, TechniqueResourceUnitAndCapacity, TechniqueStrengthMetadataValid

Traversal10Duration3 · operator

reference-profile · input revision 2 · CC0 1.0

Traversal10Duration3(duration) == duration.scope = "SchemaAtom138" /\ duration.token = 10

Exact module download · Source bundle and reproduction instructions

UpgradeChecks3 · operator

reference-profile · input revision 2 · CC0 1.0

UpgradeChecks3 ==
    LET dest == [zone |-> "Play",area |-> "Root",targetSiteKind |-> "SchemaAtom033",targetSite |-> "SchemaAtom082"]
        upgrade == [card |-> "u",form |-> "Card",kind |-> "Attachment",deployed |-> TRUE,
                    zone |-> "Play",face |-> "Down",activated |-> FALSE,
                    area |-> "Root",targetSiteKind |-> "SchemaAtom033",targetSite |-> "SchemaAtom082",
                    subtypes |-> {"SchemaAtom130"},active |-> FALSE]
        activated == [upgrade EXCEPT !.face = "Up",!.activated = TRUE]
        data == [u |-> [kind |-> "Attachment",side |-> "SideA"]]
        empty == [id \in {} |-> upgrade]
        old == [id \in {1} |-> upgrade]
        pending == [id \in {2} |->
                    [form |-> "Card",kind |-> "Attachment",subtypes |-> {"SchemaAtom130"},destination |-> dest]]
        two == [id \in {1,2} |-> upgrade]
    IN /\ UpgradeDeployTypeLocation("SideA","Attachment",dest)
       /\ UpgradeDeployTypeLocation("SideA","Attachment",[dest EXCEPT !.targetSiteKind = "SchemaAtom132"])
       /\ ~UpgradeDeployTypeLocation("SideA","Facility",dest)
       /\ ~UpgradeDeployTypeLocation("SideA","Attachment",[dest EXCEPT !.area = "Protecting"])
       /\ CentralRootCardTypeValid(upgrade)
       /\ ~CentralRootCardTypeValid([upgrade EXCEPT !.kind = "Objective"])
       /\ \A n \in 0..20 : StandardUpgradeCountAllowed(n)
       /\ StandardUpgradeCountAllowed(1000000)
       /\ UpgradeDeploymentPost(upgrade) /\ ~DefaultActive(upgrade,TRUE,data)
       /\ UpgradeActivationStep(upgrade,activated,"SideA",TRUE,TRUE,TRUE)
       /\ DefaultActive(activated,TRUE,data)
       /\ ~UpgradeActivationStep(upgrade,activated,"SideA",FALSE,TRUE,TRUE)
       /\ ~UpgradeActivationStep(upgrade,activated,"SideA",TRUE,FALSE,TRUE)
       /\ RegionPrintedDeclarationValid([printedSubtypes |-> {"SchemaAtom130"},printedRegionLimit |-> 1])
       /\ ~RegionPrintedDeclarationValid([printedSubtypes |-> {"SchemaAtom130"},printedRegionLimit |-> 2])
       /\ DeployedRootRegions(old,"SchemaAtom082") = {1}
       /\ DeployedRootRegions([old EXCEPT ![1].active = TRUE],"SchemaAtom082") = {1}
       /\ DeployedRootRegions([old EXCEPT ![1].kind = "Facility"],"SchemaAtom082") = {1}
       /\ DeployedRootRegions([old EXCEPT ![1].kind = "Barrier"],"SchemaAtom082") = {}
       /\ DeployedRootRegions([old EXCEPT ![1].area = "CentralCards"],"SchemaAtom082") = {}
       /\ DeployedRootRegions([old EXCEPT ![1].deployed = FALSE],"SchemaAtom082") = {}
       /\ RegionRootLimit(old,empty,"SchemaAtom082") /\ RegionRootLimit(empty,pending,"SchemaAtom082")
       /\ ~RegionRootLimit(old,pending,"SchemaAtom082")
       /\ ~RegionRootLimit(two,empty,"SchemaAtom082")
       /\ RegionRootLimit([two EXCEPT ![2].targetSite = "r1"],empty,"SchemaAtom082")
       /\ RegionRequiredOldRetire(old,2,upgrade,dest) = {1}
       /\ RegionRequiredOldRetire(old,2,[upgrade EXCEPT !.subtypes = {}],dest) = {}
       /\ RegionRequiredOldRetire(old,2,[upgrade EXCEPT !.kind = "Barrier"],dest) = {}
       /\ RegionReplacementRetireSatisfied({1},{1,3})
       /\ ~RegionReplacementRetireSatisfied({1},{})
       /\ ~RegionMoveSwapGate(two,empty,{"SchemaAtom082"})
       /\ RegionMoveSwapGate([two EXCEPT ![2].targetSite = "r1"],empty,{"SchemaAtom082","r1"})
       /\ ItemInspectionRetireCostOpportunity("SideB",upgrade,TRUE,[exists |-> TRUE,amount |-> 0])
       /\ ~ItemInspectionRetireCostOpportunity("SideB",[upgrade EXCEPT !.zone = "SideADiscard"],TRUE,
                                      [exists |-> TRUE,amount |-> 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultActive, CentralRootCardTypeValid, DeployedRootRegions, ItemInspectionRetireCostOpportunity, RegionMoveSwapGate, RegionPrintedDeclarationValid, RegionReplacementRetireSatisfied, RegionRequiredOldRetire, RegionRootLimit, StandardUpgradeCountAllowed, UpgradeActivationStep, UpgradeDeployTypeLocation, UpgradeDeploymentPost

block3 · variable

reference-profile · input revision 2 · CC0 1.0

block3

Exact module download · Source bundle and reproduction instructions