---------------------------- MODULE TypeChecksMC ---------------------------- EXTENDS TypeContracts VARIABLE block3 Init3 == block3 \in 1..10 Next3 == UNCHANGED block3 Spec3 == Init3 /\ [][Next3]_block3 ProfileData3 == [c \in {"sideA","sideB","other"} |-> [kind |-> "Profile",side |-> IF c = "sideA" THEN "SideA" ELSE "SideB", owner |-> IF c = "sideA" THEN "SideA" ELSE "SideB"]] ProfileObject3(card) == [card |-> card,form |-> "Card",kind |-> "Profile",zone |-> "Play", deployed |-> FALSE,face |-> "Up",front |-> TRUE,activated |-> FALSE] ProfileFace3 == [kind |-> "Profile",side |-> "SideB",front |-> TRUE, minDeckSize |-> NumberPart(TRUE,45),importBudget |-> NumberPart(TRUE,15), baseLink |-> NumberPart(TRUE,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" RootObject3(kind, targetSite, area) == [form |-> "Card",kind |-> kind,deployed |-> TRUE,zone |-> "Play", targetSite |-> targetSite,area |-> area] ObjectiveObject3 == [card |-> "objective",form |-> "Card",kind |-> "Objective",deployed |-> TRUE, zone |-> "Play",face |-> "Down",activated |-> FALSE] ObjectiveData3 == [objective |-> [side |-> "SideA",kind |-> "Objective"]] 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) 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") 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" PlayEvent3(tag, object, kind, subtypes, actor, sideATurn) == [tag |-> tag,object |-> object,kind |-> kind,subtypes |-> subtypes, actor |-> actor,sideATurn |-> sideATurn] 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]) 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]) 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 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} CapacityFixtureDemand3 == [id \in 1..3 |-> IF id = 3 THEN 0 ELSE 2] CapacityFixtureAfter3(trashed) == [techniqueIds |-> DOMAIN CapacityFixtureDemand3 \ trashed, demand |-> [id \in DOMAIN CapacityFixtureDemand3 \ trashed |-> CapacityFixtureDemand3[id]], limit |-> 2,allocationFits |-> TRUE] 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] OnlyEmptyAfterRetire3(trashed) == [techniqueIds |-> {1} \ trashed,demand |-> [id \in {1} \ trashed |-> 2], limit |-> 2,allocationFits |-> 1 \in trashed] OmittedNewDemand3(trashed) == [techniqueIds |-> {3},demand |-> [id \in {} |-> 0],limit |-> 4,allocationFits |-> TRUE] DeployFitsWithoutRetire3(trashed) == [DeployFixtureAfter3(trashed) EXCEPT !.limit = 5] NoExplicitDuration3(duration) == FALSE Traversal10Duration3(duration) == duration.scope = "SchemaAtom138" /\ duration.token = 10 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,<>) /\ ~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) 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) 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 =============================================================================