---------------------------- MODULE OperationChecksMC ---------------------------- EXTENDS OperationContracts VARIABLE block8 Init8 == block8 \in 1..8 Next8 == UNCHANGED block8 Spec8 == Init8 /\ [][Next8]_block8 FaceCardFixture8(side,kind,face,deployed) == [form |-> "Card",side |-> side,kind |-> kind,face |-> face,deployed |-> deployed, zone |-> "Play",loc |-> "loc1",activated |-> side = "SideA" /\ deployed /\ face = "Up" /\ kind \in {"Facility","Attachment","Barrier"}, host |-> 0] FaceChecks8 == LET card == FaceCardFixture8("SideA","Facility","Down",TRUE) objects == [id \in {1,2} |-> IF id=1 THEN card ELSE FaceCardFixture8("SideA","Objective","Down",TRUE)] paid == [route |-> "Paid",effectAuthorizes |-> FALSE,open |-> TRUE,kind |-> "Paid",priority |-> "SideA", step |-> "ProcedureCode2cd618a9e624",approachedBarrier |-> 0,nonBarrierActivationAllowed |-> TRUE] effect == [paid EXCEPT !.route = "CardEffect",!.effectAuthorizes = TRUE,!.open = FALSE] initial == OpenActivation8(4,1,"ability4") paying == [initial EXCEPT !.stage = "CostCheckpoint",!.transaction = 9] ready == [paying EXCEPT !.stage = "TurnFaceUp"] finished == [ready EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "ItemActivated"] up == [objects EXCEPT ![1].face = "Up",![1].activated = TRUE] sideB == FaceCardFixture8("SideB","Technique","Up",TRUE) sideBs == [id \in {1,2} |-> sideB] down == [sideBs EXCEPT ![1].face = "Down"] chars == [name |-> "Known technique",kind |-> "Technique",cost |-> 3] empty == [id \in {} |-> id] origins == [id \in {1} |-> [method |-> "TurnedFacedown",serial |-> 8,ability |-> 6,eventId |-> 10]] eventA == [id |-> 10,tag |-> "TurnFacedown",object |-> 1,serial |-> 8,ability |-> 6, previousFaceupProfile |-> [known |-> TRUE,card |-> "TechniqueA"]] eventB == [eventA EXCEPT !.id = 11,!.object = 2,!.serial = 9,!.previousFaceupProfile.card = "TechniqueB"] deployedEvent == [id |-> 12,tag |-> "Deployed",object |-> 2,face |-> "Down",serial |-> 10,ability |-> 7, previousFaceupProfile |-> [known |-> FALSE,card |-> "Hidden"]] history == [id \in {10,11} |-> IF id=10 THEN eventA ELSE eventB] deployedHistory == [id \in {10,12} |-> IF id=10 THEN eventA ELSE deployedEvent] laterEvent == [eventA EXCEPT !.id = 13,!.serial = 11,!.ability = 8] laterHistory == [id \in {10,13} |-> IF id=10 THEN eventA ELSE laterEvent] laterOrigins == [origins EXCEPT ![1].serial = 11,![1].ability = 8,![1].eventId = 13] bothOrigins == [id \in {1,2} |-> IF id=1 THEN origins[1] ELSE [method |-> "TurnedFacedown",serial |-> 9,ability |-> 6,eventId |-> 11]] deployedOrigins == [bothOrigins EXCEPT ![2] = [method |-> "DeployedFacedown",serial |-> 10,ability |-> 7,eventId |-> 12]] bothDown == [sideBs EXCEPT ![1].face = "Down",![2].face = "Down"] r == [OpenTraversal6(1,1,"traversal1") EXCEPT !.phase = "Encounter"] IN /\ ActivationStatus8(card) = "Dormant" /\ ActivationCacheValid8(card) /\ ActivationStatus8(objects[2]) = "Dormant" /\ ~ItemActivatable8(objects[2]) /\ ActivationStatus8([objects[2] EXCEPT !.face = "Up"]) = "Neither" /\ \A kind \in {"Facility","Attachment","Barrier"} : ActivationStatus8(FaceCardFixture8("SideA",kind,"Up",TRUE)) = "ItemActivated" /\ \A kind \in {"Plan","Profile"} : ActivationStatus8(FaceCardFixture8("SideA",kind,"Down",FALSE)) = "Neither" /\ \A face \in {"Up","Down"} : ActivationStatus8(FaceCardFixture8("SideB","Technique",face,TRUE)) = "Neither" /\ ActivationStatus8([card EXCEPT !.form = "Counter"]) = "Neither" /\ ActivationStatus8([card EXCEPT !.deployed = FALSE]) = "Neither" /\ ActivationStatus8([card EXCEPT !.zone = "SideAHand"]) = "Neither" /\ ActivationPermission8(1,card,paid) /\ ActivationPermission8(1,card,effect) /\ ~ActivationPermission8(1,card,[paid EXCEPT !.priority = "SideB"]) /\ ~ActivationPermission8(1,card,[paid EXCEPT !.open = FALSE]) /\ ~ActivationPermission8(1,card,[paid EXCEPT !.nonBarrierActivationAllowed = FALSE]) /\ ActivationPermission8(1,[card EXCEPT !.kind = "Barrier"],[paid EXCEPT !.step = "ProcedureCode3a6daf593ad4",!.approachedBarrier = 1]) /\ ~ActivationPermission8(1,[card EXCEPT !.kind = "Barrier"],[paid EXCEPT !.step = "ProcedureCode3a6daf593ad4",!.approachedBarrier = 2]) /\ ~ActivationPermission8(1,[card EXCEPT !.kind = "Barrier"],[paid EXCEPT !.approachedBarrier = 1]) /\ ~ActivationPermission8(2,objects[2],effect) /\ ~ActivationPermission8(1,card,[effect EXCEPT !.effectAuthorizes = FALSE]) /\ PayActivation8(initial,paying,objects,paid,TRUE,9) /\ ~PayActivation8([initial EXCEPT !.id = 0],[paying EXCEPT !.id = 0],objects,paid,TRUE,9) /\ ~PayActivation8(initial,paying,objects,paid,FALSE,9) /\ ~PayActivation8(initial,[paying EXCEPT !.transaction = 0],objects,paid,TRUE,0) /\ ~PayActivation8(initial,paying,empty,paid,TRUE,9) /\ ~FinishActivation8(initial,[initial EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "ItemActivated"],objects,up,TRUE,{[tag |-> "Activation",object |-> 1,activationId |-> 4]}) /\ ~FinishActivation8(paying,[paying EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "ItemActivated"],objects,up,TRUE,{[tag |-> "Activation",object |-> 1,activationId |-> 4]}) /\ DrainActivationCostCheckpoint8(paying,ready,9,TRUE) /\ ~DrainActivationCostCheckpoint8(paying,ready,10,TRUE) /\ ~DrainActivationCostCheckpoint8(paying,ready,9,FALSE) /\ FinishActivation8(ready,finished,objects,up,TRUE,{[tag |-> "Activation",object |-> 1,activationId |-> 4]}) /\ ~FinishActivation8(ready,finished,objects,up,FALSE,{[tag |-> "Activation",object |-> 1,activationId |-> 4]}) /\ ~FinishActivation8(ready,finished,empty,empty,TRUE,{[tag |-> "Activation",object |-> 1,activationId |-> 4]}) /\ ~FinishActivation8(finished,finished,up,up,TRUE,{[tag |-> "Activation",object |-> 1,activationId |-> 4]}) /\ CancelActivation8(initial,[initial EXCEPT !.stage = "Complete",!.complete = TRUE,!.result = "NotItemActivated"],TRUE,{}) /\ ReturnActivation8(finished,[finished EXCEPT !.returned = TRUE],TRUE,"ability4") /\ ~ReturnActivation8(finished,[finished EXCEPT !.returned = TRUE],FALSE,"ability4") /\ ~ReturnActivation8(finished,[finished EXCEPT !.returned = TRUE],TRUE,"foreign") /\ Deactivation8(up,objects,1,TRUE,{[tag |-> "Deactivation",object |-> 1]}) /\ ~Deactivation8(up,objects,1,FALSE,{[tag |-> "Deactivation",object |-> 1]}) /\ ~Deactivation8(objects,objects,1,TRUE,{[tag |-> "Deactivation",object |-> 1]}) /\ BarrierChangeTraversalPlan6(r,"Deactivation","NoValue","SchemaAtom082").needsRedirect /\ TurnSideBFace8(sideBs,down,1,"Down",TRUE,{[tag |-> "TurnFacedown",object |-> 1]}) /\ down[1].deployed /\ down[1].zone = "Play" /\ down[1].host = sideBs[1].host /\ TurnSideBFace8(down,sideBs,1,"Up",TRUE,{[tag |-> "TurnFaceup",object |-> 1]}) /\ ~TurnSideBFace8(down,sideBs,1,"Up",FALSE,{[tag |-> "TurnFaceup",object |-> 1]}) /\ ~TurnSideBFace8(sideBs,sideBs,1,"Up",TRUE,{[tag |-> "TurnFaceup",object |-> 1]}) /\ ~TurnSideBFace8(objects,objects,1,"Up",TRUE,{[tag |-> "TurnFaceup",object |-> 1]}) /\ DOMAIN SideBCharacteristics8(down[1],chars) = {} /\ SideBCharacteristics8(sideBs[1],chars) = chars /\ ~SideBAbilityActivity8(down[1],TRUE) /\ SideBAbilityActivity8(sideBs[1],TRUE) /\ RecordSideBFaceOrigin8(empty,origins,1,"TurnedFacedown",8,6,eventA) /\ ~RecordSideBFaceOrigin8(empty,origins,1,"TurnedFacedown",8,6,[eventA EXCEPT !.tag = "Deployed",!.face = "Down"]) /\ ~RecordSideBFaceOrigin8(empty,[origins EXCEPT ![1].serial = 99],1,"TurnedFacedown",99,6,eventA) /\ ~RecordSideBFaceOrigin8(empty,[origins EXCEPT ![1].ability = 77],1,"TurnedFacedown",8,77,eventA) /\ ~RecordSideBFaceOrigin8(empty,origins,1,"TurnedFacedown",8,6,[eventA EXCEPT !.previousFaceupProfile.known = FALSE]) /\ RecordSideBFaceOrigin8(origins,bothOrigins,2,"TurnedFacedown",9,6,eventB) /\ RecordSideBFaceOrigin8(origins,deployedOrigins,2,"DeployedFacedown",10,7,deployedEvent) /\ ~RecordSideBFaceOrigin8(origins,deployedOrigins,2,"DeployedFacedown",10,7, [deployedEvent EXCEPT !.previousFaceupProfile = [known |-> TRUE,card |-> "SecretTechnique"]]) /\ RecordSideBFaceOrigin8(origins,laterOrigins,1,"TurnedFacedown",11,8,laterEvent) /\ ~RecordSideBFaceOrigin8(origins,origins,1,"TurnedFacedown",8,6,eventA) /\ SideBOriginsComplete8(down,origins,history) /\ ~SideBOriginsComplete8(down,empty,history) /\ ~SideBOriginsComplete8(down,origins,[id \in {11} |-> history[id]]) /\ ~SideBOriginsComplete8(down,origins,[history EXCEPT ![10].id = 99]) /\ ~SideBOriginsComplete8(down,origins,laterHistory) /\ SideBOriginsComplete8(down,laterOrigins,laterHistory) /\ PublicSideBOrigins8(down,laterOrigins,laterHistory)[1].serial = 11 /\ PublicSideBOrigins8(down,laterOrigins,laterHistory)[1].ability = 8 /\ PublicSideBOrigins8(down,laterOrigins,laterHistory)[1].previousFaceupProfile.card = "TechniqueA" /\ SideBOriginsComplete8(bothDown,bothOrigins,history) /\ PublicSideBOrigins8(bothDown,bothOrigins,history)[1].previousFaceupProfile.card = "TechniqueA" /\ PublicSideBOrigins8(bothDown,bothOrigins,history)[2].previousFaceupProfile.card = "TechniqueB" /\ SideBOriginsComplete8(bothDown,deployedOrigins,deployedHistory) /\ ~PublicSideBOrigins8(bothDown,deployedOrigins,deployedHistory)[2].previousFaceupProfile.known /\ PublicSideBOrigins8(bothDown,deployedOrigins,deployedHistory)[2].previousFaceupProfile.card = "Hidden" /\ DOMAIN PublicSideBOrigins8(down,origins,history) = {1} /\ ~SideBBDiscardPileFacePost8([sideB EXCEPT !.zone = "SideBDiscard",!.deployed = FALSE,!.face = "Down"]) /\ SideBBDiscardPileFacePost8([sideB EXCEPT !.zone = "SideBDiscard",!.deployed = FALSE,!.face = "Up"]) MovementChecks8 == LET empty == [id \in {} |-> id] event == MovementEvent8(10,"Retire",{1}) history == [id \in {10} |-> event] objective == [form |-> "Card",kind |-> "Objective",zone |-> "SideAObjectiveCompletion",card |-> "PhysicalA",host |-> 0,deployed |-> FALSE] objects == [id \in {1,2,3,4} |-> IF id=1 THEN objective ELSE [form |-> "Counter",kind |-> "Power",zone |-> "SideAObjectiveCompletion",host |-> IF id=4 THEN 2 ELSE 1]] normal == ForfeitPlan8(objects,1,{}) protected == ForfeitPlan8(objects,1,{2}) transits == [id \in {2} |-> SetAsideTransit4(20,"SideAObjectiveCompletion","host1",4,7,TRUE,TRUE)] removed == [id \in {5} |-> [objective EXCEPT !.zone = "Removed"]] converted == [removed EXCEPT ![5].kind = "Facility"] IN /\ Cardinality(CardMovements8) = 10 /\ \A kind \in CardMovements8 : MovementRuleBlock8(kind) # "NoValue" /\ MovementRuleBlock8("ObjectiveCompletion") = "ProcedureCode3d7a51acc5cb" /\ MovementRuleBlock8("Retire") = "ProcedureCodea93d4fa2a792" /\ \A verb \in DirectRelocations8 : verb \notin CardMovements8 /\ MovementOccurred8("Retire","ModifiedEffects",TRUE) /\ ~MovementOccurred8("Retire","ReplacedByName",TRUE) /\ ~MovementOccurred8("Retire","Prevented",TRUE) /\ ~MovementOccurred8("Retire","Impossible",TRUE) /\ ~MovementOccurred8("Arrange","NoEffect",TRUE) /\ ~MovementOccurred8("Draw","Complete",FALSE) /\ RecordMovement8(empty,history,10,"Retire",{1},"ModifiedEffects",TRUE,{event}) /\ RecordMovement8(empty,history,10,"Retire",{1},"Complete",TRUE,{event}) /\ \A disposition \in {"ReplacedByName","Prevented","Impossible","NoEffect"} : RecordMovement8(empty,empty,10,"Retire",{1},disposition,TRUE,{}) /\ ~RecordMovement8(empty,history,10,"Retire",{1},"Prevented",TRUE,{event}) /\ ~RecordMovement8(history,history,10,"Retire",{1},"Complete",TRUE,{event}) /\ ~RecordMovement8(empty,empty,10,"Retire",{1},"Complete",FALSE,{}) /\ DirectRelocationPlan8("Discard","SideA","Play").destination = "SideADiscard" /\ DirectRelocationPlan8("Discard","SideB","Play").destination = "SideBDiscard" /\ DirectRelocationPlan8("SetAside","SideB","SideAHand").destination = "SetAside" /\ DirectRelocationPlan8("RemoveFromGame","SideA","SideAHand").destination = "Removed" /\ DirectRelocationPlan8("Move","SideA","SideAHand").destination = "SideAHand" /\ ~DirectRelocationPlan8("Add","SideA","Outside").valid /\ DirectRelocationPlan8("Discard","SideA","Play").namedMovement = "NoValue" /\ normal.valid /\ normal.trashNow = {2,3} /\ normal.cleanupLater = {} /\ ForfeitHostedCleanup8(normal,{2,3},empty,7) /\ ~ForfeitHostedCleanup8(normal,{2},empty,7) /\ protected.trashNow = {3} /\ protected.cleanupLater = {2} /\ ForfeitHostedCleanup8(protected,{3},transits,7) /\ ~ForfeitHostedCleanup8(protected,{2,3},transits,7) /\ ~ForfeitHostedCleanup8(protected,{3},transits,8) /\ ~ForfeitHostedCleanup8(protected,{3},[transits EXCEPT ![2].cleanupStage = "ProcedureCode96bfa1b6a970"],7) /\ ~ForfeitPlan8(objects,2,{}).valid /\ ~ForfeitPlan8(objects,1,{4}).valid /\ ForfeitObjectivePost8(objects,removed,1,5,DOMAIN objects) /\ ForfeitObjectivePost8(objects,converted,1,5,DOMAIN objects) /\ ~ForfeitObjectivePost8(objects,[removed EXCEPT ![5].zone = "SideADiscard"],1,5,DOMAIN objects) /\ ~ForfeitObjectivePost8(objects,[removed EXCEPT ![5].card = "PhysicalB"],1,5,DOMAIN objects) /\ ~ForfeitObjectivePost8(objects,removed,1,5,1..5) /\ ForfeitObjectiveCompletionMembership8({1,6},{6},1) /\ ~ForfeitObjectiveCompletionMembership8({1,6},{1,6},1) LocationCardFixture8(card,zone,kind,side,position) == [card |-> card,form |-> "Card",side |-> side,zone |-> zone,kind |-> kind,face |-> "Down", deployed |-> zone = "Play",activated |-> FALSE,host |-> 0,marks |-> {}, loc |-> position,area |-> IF zone="Play" THEN "Protecting" ELSE "NoValue", targetSite |-> IF zone="Play" THEN "SchemaAtom082" ELSE "NoValue",targetSiteKind |-> "SchemaAtom033",position |-> position] ArrangementChecks8 == LET barrierObjects == [id \in {1,2,3} |-> IF id=3 THEN [LocationCardFixture8("HostCounter","Play","Power","SideA","host1") EXCEPT !.form = "Counter",!.host = 1] ELSE LocationCardFixture8(IF id=1 THEN "BarrierA" ELSE "BarrierB","Play","Barrier","SideA",IF id=1 THEN "inner" ELSE "outer")] f == OpenBarrierArrangement8(9,{1,2}) swapped == ExchangeDeployedLocations8(barrierObjects,1,2) g == [f EXCEPT !.swapEvents = {10}] done == [g EXCEPT !.stage = "Complete",!.complete = TRUE] empty == [id \in {} |-> id] deckObjects == [id \in 1..3 |-> LocationCardFixture8(IF id=1 THEN "A" ELSE IF id=2 THEN "B" ELSE "C","SideADeck","Facility","SideA",id)] d == OpenDeckArrangement8(20,"SideB","SideA",2,7) aside == [d EXCEPT !.stage = "OtherEffects",!.originalIds = {1,2},!.originalCount = 2] successors == [id \in {1,2} |-> id+3] asides == [id \in {3,4,5} |-> IF id=3 THEN deckObjects[3] ELSE [deckObjects[id-3] EXCEPT !.zone = "SetAside",!.loc = "SetAside"]] transits == [id \in {4,5} |-> SetAsideTransit4(id,"SideADeck",id-3,20,7,FALSE,FALSE)] returnedIds == [id \in {4,5} |-> id+2] returned == [id \in {3,6,7} |-> IF id=3 THEN deckObjects[3] ELSE [asides[id-2] EXCEPT !.zone = "SideADeck",!.loc = <<"Deck",20,IF id=6 THEN 2 ELSE 1>>]] sameOrder == [returned EXCEPT ![6].loc = <<"Deck",20,1>>,![7].loc = <<"Deck",20,2>>] completeDeck == [aside EXCEPT !.stage = "Complete",!.complete = TRUE] changedObjects == [id \in {3,4,8} |-> IF id=8 THEN [asides[5] EXCEPT !.zone = "SideAHand",!.loc = "SchemaAtom082"] ELSE asides[id]] changedTransits == [id \in {4} |-> transits[id]] oneSuccessor == [id \in {4} |-> 6] oneReturned == [id \in {3,6,8} |-> IF id=6 THEN [asides[4] EXCEPT !.zone = "SideADeck",!.loc = <<"Deck",20,1>>] ELSE changedObjects[id]] oneAside == [id \in {2,3,4} |-> IF id=4 THEN asides[4] ELSE deckObjects[id]] IN /\ ArrangeWord8("Arrange") /\ ArrangeWord8("Rearrange") /\ SmallArrangement8({}) /\ SmallArrangement8({1}) /\ ~SmallArrangement8({1,2}) /\ SwapArrangingBarrier8(f,g,barrierObjects,swapped,1,2,10,TRUE,4,4,{"old"},{"old"},{MovementEvent8(10,"Swap",{1,2})}) /\ ~SwapArrangingBarrier8(f,g,barrierObjects,swapped,1,2,10,FALSE,4,4,{"old"},{"old"},{MovementEvent8(10,"Swap",{1,2})}) /\ ~SwapArrangingBarrier8(f,g,barrierObjects,swapped,1,2,10,TRUE,4,5,{"old"},{"old"},{MovementEvent8(10,"Swap",{1,2})}) /\ ~SwapArrangingBarrier8(f,g,barrierObjects,swapped,1,2,10,TRUE,4,4,{},{"newPending"},{MovementEvent8(10,"Swap",{1,2})}) /\ swapped[1].loc = "outer" /\ swapped[2].loc = "inner" /\ swapped[3].host = 1 /\ swapped[3] = barrierObjects[3] /\ FinishBarrierArrangement8(g,done,TRUE,{MovementEvent8(9,"Arrange",{1,2})}) /\ FinishBarrierArrangement8(OpenBarrierArrangement8(9,{1}),[OpenBarrierArrangement8(9,{1}) EXCEPT !.stage = "Complete",!.complete = TRUE],TRUE,{}) /\ ~ArrangementInstructionCheckpointAllowed8(f,TRUE) /\ ~ArrangementInstructionCheckpointAllowed8(done,FALSE) /\ ArrangementInstructionCheckpointAllowed8(done,TRUE) /\ BeginDeckArrangement8(d,aside,deckObjects,asides,<<1,2,3>>,<<3>>,empty,transits,successors,1..3,FALSE) /\ ~BeginDeckArrangement8(d,aside,deckObjects,asides,<<1,2,3>>,<<2,3>>,empty,transits,successors,1..3,FALSE) /\ DeckArrangeMayLook8(aside,"SideB") /\ ~DeckArrangeMayLook8(aside,"SideA") /\ DeckArrangeEffectiveViewers8(aside,asides,transits,4,{"SideA"}) = {"SideB"} /\ DeckArrangeEffectiveViewers8(aside,asides,transits,3,{"SideA"}) = {"SideA"} /\ DeckArrangeEffectiveViewers8(aside,asides,[transits EXCEPT ![5].effect = 21],5,{"SideA"}) = {"SideA"} /\ DeckArrangeEffectiveViewers8(completeDeck,asides,transits,4,{"SideA"}) = {"SideA"} /\ DeckArrangeEffectiveViewers8([aside EXCEPT !.actor = "SideA"],asides,transits,4,{"SideA"}) = {"SideA"} /\ ~DeckArrangeMayLook8(completeDeck,"SideB") /\ DeckArrangeOtherEffects8(aside,asides,transits,{4},{}) /\ ~DeckArrangeOtherEffects8(aside,asides,transits,{3},{}) /\ ~DeckArrangeOtherEffects8(aside,asides,transits,{4},{1}) /\ ReturnDeckArrangement8(aside,completeDeck,asides,returned,<<3>>,<<7,6,3>>,transits,empty,<<5,4>>,returnedIds,1..5,TRUE) /\ ReturnDeckArrangement8(aside,completeDeck,asides,sameOrder,<<3>>,<<6,7,3>>,transits,empty,<<4,5>>,returnedIds,1..5,TRUE) /\ ReturnDeckArrangement8(aside,completeDeck,changedObjects,oneReturned,<<3>>,<<6,3>>,changedTransits,empty, <<4>>,oneSuccessor,{1,2,3,4,5,8},TRUE) /\ oneReturned[8].zone = "SideAHand" /\ ~ReturnDeckArrangement8(aside,completeDeck,asides,returned,<<3>>,<<7,6,3>>,transits,empty,<<5,4>>,returnedIds,1..5,FALSE) /\ ~FreshSuccessors8({4,5},[id \in {4,5} |-> 6],1..5) /\ ~FreshSuccessors8({4,5},[id \in {4,5} |-> id],1..5) /\ NoOpDeckArrangement8([d EXCEPT !.amount = 1],[d EXCEPT !.amount = 1,!.stage = "Complete",!.complete = TRUE],deckObjects,<<1,2,3>>,FALSE,{}) /\ ~NoOpDeckArrangement8(d,[d EXCEPT !.stage = "Complete",!.complete = TRUE],deckObjects,<<1,2,3>>,FALSE,{}) /\ NoOpDeckArrangement8([d EXCEPT !.amount = 0],[d EXCEPT !.amount = 0,!.stage = "Complete",!.complete = TRUE],deckObjects,<<1,2,3>>,FALSE,{}) /\ ~NoOpDeckArrangement8([d EXCEPT !.amount = 1],[d EXCEPT !.amount = 1,!.stage = "Complete",!.complete = TRUE],deckObjects,<<1,2,3>>,TRUE,{}) /\ BeginDeckArrangement8([d EXCEPT !.amount = 1],[aside EXCEPT !.amount = 1,!.originalIds = {1},!.originalCount = 1], deckObjects,oneAside,<<1,2,3>>,<<2,3>>,empty,[id \in {4} |-> transits[id]], [id \in {1} |-> 4],1..3,TRUE) /\ DeckArrangementPublicAction8("Retire","SideADiscard",[known |-> TRUE,card |-> "A"],1) = DeckArrangementPublicAction8("Retire","SideADiscard",[known |-> TRUE,card |-> "A"],5) /\ DOMAIN DeckArrangementPublicSummary8(aside) = {"actor","owner","count"} DrawChecks8 == LET empty == [id \in {} |-> id] participants == SetupPlayers amounts == [p \in participants |-> 1] initial == OpenDrawBatch8(30,participants,amounts,TRUE,"SideA",7,"ability7") sideAChose == [initial EXCEPT !.nextChoice = 2] allChose == [sideAChose EXCEPT !.nextChoice = 3,!.stage = "SetAside"] locked == [allChose EXCEPT !.countsReady = TRUE,!.effective = amounts] objects == [id \in {1,2} |-> LocationCardFixture8(IF id=1 THEN "SideAA" ELSE "SideBA", IF id=1 THEN "SideADeck" ELSE "SideBDeck",IF id=1 THEN "Facility" ELSE "Technique",IF id=1 THEN "SideA" ELSE "SideB",id)] decks == [p \in participants |-> IF p="SideA" THEN <<1>> ELSE <<2>>] afterDecks == [p \in participants |-> <<>>] successors == [id \in {1,2} |-> id+2] asides == [id \in {3,4} |-> [objects[id-2] EXCEPT !.zone = "SetAside",!.loc = "SetAside"]] transits == DrawAsideTransits8(empty,objects,{1,2},successors,locked) drawn == [locked EXCEPT !.stage = "Checkpoint",!.initialDrawn = [p \in participants |-> IF p="SideA" THEN {3} ELSE {4}], !.actualCounts = amounts] reactions == [drawn EXCEPT !.stage = "DrawReactions",!.checkpointId = 50,!.reactionId = 60] returning == [reactions EXCEPT !.stage = "Return"] complete == [returning EXCEPT !.stage = "Complete",!.complete = TRUE] cardData == [c \in {"SideAA","SideBA","Specimen0248"} |-> [owner |-> IF c="SideBA" THEN "SideB" ELSE "SideA"]] toHand == [id \in {3,4} |-> id+2] hands == [id \in {5,6} |-> [asides[id-2] EXCEPT !.zone = IF id=5 THEN "SideAHand" ELSE "SideBHand", !.loc = IF id=5 THEN "SideAHand" ELSE "SideBHand"]] ability == [triggerRefersDrawn |-> TRUE,batchId |-> 30,player |-> "SideA"] changed == [id \in {4,7,8} |-> IF id=4 THEN asides[4] ELSE IF id=7 THEN [asides[3] EXCEPT !.zone = "SideADiscard",!.loc = "SideADiscard",!.face = "Up"] ELSE [LocationCardFixture8("Specimen0248","SetAside","Barrier","SideA","SetAside") EXCEPT !.deployed = FALSE]] changedTransits == [id \in {4,8} |-> IF id=4 THEN transits[4] ELSE [object |-> 8,originZone |-> "SideADiscard",originLocation |-> "SchemaAtom018",effect |-> 30,ability |-> 7, protected |-> FALSE,cleanupStage |-> "ProcedureCode96bfa1b6a970",drawPlayer |-> "SideA"]] changedHands == [id \in {7,9,10} |-> IF id=7 THEN changed[7] ELSE IF id=9 THEN [changed[4] EXCEPT !.zone = "SideBHand",!.loc = "SideBHand"] ELSE [changed[8] EXCEPT !.zone = "SideAHand",!.loc = "SideAHand"]] changedSuccessors == [id \in {4,8} |-> IF id=4 THEN 9 ELSE 10] allowed == [p \in participants |-> 0..2] zero == [locked EXCEPT !.effective = [p \in participants |-> 0]] IN /\ DrawChoiceOrder8("SideA",participants) = <<"SideA","SideB">> /\ DrawChoiceOrder8("SideB",participants) = <<"SideB","SideA">> /\ DrawChoiceOrder8("SideA",{"SideB"}) = <<"SideB">> /\ ChooseDrawAmount8(initial,sideAChose,"SideA",1,allowed) /\ ~ChooseDrawAmount8(initial,[initial EXCEPT !.nextChoice = 2],"SideB",1,allowed) /\ ChooseDrawAmount8(sideAChose,allChose,"SideB",1,allowed) /\ ~ChooseDrawAmount8(initial,[sideAChose EXCEPT !.amounts["SideA"] = 3],"SideA",3,allowed) /\ LockDrawCounts8(allChose,locked,amounts,TRUE) /\ ~LockDrawCounts8(allChose,locked,amounts,FALSE) /\ BeginDrawBatch8(locked,drawn,objects,asides,decks,afterDecks,empty,transits,successors,{1,2},DrawStartEvents8(drawn)) /\ ~BeginDrawBatch8(sideAChose,drawn,objects,asides,decks,afterDecks,empty,transits,successors,{1,2},DrawStartEvents8(drawn)) /\ Cardinality(DrawStartEvents8(drawn)) = 2 /\ ~BeginDrawBatch8(locked,drawn,objects,asides,decks,[afterDecks EXCEPT !["SideB"] = <<2>>],empty,transits,successors,{1,2},DrawStartEvents8(drawn)) /\ DrawDeckoutWinner8([locked EXCEPT !.effective["SideA"] = 2],decks) = "SideB" /\ DrawDeckoutWinner8([locked EXCEPT !.effective["SideB"] = 2],decks) = "NoValue" /\ BeginDrawBatch8([locked EXCEPT !.effective["SideB"] = 2],[drawn EXCEPT !.effective["SideB"] = 2], objects,asides,decks,afterDecks,empty,transits,successors,{1,2},DrawStartEvents8(drawn)) /\ ~BeginDrawBatch8([locked EXCEPT !.effective["SideA"] = 2],[drawn EXCEPT !.effective["SideA"] = 2], objects,asides,decks,afterDecks,empty,transits,successors,{1,2},DrawStartEvents8(drawn)) /\ CompleteZeroDraw8(zero,[zero EXCEPT !.stage = "Complete",!.complete = TRUE],{}) /\ ~CompleteZeroDraw8(locked,[locked EXCEPT !.stage = "Complete",!.complete = TRUE],{}) /\ OpenDrawReactions8(drawn,reactions,50,60,TRUE) /\ ~OpenDrawReactions8(drawn,reactions,50,60,FALSE) /\ DrawGroupsValid8(reactions,asides,transits) /\ ~DrawGroupsValid8(reactions,asides,[transits EXCEPT ![3].ability = 8]) /\ ~DrawGroupsValid8(reactions,asides,[transits EXCEPT ![3].drawPlayer = "NoValue"]) /\ DrawLookGrant8(drawn,asides,transits,[id \in {3,4} |-> IF id=3 THEN "SideA" ELSE "SideB"],"SideA",3) /\ ~DrawLookGrant8(drawn,asides,transits,[id \in {3,4} |-> IF id=3 THEN "SideA" ELSE "SideB"],"SideB",3) /\ DrawSpecificAbilitySees8(reactions,asides,transits,3,ability) /\ ~DrawSpecificAbilitySees8(reactions,asides,transits,3,[ability EXCEPT !.triggerRefersDrawn = FALSE]) /\ ~DrawSpecificAbilitySees8(reactions,asides,transits,3,[ability EXCEPT !.batchId = 31]) /\ ~DrawSpecificAbilitySees8(reactions,asides,transits,3,[ability EXCEPT !.player = "SideB"]) /\ DrawTransitObservation8(transits[3],FALSE,"Enter","SetAside").visible = FALSE /\ DrawTransitObservation8(transits[3],FALSE,"Leave","SideAHand") = [visible |-> TRUE,fromZone |-> "SideADeck",toZone |-> "SideAHand"] /\ DrawTransitObservation8(transits[3],TRUE,"Leave","SideAHand").fromZone = "SetAside" /\ FinishDrawReactions8(reactions,returning,TRUE) /\ ~FinishDrawReactions8(reactions,returning,FALSE) /\ ReturnDrawnCards8(returning,complete,asides,hands,transits,empty,toHand,1..4,cardData,{}) /\ ~ReturnDrawnCards8(reactions,[complete EXCEPT !.stage = "Complete"],asides,hands,transits,empty,toHand,1..4,cardData,{}) /\ ReturnDrawnCards8(returning,complete,changed,changedHands,changedTransits,empty,changedSuccessors,1..8,cardData,{}) /\ DrawnIds8(reactions,changed,changedTransits,"SideA") = {8} /\ changedHands[7].zone = "SideADiscard" /\ ~DrawSpecificAbilitySees8(reactions,changed,changedTransits,7,ability) /\ ReturnDrawToCaller8(complete,[complete EXCEPT !.returned = TRUE],TRUE,"ability7") /\ ~ReturnDrawToCaller8(complete,[complete EXCEPT !.returned = TRUE],FALSE,"ability7") /\ ~ReturnDrawToCaller8(complete,[complete EXCEPT !.returned = TRUE],TRUE,"foreign") /\ DrawBatchValid8(complete) DeployCardFixture8(card,side,kind,zone,deployed,face,area,targetSite) == [card |-> card,form |-> "Card",side |-> side,kind |-> kind,zone |-> zone,loc |-> <>, deployed |-> deployed,face |-> face,activated |-> deployed /\ face="Up" /\ side="SideA" /\ kind \in {"Facility","Attachment","Barrier"}, area |-> area,targetSite |-> targetSite,targetSiteKind |-> IF targetSite \in CentralTargetSites4 THEN "SchemaAtom033" ELSE "SchemaAtom132", position |-> IF area="Protecting" THEN "inner" ELSE "NoValue",host |-> 0,marks |-> {"old"}, subtypes |-> {},deployCost |-> 3,deployX |-> FALSE] DeployCapacityFixture8(trashed) == LET ids == ({10} \ trashed) \cup {5} IN [techniqueIds |-> ids,demand |-> [id \in ids |-> IF id=5 THEN 3 ELSE 2],limit |-> 4,allocationFits |-> TRUE] DeployChecks8 == LET empty == [id \in {} |-> id] card == DeployCardFixture8("New","SideA","Facility","SideAHand",FALSE,"Down","NoValue","NoValue") objects == [id \in 1..4 |-> CASE id=1 -> card [] id=2 -> DeployCardFixture8("OldFacility","SideA","Facility","Play",TRUE,"Up","Root","r1") [] id=3 -> [DeployCardFixture8("OldUpgrade","SideA","Attachment","Play",TRUE,"Down","Root","r1") EXCEPT !.subtypes = {"SchemaAtom130"}] [] OTHER -> DeployCardFixture8("OldBarrier","SideA","Barrier","Play",TRUE,"Down","Protecting","r1")] initial == OpenDeploy8(50,1,"SideA","Down","ability50","NoValue") staged == [initial EXCEPT !.object = 5,!.stage = "ProcedureCode6eba7e0bfa75"] stagedObjects == [id \in {2,3,4,5} |-> IF id=5 THEN DeployStagingRow8(card,"Down",TRUE) ELSE objects[id]] destination == [zone |-> "Play",loc |-> <<"Root","r1">>,area |-> "Root",targetSite |-> "r1",targetSiteKind |-> "SchemaAtom132",position |-> "NoValue",host |-> 0] declared == [staged EXCEPT !.destination = destination,!.stage = "ProcedureCode61973f2a75d8"] afterLike == [declared EXCEPT !.stage = "ProcedureCode1ff52d705816"] trashedObjects == [id \in {3,4,5,6} |-> IF id=6 THEN [objects[2] EXCEPT !.zone = "SideADiscard",!.deployed = FALSE,!.activated = FALSE] ELSE stagedObjects[id]] transaction == [id |-> 80,procedureId |-> 50,object |-> 5,allPaid |-> TRUE, basePart |-> [applicable |-> TRUE,exists |-> FALSE,amount |-> 0],deployCostIgnored |-> FALSE,paidSomething |-> FALSE,checkpointRequired |-> FALSE] barrier == [afterLike EXCEPT !.stage = "CostBarrier",!.transaction = 80] ready == [barrier EXCEPT !.stage = "ProcedureCode0f76bcc2eb00"] placed == [ready EXCEPT !.stage = "ProcedureCode4585e6a51427"] deployedObjects == [trashedObjects EXCEPT ![5] = [WithCardLocation8(trashedObjects[5],destination) EXCEPT !.deployed = TRUE]] complete == [placed EXCEPT !.stage = "Complete",!.complete = TRUE,!.deployedOccurred = TRUE] verified == [complete EXCEPT !.verificationDone = TRUE] targetSites == [s \in CentralTargetSites4 \cup {"r1"} |-> [kind |-> IF s="r1" THEN "SchemaAtom132" ELSE "SchemaAtom033"]] centralOnly == [s \in CentralTargetSites4 |-> targetSites[s]] newDest == [destination EXCEPT !.targetSite = "r2",!.loc = <<"Root","r2">>] newDeclared == [declared EXCEPT !.destination = newDest,!.newAuxiliarySite = TRUE] newReady == [ready EXCEPT !.destination = newDest,!.newAuxiliarySite = TRUE] newPlaced == [newReady EXCEPT !.stage = "ProcedureCode4585e6a51427"] newObjects == [trashedObjects EXCEPT ![5] = [WithCardLocation8(trashedObjects[5],newDest) EXCEPT !.deployed = TRUE]] newTargetSites == [s \in DOMAIN targetSites \cup {"r2"} |-> IF s="r2" THEN [kind |-> "SchemaAtom132"] ELSE targetSites[s]] types == [id \in DOMAIN stagedObjects |-> {stagedObjects[id].kind}] controllers == [id \in DOMAIN stagedObjects |-> "SideA"] technique == DeployCardFixture8("Technique","SideB","Technique","Play",FALSE,"Up","Staging","NoValue") techniqueObjects == [id \in {5,10} |-> IF id=5 THEN technique ELSE [technique EXCEPT !.deployed = TRUE,!.area = "SideBRig"]] techniqueFrame == [declared EXCEPT !.actor = "SideB",!.face = "Up",!.destination = [destination EXCEPT !.area = "SideBRig",!.targetSite = "NoValue"]] capacityTypes == [id \in {5,10} |-> {"Technique"}] capacityControllers == [id \in {5,10} |-> "SideB"] barrierCard == [card EXCEPT !.kind = "Barrier"] barrierObjects == [stagedObjects EXCEPT ![5].kind = "Barrier"] noOldBarrier == [id \in {2,3,5} |-> barrierObjects[id]] activationDeploy == [complete EXCEPT !.activationMode = "Normal"] activationStarted == [activationDeploy EXCEPT !.activationStarted = TRUE] failedActivation == [OpenActivation8(90,5,<<"DeployAndActivation",50>>) EXCEPT !.stage = "Complete",!.complete = TRUE,!.returned = TRUE,!.result = "NotItemActivated"] activationProcessed == [activationStarted EXCEPT !.activationProcessed = TRUE] reveal == [performed |-> TRUE,object |-> 5,afterDeployment |-> TRUE] noReveal == [performed |-> FALSE,object |-> 5,afterDeployment |-> FALSE] barrierDest == [destination EXCEPT !.area = "Protecting",!.position = "outer",!.loc = "outer"] barrierDeclared == [declared EXCEPT !.destination = barrierDest] layout == [orders |-> [r1 |-> <<"inner">>],slots |-> [inner |-> [targetSite |-> "r1",barrierCard |-> 4,reservation |-> 0,retained |-> FALSE]],used |-> {"inner"}] reserved == [orders |-> [r1 |-> <<"inner","outer">>],slots |-> [p \in {"inner","outer"} |-> IF p="inner" THEN layout.slots[p] ELSE [targetSite |-> "r1",barrierCard |-> 0,reservation |-> 50,retained |-> FALSE]],used |-> {"inner","outer"}] regionObjects == [stagedObjects EXCEPT ![5].kind = "Attachment",![5].subtypes = {"SchemaAtom130"}] zeroBarrierTransaction == [transaction EXCEPT !.basePart = [applicable |-> TRUE,exists |-> TRUE,amount |-> 0], !.paidSomething = TRUE,!.checkpointRequired = TRUE] xObjects == [techniqueObjects EXCEPT ![5].deployX = TRUE] xBefore == [techniqueFrame EXCEPT !.stage = "ProcedureCode1ff52d705816"] xTransaction == [zeroBarrierTransaction EXCEPT !.basePart.amount = 2] xPaid == [xBefore EXCEPT !.stage = "CostBarrier",!.transaction = 80,!.checkpointRequired = TRUE,!.x = [exists |-> TRUE,amount |-> 2]] hostDestination == [NoDeployDestination8 EXCEPT !.area = "Hosted",!.loc = 10,!.host = 10] hostedObjects == [objects EXCEPT ![1].zone = "Play",![1].area = "Hosted",![1].host = 2,![1].loc = 2] hostedAfter == [hostedObjects EXCEPT ![1] = DeployStagingRow8(hostedObjects[1],"Down",FALSE)] faceupReady == [ready EXCEPT !.face = "Up"] faceupPlaced == [placed EXCEPT !.face = "Up"] faceupStaging == [trashedObjects EXCEPT ![5].face = "Up"] faceupDeployed == [deployedObjects EXCEPT ![5].face = "Up",![5].activated = TRUE] IN /\ DeployTypeAllowed8(card,"SideA","Down",FALSE) /\ ~DeployTypeAllowed8([card EXCEPT !.kind = "Plan"],"SideA","Down",FALSE) /\ ~DeployTypeAllowed8([card EXCEPT !.kind = "Objective"],"SideA","Up",FALSE) /\ DeployTypeAllowed8([technique EXCEPT !.kind = "Action"],"SideB","Down",TRUE) /\ ~DeployTypeAllowed8([technique EXCEPT !.kind = "Action"],"SideB","Up",TRUE) /\ DeployTypeAllowed8([technique EXCEPT !.form = "Counter",!.kind = "SchemaAtom043"],"SideB","Up",TRUE) /\ BeginDeploy8(initial,staged,objects,stagedObjects,5,1..4,TRUE,FALSE,TRUE) /\ ~BeginDeploy8(initial,staged,objects,stagedObjects,5,1..4,FALSE,FALSE,TRUE) /\ ~BeginDeploy8(initial,staged,objects,stagedObjects,5,1..4,TRUE,FALSE,FALSE) /\ ~stagedObjects[5].deployed /\ stagedObjects[5].marks = {} /\ BeginDeploy8(initial,[staged EXCEPT !.object = 1],hostedObjects,hostedAfter,1,1..4,TRUE,FALSE,TRUE) /\ hostedAfter[1].host = 0 /\ hostedAfter[1].marks = {"old"} /\ ~DeployCardDefaultActive8(staged,stagedObjects[5]) /\ DeclareDeployDestination8(staged,declared,stagedObjects,destination,FALSE,targetSites,DOMAIN targetSites,FALSE,TRUE,DOMAIN targetSites,{}) /\ ~DeclareDeployDestination8(staged,declared,stagedObjects,destination,FALSE,targetSites,DOMAIN targetSites,FALSE,FALSE,DOMAIN targetSites,{}) /\ ~DeployDestinationAllowed8([card EXCEPT !.kind = "Attachment"],"SideA","Down",destination,FALSE,targetSites,DOMAIN targetSites,stagedObjects,FALSE,TRUE,CentralTargetSites4,{}) /\ DeclareDeployDestination8(staged,newDeclared,stagedObjects,newDest,TRUE,targetSites,DOMAIN targetSites,FALSE,TRUE,DOMAIN targetSites \cup {"r2"},{2}) /\ ~DeclareDeployDestination8(staged,newDeclared,stagedObjects,newDest,TRUE,targetSites,DOMAIN targetSites,FALSE,TRUE,DOMAIN targetSites \cup {"r2"},{1}) /\ "r2" \notin DOMAIN targetSites /\ DeployRequiredRootRetire8(declared,stagedObjects) = {2} /\ FinishDeployLikeRetire8(declared,afterLike,stagedObjects,{2},{2},types,controllers,DeployCapacityFixture8,TRUE) /\ ~FinishDeployLikeRetire8(declared,afterLike,stagedObjects,{}, {},types,controllers,DeployCapacityFixture8,TRUE) /\ DeployRequiredRootRetire8(declared,regionObjects) = {3} /\ ~FinishDeployLikeRetire8(techniqueFrame,[techniqueFrame EXCEPT !.stage = "ProcedureCode1ff52d705816"],techniqueObjects,{}, {},capacityTypes,capacityControllers,DeployCapacityFixture8,TRUE) /\ FinishDeployLikeRetire8(techniqueFrame,[techniqueFrame EXCEPT !.stage = "ProcedureCode1ff52d705816"],techniqueObjects,{10},{10},capacityTypes,capacityControllers,DeployCapacityFixture8,TRUE) /\ DeployRetireArrivalFace8(objects[2],trashedObjects[6]) /\ ~DeployRetireArrivalFace8(objects[2],[trashedObjects[6] EXCEPT !.face = "Down"]) /\ DeployInherentPart8(barrierCard,"Down",barrierObjects,barrierDest,0).amount = 1 /\ DeployInherentPart8(barrierCard,"Down",noOldBarrier,barrierDest,0).amount = 0 /\ ~DeployInherentPart8(technique,"Down",techniqueObjects,destination,0).exists /\ DeployInherentPart8([technique EXCEPT !.deployX = TRUE],"Up",techniqueObjects,destination,3).amount = 3 /\ PayDeployStep8(afterLike,barrier,trashedObjects,transaction,0,TRUE) /\ PayDeployStep8([afterLike EXCEPT !.destination = barrierDest], [barrier EXCEPT !.destination = barrierDest,!.checkpointRequired = TRUE],noOldBarrier,zeroBarrierTransaction,0,TRUE) /\ ~PayDeployStep8([afterLike EXCEPT !.destination = barrierDest],[barrier EXCEPT !.destination = barrierDest], noOldBarrier,[zeroBarrierTransaction EXCEPT !.paidSomething = FALSE,!.checkpointRequired = FALSE],0,TRUE) /\ PayDeployStep8(xBefore,xPaid,xObjects,xTransaction,2,TRUE) /\ ~PayDeployStep8(xBefore,xPaid,xObjects,xTransaction,2,FALSE) /\ DrainDeployCostBarrier8(xPaid,[xPaid EXCEPT !.stage = "ProcedureCode0f76bcc2eb00"],80,9,TRUE) /\ xPaid.x.amount = 2 /\ ~PayDeployStep8(afterLike,barrier,trashedObjects,[transaction EXCEPT !.allPaid = FALSE],0,TRUE) /\ ~PayDeployStep8(afterLike,barrier,trashedObjects,[transaction EXCEPT !.procedureId = 51],0,TRUE) /\ DrainDeployCostBarrier8(barrier,ready,80,0,TRUE) /\ ~DrainDeployCostBarrier8(barrier,ready,81,0,TRUE) /\ ~DrainDeployCostBarrier8(barrier,ready,80,0,FALSE) /\ DrainDeployCostBarrier8([barrier EXCEPT !.checkpointRequired = TRUE],[ready EXCEPT !.checkpointRequired = TRUE],80,9,TRUE) /\ ~DrainDeployCostBarrier8([barrier EXCEPT !.checkpointRequired = TRUE],[ready EXCEPT !.checkpointRequired = TRUE],80,0,TRUE) /\ DeployAtDestination8(ready,placed,trashedObjects,deployedObjects,targetSites,targetSites,DOMAIN targetSites,{},TargetSiteRootLimits4(deployedObjects,empty,"r1")) /\ ~DeployAtDestination8(ready,placed,trashedObjects,deployedObjects,targetSites,targetSites,DOMAIN targetSites,{},FALSE) /\ DeployAtDestination8(newReady,newPlaced,trashedObjects,newObjects,targetSites,newTargetSites,DOMAIN targetSites,{2},TRUE) /\ ~DeployAtDestination8(newReady,newPlaced,trashedObjects,newObjects,targetSites,newTargetSites,DOMAIN targetSites,{1},TRUE) /\ ~DeployAtDestination8(newReady,newPlaced,trashedObjects,newObjects,targetSites,newTargetSites,DOMAIN targetSites \cup {"r2"},{2},TRUE) /\ DeployAtDestination8(faceupReady,faceupPlaced,faceupStaging,faceupDeployed,targetSites,targetSites,DOMAIN targetSites,{},TRUE) /\ ActivationCacheValid8(faceupDeployed[5]) /\ DeployCardDefaultActive8(faceupPlaced,faceupDeployed[5]) /\ ~DeployAtDestination8(barrier,placed,trashedObjects,deployedObjects,targetSites,targetSites,DOMAIN targetSites,{},TRUE) /\ FinishDeploy8(placed,complete,deployedObjects,{DeployBeginEvent8(placed)}) /\ ~FinishDeploy8(ready,complete,deployedObjects,{DeployBeginEvent8(ready)}) /\ ~DeployCardDefaultActive8(complete,deployedObjects[5]) /\ DeployCardDefaultActive8([complete EXCEPT !.actor = "SideB",!.face = "Up"],[technique EXCEPT !.deployed = TRUE]) /\ AuxiliarySiteRegistryCheckpoint4(targetSites,targetSites,empty,DeployPendingProjection8([id \in {50} |-> declared],stagedObjects),"ProcedureCode2d73b20aa788") /\ DeployPendingProjection8([id \in {1,50} |-> IF id=1 THEN [complete EXCEPT !.destination = newDest] ELSE declared],stagedObjects)[5].destination.targetSite = "r1" /\ AuxiliarySiteRegistryCheckpoint4(targetSites,centralOnly,empty,empty,"ProcedureCode2d73b20aa788") /\ DeclareDeployBarrierPosition8(staged,barrierDeclared,layout,reserved,1,"Outermost","NoValue",[gap |-> 0,targetSite |-> "r1"]) /\ ~DeclareDeployBarrierPosition8(staged,barrierDeclared,layout,reserved,1,"DirectlyInward","missing",[gap |-> 0,targetSite |-> "r1"]) /\ OccupyDeployBarrierPosition8([ready EXCEPT !.destination = barrierDest],[placed EXCEPT !.destination = barrierDest],reserved, [reserved EXCEPT !.slots["outer"].barrierCard = 5,!.slots["outer"].reservation = 0],TRUE) /\ ~DeployAndActivationChoiceAllowed8("IfAble",TRUE,FALSE,FALSE) /\ ~DeployAndActivationChoiceAllowed8("IfAble",TRUE,TRUE,TRUE) /\ DeployAndActivationChoiceAllowed8("Normal",TRUE,FALSE,TRUE) /\ StartDeployActivation8(activationDeploy,activationStarted,[kind |-> "Activation",object |-> 5,caller |-> <<"DeployAndActivation",50>>]) /\ ~StartDeployActivation8([placed EXCEPT !.activationMode = "Normal"],activationStarted,[kind |-> "Activation",object |-> 5,caller |-> <<"DeployAndActivation",50>>]) /\ FinishDeployActivation8(activationStarted,activationProcessed,failedActivation) /\ ~FinishDeployActivation8(activationStarted,activationProcessed,[failedActivation EXCEPT !.caller = <<"DeployAndActivation",51>>]) /\ ~DeployRevealRequired8(FALSE,FALSE,FALSE) /\ VerifyDeployedCard8(complete,verified,FALSE,FALSE,noReveal) /\ ~VerifyDeployedCard8(complete,verified,TRUE,FALSE,noReveal) /\ VerifyDeployedCard8(complete,verified,TRUE,TRUE,noReveal) /\ VerifyDeployedCard8(activationProcessed,[activationProcessed EXCEPT !.verificationDone = TRUE],FALSE,TRUE,reveal) /\ ~VerifyDeployedCard8(activationProcessed,[activationProcessed EXCEPT !.verificationDone = TRUE],FALSE,TRUE,noReveal) /\ ~VerifyDeployedCard8(activationProcessed,[activationProcessed EXCEPT !.verificationDone = TRUE],FALSE,TRUE,[reveal EXCEPT !.object = 6]) /\ ~VerifyDeployedCard8(activationProcessed,[activationProcessed EXCEPT !.verificationDone = TRUE],FALSE,TRUE,[reveal EXCEPT !.afterDeployment = FALSE]) /\ DeployDestinationAllowed8(technique,"SideB","Up",hostDestination,FALSE,targetSites,DOMAIN targetSites,techniqueObjects,TRUE,TRUE,{}, {}) /\ ~DeployDestinationAllowed8(technique,"SideB","Up",hostDestination,FALSE,targetSites,DOMAIN targetSites,techniqueObjects,FALSE,TRUE,{}, {}) /\ ReturnDeployToCaller8(verified,[verified EXCEPT !.returned = TRUE],TRUE,"ability50") /\ ~ReturnDeployToCaller8(verified,[verified EXCEPT !.returned = TRUE],FALSE,"ability50") /\ ~ReturnDeployToCaller8(verified,[verified EXCEPT !.returned = TRUE],TRUE,"foreign") /\ ~NextDeployInBatch8(1,2,verified,TRUE) /\ NextDeployInBatch8(1,2,[verified EXCEPT !.returned = TRUE],TRUE) /\ ~NextDeployInBatch8(1,2,[verified EXCEPT !.returned = TRUE],FALSE) /\ ~UninstallationOccurred8(technique,[technique EXCEPT !.face = "Down"]) /\ UninstallationOccurred8(objects[4],[objects[4] EXCEPT !.deployed = FALSE]) /\ DeployPublicLayout8("Barrier").orientation = "Horizontal" /\ DeployPublicLayout8("Facility") = DeployPublicLayout8("Objective") /\ FinishDeployWithoutDeployment8(staged,[staged EXCEPT !.stage = "Complete",!.complete = TRUE,!.verificationDone = TRUE, !.activationProcessed = TRUE,!.activationPerformed = FALSE,!.deployedOccurred = FALSE],TRUE) PlayCardFixture8(card,side,kind,cost,x) == LET base == DeployCardFixture8(card,side,kind,side\o"Hand",FALSE,"Down","NoValue","NoValue") IN [key \in DOMAIN base \cup {"playCost","playX"} |-> CASE key = "playCost" -> cost [] key = "playX" -> x [] OTHER -> base[key]] PlayChecks8 == LET empty == [id \in {} |-> id] op == PlayCardFixture8("Op","SideA","Plan",5,FALSE) objects == [id \in {1} |-> op] playedObjects == [id \in {2} |-> PlayedPlacementRow8(op,TRUE)] start == OpenPlay8(60,1,"SideA","Subcontract") b == [start EXCEPT !.object = 2,!.stage = "ProcedureCode0f076861472c",!.kind = "Plan",!.subtypes = op.subtypes] tx == [id |-> 100,procedureId |-> 60,object |-> 2,allPaid |-> TRUE, basePart |-> [applicable |-> TRUE,exists |-> TRUE,amount |-> 5], playCostIgnored |-> FALSE,paidSomething |-> TRUE,checkpointRequired |-> TRUE] cost == [b EXCEPT !.stage = "CostBarrier",!.transaction = 100,!.checkpointRequired = TRUE] c == [cost EXCEPT !.stage = "ProcedureCodecbf6b11f0ae0"] d == [c EXCEPT !.stage = "ProcedureCode7647b901fcb1",!.activationReached = TRUE] e == [d EXCEPT !.stage = "ProcedureCodebddd9a1a600b"] f == [e EXCEPT !.stage = "ProcedureCode3d7f756d78f7"] g == [f EXCEPT !.stage = "ProcedureCodee977e478b45b"] h == [g EXCEPT !.stage = "ProcedureCodec610fc738935"] i == [h EXCEPT !.stage = "ProcedureCode03de9212dc90"] done == [i EXCEPT !.stage = "Complete",!.complete = TRUE] completion == [playId |-> 60,object |-> 2,allPlayAbilitiesResolved |-> TRUE, ownedTimingIds |-> {77},returnedTimingIds |-> {77},ownEndTriggersResolved |-> TRUE] cleanup == [playId |-> 60,object |-> 2,disposition |-> "Retire",trashInstructionComplete |-> TRUE] retention == [id |-> 200,playId |-> 60,source |-> 2,created |-> TRUE,expiryEffect |-> "NextSideATurn"] effects == [id \in {199} |-> [source |-> 2,kind |-> "DelayedIndependentEffect"]] retainedEffects == [id \in {199,200} |-> IF id = 200 THEN retention ELSE effects[id]] xObjects == [playedObjects EXCEPT ![2].playX = TRUE] xTx == [tx EXCEPT !.basePart.amount = 3] xCost == [cost EXCEPT !.x = [exists |-> TRUE,amount |-> 3]] ignoredTx == [tx EXCEPT !.playCostIgnored = TRUE,!.paidSomething = FALSE,!.checkpointRequired = FALSE] ignoredCost == [cost EXCEPT !.checkpointRequired = FALSE] zeroObjects == [playedObjects EXCEPT ![2].playCost = 0] zeroTx == [tx EXCEPT !.basePart.amount = 0] gone == [playedObjects EXCEPT ![2].zone = "Removed"] hosted == [playedObjects EXCEPT ![2].host = 9] converted == [playedObjects EXCEPT ![2].form = "Counter",![2].kind = "SchemaAtom043"] IN /\ BeginPlay8(start,b,objects,playedObjects,2,{1},TRUE) /\ ~BeginPlay8(start,b,objects,playedObjects,2,{1},FALSE) /\ ~PlayTypeAllowed8([op EXCEPT !.kind = "Facility"],"SideA") /\ ~PlayTypeAllowed8(op,"SideB") /\ PlayTypeAllowed8([op EXCEPT !.side = "SideB",!.kind = "Action"],"SideB") /\ ~playedObjects[2].deployed /\ playedObjects[2].face = "Up" /\ playedObjects[2].marks = {} /\ ~PlayEffectiveCardActivity8(b,2,playedObjects[2],TRUE) /\ ~PlayEffectiveCardActivity8(cost,2,playedObjects[2],TRUE) /\ PlayEffectiveCardActivity8(d,2,playedObjects[2],FALSE) /\ PlayEffectiveCardActivity8(b,3,playedObjects[2],TRUE) /\ ~PlayEffectiveCardActivity8(f,2,converted[2],TRUE) /\ PayPlayStep8(b,cost,playedObjects,tx,FALSE,0,TRUE) /\ ~PayPlayStep8(b,cost,playedObjects,[tx EXCEPT !.allPaid = FALSE],FALSE,0,TRUE) /\ ~PayPlayStep8(b,cost,playedObjects,[tx EXCEPT !.object = 9],FALSE,0,TRUE) /\ PayPlayStep8(b,ignoredCost,playedObjects,ignoredTx,TRUE,0,TRUE) /\ ~PayPlayStep8(b,ignoredCost,playedObjects,ignoredTx,FALSE,0,TRUE) /\ PayPlayStep8(b,cost,zeroObjects,zeroTx,FALSE,0,TRUE) /\ ~PayPlayStep8(b,ignoredCost,zeroObjects,[zeroTx EXCEPT !.paidSomething = FALSE,!.checkpointRequired = FALSE],FALSE,0,TRUE) /\ PayPlayStep8(b,xCost,xObjects,xTx,FALSE,3,TRUE) /\ ~PayPlayStep8(b,xCost,xObjects,xTx,FALSE,3,FALSE) /\ DrainPlayCostBarrier8(xCost,[xCost EXCEPT !.stage = "ProcedureCodecbf6b11f0ae0"],100,10,TRUE) /\ xCost.x.amount = 3 /\ DrainPlayCostBarrier8(cost,c,100,10,TRUE) /\ ~DrainPlayCostBarrier8(cost,c,100,0,TRUE) /\ ~DrainPlayCostBarrier8(cost,c,100,10,FALSE) /\ ActivatePlayedCard8(c,d) /\ ~ActivatePlayedCard8(cost,d) /\ MeetPlayedConditions8(d,e,{PlayedCondition8(d)}) /\ ~MeetPlayedConditions8(c,e,{PlayedCondition8(c)}) /\ OpenPlayAbilities8(e,f,11,TRUE) /\ ~OpenPlayAbilities8(e,f,0,TRUE) /\ ~OpenPlayAbilities8(e,f,11,FALSE) /\ FinishPlayAbilities8(f,g,completion) /\ ~FinishPlayAbilities8(f,g,[completion EXCEPT !.returnedTimingIds = {}]) /\ ~FinishPlayAbilities8(f,g,[completion EXCEPT !.ownEndTriggersResolved = FALSE]) /\ ~FinishPlayAbilities8(f,g,[completion EXCEPT !.playId = 61]) /\ PlayEffectiveCardActivity8(f,2,playedObjects[2],FALSE) /\ PlayCleanupDisposition8(g,empty,FALSE,FALSE) = "LeftPlay" /\ PlayCleanupDisposition8(g,gone,FALSE,FALSE) = "LeftPlay" /\ PlayCleanupDisposition8(g,converted,FALSE,FALSE) = "ConvertedOrHosted" /\ PlayCleanupDisposition8(g,hosted,FALSE,FALSE) = "ConvertedOrHosted" /\ PlayCleanupDisposition8(g,playedObjects,FALSE,TRUE) = "NestedRemoval" /\ PlayCleanupDisposition8(g,playedObjects,FALSE,FALSE) = "Retire" /\ FinishPlayCleanup8(g,h,playedObjects,FALSE,FALSE,cleanup,effects,effects,retention) /\ ~FinishPlayCleanup8(g,h,playedObjects,FALSE,FALSE,[cleanup EXCEPT !.trashInstructionComplete = FALSE],effects,effects,retention) /\ FinishPlayCleanup8(g,h,playedObjects,TRUE,FALSE,[cleanup EXCEPT !.disposition = "RetainSelf"],effects,retainedEffects,retention) /\ ~FinishPlayCleanup8(g,h,playedObjects,TRUE,FALSE,[cleanup EXCEPT !.disposition = "RetainSelf"],effects,effects,retention) /\ ~FinishPlayCleanup8(g,h,playedObjects,TRUE,FALSE,[cleanup EXCEPT !.disposition = "RetainSelf"],effects,[retainedEffects EXCEPT ![200].source = 9],[retention EXCEPT !.source = 9]) /\ FinishPlayCleanup8(g,h,playedObjects,FALSE,TRUE,[cleanup EXCEPT !.disposition = "NestedRemoval"],effects,effects,retention) /\ MeetPlayResolvedConditions8(h,i,{[tag |-> "PlayResolved",object |-> 2,kind |-> "Plan",actor |-> "SideA",playId |-> 60]}) /\ ~MeetPlayResolvedConditions8(g,i,{[tag |-> "PlayResolved",object |-> 2,kind |-> "Plan",actor |-> "SideA",playId |-> 60]}) /\ CompletePlay8(i,done) /\ ~CompletePlay8(h,done) /\ ReturnPlayToCaller8(done,[done EXCEPT !.returned = TRUE],TRUE,"Subcontract") /\ ~ReturnPlayToCaller8(done,[done EXCEPT !.returned = TRUE],FALSE,"Subcontract") /\ ~NextPlayInBatch8(1,2,done,TRUE) /\ NextPlayInBatch8(1,2,[done EXCEPT !.returned = TRUE],TRUE) /\ ~NextPlayInBatch8(1,2,[done EXCEPT !.returned = TRUE],FALSE) SearchChecks8 == LET empty == [id \in {} |-> id] a == DeployCardFixture8("Imp","SideB","Technique","SideBDeck",FALSE,"Down","NoValue","NoValue") b == DeployCardFixture8("Action","SideB","Action","SideBDeck",FALSE,"Down","NoValue","NoValue") objects == [id \in {1,2} |-> IF id = 1 THEN a ELSE b] start == OpenSearch8(70,"SideB","SideBDeck",1,TRUE,"Deploy","SMC","ability70") closed == [start EXCEPT !.complete = TRUE,!.foundCount = 1,!.stage = "Shuffle"] found == [id \in {2,3} |-> IF id = 3 THEN [a EXCEPT !.zone = "SetAside",!.loc = "SetAside",!.marks = {}] ELSE b] successor == [id \in {1} |-> 3] transit == [id \in {3} |-> SetAsideTransit4(3,"SideBDeck",a.loc,70,"SMC",FALSE,FALSE)] findReceipt == [searchId |-> 70,ability |-> "SMC",sources |-> {1},successors |-> successor,complete |-> TRUE] shuffleReceipt == [searchId |-> 70,zone |-> "SideBDeck",performed |-> TRUE] shuffled == [id \in {3,4} |-> IF id = 4 THEN [b EXCEPT !.loc = <<"SideBDeck",1>>,!.marks = {}] ELSE found[id]] conditions == [closed EXCEPT !.stage = "Conditions",!.shuffled = TRUE] pending == [searchId |-> 70,allRequiredMarked |-> TRUE] resume == [conditions EXCEPT !.stage = "Resume",!.conditionsMarked = TRUE] resumed == [resume EXCEPT !.stage = "Resumed",!.returned = TRUE] event == [tag |-> "Searched",searchId |-> 70,actor |-> "SideB",zone |-> "SideBDeck",foundCount |-> 1] reveal == [performed |-> TRUE,object |-> 3,searchId |-> 70] noFind == [closed EXCEPT !.foundCount = 0] noFindReceipt == [findReceipt EXCEPT !.sources = {},!.successors = empty] shuffledBoth == [id \in {4,5} |-> IF id = 4 THEN [a EXCEPT !.loc = <<"SideBDeck",2>>,!.marks = {}] ELSE [b EXCEPT !.loc = <<"SideBDeck",1>>,!.marks = {}]] otherZone == [start EXCEPT !.zone = "SideBDiscard"] bDiscardPile == [id \in {1,2} |-> [objects[id] EXCEPT !.zone = "SideBDiscard",!.face = "Up"]] emptySearch == [start EXCEPT !.hasCriteria = FALSE,!.amount = 3] sideAObjects == [id \in {1} |-> DeployCardFixture8("Pharos","SideA","Barrier","SideADeck",FALSE,"Down","NoValue","NoValue")] sideASearch == OpenSearch8(71,"SideA","SideADeck",1,TRUE,"Deploy","Tucana","ability71") IN /\ SearchLookGrant8(start,"SideB",1,objects) /\ ~SearchLookGrant8(start,"SideA",1,objects) /\ ~SearchLookGrant8(closed,"SideB",2,found) /\ SearchChoiceAllowed8(start,objects,{1},{1},{{1}},{1}) /\ ~SearchChoiceAllowed8(start,objects,{2},{1},{{2}},{1}) /\ ~SearchChoiceAllowed8(start,objects,{1},{1},{},{1}) /\ SearchChoiceAllowed8(start,objects,{}, {1}, {},{1}) /\ ~SearchChoiceAllowed8(otherZone,bDiscardPile,{}, {1}, {},{1}) /\ SearchChoiceAllowed8([start EXCEPT !.hasCriteria = FALSE],objects,{1},{1,2},{{1}},{1}) /\ ~SearchChoiceAllowed8([start EXCEPT !.hasCriteria = FALSE],objects,{}, {1,2},{{1}},{1}) /\ SearchChoiceAllowed8(emptySearch,objects,{1,2},{1,2},{{1,2}},{3}) /\ SearchChoiceAllowed8(emptySearch,empty,{}, {}, {},{3}) /\ SearchChoiceAllowed8(sideASearch,sideAObjects,{1},{1},{{1}},{1}) /\ SearchChoiceAllowed8([start EXCEPT !.hasCriteria = FALSE],objects,{}, {1,2}, {},{1}) /\ SearchChoiceAllowed8([emptySearch EXCEPT !.amount = 2],objects,{1},{1,2},{{1}},{2}) /\ ~SearchChoiceAllowed8([emptySearch EXCEPT !.amount = 2],objects,{}, {1,2},{{1}},{2}) /\ ~SearchChoiceAllowed8([emptySearch EXCEPT !.amount = 2],objects,{1},{1,2},{{1},{1,2}},{2}) /\ SearchChoiceAllowed8([emptySearch EXCEPT !.followup = "NoValue"],objects,{1,2},{1,2},{},{3}) /\ FinishSearchChoice8([start EXCEPT !.hasCriteria = FALSE],[noFind EXCEPT !.hasCriteria = FALSE], objects,objects,{},empty,{1,2},{1,2},{},{1},noFindReceipt,<<1,2>>,<<1,2>>,empty,empty) /\ ~SearchChoiceAllowed8([start EXCEPT !.followup = "Play"],objects,{1},{1},{},{1}) /\ FinishSearchChoice8(start,closed,objects,found,{1},successor,{1,2},{1},{{1}},{1},findReceipt,<<1,2>>,<<2>>,empty,transit) /\ ~FinishSearchChoice8(start,closed,objects,[found EXCEPT ![3].face = "Up"],{1},successor,{1,2},{1},{{1}},{1},findReceipt,<<1,2>>,<<2>>,empty,transit) /\ ~FinishSearchChoice8(start,closed,objects,found,{1},successor,{1,2,3},{1},{{1}},{1},findReceipt,<<1,2>>,<<2>>,empty,transit) /\ ~FinishSearchChoice8(start,closed,objects,found,{1},successor,{1,2},{1},{{1}},{1},[findReceipt EXCEPT !.searchId = 71],<<1,2>>,<<2>>,empty,transit) /\ SearchShuffle8(closed,conditions,found,shuffled,<<2>>,<<4>>,<<2>>,[id \in {2} |-> 4],{1,2,3},shuffleReceipt,transit,transit) /\ ~SearchShuffle8(closed,conditions,found,shuffled,<<2>>,<<4>>,<<2>>,[id \in {2} |-> 4],{1,2,3},[shuffleReceipt EXCEPT !.performed = FALSE],transit,transit) /\ ~SearchShuffle8(closed,conditions,found,found,<<2>>,<<2>>,<<2>>,[id \in {2} |-> 2],{1,2,3},shuffleReceipt,transit,transit) /\ FinishSearchChoice8(start,noFind,objects,objects,{},empty,{1,2},{1}, {},{1},noFindReceipt,<<1,2>>,<<1,2>>,empty,empty) /\ SearchShuffle8(noFind,[conditions EXCEPT !.foundCount = 0],objects,shuffledBoth,<<1,2>>,<<5,4>>,<<2,1>>,[id \in {1,2} |-> IF id = 1 THEN 4 ELSE 5],{1,2},shuffleReceipt,empty,empty) /\ ~SearchFoundActionAllowed8(closed) /\ ~SearchChainReactionsAllowed8(closed) /\ ~MarkSearchConditions8([conditions EXCEPT !.shuffled = FALSE],[resume EXCEPT !.shuffled = FALSE],pending,{event}) /\ MarkSearchConditions8(conditions,resume,pending,{event}) /\ ~MarkSearchConditions8(conditions,resume,[pending EXCEPT !.allRequiredMarked = FALSE],{event}) /\ ResumeSearchAbility8(resume,resumed,"ability70") /\ ~ResumeSearchAbility8(resume,resumed,"foreign") /\ SearchFoundActionAllowed8(resumed) /\ SearchChainReactionsAllowed8(resumed) /\ ~SearchRevealRequired8(closed,TRUE) /\ ~SearchRevealRequired8(resumed,FALSE) /\ SearchRevealFound8(resumed,shuffled,transit,3,TRUE,reveal) /\ ~SearchRevealFound8(resumed,shuffled,transit,3,TRUE,[reveal EXCEPT !.object = 4]) /\ ~SearchRevealFound8(resumed,shuffled,transit,4,TRUE,[reveal EXCEPT !.object = 4]) /\ SearchRemainingEffectsContinue8([resumed EXCEPT !.foundCount = 0]) /\ MarkSearchConditions8([conditions EXCEPT !.zone = "SideBDiscard",!.shuffled = FALSE], [resume EXCEPT !.zone = "SideBDiscard",!.shuffled = FALSE],pending,{[event EXCEPT !.zone = "SideBDiscard"]}) /\ SearchShuffle8(noFind,[conditions EXCEPT !.foundCount = 0],empty,empty,<<>>,<<>>,<<>>,empty,{},shuffleReceipt,empty,empty) /\ ~SearchShuffle8(noFind,[conditions EXCEPT !.foundCount = 0],empty,empty,<<>>,<<>>,<<>>,empty,{}, [shuffleReceipt EXCEPT !.searchId = 71],empty,empty) SwapChecks8 == LET empty == [id \in {} |-> id] barrierA == [DeployCardFixture8("Thimblerig","SideA","Barrier","Play",TRUE,"Up","Protecting","r1") EXCEPT !.activated = TRUE,!.position = "p1",!.loc = <<"Barrier","p1">>] barrierB == [barrierA EXCEPT !.card = "Palisade",!.targetSite = "r2",!.position = "p2",!.loc = <<"Barrier","p2">>,!.face = "Down",!.activated = FALSE] child == [DeployCardFixture8("Botulus","SideB","Technique","Play",TRUE,"Up","Hosted","NoValue") EXCEPT !.host = 2,!.loc = <<"Host",2>>] objects == [id \in {1,2,3} |-> CASE id = 1 -> barrierA [] id = 2 -> barrierB [] OTHER -> child] checks == [id \in {1,2} |-> [destination |-> CardLocation8(objects[IF id = 1 THEN 2 ELSE 1]),gameRulesHold |-> TRUE,cardAbilitiesHold |-> TRUE]] swapped == ExchangeDeployedLocations8(objects,1,2) swapEvent == MovementEvent8(500,"Swap",{1,2}) frame == OpenBarrierArrangement8(90,{1,2}) arranged == [frame EXCEPT !.swapEvents = {500}] layout == [orders |-> [r1 |-> <<"p1">>,r2 |-> <<"p2">>],slots |-> [p \in {"p1","p2"} |-> [targetSite |-> IF p = "p1" THEN "r1" ELSE "r2",barrierCard |-> IF p = "p1" THEN 1 ELSE 2,reservation |-> 0,retained |-> FALSE]],used |-> {"p1","p2"}] swappedLayout == [layout EXCEPT !.slots["p1"].barrierCard = 2,!.slots["p2"].barrierCard = 1] handBarrier == [barrierB EXCEPT !.zone = "SideAHand",!.loc = "SideAHand",!.deployed = FALSE, !.area = "NoValue",!.targetSite = "NoValue",!.targetSiteKind = "NoValue",!.position = "NoValue",!.marks = {}] crossObjects == [objects EXCEPT ![2] = handBarrier,![3].host = 1,![3].loc = <<"Host",1>>] succ == [id \in {1,2} |-> id+3] outgoing == [WithCardLocation8(barrierA,CardLocation8(handBarrier)) EXCEPT !.deployed = FALSE,!.face = "Down",!.activated = FALSE,!.marks = {}] incoming == [WithCardLocation8(handBarrier,CardLocation8(barrierA)) EXCEPT !.deployed = TRUE,!.face = "Down",!.activated = FALSE,!.marks = {}] crossAfter == [id \in {3,4,5} |-> CASE id = 4 -> outgoing [] id = 5 -> incoming [] OTHER -> crossObjects[id]] crossChecks == [id \in {1,2} |-> [destination |-> CardLocation8(crossObjects[IF id=1 THEN 2 ELSE 1]),gameRulesHold |-> TRUE,cardAbilitiesHold |-> TRUE]] arrivals == [id \in {1,2} |-> [source |-> id,destination |-> CardLocation8(crossObjects[IF id=1 THEN 2 ELSE 1]), row |-> crossAfter[succ[id]],complete |-> TRUE,destinationHidden |-> id=1,sideBCouldSee |-> TRUE,faceExceptionAuthorized |-> FALSE]] receipt == [complete |-> TRUE,sources |-> {1,2},successors |-> succ, deployProcedurePerformed |-> FALSE,deployCostPaid |-> FALSE,likeCardsRetireed |-> FALSE] conditionPlan == OpenSwapCheckpoint8(500,crossObjects,crossAfter,1,2,succ,20) deployEvents == {[tag |-> "Uninstalled",object |-> 1,swapId |-> 500],[tag |-> "Deployed",object |-> 5,swapId |-> 500]} objectiveA == DeployCardFixture8("ObjectiveA","SideA","Objective","SideAObjectiveCompletion",FALSE,"Up","NoValue","NoValue") objectiveB == [objectiveA EXCEPT !.card = "ObjectiveB",!.zone = "SideBObjectiveCompletion",!.loc = "SideBObjectiveCompletion"] objectiveChild == [objectiveA EXCEPT !.form = "Counter",!.kind = "SchemaAtom043",!.card = "CounterC",!.zone = "SideAObjectiveCompletion", !.host = 1,!.loc = <<"Host",1>>,!.area = "Hosted"] grandchild == [objectiveChild EXCEPT !.card = "CounterD",!.host = 3,!.loc = <<"Host",3>>] objectiveObjects == [id \in 1..4 |-> CASE id=1 -> objectiveA [] id=2 -> objectiveB [] id=3 -> objectiveChild [] OTHER -> grandchild] objectiveSucc == [id \in 1..4 |-> id+4] objectiveAfter == [id \in 5..8 |-> CASE id=5 -> [WithCardLocation8(objectiveA,CardLocation8(objectiveB)) EXCEPT !.marks = {}] [] id=6 -> [WithCardLocation8(objectiveB,CardLocation8(objectiveA)) EXCEPT !.marks = {}] [] id=7 -> [objectiveChild EXCEPT !.zone = "SideBObjectiveCompletion",!.host = 5,!.loc = <<"Host",5>>,!.marks = {}] [] OTHER -> [grandchild EXCEPT !.zone = "SideBObjectiveCompletion",!.host = 7,!.loc = <<"Host",7>>,!.marks = {}]] objectiveChecks == [id \in {1,2} |-> [destination |-> CardLocation8(objectiveObjects[IF id=1 THEN 2 ELSE 1]),gameRulesHold |-> TRUE,cardAbilitiesHold |-> TRUE]] asideA == [handBarrier EXCEPT !.zone = "SetAside",!.loc = "SetAside",!.card = "DrawnA"] bDiscardPileB == [handBarrier EXCEPT !.zone = "SideADiscard",!.loc = "SideADiscard",!.face = "Up"] asideObjects == [id \in {1,2} |-> IF id=1 THEN asideA ELSE bDiscardPileB] asideAfter == [id \in {4,5} |-> IF id=4 THEN [asideA EXCEPT !.zone = "SideADiscard",!.loc = "SideADiscard",!.face = "Up"] ELSE [bDiscardPileB EXCEPT !.zone = "SetAside",!.loc = "SetAside",!.face = "Down"]] transitBase == SetAsideTransit4(1,"SideADeck","DeckTop",40,"DrawAbility",FALSE,FALSE) drawTransit == [key \in DOMAIN transitBase \cup {"drawPlayer"} |-> IF key="drawPlayer" THEN "SideA" ELSE transitBase[key]] beforeTransits == [id \in {1} |-> drawTransit] afterTransits == [id \in {5} |-> [drawTransit EXCEPT !.object = 5,!.originZone = "SideADiscard",!.originLocation = "SideADiscard"]] drawFrame == [OpenDrawBatch8(40,{"SideA"},[p \in {"SideA"} |-> 1],FALSE,"SideA","DrawAbility","caller") EXCEPT !.stage = "Reactions"] arrangeFrame == [OpenDeckArrangement8(40,"SideA","SideA",1,"DrawAbility") EXCEPT !.stage = "OtherEffects"] traversal == [OpenTraversal6(1,10,"action") EXCEPT !.formalBegun = TRUE,!.phase = "Encounter",!.step = "ProcedureCode8b3260c0010f",!.attacked = "r1",!.position = "p1"] IN /\ SwapDeployedCards8(objects,swapped,1,2,checks,500,{}, {swapEvent}) /\ swapped[2].face = "Down" /\ swapped[1].activated /\ swapped[3] = child /\ ~SwapDeployedCards8(objects,swapped,1,2,[checks EXCEPT ![1].gameRulesHold = FALSE],500,{}, {swapEvent}) /\ ~SwapDeployedCards8(objects,swapped,1,2,[checks EXCEPT ![2].cardAbilitiesHold = FALSE],500,{}, {swapEvent}) /\ ~SwapDeployedCards8(objects,swapped,1,2,checks,500,{500}, {swapEvent}) /\ SwapNoLegalExchange8({},objects,objects,{}) /\ ~SwapNoLegalExchange8({<<1,2>>},objects,objects,{}) /\ ComposeArrangementSwap8(frame,arranged,objects,swapped,1,2,500,{},checks,9,9,{}, {},{swapEvent}) /\ ~ComposeArrangementSwap8(frame,arranged,objects,swapped,1,2,500,{},checks,9,10,{}, {},{swapEvent}) /\ ~ComposeArrangementSwap8(frame,arranged,objects,swapped,1,2,500,{},[checks EXCEPT ![1].gameRulesHold = FALSE],9,9,{}, {},{swapEvent}) /\ ComposeSwapBarrierPosition8(layout,swappedLayout,"p1",2,"p2",TRUE) /\ ~ComposeSwapBarrierPosition8(layout,swappedLayout,"p1",2,"p2",FALSE) /\ SwapOtherCards8(crossObjects,crossAfter,1,2,succ,1..3,crossChecks,arrivals,receipt,{}, {3},500,{}, {swapEvent}) /\ SwapHostedRetireDue8(crossObjects,1,2) = {3} /\ ~SwapOtherCards8(crossObjects,crossAfter,1,2,succ,1..3,crossChecks,arrivals,receipt,{}, {},500,{}, {swapEvent}) /\ ~SwapOtherCards8(crossObjects,crossAfter,1,2,succ,1..3,crossChecks,arrivals,[receipt EXCEPT !.deployCostPaid = TRUE],{}, {3},500,{}, {swapEvent}) /\ ~SwapOtherCards8(crossObjects,crossAfter,1,2,succ,1..3,crossChecks,arrivals,[receipt EXCEPT !.likeCardsRetireed = TRUE],{}, {3},500,{}, {swapEvent}) /\ ~SwapOtherCards8(crossObjects,crossAfter,1,2,succ,1..3,crossChecks,arrivals,[receipt EXCEPT !.deployProcedurePerformed = TRUE],{}, {3},500,{}, {swapEvent}) /\ ~SwapOtherCards8(crossObjects,crossAfter,1,2,succ,1..5,crossChecks,arrivals,receipt,{}, {3},500,{}, {swapEvent}) /\ ~SwapTargetPost8(handBarrier,barrierA,[incoming EXCEPT !.face = "Up",!.activated = TRUE],TRUE, [arrivals[2] EXCEPT !.row.face = "Up",!.row.activated = TRUE]) /\ SwapTargetPost8(handBarrier,barrierA,[incoming EXCEPT !.face = "Up",!.activated = TRUE],TRUE, [arrivals[2] EXCEPT !.row.face = "Up",!.row.activated = TRUE,!.faceExceptionAuthorized = TRUE]) /\ SwapTargetPost8(barrierA,[handBarrier EXCEPT !.zone = "SideADiscard"],[outgoing EXCEPT !.zone = "SideADiscard",!.face = "Up"],TRUE, [arrivals[1] EXCEPT !.destination.zone = "SideADiscard",!.row.zone = "SideADiscard",!.row.face = "Up"]) /\ ~SwapTargetPost8(barrierA,[handBarrier EXCEPT !.zone = "SideADiscard"],[outgoing EXCEPT !.zone = "SideADiscard",!.face = "Up"],TRUE, [arrivals[1] EXCEPT !.destination.zone = "SideADiscard",!.row.zone = "SideADiscard",!.row.face = "Up",!.sideBCouldSee = FALSE]) /\ MeetSwapDeployConditions8(conditionPlan,[conditionPlan EXCEPT !.met = TRUE],21,TRUE,deployEvents) /\ ~MeetSwapDeployConditions8(conditionPlan,[conditionPlan EXCEPT !.met = TRUE],20,TRUE,deployEvents) /\ ~MeetSwapDeployConditions8([conditionPlan EXCEPT !.met = TRUE],[conditionPlan EXCEPT !.met = TRUE],21,TRUE,deployEvents) /\ HostDescendants8(objectiveObjects,1) = {3,4} /\ SwapObjectiveFamilies8(objectiveObjects,objectiveAfter,1,2,objectiveSucc,1..4,objectiveChecks,500,{}, {swapEvent}) /\ SwapHostedRetireDue8(objectiveObjects,1,2) = {} /\ ~SwapObjectiveFamilies8(objectiveObjects,[objectiveAfter EXCEPT ![7].host = 1],1,2,objectiveSucc,1..4,objectiveChecks,500,{}, {swapEvent}) /\ ~SwapObjectiveFamilies8(objectiveObjects,objectiveAfter,1,2,objectiveSucc,1..8,objectiveChecks,500,{}, {swapEvent}) /\ TransferSwapAsideGroups8(asideObjects,asideAfter,beforeTransits,afterTransits,1,2,succ) /\ ~TransferSwapAsideGroups8(asideObjects,asideAfter,beforeTransits,[afterTransits EXCEPT ![5].effect = 41],1,2,succ) /\ ~TransferSwapAsideGroups8(asideObjects,asideAfter,beforeTransits,[afterTransits EXCEPT ![5].originZone = "SideADeck"],1,2,succ) /\ DrawnIds8(drawFrame,asideAfter,afterTransits,"SideA") = {5} /\ DrawnIds8(drawFrame,asideAfter,afterTransits,"SideB") = {} /\ AsideGroupIds8(asideAfter,afterTransits,40) = {5} /\ DeckArrangeEffectiveViewers8(arrangeFrame,asideAfter,afterTransits,5,{"SideB"}) = {"SideA","SideB"} /\ SwapDeployedBarrierTraversalPlan8(traversal,"p2","r2").traversal.position = "p2" /\ SwapDeployedBarrierTraversalPlan8(traversal,"p2","r2").traversal.attacked = "r2" /\ SwapBarrierTraversalPlan8(traversal,swapped,1).traversal.position = "p2" /\ SwapBarrierTraversalPlan8(traversal,crossAfter,4).needsRedirect /\ ~SwapBarrierTraversalPlan8([traversal EXCEPT !.phase = "Approach"],crossAfter,4).needsRedirect /\ SwapBarrierTraversalPlan8([traversal EXCEPT !.phase = "Approach"],crossAfter,4).traversal.position = "p1" Block8Assertions == CASE block8 = 0 -> TRUE [] block8 = 1 -> FaceChecks8 [] block8 = 2 -> MovementChecks8 [] block8 = 3 -> ArrangementChecks8 [] block8 = 4 -> DrawChecks8 [] block8 = 5 -> DeployChecks8 [] block8 = 6 -> PlayChecks8 [] block8 = 7 -> SearchChecks8 [] block8 = 8 -> SwapChecks8 =============================================================================