LocationChecksMC¶
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 69 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.
BankChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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) = {}Exact module download · Source bundle and reproduction instructions
Resolved project definitions: BankToken4, BankCheckpointReturn4, BankDefaultSource4, BankMintProjection4, BankObjectsValid4, BankProfile4, BankSpendReturn4, BankSupplyAvailable4, IllegalPhysicalCounterIds4
BankToken4 · operator
reference-profile · input revision 2 · CC0 1.0
BankToken4(kind, zone, host) ==
[form |-> "Counter",card |-> "none",virtual |-> FALSE,kind |-> kind,zone |-> zone,host |-> host]Exact module download · Source bundle and reproduction instructions
Block4Assertions · operator
reference-profile · input revision 2 · CC0 1.0
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 -> RemovedChecks4Exact module download · Source bundle and reproduction instructions
Resolved project definitions: BankChecks4, DeckChecks4, DiscardChecks4, HandChecks4, ObjectiveCompletionChecks4, PlayAreaChecks4, RemovedChecks4, SetAsideChecks4, ZoneGeneralChecks4, block4
CentralRegistry4 · operator
reference-profile · input revision 2 · CC0 1.0
CentralRegistry4 == [id \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CentralTargetSites4
DeckChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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"Exact module download · Source bundle and reproduction instructions
Resolved project definitions: DeckCardInactive4, DeckCentralTargetSite4, DeckCount4, DeckMayLook4, DeckName4, DeckPhysicalFace4, DeckReorder4, DeckSearchCompletion4, DeckSequenceValid4, DeckStartHandoff4, RequiredEmptyDeckWinner4, SetupPlayers
DiscardChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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")Exact module download · Source bundle and reproduction instructions
Resolved project definitions: BDiscardPileFaceValid4, BDiscardPileVisibleCards4, DiscardArrivalFace4, DiscardArrivalPost4, DiscardCardInactive4, DiscardCentralTargetSite4, DiscardCount4, DiscardDestination4, DiscardName4, DiscardPilesInitiallyEmpty4, DiscardSiteFaceValid4, DiscardSiteFacedownOrientation4, DiscardSiteVisibleCards4, UnorderedArrangement4, ZoneInstances4
HandChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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"Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CentralASpecimen0139Layout4, HandArrival4, HandCardInactive4, HandCentralTargetSite4, HandCount4, HandDiscardDemand4, HandDiscardResult4, HandHeldCountAllowed4, HandName4, HandSetupProjection4, HandVisibleCards4, HandWithinMaximum4, SideBHandHarmElimination4, StandardMaximumHandSize4, UnorderedArrangement4, SetupPlayers
Init4 · operator
reference-profile · input revision 2 · CC0 1.0
Init4 == block4 \in 1..9Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block4
Next4 · operator
reference-profile · input revision 2 · CC0 1.0
Next4 == UNCHANGED block4Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block4
ObjectiveCompletionChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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) = 2Exact module download · Source bundle and reproduction instructions
Resolved project definitions: NormalObjectiveCompletionClaimObjectivePost4, ObjectiveAreaCount4, ObjectiveAreaObjectActive4, ObjectiveAreaOpenObjectives4, ObjectiveAreaPoints4, ObjectiveAreasInitiallyEmpty4, UnorderedArrangement4, ZoneInstances4
PlayAreaChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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"]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CentralRegistry4, PlayObject4, AnotherTargetSiteCandidates4, AnotherTargetSiteContextValid4, AnotherTargetSiteReference4, AssociatedTargetSite4, AuxiliarySiteLimitPlan4, AuxiliarySiteRegistryCheckpoint4, AuxiliarySiteSurvivesCheckpoint4, CentralSpecimen0139Layout4, CentralTargetSiteForZone4, CentralTargetSiteZone4, CentralTargetSites4, DeployedTargetSiteMoveGate4, HostPlayRelationship4, InnermostBarrier4, NewAuxiliarySiteDeclaration4, NonfunctionalOrHostedCounter4, OutermostBarrier4, PlayCardCount4, PlayCardDefaultActive4, PlayCardVisible4, PlayLocation4, PlayResourceUnitLocationValid4, ProtectionLayoutValid4, RootCardLayout4, SameBarrierPosition4, SideBPositionAfterBarrierShift4, StandardAuxiliarySiteCountAllowed4, StartingPlayCards4, TargetSiteDeployDestinationGate4, TargetSiteRegistryAtStart4, TargetSiteRegistryValid4, TargetSiteRootLimits4, TargetSiteRootTypeValid4, TargetSiteTraversalTargetGate4, ThisTargetSiteBinding4, ThisTargetSiteDuringResolution4, TraversalAfterAuxiliarySiteCleanup4, UpgradeTargetSiteRestriction4, StandardBarrierInsertion
PlayObject4 · operator
reference-profile · input revision 2 · CC0 1.0
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 |-> {}]Exact module download · Source bundle and reproduction instructions
RemovedChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ForfeitObjectivePost4, RemovedCardCount4, RemovedCardPost4, RemovedCardZonePersistence4, RemovedController4, RemovedDefaultActivity4, RemovedObjectInteractionGate4, RemovedOpenCardIds4, RemovedProfile4, RemovedSourceMoveGate4, ZoneDefaultActivityGate4
SetAsideChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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}Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CostAsideCleanupIds4, CostAsideStillHosted4, FacedownSetAsideGroupView4, HostedCostSetAsideChoice4, HostedCostSetAsideRequired4, SetAsideAbilityCanSee4, SetAsideDefaultActivity4, SetAsideEntryPost4, SetAsideExitView4, SetAsideFace4, SetAsideGroupRearrangement4, SetAsidePlayerVisibleCards4, SetAsideProfile4, SetAsidePublicGroupCounts4, SetAsideTransit4
Spec4 · operator
reference-profile · input revision 2 · CC0 1.0
Spec4 == Init4 /\ [][Next4]_block4Exact module download · Source bundle and reproduction instructions
ZoneFixture4 · operator
reference-profile · input revision 2 · CC0 1.0
ZoneFixture4 == [z \in ZoneInstances4 |-> IF z = "SideAHand" THEN {1,2} ELSE {}]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ZoneInstances4
ZoneGeneralChecks4 · operator
reference-profile · input revision 2 · CC0 1.0
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) = noPlayLocationExact module download · Source bundle and reproduction instructions
Resolved project definitions: ZoneFixture4, AtomicZoneMove4, CanonicalZone4, CounterPlayAliases4, DefaultZoneLook4, MoveRevealRequired4, ObjectLocation4, OutsideCardCanAffect4, OutsideCardCanBeAffected4, SharedZoneInstances4, ZoneClass4, ZoneInstances4, ZonePartition4, ZoneType4, ZoneTypes4
block4 · variable
reference-profile · input revision 2 · CC0 1.0
block4Exact module download · Source bundle and reproduction instructions