OperationChecksMC¶
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 244 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.
ArrangementChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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"}Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetAsideTransit4, LocationCardFixture8, ArrangeWord8, ArrangementInstructionCheckpointAllowed8, BeginDeckArrangement8, DeckArrangeEffectiveViewers8, DeckArrangeMayLook8, DeckArrangeOtherEffects8, DeckArrangementPublicAction8, DeckArrangementPublicSummary8, ExchangeDeployedLocations8, FinishBarrierArrangement8, FreshSuccessors8, MovementEvent8, NoOpDeckArrangement8, OpenBarrierArrangement8, OpenDeckArrangement8, ReturnDeckArrangement8, SmallArrangement8, SwapArrangingBarrier8
Block8Assertions · operator
reference-profile · input revision 2 · CC0 1.0
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 -> SwapChecks8Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ArrangementChecks8, DeployChecks8, DrawChecks8, FaceChecks8, MovementChecks8, PlayChecks8, SearchChecks8, SwapChecks8, block8
DeployCapacityFixture8 · operator
reference-profile · input revision 2 · CC0 1.0
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]Exact module download · Source bundle and reproduction instructions
DeployCardFixture8 · operator
reference-profile · input revision 2 · CC0 1.0
DeployCardFixture8(card,side,kind,zone,deployed,face,area,targetSite) ==
[card |-> card,form |-> "Card",side |-> side,kind |-> kind,zone |-> zone,loc |-> <<zone,area,targetSite>>,
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]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CentralTargetSites4
DeployChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AuxiliarySiteRegistryCheckpoint4, CentralTargetSites4, TargetSiteRootLimits4, DeployCapacityFixture8, DeployCardFixture8, ActivationCacheValid8, BeginDeploy8, DeclareDeployBarrierPosition8, DeclareDeployDestination8, DeployAndActivationChoiceAllowed8, DeployAtDestination8, DeployBeginEvent8, DeployCardDefaultActive8, DeployDestinationAllowed8, DeployInherentPart8, DeployPendingProjection8, DeployPublicLayout8, DeployRequiredRootRetire8, DeployRetireArrivalFace8, DeployRevealRequired8, DeployStagingRow8, DeployTypeAllowed8, DrainDeployCostBarrier8, FinishDeploy8, FinishDeployActivation8, FinishDeployLikeRetire8, FinishDeployWithoutDeployment8, NextDeployInBatch8, NoDeployDestination8, OccupyDeployBarrierPosition8, OpenActivation8, OpenDeploy8, PayDeployStep8, ReturnDeployToCaller8, StartDeployActivation8, UninstallationOccurred8, VerifyDeployedCard8, WithCardLocation8
DrawChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: LocationCardFixture8, BeginDrawBatch8, ChooseDrawAmount8, CompleteZeroDraw8, DrawAsideTransits8, DrawBatchValid8, DrawChoiceOrder8, DrawDeckoutWinner8, DrawGroupsValid8, DrawLookGrant8, DrawSpecificAbilitySees8, DrawStartEvents8, DrawTransitObservation8, DrawnIds8, FinishDrawReactions8, LockDrawCounts8, OpenDrawBatch8, OpenDrawReactions8, ReturnDrawToCaller8, ReturnDrawnCards8, SetupPlayers
FaceCardFixture8 · operator
reference-profile · input revision 2 · CC0 1.0
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]Exact module download · Source bundle and reproduction instructions
FaceChecks8 · operator
reference-profile · input revision 2 · CC0 1.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"])Exact module download · Source bundle and reproduction instructions
Resolved project definitions: FaceCardFixture8, ActivationCacheValid8, ActivationPermission8, ActivationStatus8, CancelActivation8, Deactivation8, DrainActivationCostCheckpoint8, FinishActivation8, ItemActivatable8, OpenActivation8, PayActivation8, PublicSideBOrigins8, RecordSideBFaceOrigin8, ReturnActivation8, SideBAbilityActivity8, SideBBDiscardPileFacePost8, SideBCharacteristics8, SideBOriginsComplete8, TurnSideBFace8, BarrierChangeTraversalPlan6, OpenTraversal6
Init8 · operator
reference-profile · input revision 2 · CC0 1.0
Init8 == block8 \in 1..8Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block8
LocationCardFixture8 · operator
reference-profile · input revision 2 · CC0 1.0
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]Exact module download · Source bundle and reproduction instructions
MovementChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetAsideTransit4, CardMovements8, DirectRelocationPlan8, DirectRelocations8, ForfeitHostedCleanup8, ForfeitObjectiveCompletionMembership8, ForfeitObjectivePost8, ForfeitPlan8, MovementEvent8, MovementOccurred8, MovementRuleBlock8, RecordMovement8
Next8 · operator
reference-profile · input revision 2 · CC0 1.0
Next8 == UNCHANGED block8Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block8
PlayCardFixture8 · operator
reference-profile · input revision 2 · CC0 1.0
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]]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: DeployCardFixture8
PlayChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: PlayCardFixture8, ActivatePlayedCard8, BeginPlay8, CompletePlay8, DrainPlayCostBarrier8, FinishPlayAbilities8, FinishPlayCleanup8, MeetPlayResolvedConditions8, MeetPlayedConditions8, NextPlayInBatch8, OpenPlay8, OpenPlayAbilities8, PayPlayStep8, PlayCleanupDisposition8, PlayEffectiveCardActivity8, PlayTypeAllowed8, PlayedCondition8, PlayedPlacementRow8, ReturnPlayToCaller8
SearchChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetAsideTransit4, DeployCardFixture8, FinishSearchChoice8, MarkSearchConditions8, OpenSearch8, ResumeSearchAbility8, SearchChainReactionsAllowed8, SearchChoiceAllowed8, SearchFoundActionAllowed8, SearchLookGrant8, SearchRemainingEffectsContinue8, SearchRevealFound8, SearchRevealRequired8, SearchShuffle8
Spec8 · operator
reference-profile · input revision 2 · CC0 1.0
Spec8 == Init8 /\ [][Next8]_block8Exact module download · Source bundle and reproduction instructions
SwapChecks8 · operator
reference-profile · input revision 2 · CC0 1.0
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"Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetAsideTransit4, DeployCardFixture8, AsideGroupIds8, CardLocation8, ComposeArrangementSwap8, ComposeSwapBarrierPosition8, DeckArrangeEffectiveViewers8, DrawnIds8, ExchangeDeployedLocations8, HostDescendants8, MeetSwapDeployConditions8, MovementEvent8, OpenBarrierArrangement8, OpenDeckArrangement8, OpenDrawBatch8, OpenSwapCheckpoint8, SwapBarrierTraversalPlan8, SwapDeployedBarrierTraversalPlan8, SwapDeployedCards8, SwapHostedRetireDue8, SwapNoLegalExchange8, SwapObjectiveFamilies8, SwapOtherCards8, SwapTargetPost8, TransferSwapAsideGroups8, WithCardLocation8, OpenTraversal6
block8 · variable
reference-profile · input revision 2 · CC0 1.0
block8Exact module download · Source bundle and reproduction instructions