---------------------------- MODULE LocationChecksMC ---------------------------- EXTENDS LocationContracts VARIABLE block4 Init4 == block4 \in 1..9 Next4 == UNCHANGED block4 Spec4 == Init4 /\ [][Next4]_block4 ZoneFixture4 == [z \in ZoneInstances4 |-> IF z = "SideAHand" THEN {1,2} ELSE {}] ZoneGeneralChecks4 == LET before == ZoneFixture4 after == [before EXCEPT !["SideAHand"] = {2},!["Play"] = {1}] framedBefore == [before EXCEPT !["SideBHand"] = {3}] framedAfter == [after EXCEPT !["SideBHand"] = {3}] object == [host |-> 0,zone |-> "SideADeck"] noPlayLocation == [kind |-> "Zone",zone |-> "Play"] IN /\ Cardinality(ZoneTypes4) = 8 /\ Cardinality(ZoneInstances4) = 12 /\ {ZoneType4(z) : z \in ZoneInstances4} = ZoneTypes4 /\ "Outside" \notin ZoneInstances4 /\ "Removed" \in ZoneInstances4 /\ \A z \in CounterPlayAliases4 : CanonicalZone4(z) = "Play" /\ CanonicalZone4("SideADeck") = "SideADeck" /\ ZonePartition4({1,2},before) /\ ~ZonePartition4({1,2},[before EXCEPT !["Play"] = {1}]) /\ ~ZonePartition4({1,2,3},before) /\ AtomicZoneMove4({1,2},before,after,1,"SideAHand","Play",TRUE,FALSE,FALSE) /\ ~AtomicZoneMove4({1,2},before,after,1,"SideAHand","Play",FALSE,FALSE,FALSE) /\ ~AtomicZoneMove4({1,2},before,after,1,"SideAHand","Play",TRUE,TRUE,FALSE) /\ AtomicZoneMove4({1,2},before,after,1,"SideAHand","Play",TRUE,TRUE,TRUE) /\ AtomicZoneMove4({1,2,3},framedBefore,framedAfter,1,"SideAHand","Play",TRUE,FALSE,FALSE) /\ ~AtomicZoneMove4({1,2,3},framedBefore, [framedAfter EXCEPT !["SideBHand"] = {}],1,"SideAHand","Play",TRUE,FALSE,FALSE) /\ ~AtomicZoneMove4({1,2},before,[after EXCEPT !["SideAHand"] = {1,2}],1,"SideAHand","Play",TRUE,FALSE,FALSE) /\ ~AtomicZoneMove4({1,2},before,[after EXCEPT !["Play"] = {}],1,"SideAHand","Play",TRUE,FALSE,FALSE) /\ ~AtomicZoneMove4({1,2},before,after,1,"SideAHand","Outside",TRUE,FALSE,FALSE) /\ MoveRevealRequired4("SideADiscard",TRUE,TRUE,FALSE,FALSE) /\ MoveRevealRequired4("SideADeck",FALSE,TRUE,FALSE,FALSE) /\ ~MoveRevealRequired4("SideAHand",FALSE,TRUE,FALSE,FALSE) /\ ~MoveRevealRequired4("SideADiscard",TRUE,FALSE,FALSE,FALSE) /\ ~MoveRevealRequired4("SideADeck",TRUE,TRUE,TRUE,FALSE) /\ MoveRevealRequired4("SideAHand",FALSE,FALSE,TRUE,TRUE) /\ ~OutsideCardCanAffect4("Outside") /\ OutsideCardCanAffect4("Removed") /\ ~OutsideCardCanBeAffected4("Outside",FALSE) /\ OutsideCardCanBeAffected4("Outside",TRUE) /\ ZoneClass4("SideADeck") = "Hidden" /\ ZoneClass4("SideBHand") = "Secret" /\ \A z \in SharedZoneInstances4 \cup {"SideAObjectiveCompletion","SideBObjectiveCompletion","SideADiscard","SideBDiscard"} : ZoneClass4(z) = "SchemaAtom128" /\ ~DefaultZoneLook4("SideADeck","Up","SideA","SideA") /\ DefaultZoneLook4("SideAHand","NA","SideA","SideA") /\ ~DefaultZoneLook4("SideAHand","NA","SideB","SideA") /\ DefaultZoneLook4("Play","Up","SideB","SideA") /\ ~DefaultZoneLook4("Play","Down","SideB","SideA") /\ DefaultZoneLook4("Play","Down","SideA","SideA") /\ ObjectLocation4(object,2,noPlayLocation) = [kind |-> "DeckPosition",zone |-> "SideADeck",position |-> 2] /\ ObjectLocation4(object,1,noPlayLocation) # ObjectLocation4([object EXCEPT !.zone = "SideBDeck"],1,noPlayLocation) /\ ObjectLocation4([object EXCEPT !.host = 7,!.zone = "Play"],0,noPlayLocation) = [kind |-> "Host",object |-> 7] /\ ObjectLocation4([object EXCEPT !.zone = "SideBHand"],0,noPlayLocation) = [kind |-> "Zone",zone |-> "SideBHand"] /\ ObjectLocation4([object EXCEPT !.zone = "Play"],0,noPlayLocation) = noPlayLocation DeckChecks4 == LET decks == [p \in SetupPlayers |-> IF p = "SideA" THEN <<1,2>> ELSE <<3,4>>] setup == [gameStarted |-> TRUE,stage |-> "Done",deck |-> decks] o == [card |-> "c",form |-> "Card",kind |-> "Plan",zone |-> "SideADeck", face |-> "NA",deployed |-> FALSE,activated |-> FALSE] data == [c |-> [side |-> "SideA",kind |-> "Plan"]] IN /\ DeckSequenceValid4(<<>>) /\ DeckSequenceValid4(<<1,2>>) /\ ~DeckSequenceValid4(<<1,1>>) /\ DeckStartHandoff4(setup,decks) /\ ~DeckStartHandoff4([setup EXCEPT !.gameStarted = FALSE],decks) /\ ~DeckStartHandoff4([setup EXCEPT !.stage = "BeginGame"],decks) /\ ~DeckStartHandoff4(setup,[decks EXCEPT !["SideA"] = <<2,1>>]) /\ DeckPhysicalFace4 = "Down" /\ \A p \in SetupPlayers : ~DeckMayLook4(p,FALSE) /\ DeckMayLook4(p,TRUE) /\ DeckReorder4(<<1,2>>,<<1,2>>,FALSE,FALSE) /\ ~DeckReorder4(<<1,2>>,<<2,1>>,FALSE,FALSE) /\ DeckReorder4(<<1,2>>,<<2,1>>,TRUE,FALSE) /\ DeckReorder4(<<1,2>>,<<2,1>>,FALSE,TRUE) /\ ~DeckReorder4(<<1,2>>,<<1,3>>,TRUE,TRUE) /\ DeckSearchCompletion4(<<1,2>>,<<2,1>>,TRUE) /\ DeckSearchCompletion4(<<1,2>>,<<1,2>>,TRUE) /\ ~DeckSearchCompletion4(<<1,2>>,<<2,1>>,FALSE) /\ ~DeckSearchCompletion4(<<>>,<<>>,FALSE) /\ DeckSearchCompletion4(<<>>,<<>>,TRUE) /\ DeckCount4(<<1,2,3>>) = 3 /\ DeckCount4(<<>>) = 0 /\ DeckCardInactive4(o,TRUE,data) /\ DeckName4("SideA") = "SchemaAtom129" /\ DeckName4("SideB") = "DrawPile" /\ DeckCentralTargetSite4("SideA") = "SchemaAtom129" /\ DeckCentralTargetSite4("SideB") = "NoValue" /\ RequiredEmptyDeckWinner4("SideA",<<>>,TRUE,TRUE) = "SideB" /\ RequiredEmptyDeckWinner4("SideA",<<>>,FALSE,TRUE) = "NoValue" /\ RequiredEmptyDeckWinner4("SideA",<<>>,TRUE,FALSE) = "NoValue" /\ RequiredEmptyDeckWinner4("SideA",<<1>>,TRUE,TRUE) = "NoValue" /\ RequiredEmptyDeckWinner4("SideB",<<>>,TRUE,TRUE) = "NoValue" HandChecks4 == LET hand == {1,2,3} setupHands == [p \in SetupPlayers |-> IF p = "SideA" THEN <<1,2>> ELSE <<3>>] o == [card |-> "c",form |-> "Card",kind |-> "Technique",zone |-> "SideBHand", face |-> "NA",deployed |-> FALSE,activated |-> FALSE] data == [c |-> [side |-> "SideB",kind |-> "Technique"]] IN /\ HandSetupProjection4(setupHands) = [SideA |-> {1,2},SideB |-> {3}] /\ HandArrival4({1},{1,2},{2},TRUE) /\ ~HandArrival4({1},{1,2},{2},FALSE) /\ ~HandArrival4({1},{1,2,3},{2},TRUE) /\ UnorderedArrangement4(<<1,2,3>>,<<3,1,2>>) /\ ~UnorderedArrangement4(<<1,2>>,<<1,3>>) /\ HandVisibleCards4(hand,"SideA","SideA",{}) = hand /\ HandVisibleCards4(hand,"SideB","SideA",{}) = {} /\ HandVisibleCards4(hand,"SideB","SideA",{2,99}) = {2} /\ HandCount4(hand) = 3 /\ HandCardInactive4(o,TRUE,data) /\ StandardMaximumHandSize4 = 5 /\ HandHeldCountAllowed4(1000000) /\ ~HandWithinMaximum4(hand,2) /\ HandWithinMaximum4(hand,3) /\ ~HandWithinMaximum4({},-1) /\ HandDiscardDemand4(hand,2,FALSE) = 0 /\ HandDiscardDemand4(hand,2,TRUE) = 1 /\ HandDiscardDemand4(hand,5,TRUE) = 0 /\ HandDiscardDemand4(hand,-1,TRUE) = 4 /\ SideBHandHarmElimination4("SideB",-1,TRUE) /\ ~SideBHandHarmElimination4("SideB",-1,FALSE) /\ ~SideBHandHarmElimination4("SideB",0,TRUE) /\ ~SideBHandHarmElimination4("SideA",-1,TRUE) /\ HandDiscardResult4(hand,{1,3},{2},2,TRUE,TRUE) /\ ~HandDiscardResult4(hand,{1},{2,3},2,TRUE,TRUE) /\ ~HandDiscardResult4(hand,{1,3},{2},2,FALSE,TRUE) /\ ~HandDiscardResult4(hand,{1,3},{2},2,TRUE,FALSE) /\ HandName4("SideA") = "SchemaAtom082" /\ HandName4("SideB") = "BHand" /\ HandCentralTargetSite4("SideA") = "SchemaAtom082" /\ HandCentralTargetSite4("SideB") = "NoValue" /\ CentralASpecimen0139Layout4.markerZone = "Play" /\ ~CentralASpecimen0139Layout4.markerInsideCentralA /\ CentralASpecimen0139Layout4.protectingBarrier = "InFront" /\ CentralASpecimen0139Layout4.rootUpgrades = "Behind" DiscardChecks4 == LET empty == [z \in ZoneInstances4 |-> {}] cards == {1,2} faces == [id \in cards |-> IF id = 1 THEN "Up" ELSE "Down"] o == [card |-> "c",form |-> "Card",kind |-> "Facility",zone |-> "SideADiscard", face |-> "Up",deployed |-> FALSE,activated |-> FALSE] data == [c |-> [side |-> "SideA",kind |-> "Facility"]] IN /\ DiscardPilesInitiallyEmpty4(empty) /\ ~DiscardPilesInitiallyEmpty4([empty EXCEPT !["SideADiscard"] = {1}]) /\ UnorderedArrangement4(<<1,2>>,<<2,1>>) /\ DiscardCount4(cards) = 2 /\ DiscardCardInactive4(o,TRUE,data) /\ DiscardDestination4("SideA") = "SideADiscard" /\ DiscardDestination4("SideB") = "SideBDiscard" /\ DiscardArrivalFace4("SideA","Play","Retire",TRUE) = "Up" /\ DiscardArrivalFace4("SideA","Play","Retire",FALSE) = "Down" /\ DiscardArrivalFace4("SideA","SideAHand","Discard",TRUE) = "Down" /\ DiscardArrivalFace4("SideA","SideAHand","Retire",TRUE) = "Up" /\ DiscardArrivalFace4("SideB","Play","Retire",FALSE) = "Up" /\ DiscardArrivalPost4(o,"SideA","Play","Retire",TRUE) /\ ~DiscardArrivalPost4([o EXCEPT !.face = "Down"],"SideA","Play","Retire",TRUE) /\ ~DiscardArrivalPost4(o,"SideB","Play","Retire",TRUE) /\ ~DiscardArrivalPost4([o EXCEPT !.deployed = TRUE],"SideA","Play","Retire",TRUE) /\ DiscardName4("SideA") = "SchemaAtom018" /\ DiscardName4("SideB") = "BDiscardPile" /\ DiscardCentralTargetSite4("SideA") = "SchemaAtom018" /\ DiscardCentralTargetSite4("SideB") = "NoValue" /\ DiscardSiteFaceValid4("Up") /\ DiscardSiteFaceValid4("Down") /\ ~DiscardSiteFaceValid4("NA") /\ DiscardSiteFacedownOrientation4("Down") = "Horizontal" /\ DiscardSiteVisibleCards4(cards,faces,"SideA",{}) = cards /\ DiscardSiteVisibleCards4(cards,faces,"SideB",{}) = {1} /\ DiscardSiteVisibleCards4(cards,faces,"SideB",{2}) = cards /\ BDiscardPileVisibleCards4(cards) = cards /\ BDiscardPileFaceValid4("Up") /\ ~BDiscardPileFaceValid4("Down") ObjectiveCompletionChecks4 == LET empty == [z \in ZoneInstances4 |-> {}] sideA == [card |-> "a",form |-> "Card",kind |-> "Objective",zone |-> "SideAObjectiveCompletion", face |-> "Up",deployed |-> FALSE,activated |-> FALSE] sideB == [sideA EXCEPT !.zone = "SideBObjectiveCompletion"] objects == [id \in 1..4 |-> CASE id = 1 -> sideA [] id = 2 -> sideB [] id = 3 -> [sideA EXCEPT !.kind = "Facility"] [] OTHER -> [sideA EXCEPT !.zone = "Play",!.deployed = TRUE]] data == [a |-> [side |-> "SideA",kind |-> "Objective"]] points == [id \in 1..4 |-> IF id = 1 THEN -1 ELSE 2] IN /\ ObjectiveAreasInitiallyEmpty4(empty) /\ ~ObjectiveAreasInitiallyEmpty4([empty EXCEPT !["SideBObjectiveCompletion"] = {1}]) /\ NormalObjectiveCompletionClaimObjectivePost4(sideA,"SideA","Scored",TRUE) /\ NormalObjectiveCompletionClaimObjectivePost4(sideB,"SideB","ClaimedObjective",TRUE) /\ ~NormalObjectiveCompletionClaimObjectivePost4(sideB,"SideB","Scored",TRUE) /\ ~NormalObjectiveCompletionClaimObjectivePost4(sideA,"SideA","Scored",FALSE) /\ ~NormalObjectiveCompletionClaimObjectivePost4([sideA EXCEPT !.face = "Down"],"SideA","Scored",TRUE) /\ ObjectiveAreaOpenObjectives4(objects,"SideA") = {1} /\ ObjectiveAreaOpenObjectives4(objects,"SideB") = {2} /\ ObjectiveAreaCount4(objects,"SideA") = 1 /\ UnorderedArrangement4(<<1,2>>,<<2,1>>) /\ ObjectiveAreaObjectActive4(sideA,TRUE,data,FALSE) /\ ~ObjectiveAreaObjectActive4(sideB,TRUE,data,FALSE) /\ ObjectiveAreaObjectActive4(sideB,TRUE,data,TRUE) /\ ~ObjectiveAreaObjectActive4(sideA,FALSE,data,TRUE) /\ ~ObjectiveAreaObjectActive4([sideA EXCEPT !.zone = "Play"],TRUE,data,TRUE) /\ ObjectiveAreaPoints4(objects,"SideA",points) = -1 /\ ObjectiveAreaPoints4(objects,"SideB",points) = 2 PlayObject4(kind, targetSite, area, deployed) == [card |-> "c",form |-> "Card",kind |-> kind,zone |-> "Play",host |-> 0, targetSite |-> targetSite,area |-> area,deployed |-> deployed,face |-> "Up",activated |-> FALSE, subtypes |-> {}] CentralRegistry4 == [id \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]] PlayAreaChecks4 == LET targetSites == [id \in CentralTargetSites4 \cup {"r1","r2"} |-> [kind |-> IF id \in CentralTargetSites4 THEN "SchemaAtom033" ELSE "SchemaAtom132"]] facility == PlayObject4("Facility","r1","Root",TRUE) barrierCard == PlayObject4("Barrier","r2","Protecting",TRUE) technique == PlayObject4("Technique","NoValue","NoValue",TRUE) profile == PlayObject4("Profile","NoValue","NoValue",FALSE) operation == PlayObject4("Plan","NoValue","NoValue",FALSE) objects == [id \in 1..5 |-> CASE id = 1 -> facility [] id = 2 -> barrierCard [] id = 3 -> [technique EXCEPT !.host = 1,!.area = "Host"] [] id = 4 -> profile [] OTHER -> [operation EXCEPT !.zone = "SideADiscard"]] empty == [id \in {} |-> facility] destination == [zone |-> "Play",area |-> "Root",targetSite |-> "r3",targetSiteKind |-> "SchemaAtom132"] newTargetSites == [id \in DOMAIN targetSites \cup {"r3"} |-> IF id = "r3" THEN [kind |-> "SchemaAtom132"] ELSE targetSites[id]] deploying == [id \in {9} |-> [form |-> "Card",destination |-> destination]] data == [c |-> [side |-> "SideB",kind |-> "Technique"]] sideAData == [c |-> [side |-> "SideA",kind |-> "Facility"]] resourceUnit == [form |-> "Counter",kind |-> "ResourceUnit",zone |-> "Play",host |-> 0, resourceUnitLocation |-> "LiabilityMarkerFund"] orders == [id \in DOMAIN targetSites |-> IF id = "r2" THEN <<2>> ELSE <<>>] plan == AuxiliarySiteLimitPlan4(targetSites,{"r1"},1,objects) traversal == [active |-> TRUE,attacked |-> "r2",targetSiteGone |-> FALSE,result |-> "Undeclared", phase |-> "Encounter",currentBarrier |-> 2,position |-> 0] afterTargetSites == [id \in DOMAIN targetSites \ {"r2"} |-> targetSites[id]] binding == ThisTargetSiteBinding4("SchemaAtom018",TRUE,"r1") IN /\ StartingPlayCards4([id \in {4} |-> profile],{4},{}) /\ StartingPlayCards4([id \in {1,4} |-> IF id = 1 THEN facility ELSE profile],{4},{1}) /\ PlayCardCount4(objects) = 4 /\ PlayCardVisible4(facility,"SideB","SideA",FALSE) /\ ~PlayCardVisible4([facility EXCEPT !.face = "Down"],"SideB","SideA",FALSE) /\ PlayCardVisible4([facility EXCEPT !.face = "Down"],"SideA","SideA",FALSE) /\ PlayCardDefaultActive4(profile,TRUE,sideAData,FALSE) /\ PlayCardDefaultActive4(technique,TRUE,data,FALSE) /\ ~PlayCardDefaultActive4([technique EXCEPT !.face = "Down"],TRUE,data,FALSE) /\ ~PlayCardDefaultActive4(facility,TRUE,sideAData,FALSE) /\ PlayCardDefaultActive4([facility EXCEPT !.activated = TRUE],TRUE,sideAData,FALSE) /\ PlayCardDefaultActive4(operation,TRUE,sideAData,TRUE) /\ ~PlayCardDefaultActive4(operation,TRUE,sideAData,FALSE) /\ ~PlayCardDefaultActive4([operation EXCEPT !.host = 1],TRUE,sideAData,TRUE) /\ ~PlayCardDefaultActive4([technique EXCEPT !.host = 1,!.deployed = FALSE],TRUE,data,FALSE) /\ PlayLocation4(technique,0) = [kind |-> "Zone",zone |-> "Play"] /\ PlayLocation4(facility,0) = [kind |-> "Root",targetSite |-> "r1"] /\ PlayLocation4(barrierCard,0) = [kind |-> "Protecting",targetSite |-> "r2",position |-> 0] /\ PlayLocation4(objects[3],0) = [kind |-> "Host",object |-> 1] /\ PlayLocation4(resourceUnit,0) = [kind |-> "ResourceUnitLocation",location |-> "LiabilityMarkerFund"] /\ PlayResourceUnitLocationValid4(resourceUnit) /\ ~PlayResourceUnitLocationValid4([resourceUnit EXCEPT !.resourceUnitLocation = "Nowhere"]) /\ HostPlayRelationship4(1,facility,[technique EXCEPT !.host = 1],TRUE,TRUE) /\ HostPlayRelationship4(1,facility,[technique EXCEPT !.host = 1,!.deployed = FALSE],FALSE,TRUE) /\ ~HostPlayRelationship4(1,facility,technique,TRUE,TRUE) /\ ~HostPlayRelationship4(1,facility,[technique EXCEPT !.host = 1],TRUE,FALSE) /\ NonfunctionalOrHostedCounter4([resourceUnit EXCEPT !.kind = "ExposureMarker"],FALSE) /\ ~NonfunctionalOrHostedCounter4([resourceUnit EXCEPT !.kind = "SchemaAtom180"],FALSE) /\ NonfunctionalOrHostedCounter4([resourceUnit EXCEPT !.kind = "SchemaAtom180"],TRUE) /\ NonfunctionalOrHostedCounter4([resourceUnit EXCEPT !.kind = "SchemaAtom180",!.host = 1],FALSE) /\ PlayLocation4([resourceUnit EXCEPT !.kind = "ExposureMarker"],0) = [kind |-> "Zone",zone |-> "Play"] /\ TargetSiteRegistryValid4(targetSites) /\ TargetSiteRegistryAtStart4(CentralRegistry4) /\ ~TargetSiteRegistryAtStart4(targetSites) /\ CentralTargetSiteZone4("SchemaAtom082") = "SideAHand" /\ CentralTargetSiteZone4("SchemaAtom129") = "SideADeck" /\ CentralTargetSiteForZone4("SideADiscard") = "SchemaAtom018" /\ TargetSiteTraversalTargetGate4("SideB",targetSites,"r1",TRUE) /\ ~TargetSiteTraversalTargetGate4("SideA",targetSites,"r1",TRUE) /\ ~TargetSiteTraversalTargetGate4("SideB",targetSites,"r1",FALSE) /\ TargetSiteDeployDestinationGate4("SideA","Facility",destination,TRUE,TRUE) /\ ~TargetSiteDeployDestinationGate4("SideA","Facility",[destination EXCEPT !.targetSiteKind = "SchemaAtom033"],TRUE,TRUE) /\ ~TargetSiteDeployDestinationGate4("SideA","Attachment",destination,TRUE,FALSE) /\ ~TargetSiteDeployDestinationGate4("SideA","Barrier",destination,TRUE,TRUE) /\ TargetSiteDeployDestinationGate4("SideA","Barrier",[destination EXCEPT !.area = "Protecting"],TRUE,TRUE) /\ ~DeployedTargetSiteMoveGate4("r1","r2",FALSE) /\ DeployedTargetSiteMoveGate4("r1","r2",TRUE) /\ DeployedTargetSiteMoveGate4("r1","r1",FALSE) /\ TargetSiteRootTypeValid4(facility,"SchemaAtom132") /\ ~TargetSiteRootTypeValid4(facility,"SchemaAtom033") /\ TargetSiteRootTypeValid4([facility EXCEPT !.kind = "Attachment"],"SchemaAtom033") /\ ~UpgradeTargetSiteRestriction4([facility EXCEPT !.kind = "Attachment",!.face = "Down"],{"r2"}) /\ TargetSiteRootLimits4(objects,empty,"r1") /\ RootCardLayout4("r1",<<1,7>>).deploymentOrder = <<1,7>> /\ RootCardLayout4("r1",<<1,7>>).orientation = "Vertical" /\ ~CentralSpecimen0139Layout4("SchemaAtom129").markerDefinesMembership /\ AssociatedTargetSite4(objects,1) = "r1" /\ AssociatedTargetSite4(objects,2) = "r2" /\ AssociatedTargetSite4(objects,3) = "r1" /\ AssociatedTargetSite4(objects,4) = "NoValue" /\ AssociatedTargetSite4(objects,5) = "SchemaAtom018" /\ AssociatedTargetSite4([id \in 1..6 |-> IF id = 6 THEN [technique EXCEPT !.form = "Counter",!.kind = "SchemaAtom043",!.host = 3,!.area = "Host"] ELSE objects[id]],6) = "r1" /\ binding.targetSite = "r1" /\ ThisTargetSiteDuringResolution4(binding,FALSE,"NoValue","SchemaAtom018") = binding /\ ThisTargetSiteDuringResolution4(ThisTargetSiteBinding4("r1",FALSE,"NoValue"),TRUE,"r1","r2").targetSite = "r1" /\ ThisTargetSiteBinding4("SchemaAtom018",FALSE,"r1").targetSite = "SchemaAtom018" /\ ThisTargetSiteBinding4("SchemaAtom018",TRUE,"NoValue").targetSite = "SchemaAtom018" /\ AnotherTargetSiteContextValid4("SchemaAtom149",TRUE,FALSE,TRUE) /\ AnotherTargetSiteContextValid4("LinkedChoice",FALSE,TRUE,TRUE) /\ ~AnotherTargetSiteContextValid4("SchemaAtom138",TRUE,FALSE,TRUE) /\ AnotherTargetSiteContextValid4("SchemaAtom138",FALSE,FALSE,TRUE) /\ ~AnotherTargetSiteContextValid4("Invalid",FALSE,FALSE,FALSE) /\ AnotherTargetSiteReference4("SchemaAtom149",binding,"r2","SchemaAtom082") = "r1" /\ AnotherTargetSiteReference4("LinkedChoice",binding,"r2","SchemaAtom082") = "r2" /\ AnotherTargetSiteReference4("SchemaAtom138",binding,"r2","SchemaAtom082") = "SchemaAtom082" /\ AnotherTargetSiteCandidates4(targetSites,"r1") = DOMAIN targetSites \ {"r1"} /\ AnotherTargetSiteCandidates4(targetSites,"NoValue") = {} /\ StandardAuxiliarySiteCountAllowed4(1000000) /\ NewAuxiliarySiteDeclaration4(targetSites,newTargetSites,"r3",DOMAIN targetSites,destination,TRUE,{}) /\ ~NewAuxiliarySiteDeclaration4(targetSites,newTargetSites,"r3",DOMAIN targetSites,destination,FALSE,{}) /\ ~NewAuxiliarySiteDeclaration4(targetSites,newTargetSites,"r3",DOMAIN targetSites \cup {"r3"},destination,TRUE,{}) /\ ~NewAuxiliarySiteDeclaration4(targetSites,newTargetSites,"r3",DOMAIN targetSites,destination,TRUE,{2}) /\ NewAuxiliarySiteDeclaration4(targetSites,newTargetSites,"r3",DOMAIN targetSites,destination,TRUE,{3}) /\ AuxiliarySiteSurvivesCheckpoint4("r1",objects,empty) /\ AuxiliarySiteSurvivesCheckpoint4("r2",objects,empty) /\ AuxiliarySiteSurvivesCheckpoint4("r3",empty,deploying) /\ ~AuxiliarySiteSurvivesCheckpoint4("r3",empty,empty) /\ AuxiliarySiteRegistryCheckpoint4(newTargetSites,newTargetSites,objects,deploying,"ProcedureCode2d73b20aa788") /\ AuxiliarySiteRegistryCheckpoint4(newTargetSites,targetSites,objects,empty,"ProcedureCode2d73b20aa788") /\ ~AuxiliarySiteRegistryCheckpoint4(newTargetSites,targetSites,objects,deploying,"ProcedureCode2d73b20aa788") /\ ~AuxiliarySiteRegistryCheckpoint4(newTargetSites,targetSites,objects,empty,"ProcedureCodea488e1ba6ca3") /\ plan.valid /\ plan.chooser = "SideA" /\ plan.stage = "ProcedureCodea488e1ba6ca3" /\ plan.trash = {2} /\ ~AuxiliarySiteLimitPlan4(targetSites,{},1,objects).valid /\ AuxiliarySiteLimitPlan4(targetSites,{},0,objects).trash = {1,2} /\ ~AuxiliarySiteLimitPlan4(targetSites,{},-1,objects).valid /\ TraversalAfterAuxiliarySiteCleanup4(traversal,afterTargetSites,TRUE).active /\ TraversalAfterAuxiliarySiteCleanup4(traversal,afterTargetSites,TRUE).targetSiteGone /\ ~TraversalAfterAuxiliarySiteCleanup4(traversal,afterTargetSites,FALSE).active /\ TraversalAfterAuxiliarySiteCleanup4(traversal,afterTargetSites,FALSE).result = "Neither" /\ TraversalAfterAuxiliarySiteCleanup4([traversal EXCEPT !.result = "Successful"],afterTargetSites,FALSE).result = "Successful" /\ ProtectionLayoutValid4(objects,orders,targetSites) /\ ~ProtectionLayoutValid4(objects,[orders EXCEPT !["r2"] = <<>>],targetSites) /\ InnermostBarrier4(<<2>>,2) /\ OutermostBarrier4(<<2>>,2) /\ SameBarrierPosition4(<<2,8>>,8,<<4,7>>,7) /\ ~SameBarrierPosition4(<<2,8>>,2,<<4,7>>,7) /\ StandardBarrierInsertion(<<2>>,<<2,8>>,8) /\ ~StandardBarrierInsertion(<<2>>,<<8,2>>,8) /\ SideBPositionAfterBarrierShift4(traversal,2,<<2>>,<<8,2>>).position = 1 /\ SideBPositionAfterBarrierShift4([traversal EXCEPT !.position = 1],2,<<8,2>>,<<2>>).position = 0 /\ SideBPositionAfterBarrierShift4([traversal EXCEPT !.phase = "Movement"],2,<<2>>,<<8,2>>) = [traversal EXCEPT !.phase = "Movement"] BankToken4(kind, zone, host) == [form |-> "Counter",card |-> "none",virtual |-> FALSE,kind |-> kind,zone |-> zone,host |-> host] BankChecks4 == LET token == BankToken4("ResourceUnit","Play",0) before == [id \in {1,2} |-> IF id = 1 THEN token ELSE BankToken4("SchemaAtom180","Play",9)] added == [id \in {3} |-> token] after == [id \in 1..3 |-> IF id = 3 THEN token ELSE before[id]] remaining == [id \in {2} |-> before[id]] bank == [kind |-> "Zone",zone |-> "Bank"] legal == [id \in {1,2} |-> id = 2] cardCounter == [token EXCEPT !.kind = "SchemaAtom043",!.card = "physicalCard"] wrongKindAdded == [id \in {3} |-> [token EXCEPT !.kind = "SchemaAtom180"]] wrongKindAfter == [id \in 1..3 |-> IF id = 3 THEN wrongKindAdded[id] ELSE before[id]] IN /\ BankProfile4.shared /\ ~BankProfile4.active /\ BankProfile4.unlimited /\ ~BankProfile4.cardsAllowed /\ BankSupplyAvailable4(0) /\ BankSupplyAvailable4(1000000) /\ ~BankSupplyAvailable4(-1) /\ BankObjectsValid4([id \in {1} |-> [token EXCEPT !.zone = "Bank"]]) /\ ~BankObjectsValid4([id \in {1} |-> [token EXCEPT !.form = "Card",!.card = "physicalCard",!.zone = "Bank"]]) /\ ~BankObjectsValid4([id \in {1} |-> [cardCounter EXCEPT !.zone = "Bank"]]) /\ \A operation \in {"Place","Load","Gain"} : BankDefaultSource4(operation,FALSE,[kind |-> "Host",object |-> 7]) = bank /\ BankDefaultSource4("Place",TRUE,[kind |-> "Host",object |-> 7]) = [kind |-> "Host",object |-> 7] /\ BankMintProjection4(before,after,added,1,"ResourceUnit",{1,2},bank,TRUE,TRUE) /\ ~BankMintProjection4(before,wrongKindAfter,wrongKindAdded,1,"ResourceUnit",{1,2},bank,TRUE,TRUE) /\ ~BankMintProjection4(before,after,added,1,"ResourceUnit",{1,2,3},bank,TRUE,TRUE) /\ ~BankMintProjection4(before,after,added,1,"ResourceUnit",{1,2},bank,FALSE,TRUE) /\ ~BankMintProjection4(before,after,added,1,"ResourceUnit",{1,2},bank,TRUE,FALSE) /\ ~BankMintProjection4(before,after,added,1,"ResourceUnit",{1,2},[kind |-> "Host",object |-> 7],TRUE,TRUE) /\ BankSpendReturn4(before,remaining,{1},TRUE) /\ ~BankSpendReturn4(before,remaining,{1},FALSE) /\ ~BankSpendReturn4([before EXCEPT ![1].virtual = TRUE],remaining,{1},TRUE) /\ ~BankSpendReturn4([before EXCEPT ![1] = cardCounter],remaining,{1},TRUE) /\ IllegalPhysicalCounterIds4(before,legal) = {1} /\ BankCheckpointReturn4(before,remaining,legal,TRUE) /\ ~BankCheckpointReturn4(before,before,legal,TRUE) /\ ~BankCheckpointReturn4(before,remaining,legal,FALSE) /\ IllegalPhysicalCounterIds4([before EXCEPT ![1] = cardCounter],legal) = {} SetAsideChecks4 == LET card == [card |-> "p",form |-> "Card",kind |-> "Technique",zone |-> "SetAside", face |-> "Down",deployed |-> FALSE,host |-> 0] origin == [kind |-> "Zone",zone |-> "SideBDiscard"] ordinary == SetAsideTransit4(1,"SideBDiscard",origin,101,42,FALSE,FALSE) protected == SetAsideTransit4(1,"Play",[kind |-> "Host",object |-> 9],101,42,TRUE,FALSE) forfeited == SetAsideTransit4(1,"SideAObjectiveCompletion",[kind |-> "Host",object |-> 9],101,42,TRUE,TRUE) objects == [id \in 1..4 |-> IF id = 4 THEN [card EXCEPT !.face = "Up"] ELSE card] transits == [id \in 1..4 |-> SetAsideTransit4(id,"SideBDiscard",origin, IF id = 3 THEN 102 ELSE 101,42,FALSE,FALSE)] groups == FacedownSetAsideGroupView4(objects,transits) controllers == [id \in 1..4 |-> "SideB"] protectedMap == [id \in {1} |-> protected] IN /\ SetAsideProfile4.shared /\ ~SetAsideProfile4.active /\ SetAsideProfile4.temporary /\ ~SetAsideDefaultActivity4("SetAside",TRUE) /\ SetAsideDefaultActivity4("Play",TRUE) /\ SetAsideFace4(FALSE,FALSE) = "Up" /\ SetAsideFace4(FALSE,TRUE) = "Down" /\ SetAsideFace4(TRUE,FALSE) = "Down" /\ SetAsideEntryPost4(card,TRUE,FALSE,TRUE) /\ ~SetAsideEntryPost4(card,FALSE,FALSE,TRUE) /\ SetAsideEntryPost4([card EXCEPT !.face = "Up"],FALSE,FALSE,TRUE) /\ ~SetAsideEntryPost4(card,TRUE,FALSE,FALSE) /\ ~SetAsideEntryPost4([card EXCEPT !.zone = "Play"],TRUE,FALSE,TRUE) /\ SetAsideAbilityCanSee4(ordinary,42,TRUE,FALSE) /\ SetAsideAbilityCanSee4(ordinary,77,FALSE,TRUE) /\ ~SetAsideAbilityCanSee4(ordinary,77,FALSE,FALSE) /\ SetAsideExitView4(ordinary,77,FALSE,FALSE,"Play").fromZone = "SideBDiscard" /\ SetAsideExitView4(ordinary,77,FALSE,FALSE,"Play").fromLocation = origin /\ SetAsideExitView4(ordinary,42,TRUE,FALSE,"Play").fromZone = "SetAside" /\ HostedCostSetAsideRequired4(TRUE,TRUE) /\ ~HostedCostSetAsideRequired4(TRUE,FALSE) /\ ~HostedCostSetAsideRequired4(FALSE,TRUE) /\ HostedCostSetAsideChoice4({1,2},{1,2},TRUE,TRUE) /\ ~HostedCostSetAsideChoice4({1,2},{1},TRUE,TRUE) /\ CostAsideStillHosted4(protected,42,TRUE,TRUE) /\ ~CostAsideStillHosted4(protected,77,TRUE,TRUE) /\ ~CostAsideStillHosted4(protected,42,FALSE,TRUE) /\ ~SetAsideAbilityCanSee4(protected,77,TRUE,TRUE) /\ SetAsideAbilityCanSee4(protected,42,TRUE,FALSE) /\ CostAsideCleanupIds4(protectedMap,objects,{},"ProcedureCode96bfa1b6a970") = {} /\ CostAsideCleanupIds4(protectedMap,objects,{42},"ProcedureCode96bfa1b6a970") = {1} /\ CostAsideCleanupIds4(protectedMap,objects,{42},"ProcedureCode76ca53ad9dd0") = {} /\ CostAsideCleanupIds4([id \in {1} |-> forfeited],objects,{42},"ProcedureCode76ca53ad9dd0") = {1} /\ CostAsideCleanupIds4(protectedMap,[objects EXCEPT ![1].zone = "Play"],{42},"ProcedureCode96bfa1b6a970") = {} /\ CostAsideCleanupIds4(protectedMap,[id \in {99} |-> card],{42},"ProcedureCode96bfa1b6a970") = {} /\ groups.valid /\ groups.groups[101] = {1,2} /\ groups.groups[102] = {3} /\ DOMAIN groups.groups = {101,102} /\ SetAsidePublicGroupCounts4(groups).counts = [e \in {101,102} |-> IF e = 101 THEN 2 ELSE 1] /\ ~FacedownSetAsideGroupView4(objects,[id \in {1} |-> ordinary]).valid /\ ~FacedownSetAsideGroupView4(objects,[transits EXCEPT ![1].object = 99]).valid /\ SetAsideGroupRearrangement4("SideB","SideB",<<1,2>>,<<2,1>>) /\ ~SetAsideGroupRearrangement4("SideA","SideB",<<1,2>>,<<2,1>>) /\ SetAsidePlayerVisibleCards4(objects,controllers,"SideB",{}) = {1,2,3,4} /\ SetAsidePlayerVisibleCards4(objects,controllers,"SideA",{}) = {4} /\ SetAsidePlayerVisibleCards4(objects,controllers,"SideA",{2}) = {2,4} RemovedChecks4 == LET before == [card |-> "a",form |-> "Card",kind |-> "Objective",zone |-> "SideAObjectiveCompletion", face |-> "Up",deployed |-> FALSE,host |-> 0] after == [before EXCEPT !.zone = "Removed"] convertedAfter == [after EXCEPT !.kind = "Technique"] objects == [id \in {1,2} |-> IF id = 1 THEN after ELSE before] zones == [c \in {"a","b"} |-> IF c = "a" THEN "Removed" ELSE "SideAHand"] IN /\ RemovedProfile4.shared /\ ~RemovedProfile4.active /\ RemovedProfile4.open /\ RemovedProfile4.controller = "none" /\ RemovedCardPost4(before,after,TRUE) /\ ~RemovedCardPost4(before,after,FALSE) /\ ~RemovedCardPost4(before,[after EXCEPT !.card = "otherPhysicalCard"],TRUE) /\ ~RemovedCardPost4(before,[after EXCEPT !.zone = "Outside"],TRUE) /\ ~RemovedCardPost4(before,[after EXCEPT !.face = "Down"],TRUE) /\ ~RemovedCardPost4(after,after,TRUE) /\ ForfeitObjectivePost4(before,after,"SideA",TRUE) /\ ForfeitObjectivePost4(before,convertedAfter,"SideA",TRUE) /\ ForfeitObjectivePost4([before EXCEPT !.zone = "SideBObjectiveCompletion"],after,"SideB",TRUE) /\ ~ForfeitObjectivePost4(before,after,"SideB",TRUE) /\ ~ForfeitObjectivePost4([before EXCEPT !.kind = "Facility"],after,"SideA",TRUE) /\ ~ForfeitObjectivePost4(before,after,"SideA",FALSE) /\ RemovedController4("Removed","SideA") = "none" /\ RemovedController4("Removed","SideB") = "none" /\ RemovedController4("Play","SideB") = "SideB" /\ ~RemovedDefaultActivity4("Removed",TRUE) /\ \A operation \in {"Move","Modify","Target","Host","Pay","Activate"} : ~RemovedObjectInteractionGate4("Removed",operation) /\ RemovedObjectInteractionGate4("Removed","Look") /\ RemovedObjectInteractionGate4("Removed","Count") /\ ~RemovedSourceMoveGate4("Removed") /\ RemovedSourceMoveGate4("Play") /\ RemovedCardZonePersistence4(zones,zones) /\ RemovedCardZonePersistence4(zones,[zones EXCEPT !["b"] = "Removed"]) /\ ~RemovedCardZonePersistence4(zones,[zones EXCEPT !["a"] = "SideAHand"]) /\ ~RemovedCardZonePersistence4(zones,[zones EXCEPT !["a"] = "Outside"]) /\ RemovedOpenCardIds4(objects) = {1} /\ RemovedCardCount4(objects) = 1 /\ \A zone \in {"Bank","SetAside","Removed","Outside"} : ~ZoneDefaultActivityGate4(zone,TRUE) /\ ZoneDefaultActivityGate4("Play",TRUE) /\ ~ZoneDefaultActivityGate4("SideBHand",FALSE) Block4Assertions == CASE block4 = 0 -> TRUE [] block4 = 1 -> ZoneGeneralChecks4 [] block4 = 2 -> DeckChecks4 [] block4 = 3 -> HandChecks4 [] block4 = 4 -> DiscardChecks4 [] block4 = 5 -> ObjectiveCompletionChecks4 [] block4 = 6 -> PlayAreaChecks4 [] block4 = 7 -> BankChecks4 [] block4 = 8 -> SetAsideChecks4 [] block4 = 9 -> RemovedChecks4 =============================================================================