----------------------------- MODULE AdditionalContracts ----------------------------- EXTENDS AbilityContracts CounterKinds101 == {"ResourceUnit","ActionPoint","ExposureMarker","LiabilityMarker","PersistentCapacityLoss","Progress","SchemaAtom180","Power","Objective","SchemaAtom043"} Without101(f,keys) == [k \in DOMAIN f \ keys |-> f[k]] UniqueActivationPlan101(objects,names,unique,beforeActive,afterActive,newlyActive) == LET applicable == newlyActive \in DOMAIN objects /\ newlyActive \in DOMAIN names /\ newlyActive \in unique /\ newlyActive \notin beforeActive /\ newlyActive \in afterActive cohort == IF newlyActive \in DOMAIN names THEN {i \in ((afterActive \ beforeActive) \cap DOMAIN objects \cap DOMAIN names) : names[i]=names[newlyActive]} ELSE {} disposition == IF ~applicable THEN "NotApplicable" ELSE IF cohort={newlyActive} THEN "Supported" ELSE "UnsupportedSimultaneousActivation" IN [valid |-> disposition="Supported",disposition |-> disposition, targets |-> IF disposition="Supported" THEN {i \in (afterActive \cap DOMAIN objects \cap DOMAIN names) \ {newlyActive} : names[i]=names[newlyActive]} ELSE {}, timing |-> "NextCheckpoint",preventable |-> FALSE] UniqueActivationRetire101(plan,actuallyRetireed,actualCheckpointStage,preventionApplied) == /\ plan.valid /\ actualCheckpointStage="ProcedureCodefe50c31480ea" /\ actuallyRetireed=plan.targets /\ ~preventionApplied PurgeClusterIds101(objects) == {i \in DOMAIN objects : objects[i].form="Counter" /\ objects[i].kind="SchemaAtom180" /\ ~objects[i].virtual /\ objects[i].host \in DOMAIN objects /\ objects[objects[i].host].form="Card"} PurgeClusterPlan101(objects) == LET targets==PurgeClusterIds101(objects) IN [targets |-> targets, bank |-> {i \in targets : objects[i].card="none"}, revertAndRetire |-> {i \in targets : objects[i].card#"none"}] PurgeClusterOriginalProjectionPost101(objects,afterObjects,returnedToBank,revertedAndRetireed) == LET plan==PurgeClusterPlan101(objects) IN /\ returnedToBank=plan.bank /\ revertedAndRetireed=plan.revertAndRetire /\ DOMAIN afterObjects=DOMAIN objects \ plan.targets /\ \A i \in DOMAIN afterObjects : afterObjects[i]=objects[i] ConversionValid101(c) == /\ c.mode \in {"Objective","Counter"} /\ c.card#"none" /\ c.createdBy \in Nat \ {0} /\ c.owner \in SetupPlayers /\ IF c.mode="Objective" THEN /\ "kind" \in DOMAIN c.gained /\ c.gained.kind="Objective" /\ "objectivePoints" \in DOMAIN c.gained /\ c.gained.objectivePoints \in Int ELSE /\ "kind" \in DOMAIN c.gained /\ c.gained.kind \in CounterKinds101 ConversionRetained101(c,oldZone,newZone) == IF c.mode="Objective" THEN oldZone \in SetupObjectiveZones /\ newZone \in SetupObjectiveZones ELSE oldZone=newZone ConversionProperties101(c,printed,oldZone,newZone) == IF ConversionRetained101(c,oldZone,newZone) THEN c.gained ELSE printed ConversionExitPlan101(c,printed,oldZone,newZone,movement) == [converted |-> ConversionRetained101(c,oldZone,newZone), properties |-> ConversionProperties101(c,printed,oldZone,newZone), trashImmediately |-> ~ConversionRetained101(c,oldZone,newZone) /\ ~(c.mode="Objective" /\ movement="Forfeit")] ConversionExitPost101(c,printed,oldObject,successor,sourceObjects,afterObjects,usedIds, destination,movement,actualRetireReceipt) == /\ ConversionValid101(c) /\ oldObject \in DOMAIN sourceObjects /\ sourceObjects[oldObject].card=c.card /\ successor \in DOMAIN afterObjects /\ afterObjects[successor].card=c.card /\ DOMAIN sourceObjects \subseteq usedIds /\ DOMAIN afterObjects=(DOMAIN sourceObjects \ {oldObject}) \cup {successor} /\ \A i \in DOMAIN sourceObjects \ {oldObject} : afterObjects[i]=sourceObjects[i] /\ sourceObjects[oldObject].owner=c.owner /\ afterObjects[successor].owner=c.owner /\ sourceObjects[oldObject].kind=c.gained.kind /\ sourceObjects[oldObject].form=(IF c.mode="Objective" THEN "Card" ELSE "Counter") /\ oldObject#successor /\ successor \notin usedIds /\ oldObject \notin DOMAIN afterObjects /\ sourceObjects[oldObject].zone#destination /\ LET plan==ConversionExitPlan101(c,printed,sourceObjects[oldObject].zone,destination,movement) IN /\ ~plan.converted /\ afterObjects[successor].form="Card" /\ afterObjects[successor].properties=printed /\ afterObjects[successor].kind=printed.kind /\ afterObjects[successor].host=0 /\ ~afterObjects[successor].deployed /\ IF plan.trashImmediately THEN /\ actualRetireReceipt.original=oldObject /\ actualRetireReceipt.successor=successor /\ actualRetireReceipt.physical=c.card /\ actualRetireReceipt.complete /\ actualRetireReceipt.owner=c.owner /\ afterObjects[successor].zone=actualRetireReceipt.owner \o "Discard" ELSE movement="Forfeit" /\ destination="Removed" /\ afterObjects[successor].zone="Removed" NamedReference101(source,printedOwnName,referenceName,copyQualifier,objects,currentNames) == IF referenceName=printedOwnName /\ ~copyQualifier THEN {source} ELSE {i \in DOMAIN objects \cap DOMAIN currentNames : currentNames[i]=referenceName} LoopTrait101(kind,duringTraversal,withdrawTraversalProhibited) == CASE kind="Mandatory" -> "ChooseCount" [] kind="Optional" /\ duringTraversal /\ ~withdrawTraversalProhibited -> "SideBWithdrawTraversal" [] kind="Optional" /\ duringTraversal /\ withdrawTraversalProhibited -> "SideAContinueTraversal" [] OTHER -> "NoRuleIn10.1.6" ResolveMandatoryLoop101(frame,afterFrame,beforeGame,afterGame,count,witness,Iteration(_,_)) == /\ frame.kind="Mandatory" /\ frame.phase="Detected" /\ frame.resolver \in SetupPlayers /\ count \in Nat /\ Len(witness)=count+1 /\ witness[1]=beforeGame /\ witness[count+1]=afterGame /\ \A i \in 1..count : Iteration(witness[i],witness[i+1]) /\ afterFrame=[frame EXCEPT !.phase="Ended",!.iterations=count] ResolveOptionalTraversalLoop101(frame,afterFrame,withdrawTraversalProhibited,actor,actualTraversalDisposition) == /\ frame.kind="Optional" /\ frame.phase="Detected" /\ frame.traversal \in Nat \ {0} /\ IF withdrawTraversalProhibited THEN actor="SideA" /\ actualTraversalDisposition="Continue" ELSE actor="SideB" /\ actualTraversalDisposition="WithdrawTraversal" /\ afterFrame=[frame EXCEPT !.phase="Ended",!.disposition=actualTraversalDisposition] InformationClass102(viewers) == IF viewers=SetupPlayers THEN "Open" ELSE "Hidden" InformationFact102(value,viewers,snapshot) == [value |-> value,viewers |-> viewers,snapshot |-> snapshot] CurrentLookViewers102(object,objects,actualLiveGrants) == UNION {actualLiveGrants[g].viewers : g \in {g \in DOMAIN actualLiveGrants : actualLiveGrants[g].object=object /\ actualLiveGrants[g].zone=objects[object].zone /\ actualLiveGrants[g].loc=objects[object].loc}} CardProfileFact102(object,objects,controllers,actualLiveGrants,snapshot) == InformationFact102(objects[object].card, {p \in SetupPlayers : DefaultZoneLook4(objects[object].zone,objects[object].face,p,controllers[object])} \cup CurrentLookViewers102(object,objects,actualLiveGrants),snapshot) ZoneCountFact102(zone,objects,snapshot) == InformationFact102(Cardinality({i \in DOMAIN objects : objects[i].form="Card" /\ objects[i].zone=zone}),SetupPlayers,snapshot) ResourceUnitPoolFact102(player,objects,snapshot) == InformationFact102(Cardinality({i \in DOMAIN objects : objects[i].form="Counter" /\ objects[i].kind="ResourceUnit" /\ objects[i].zone=player \o "ResourceUnits"}),SetupPlayers,snapshot) PublicChoiceFacts102(actualOpenRememberedChoices,snapshot) == [id \in DOMAIN actualOpenRememberedChoices |-> InformationFact102(actualOpenRememberedChoices[id],SetupPlayers,snapshot)] CoreInformationCatalog102(objects,controllers,actualLiveGrants,actualOpenRememberedChoices,snapshot) == LET keys=={<<"CardProfile",id>> : id \in {i \in DOMAIN objects : objects[i].form="Card"}} \cup {<<"ZoneCount",z>> : z \in {"SideAHand","SideADeck","SideBHand","SideBDeck"}} \cup {<<"ResourceUnitPool",p>> : p \in SetupPlayers} \cup {<<"Choice",id>> : id \in DOMAIN actualOpenRememberedChoices} choices==PublicChoiceFacts102(actualOpenRememberedChoices,snapshot) IN [key \in keys |-> CASE key[1]="CardProfile" -> CardProfileFact102(key[2],objects,controllers,actualLiveGrants,snapshot) [] key[1]="ZoneCount" -> ZoneCountFact102(key[2],objects,snapshot) [] key[1]="ResourceUnitPool" -> ResourceUnitPoolFact102(key[2],objects,snapshot) [] OTHER -> choices[key[2]]] PlayerInformationView102(facts,player,currentSnapshot) == [id \in {i \in DOMAIN facts : player \in facts[i].viewers /\ facts[i].snapshot=currentSnapshot} |-> facts[id].value] ObserveCurrentInformation102(before,after,facts,fact,player,currentSnapshot) == /\ player \in SetupPlayers /\ fact \in DOMAIN facts /\ facts[fact].snapshot=currentSnapshot /\ player \in facts[fact].viewers /\ after=Append(before,[tag |-> "AuthoritativeObservation",player |-> player,fact |-> fact, value |-> facts[fact].value,snapshot |-> currentSnapshot]) CommunicateInformation102(beforeTranscript,afterTranscript,beforeTruth,afterTruth, facts,fact,speaker,recipient,claimedValue,currentSnapshot) == /\ speaker \in SetupPlayers /\ recipient \in SetupPlayers \ {speaker} /\ fact \in DOMAIN facts /\ facts[fact].snapshot=currentSnapshot /\ speaker \in facts[fact].viewers /\ InformationClass102(facts[fact].viewers)="Open" => claimedValue=facts[fact].value /\ afterTruth=beforeTruth /\ afterTranscript=Append(beforeTranscript,[tag |-> "Claim",speaker |-> speaker,recipient |-> recipient, fact |-> fact,value |-> claimedValue,snapshot |-> currentSnapshot, verifiedOpen |-> InformationClass102(facts[fact].viewers)="Open"]) DiscoverOpenInformation102(facts,player,requested,responses,currentSnapshot) == /\ player \in SetupPlayers /\ requested \subseteq DOMAIN facts /\ \A id \in requested : facts[id].viewers=SetupPlayers /\ facts[id].snapshot=currentSnapshot /\ responses=[id \in requested |-> [value |-> facts[id].value,snapshot |-> currentSnapshot]] CheckpointStages103 == <<"ProcedureCodee605a78f5d5e","ProcedureCode88eda145024f","ProcedureCodeb681cc249a04","ProcedureCodefe50c31480ea","ProcedureCodea488e1ba6ca3","ProcedureCode76ca53ad9dd0", "ProcedureCode96bfa1b6a970","ProcedureCode2d73b20aa788","ProcedureCode2d6279f9d639","ProcedureCode7f181ce21011","ProcedureCodeda83a77a1f12","ProcedureCode0811ebc5f40e">> CheckpointStageSet103 == {CheckpointStages103[i] : i \in 1..Len(CheckpointStages103)} NewCheckpoint103(id,caller,beginSnapshotId,insideStructures) == [id |-> id,caller |-> caller,beginSnapshotId |-> beginSnapshotId,snapshotId |-> beginSnapshotId, inside |-> insideStructures,point |-> "ProcedureCodee605a78f5d5e",owed |-> CheckpointStages103,done |-> {},discharged |-> {}, recognition |-> [id |-> 0,caller |-> "NoValue"],recognized |-> [emptyId \in {} |-> emptyId],phase |-> "Steps",returned |-> FALSE, windowId |-> 0,outcome |-> "Playing",overrideLog |-> <<>>,hostPasses |-> 0,retiredRemotes |-> {}] CheckpointAt103(f,stage) == f.id \in Nat \ {0} /\ f.phase="Steps" /\ ~f.returned /\ Len(f.owed)>0 /\ f.point=stage /\ f.owed[1]=stage CheckpointStageAdvance103(before,after,stage,newSnapshotId) == /\ CheckpointAt103(before,stage) /\ stage \in CheckpointStageSet103 /\ LET rest==SubSeq(before.owed,2,Len(before.owed)) IN after=[before EXCEPT !.owed=rest,!.done=@ \cup {stage},!.snapshotId=newSnapshotId, !.point=IF rest= <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE rest[1],!.phase=IF rest= <<>> THEN "Completed" ELSE "Steps"] CheckpointMemberMap103(ledger,cpId) == [id \in PersistentRecognizedIds912(ledger,cpId) |-> ledger.instances[id].member] CheckpointCaptured103(frame,ledger) == /\ frame.recognition.id#0 /\ frame.recognition.id=frame.id /\ frame.recognition.caller=frame.caller /\ frame.id \in DOMAIN ledger.checkpoints /\ ledger.checkpoints[frame.id].caller=frame.caller /\ frame.recognized=CheckpointMemberMap103(ledger,frame.id) CheckpointSite103(site,event,insideStructures) == /\ site.snapshotId \in Nat \ {0} /\ site.caller=event.caller /\ site.eventId=event.id /\ event.id \in Nat \ {0} /\ event.complete /\ CASE site.kind="SchemaAtom126" -> event.tag="PriorityAboutToBeReceived" /\ event.player \in SetupPlayers [] site.kind="Cost" -> event.tag="CostPaid" /\ event.transactionId \in Nat \ {0} [] site.kind="Instruction" -> event.tag="InstructionFinished" /\ event.origin \in {"Ability","TimingStep"} /\ event.instruction \notin CheckpointStageSet103 \cup {"ProcedureCodeb74d673a0fc6"} [] site.kind="StructureEnd" -> event.tag="TimingStructureEnded" /\ TimingRefValid9(event.structure) [] OTHER -> FALSE /\ site.inside=IF site.kind="StructureEnd" THEN insideStructures \ {event.structure} ELSE insideStructures OpenCheckpointAtSite103(frame,id,site,event,insideStructures,usedCheckpoints) == /\ CheckpointSite103(site,event,insideStructures) /\ id \in (Nat \ {0}) \ usedCheckpoints /\ frame=NewCheckpoint103(id,site.caller,site.snapshotId,site.inside) RecognizeCheckpoint103(before,after,beforeLedger,afterLedger,beforeStack,afterStack,x) == /\ CheckpointAt103(before,"ProcedureCodee605a78f5d5e") /\ x.cp.id=before.id /\ x.cp.caller=before.caller /\ x.cp.beginSnapshot.id=before.beginSnapshotId /\ x.cp.processingSnapshot.id=before.snapshotId /\ CASE x.route="Persistent" -> ProcessPersistentCheckpoint912(x.registry,beforeLedger,afterLedger,beforeStack,afterStack,x.definitions,x.lexemes,x.cp, x.conditions,x.allocation,x.bindings,x.departures,x.holds,x.scope,x.usedWindows,x.cardFacts,x.world,x.authority) [] x.route="Ordinary" -> ProcessConditionalCheckpoint99(beforeLedger,afterLedger,beforeStack,afterStack,x.definitions,x.lexemes,x.cp, x.conditions,x.allocation,x.bindings,x.departures,x.holds,x.usedWindows,x.cardFacts) [] OTHER -> FALSE /\ LET advanced==[after EXCEPT !.recognition=before.recognition,!.recognized=before.recognized] IN /\ CheckpointStageAdvance103(before,advanced,"ProcedureCodee605a78f5d5e",before.snapshotId) /\ after=[advanced EXCEPT !.recognition=x.cp,!.recognized=CheckpointMemberMap103(afterLedger,before.id)] CheckpointPrivatePersistentBound103(frame,registry,ledger) == /\ frame.phase \in {"Steps","Completed"} /\ CheckpointCaptured103(frame,ledger) /\ PersistentCheckpointBound912(registry,[ledger EXCEPT !.checkpoints=Without101(@,{frame.id})]) ObserveCheckpointKernel103(frame,beforeRegistry,afterRegistry,beforeLedger,afterLedger,beforeStack,afterStack, beforeSnapshot,afterSnapshot,baseWorld,execution,beforeAuthority,afterAuthority) == /\ CheckpointPrivatePersistentBound103(frame,beforeRegistry,beforeLedger) /\ frame.snapshotId=beforeAuthority.current.id /\ LifetimeReady910(beforeRegistry,beforeAuthority) /\ PersistentRegistryWorldBound912(beforeRegistry,beforeAuthority.current) /\ PersistentConditionalDefinitions912(beforeRegistry,beforeSnapshot.definitions) /\ afterAuthority.current=PersistentWorld912(baseWorld,beforeRegistry) /\ CommitLifetimeKernelCore910(beforeAuthority,afterAuthority,afterAuthority.current,execution) /\ LET local==[afterRegistry EXCEPT !.frontier=beforeRegistry.frontier] IN /\ ObserveLingering910(beforeRegistry,local,afterAuthority.current) /\ afterRegistry.frontier=LifetimeFrontier910(afterAuthority,Len(afterAuthority.order)) /\ PersistentRegistryWorldBound912(afterRegistry,afterAuthority.current) /\ beforeSnapshot.id=beforeAuthority.current.id /\ afterSnapshot.id=afterAuthority.current.id /\ LingeringConditionalWorld910(beforeSnapshot,beforeLedger,beforeAuthority.current) /\ LingeringConditionalWorld910(afterSnapshot,beforeLedger,afterAuthority.current) /\ afterSnapshot=LingeringConditionalSnapshot910(afterSnapshot,local,beforeLedger,afterAuthority.current) /\ PersistentConditionalDefinitions912(local,afterSnapshot.definitions) /\ ObserveConditionalActivity96(beforeLedger,beforeLedger,afterLedger,beforeStack,afterStack,beforeSnapshot,afterSnapshot) /\ CheckpointCaptured103(frame,afterLedger) CheckpointCompletion103(frame,ledger,world,receipt) == /\ frame.phase="Completed" /\ ~frame.returned /\ frame.point="ProcedureCodeb74d673a0fc6" /\ frame.owed= <<>> /\ frame.done \cup frame.discharged=CheckpointStageSet103 /\ frame.done \cap frame.discharged={} /\ CheckpointCaptured103(frame,ledger) /\ frame.snapshotId=world.id /\ frame.outcome="Playing" /\ receipt=PersistentCheckpointCompletion912(ledger,frame.recognition,world) CheckpointRecognizedWindow103(frame) == IF DOMAIN frame.recognized={} THEN 0 ELSE frame.recognized[CHOOSE id \in DOMAIN frame.recognized : TRUE].windowId CutoffPersistentAtCheckpoint103(before,after,ledger,frame,completion,beforeEnd,afterEnd,events,expired,boundary) == /\ CheckpointCompletion103(frame,ledger,before.frontier.world,completion) /\ CompleteTraversal6(beforeEnd,afterEnd,TRUE,events,expired) /\ CheckpointPrivatePersistentBound103(frame,before,ledger) /\ PersistentRegistryWorldBound912(before,before.frontier.world) /\ before.frontier.world.control.traversal=afterEnd.traversal /\ frame.caller=PersistentTraversalEndCaller912(afterEnd.traversal.id) /\ \E id \in DOMAIN frame.recognition.occurrences : /\ frame.recognition.occurrences[id].kind="TraversalEnds" /\ frame.recognition.occurrences[id].traversal=afterEnd.traversal /\ frame.recognition.occurrences[id].actualEvent \in events /\ frame.recognition.occurrences[id].actualEvent=[tag |-> "TraversalEnds",traversalId |-> afterEnd.traversal.id] /\ \A id \in DOMAIN frame.recognized : frame.recognized[id].windowId=CheckpointRecognizedWindow103(frame) /\ boundary=[tag |-> "PersistentLastCreationCheckpoint",traversal |-> afterEnd.traversal,checkpointId |-> frame.id,caller |-> frame.caller, windowId |-> CheckpointRecognizedWindow103(frame),completion |-> completion] /\ LET keys=={key \in DOMAIN before.persistent : before.persistent[key].phase="Persisting" /\ before.persistent[key].traversalId=afterEnd.traversal.id} IN /\ keys#{} /\ \A key \in keys : before.persistent[key].creationOpen /\ after=[before EXCEPT !.persistent=[key \in DOMAIN @ |-> IF key \in keys THEN [@[key] EXCEPT !.creationOpen=FALSE,!.endCheckpoint=frame.id,!.endWindow=boundary.windowId, !.endMembers=DOMAIN frame.recognized] ELSE @[key]]] /\ PersistentRegistryWorldBound912(after,after.frontier.world) /\ PersistentCheckpointBound912(after,ledger) OpenCheckpointReaction103(before,after,ledger,beforeStack,afterStack,site,opening,usedWindows) == /\ DOMAIN before.recognized#{} /\ CheckpointCaptured103(before,ledger) /\ CheckpointCompletion103(before,ledger,[id |-> before.snapshotId],opening.completion) /\ opening.checkpointId=before.id /\ opening.caller=before.caller /\ opening.windowId=CheckpointRecognizedWindow103(before) /\ \A id \in DOMAIN before.recognized : before.recognized[id].windowId=opening.windowId /\ LET canonicalOpening==[opening EXCEPT !.completion=opening.completion] raw==Append(beforeStack,NewPriorityWindow9(opening.windowId,"Reaction",PriorityOpeningSite9(beforeStack,site), before.recognized,opening.group,opening.beginning,opening.instruction,opening.effectRevision)) pending=={id \in DOMAIN before.recognized : ledger.instances[id].status="Pending"} IN /\ OpenPriorityWindow9(beforeStack,raw,opening.windowId,"Reaction",site,before.recognized,canonicalOpening,usedWindows) /\ afterStack=ReplaceWindowTop9(raw,[WindowTop9(raw) EXCEPT !.pending=pending,!.lostPending=DOMAIN before.recognized \ pending]) /\ after=[before EXCEPT !.phase="Reaction",!.windowId=opening.windowId] ReturnCheckpointWithoutReaction103(before,after,ledger,world,completion,caller) == /\ CheckpointCompletion103(before,ledger,world,completion) /\ DOMAIN before.recognized={} /\ caller=before.caller /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE] ReturnCheckpointAfterReaction103(before,after,ledger,beforeStack,afterStack,caller) == /\ before.phase="Reaction" /\ ~before.returned /\ caller=before.caller /\ CheckpointCaptured103(before,ledger) /\ DOMAIN before.recognized#{} /\ ConditionalCheckpointDrained96(ledger,beforeStack,before.id) /\ Len(beforeStack)>0 /\ WindowTop9(beforeStack).id=before.windowId /\ DOMAIN WindowTop9(beforeStack).members=DOMAIN before.recognized /\ \A id \in DOMAIN before.recognized : WindowTop9(beforeStack).members[id]=before.recognized[id] /\ PopClosedPriorityWindow9(beforeStack,afterStack) /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE] RewriteCheckpointOrder103(before,after,a,execution,compiledExceptions) == /\ before.phase="Steps" /\ ~before.returned /\ a.id \in DOMAIN compiledExceptions /\ compiledExceptions[a.id]=a /\ a.checkpointId=before.id /\ a.snapshotId=before.snapshotId /\ a.rule="CheckpointOrder" /\ a.directContradiction /\ ~a.prohibited /\ a.source.kind="Object" /\ a.source.object \in Nat \ {0} /\ execution.tag="ActualCheckpointCardOverride" /\ execution.id=a.executionId /\ execution.source=a.source /\ execution.instruction=a.instruction /\ execution.checkpointId=before.id /\ execution.snapshotId=before.snapshotId /\ execution.resolved /\ a.beforeOwed=before.owed /\ a.discharged \subseteq SetupRange(before.owed) /\ a.discharged \subseteq a.explicitlyReplacedObligations /\ SetupRange(a.afterOwed)=SetupRange(before.owed) \ a.discharged /\ Len(a.afterOwed)=Cardinality(SetupRange(a.afterOwed)) /\ after=[before EXCEPT !.owed=a.afterOwed,!.discharged=@ \cup a.discharged,!.overrideLog=Append(@,a), !.point=IF a.afterOwed = <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE a.afterOwed[1],!.phase=IF a.afterOwed = <<>> THEN "Completed" ELSE "Steps"] CheckpointPhysicalIds103(objects) == {id \in DOMAIN objects : ~objects[id].virtual} CheckpointRetireMap103(objects,selected,successors,printed,owners,sideBVisible) == LET cards=={id \in selected : objects[id].card#"none"} fresh=={successors[id] : id \in cards} IN [id \in (DOMAIN objects \ selected) \cup fresh |-> IF id \notin fresh THEN objects[id] ELSE LET old==CHOOSE old \in cards : successors[old]=id o==objects[old] IN [o EXCEPT !.form="Card",!.kind=printed[o.card].kind,!.properties=printed[o.card], !.zone=owners[o.card] \o "Discard",!.loc="discard",!.host=0,!.deployed=FALSE,!.activated=FALSE,!.marks={}, !.face=DiscardArrivalFace4(owners[o.card],o.zone,"Retire",old \in sideBVisible)]] CheckpointRetirePost103(objects,afterObjects,selected,successors,usedIds,printed,owners,sideBVisible) == /\ selected \subseteq CheckpointPhysicalIds103(objects) /\ DOMAIN objects \subseteq usedIds /\ FreshSuccessors8({id \in selected : objects[id].card#"none"},successors,usedIds) /\ afterObjects=CheckpointRetireMap103(objects,selected,successors,printed,owners,sideBVisible) CheckpointCleanupEffects103(before,after,beforeRegistry,afterRegistry,beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack, beforeSnapshot,afterSnapshot,world,cleanupFrame,afterCleanupFrame,actualCleanup) == /\ CheckpointAt103(before,"ProcedureCode88eda145024f") /\ CheckpointCaptured103(before,beforeLedger) /\ cleanupFrame.checkpointId=before.id /\ cleanupFrame.recognition=before.recognition /\ CleanupLingeringConditionals910(beforeRegistry,afterRegistry,beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack, beforeSnapshot,afterSnapshot,world,cleanupFrame,afterCleanupFrame,actualCleanup) /\ CheckpointStageAdvance103(before,after,"ProcedureCode88eda145024f",world.id) ExpiredRetainedPlayIds103(retentions,objects,liveIds) == {retentions[id].source : id \in {i \in DOMAIN retentions \ liveIds : retentions[i].source \in DOMAIN objects /\ objects[retentions[i].source].zone="Play"}} CheckpointRetentionRetire103(frame,retentions,afterRetentions,objects,afterObjects,liveIds,successors,usedIds,printed,owners,sideBVisible) == /\ CheckpointAt103(frame,"ProcedureCode88eda145024f") /\ liveIds \subseteq DOMAIN retentions /\ CheckpointRetirePost103(objects,afterObjects,ExpiredRetainedPlayIds103(retentions,objects,liveIds),successors,usedIds,printed,owners,sideBVisible) /\ afterRetentions=Without101(retentions,DOMAIN retentions \ liveIds) CheckpointObjectiveOutcome103(objects,effectivePoints) == LET points==[p \in SetupPlayers |-> ObjectiveAreaPoints4(objects,p,effectivePoints)] winners=={p \in SetupPlayers : points[p]>=7} IN CASE winners={} -> "Playing" [] winners=SetupPlayers -> "Draw" [] OTHER -> CHOOSE p \in winners : TRUE CheckpointVictory103(before,after,objects,effectivePoints,currentSnapshot) == /\ CheckpointAt103(before,"ProcedureCodeb681cc249a04") /\ before.snapshotId=currentSnapshot /\ LET result==CheckpointObjectiveOutcome103(objects,effectivePoints) IN IF result="Playing" THEN CheckpointStageAdvance103(before,after,"ProcedureCodeb681cc249a04",currentSnapshot) ELSE after=[before EXCEPT !.outcome=result,!.phase="SchemaAtom160",!.point="GameEnded"] CheckpointLatestExists103(group,activationOrder) == group \subseteq DOMAIN activationOrder /\ \E id \in group : \A other \in group \ {id} : activationOrder[id]>activationOrder[other] CheckpointLatest103(group,activationOrder) == CHOOSE id \in group : \A other \in group \ {id} : activationOrder[id]>activationOrder[other] CheckpointUniquePlan103(objects,names,unique,active,consoles,controllers,activationOrder) == LET activeCards==active \cap {id \in DOMAIN objects : objects[id].form="Card"} uniqueNames=={names[id] : id \in unique \cap activeCards} mixed==\E name \in uniqueNames : \E id \in activeCards \ unique : names[id]=name uniqueGroups=={{id \in unique \cap activeCards : names[id]=name} : name \in uniqueNames} consoleGroups=={{id \in consoles \cap DOMAIN objects : objects[id].deployed /\ controllers[id]=player} : player \in SetupPlayers} groups=={group \in uniqueGroups \cup consoleGroups : Cardinality(group)>1} supported==~mixed /\ \A group \in groups : CheckpointLatestExists103(group,activationOrder) IN [disposition |-> IF mixed THEN "UnsupportedMixedUniqueness" ELSE IF supported THEN "Supported" ELSE "UnsupportedActivationTie", targets |-> IF supported THEN UNION {group \ {CheckpointLatest103(group,activationOrder)} : group \in groups} ELSE {}] CheckpointUniqueRetire103(before,after,objects,afterObjects,names,unique,active,consoles,controllers,activationOrder, successors,usedIds,printed,owners,sideBVisible,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCodefe50c31480ea") /\ LET plan==CheckpointUniquePlan103(objects,names,unique,active,consoles,controllers,activationOrder) IN /\ plan.disposition="Supported" /\ CheckpointRetirePost103(objects,afterObjects,plan.targets,successors,usedIds,printed,owners,sideBVisible) /\ CheckpointStageAdvance103(before,after,"ProcedureCodefe50c31480ea",newSnapshotId) AppropriateRetireSets103(eligible,LegalAfterRetire(_)) == {selected \in SUBSET eligible : LegalAfterRetire(selected) /\ \A smaller \in SUBSET selected : smaller#selected => ~LegalAfterRetire(smaller)} IllegalRetireChooser103(choices,controllers,activePlayer) == LET objects==UNION choices players=={controllers[id] : id \in objects} IN IF Cardinality(choices)<=1 THEN "NoValue" ELSE IF Cardinality(players)=1 /\ players \subseteq SetupPlayers THEN CHOOSE p \in players : TRUE ELSE activePlayer CheckpointIllegalRetire103(before,after,objects,afterObjects,eligible,LegalAfterRetire(_),controllers,activePlayer,auxiliarySiteTargetSites,auxiliarySiteLimit,chooser,selected, successors,usedIds,printed,owners,sideBVisible,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCodea488e1ba6ca3") /\ eligible \subseteq CheckpointPhysicalIds103(objects) /\ IF auxiliarySiteLimit.applies THEN Cardinality(AuxiliarySiteTargetSiteIds4(Without101(auxiliarySiteTargetSites,before.retiredRemotes)))<=auxiliarySiteLimit.value ELSE TRUE /\ LET choices==AppropriateRetireSets103(eligible,LegalAfterRetire) IN /\ selected \in choices /\ chooser=IllegalRetireChooser103(choices,controllers,activePlayer) /\ CheckpointRetirePost103(objects,afterObjects,selected,successors,usedIds,printed,owners,sideBVisible) /\ CheckpointStageAdvance103(before,after,"ProcedureCodea488e1ba6ca3",newSnapshotId) CheckpointAuxiliarySiteLimit103(before,after,targetSites,objects,afterObjects,keep,effectiveLimit, successors,usedIds,printed,owners,sideBVisible,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCodea488e1ba6ca3") /\ LET remaining==Without101(targetSites,before.retiredRemotes) plan==AuxiliarySiteLimitPlan4(remaining,keep,effectiveLimit,objects) retired==AuxiliarySiteTargetSiteIds4(remaining) \ keep IN /\ Cardinality(AuxiliarySiteTargetSiteIds4(remaining))>effectiveLimit /\ plan.valid /\ plan.chooser="SideA" /\ CheckpointRetirePost103(objects,afterObjects,plan.trash,successors,usedIds,printed,owners,sideBVisible) /\ after=[before EXCEPT !.retiredRemotes=@ \cup retired,!.snapshotId=newSnapshotId] RecordHostDeparture103(beforeHistory,afterHistory,eventId,beforeObjects,afterObjects,source,sourceAfter,hostedSuccessors) == /\ eventId \in Nat \ {0} /\ <<"Movement",eventId>> \notin DOMAIN beforeHistory /\ source \in DOMAIN beforeObjects /\ sourceAfter \in DOMAIN afterObjects /\ afterObjects[sourceAfter].card=beforeObjects[source].card /\ LET hosted=={id \in DOMAIN beforeObjects : beforeObjects[id].host=source} current=={IF id \in DOMAIN hostedSuccessors THEN hostedSuccessors[id] ELSE id : id \in hosted} objectiveCompletionLeft==beforeObjects[source].form="Card" /\ beforeObjects[source].kind="Objective" /\ beforeObjects[source].zone \in SetupObjectiveZones /\ afterObjects[sourceAfter].zone \notin SetupObjectiveZones uninstalled==beforeObjects[source].form="Card" /\ beforeObjects[source].deployed /\ ~afterObjects[sourceAfter].deployed IN /\ DOMAIN hostedSuccessors \subseteq hosted /\ \A id \in DOMAIN hostedSuccessors : hostedSuccessors[id] \in DOMAIN afterObjects /\ afterObjects[hostedSuccessors[id]].card=beforeObjects[id].card /\ hostedSuccessors[id]#id /\ id \notin DOMAIN afterObjects /\ objectiveCompletionLeft \/ uninstalled /\ afterHistory=[id \in DOMAIN beforeHistory \cup {<<"Movement",eventId>>} |-> IF id= <<"Movement",eventId>> THEN [source |-> source,objectiveCompletionLeft |-> objectiveCompletionLeft,uninstalled |-> uninstalled,hostRemoved |-> uninstalled \/ objectiveCompletionLeft,children |-> current] ELSE beforeHistory[id]] CheckpointProtectedIds103(objects,transits,paidProcedures) == UNION {{id \in DOMAIN objects : PaidHeldObject95(paidProcedures[p],objects,transits,id)} : p \in {p \in DOMAIN paidProcedures : paidProcedures[p].id=p /\ PaidProtectionAlive95(paidProcedures[p])}} CheckpointHostedTargets103(objects,departures,kind,transits,paidProcedures) == LET historical==UNION {departures[id].children : id \in {id \in DOMAIN departures : IF kind="ProcedureCode76ca53ad9dd0" THEN departures[id].objectiveCompletionLeft ELSE departures[id].uninstalled \/ departures[id].hostRemoved}} finished=={p \in DOMAIN paidProcedures : paidProcedures[p].ability.lastFinished} IN ((historical \cap DOMAIN objects) \ CheckpointProtectedIds103(objects,transits,paidProcedures)) \cup CostAsideCleanupIds4(transits,objects,finished,kind) CheckpointNewUninstallDepartures103(objects,selected) == [key \in {<<"CleanupUninstall",i>> : i \in selected} |-> [source |-> key[2],objectiveCompletionLeft |-> FALSE,uninstalled |-> objects[key[2]].form="Card" /\ objects[key[2]].deployed,hostRemoved |-> TRUE, children |-> {child \in DOMAIN objects : objects[child].host=key[2]}]] MergeCheckpointDepartures103(before,added) == [id \in DOMAIN before \cup DOMAIN added |-> IF id \in DOMAIN added THEN added[id] ELSE before[id]] CheckpointHostedCleanup103(before,after,objects,afterObjects,departures,afterDepartures,transits,paidProcedures, successors,usedIds,printed,owners,sideBVisible,newSnapshotId) == /\ before.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} /\ CheckpointAt103(before,before.point) /\ \A p \in DOMAIN paidProcedures : paidProcedures[p].id=p /\ PaidHeldProvenance95(paidProcedures[p],objects,transits) /\ LET due==CheckpointHostedTargets103(objects,departures,before.point,transits,paidProcedures) added==CheckpointNewUninstallDepartures103(objects,due) IN /\ CheckpointRetirePost103(objects,afterObjects,due,successors,usedIds,printed,owners,sideBVisible) /\ afterDepartures=MergeCheckpointDepartures103(departures,added) /\ IF before.point="ProcedureCode96bfa1b6a970" /\ due#{} THEN after=[before EXCEPT !.snapshotId=newSnapshotId,!.hostPasses=@+1] ELSE CheckpointStageAdvance103(before,after,before.point,newSnapshotId) CheckpointAuxiliarySiteCleanup103(before,after,targetSites,afterTargetSites,objects,deploying,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCode2d73b20aa788") /\ AuxiliarySiteRegistryCheckpoint4(targetSites,afterTargetSites,objects,deploying,"ProcedureCode2d73b20aa788") /\ CheckpointStageAdvance103(before,after,"ProcedureCode2d73b20aa788",newSnapshotId) CheckpointPendingBarrierTargetSites103(deploying) == {deploying[id].destination.targetSite : id \in {id \in DOMAIN deploying : deploying[id].form="Card" /\ deploying[id].kind="Barrier" /\ deploying[id].destination.zone="Play" /\ deploying[id].destination.area="Protecting"}} CheckpointPositionCleanup103(before,after,layout,afterLayout,currentSideBPosition,deploying,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCode2d6279f9d639") /\ LET pendingTargetSites==CheckpointPendingBarrierTargetSites103(deploying) remove=={p \in DOMAIN layout.slots : layout.slots[p].barrierCard=0 /\ p#currentSideBPosition /\ layout.slots[p].targetSite \notin pendingTargetSites} IN /\ afterLayout=[layout EXCEPT !.slots=[p \in DOMAIN layout.slots \ remove |-> [layout.slots[p] EXCEPT !.retained=(p=currentSideBPosition /\ layout.slots[p].barrierCard=0)]], !.orders=[targetSite \in DOMAIN @ |-> SelectSeq(layout.orders[targetSite],LAMBDA p : p \notin remove)]] /\ CheckpointStageAdvance103(before,after,"ProcedureCode2d6279f9d639",newSnapshotId) CheckpointRootAdmissions103(before,after,capacity,afterCapacity,siteInspection,objects,entries,previousBoundary,currentBoundary,accepted,actor,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCode7f181ce21011") /\ previousBoundary<=currentBoundary /\ IF siteInspection.active /\ ~siteInspection.complete THEN /\ actor="SideB" /\ LET arrivals=={entries[id].object : id \in {id \in DOMAIN entries : entries[id].tag="RootEntry" /\ entries[id].siteInspectionId=siteInspection.id /\ entries[id].serial>previousBoundary /\ entries[id].serial<=currentBoundary /\ entries[id].targetSite=siteInspection.targetSite}} observed==[capacity EXCEPT !.admittedRoots=(@ \cap InspectionRootCards7(siteInspection,objects)) \ arrivals, !.pendingRoots=(@ \cup arrivals) \cap InspectionRootCards7(siteInspection,objects)] IN /\ ObserveRootEntries7(capacity,observed,siteInspection,objects,arrivals) /\ DecideRootAdmissions7(observed,afterCapacity,siteInspection,objects,accepted,"ProcedureCode7f181ce21011",TRUE) ELSE afterCapacity=capacity /\ accepted={} /\ actor="NoValue" /\ CheckpointStageAdvance103(before,after,"ProcedureCode7f181ce21011",newSnapshotId) RestoreDiscardConversions103(objects,afterObjects,conversions,afterConversions,printed) == LET due=={id \in DOMAIN objects \cap DOMAIN conversions : objects[id].zone \in {"SideADiscard","SideBDiscard"} /\ objects[id].card#"none"} IN /\ \A id \in due : ConversionValid101(conversions[id]) /\ conversions[id].card=objects[id].card /\ afterObjects=[id \in DOMAIN objects |-> IF id \in due THEN [objects[id] EXCEPT !.form="Card",!.kind=printed[objects[id].card].kind,!.properties=printed[objects[id].card],!.host=0,!.deployed=FALSE] ELSE objects[id]] /\ afterConversions=Without101(conversions,due) CheckpointRestoreDiscard103(before,after,objects,afterObjects,conversions,afterConversions,printed,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCodeda83a77a1f12") /\ RestoreDiscardConversions103(objects,afterObjects,conversions,afterConversions,printed) /\ CheckpointStageAdvance103(before,after,"ProcedureCodeda83a77a1f12",newSnapshotId) CheckpointReturnDiscardCounters103(before,after,objects,afterObjects,newSnapshotId) == /\ CheckpointAt103(before,"ProcedureCode0811ebc5f40e") /\ LET due=={id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].zone \in {"SideADiscard","SideBDiscard"}} IN /\ \A id \in due : objects[id].card="none" /\ ~objects[id].virtual /\ afterObjects=Without101(objects,due) /\ CheckpointStageAdvance103(before,after,"ProcedureCode0811ebc5f40e",newSnapshotId) CheckpointDrained103(frame,ledger,stack) == /\ frame.phase="Returned" /\ frame.returned /\ frame.owed = <<>> /\ frame.outcome="Playing" /\ frame.done \cup frame.discharged=CheckpointStageSet103 /\ CheckpointCaptured103(frame,ledger) /\ ConditionalCheckpointDrained96(ledger,stack,frame.id) ReceivePriorityAfterCheckpoint103(frame,ledger,beforeStack,afterStack,receipt) == /\ CheckpointDrained103(frame,ledger,beforeStack) /\ receipt.id=frame.id /\ CheckpointPriorityWithConditionals96(ledger,beforeStack,afterStack,receipt) ResumePaidAfterCheckpoint103(frame,ledger,stack,before,after,objects,transits,receipt) == /\ CheckpointDrained103(frame,ledger,stack) /\ receipt.id=frame.id /\ PaidCheckpointWithConditionals96(ledger,stack,before,after,objects,transits,receipt) ResumeConditionalInstructionAfterCheckpoint103(frame,ledger,stack,before,after,receipt) == /\ CheckpointDrained103(frame,ledger,stack) /\ receipt.id=frame.id /\ ConditionalInstructionCheckpoint96(ledger,stack,before,after,receipt) CheckpointIllegalDisposition103(eligible,LegalAfterRetire(_)) == IF AppropriateRetireSets103(eligible,LegalAfterRetire)={} THEN "UnsupportedNoLegalizingSet" ELSE "Supported" CheckpointSiteKey103(site) == <> BeginCheckpointSite103(beforeSites,afterSites,beforeFrames,afterFrames,frame,id,site,event,insideStructures) == /\ CheckpointSiteKey103(site) \notin beforeSites /\ \A old \in DOMAIN beforeFrames : beforeFrames[old].phase \notin {"Steps","Completed"} /\ OpenCheckpointAtSite103(frame,id,site,event,insideStructures,DOMAIN beforeFrames) /\ afterSites=beforeSites \cup {CheckpointSiteKey103(site)} /\ afterFrames=[key \in DOMAIN beforeFrames \cup {id} |-> IF key=id THEN frame ELSE beforeFrames[key]] DamageTypes104 == {"HarmClassB","HarmClassA","PersistentCapacityHarm"} NormalizeDamageType104(kind) == IF kind="CapacityHarmAlias" THEN "PersistentCapacityHarm" ELSE kind DamageResponsible104(verb) == CASE verb="Do" -> "SideA" [] verb="Suffer" -> "SideB" [] OTHER -> "UnsupportedDamageWording" DamageBHand104(objects) == {id \in DOMAIN objects : objects[id].form="Card" /\ objects[id].zone="SideBHand"} DamagePacketKey104(context,id) == <> DamagePacketFromExpected104(context,reference,world,id,cardFacts,packet) == /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ ExpectedEffectsValid99(context.actualEffects) /\ id \in DOMAIN context.actualEffects /\ LET effect==context.actualEffects[id] IN /\ effect.kind="Damage" /\ effect.value>0 /\ effect.damageType \in DamageTypes104 /\ effect.damageVerb \in {"Do","Suffer"} /\ effect.actor=DamageResponsible104(effect.damageVerb) /\ effect.baseOrigin=reference.source /\ effect.sourceCard \in DOMAIN cardFacts /\ effect.sourceSHA=cardFacts[effect.sourceCard].sourceSHA /\ (effect.damageVerb="Do" => cardFacts[effect.sourceCard].side="SideA") /\ packet=[key |-> DamagePacketKey104(context,id),contextId |-> context.id,imminenceId |-> context.imminenceId,effectId |-> id, reference |-> reference,snapshotId |-> world.id,turnId |-> world.turn.id,source |-> effect.baseOrigin, sourceCard |-> effect.sourceCard,sourceSHA |-> effect.sourceSHA,verb |-> effect.damageVerb, responsible |-> effect.actor,damageType |-> effect.damageType,amount |-> effect.value] DamageOmitted104(context,reference,world,id,receipt) == /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates /\ context.templates[id].kind="Damage" /\ id \notin DOMAIN context.actualEffects /\ receipt=[tag |-> "NoActualDamagePacket",contextId |-> context.id,reference |-> reference,effectId |-> id,snapshotId |-> world.id] SideAMeatDamage104(packet) == packet.responsible="SideA" /\ packet.damageType="HarmClassB" BeginDamage104(context,reference,world,id,cardFacts,packet,frame,usedPackets,afterOutcome,actualOtherWinners) == /\ DamagePacketFromExpected104(context,reference,world,id,cardFacts,packet) /\ packet.key \notin usedPackets /\ actualOtherWinners \subseteq SetupPlayers /\ LET bHand==DamageBHand104(world.objects) fatal==packet.amount>Cardinality(bHand) IN /\ (~fatal => actualOtherWinners={}) /\ afterOutcome=IF fatal THEN (IF "SideB" \in actualOtherWinners THEN "Draw" ELSE "SideA") ELSE "Playing" /\ frame=[packet |-> packet,beforeObjects |-> world.objects,bHand |-> bHand,selected |-> {},selectionOrder |-> <<>>, selections |-> <<>>,policy |-> [id |-> 0],phase |-> IF fatal THEN "EliminatedByHarm" ELSE "Selecting", outcome |-> afterOutcome,completion |-> [batchId |-> 0],finalObjects |-> [emptyId \in {} |-> emptyId]] RandomDamageChoices104(population,amount) == {selected \in SUBSET population : Cardinality(selected)=amount} DamageRandomReceipt104(packet,remaining,amount,selected,actor,receipt) == /\ selected \in RandomDamageChoices104(remaining,amount) /\ actor=packet.responsible /\ receipt=[tag |-> "ActualRandomDamageSelection",packet |-> packet.key,reference |-> packet.reference, population |-> remaining,amount |-> amount,selected |-> selected,actor |-> actor] SelectDamageRandomBatch104(before,after,objects,selected,actor,receipt) == /\ before.phase="Selecting" /\ before.outcome="Playing" /\ objects=before.beforeObjects /\ before.selected={} /\ DamageRandomReceipt104(before.packet,before.bHand,before.packet.amount,selected,actor,receipt) /\ after=[before EXCEPT !.selected=selected,!.selections= <>,!.phase="ReadyToRetire"] BeginSequentialDamage104(before,after,objects,authority,compiled,cardFacts) == /\ before.phase="Selecting" /\ before.outcome="Playing" /\ objects=before.beforeObjects /\ before.selected={} /\ authority.id \in DOMAIN compiled /\ compiled[authority.id]=authority /\ authority.tag="SourceBoundDamageSelectionOverride" /\ authority.packet=before.packet.key /\ authority.reference=before.packet.reference /\ authority.snapshotId=before.packet.snapshotId /\ authority.source.kind="Object" /\ authority.source.object \in DOMAIN objects /\ authority.card \in DOMAIN cardFacts /\ authority.sourceSHA=cardFacts[authority.card].sourceSHA /\ authority.sourceObject=objects[authority.source.object] /\ authority.sourceObject.card=authority.card /\ Len(authority.slots)=before.packet.amount /\ \A i \in 1..Len(authority.slots) : authority.slots[i].mode \in {"Random","Choose"} /\ authority.slots[i].actor \in SetupPlayers /\ (authority.slots[i].mode="Random" => authority.slots[i].actor=before.packet.responsible) /\ after=[before EXCEPT !.policy=authority,!.phase="SelectingSequentially"] DamageFirstNetThisTurn104(packet,actualDamageHistory) == packet.damageType="HarmClassA" /\ ~\E id \in DOMAIN actualDamageHistory : actualDamageHistory[id].tag="DamageSuffered" /\ actualDamageHistory[id].turnId=packet.turnId /\ actualDamageHistory[id].damageType="HarmClassA" /\ actualDamageHistory[id].amount>0 ExampleFamily009SelectionShape104(packet,authority,actualDamageHistory) == /\ authority.card="Specimen0051" /\ DamageFirstNetThisTurn104(packet,actualDamageHistory) /\ authority.slots[1]=[mode |-> "Choose",actor |-> "SideA"] /\ \A i \in 2..Len(authority.slots) : authority.slots[i]=[mode |-> "Random",actor |-> packet.responsible] BeginExampleFamily009Damage104(before,after,objects,authority,compiled,cardFacts,actualDamageHistory) == /\ BeginSequentialDamage104(before,after,objects,authority,compiled,cardFacts) /\ ExampleFamily009SelectionShape104(before.packet,authority,actualDamageHistory) SelectDamageNext104(before,after,objects,card,actor,receipt) == /\ before.phase="SelectingSequentially" /\ before.outcome="Playing" /\ objects=before.beforeObjects /\ card \in before.bHand \ before.selected /\ LET index==Len(before.selectionOrder)+1 slot==before.policy.slots[index] selected==before.selected \cup {card} IN /\ index<=before.packet.amount /\ actor=slot.actor /\ IF slot.mode="Random" THEN DamageRandomReceipt104(before.packet,before.bHand \ before.selected,1,{card},actor,receipt) ELSE receipt=[tag |-> "ActualAuthorizedDamageChoice",packet |-> before.packet.key,reference |-> before.packet.reference, authorityId |-> before.policy.id,index |-> index,card |-> card,actor |-> actor] /\ after=[before EXCEPT !.selected=selected,!.selectionOrder=Append(@,card),!.selections=Append(@,receipt), !.phase=IF Cardinality(selected)=before.packet.amount THEN "ReadyToRetire" ELSE "SelectingSequentially"] DamageOwnerMoveMap104(objects,selected,successors,owner) == LET fresh=={successors[id] : id \in selected} IN [id \in (DOMAIN objects \ selected) \cup fresh |-> IF id \notin fresh THEN objects[id] ELSE [objects[CHOOSE old \in selected : successors[old]=id] EXCEPT !.zone=owner \o "Discard",!.loc="discard", !.deployed=FALSE,!.activated=FALSE,!.host=0,!.face="Up",!.marks={}]] DamageCardBatchTransfer104(objects,afterObjects,selected,successors,usedIds,owners) == /\ selected \subseteq DamageBHand104(objects) /\ DOMAIN objects \subseteq usedIds /\ FreshSuccessors8(selected,successors,usedIds) /\ \A id \in selected : objects[id].card \in DOMAIN owners /\ owners[objects[id].card] \in SetupPlayers /\ LET sideB=={id \in selected : owners[objects[id].card]="SideB"} sideA==selected \ sideB first==DamageOwnerMoveMap104(objects,sideB,[id \in sideB |-> successors[id]],"SideB") sideBFresh=={successors[id] : id \in sideB} IN /\ CardBatchTransfer8(objects,first,sideB,[id \in sideB |-> successors[id]],usedIds,"SideBDiscard","Up",[id \in sideB |-> "discard"]) /\ CardBatchTransfer8(first,afterObjects,sideA,[id \in sideA |-> successors[id]],usedIds \cup sideBFresh,"SideADiscard","Up",[id \in sideA |-> "discard"]) /\ afterObjects=DamageOwnerMoveMap104(first,sideA,[id \in sideA |-> successors[id]],"SideA") PersistentCapacityLossQuantity104(objects) == Cardinality({id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="PersistentCapacityLoss" /\ objects[id].zone="SideBPersistentCapacityLoss" /\ objects[id].host=0}) DamageMaximumHandSize104(objects,effectiveOtherAdjustment) == MaximumHandSize5("SideB",PersistentCapacityLossQuantity104(objects),effectiveOtherAdjustment) DamageCoreCounterRow104 == [card |-> "none",form |-> "Counter",kind |-> "PersistentCapacityLoss",zone |-> "SideBPersistentCapacityLoss",loc |-> 0, deployed |-> FALSE,face |-> "Up",front |-> TRUE,activated |-> FALSE,host |-> 0,placedBy |-> "SideB",virtual |-> FALSE, objectivePoints |-> 0,marks |-> {}] DamageCoreCounters104(packet,objects,afterObjects,added,usedIds) == LET amount==IF packet.damageType="PersistentCapacityHarm" THEN packet.amount ELSE 0 IN /\ DOMAIN added \subseteq (Nat \ {0}) \ usedIds /\ \A id \in DOMAIN added : added[id]=DamageCoreCounterRow104 /\ BankMintProjection4(objects,afterObjects,added,amount,"PersistentCapacityLoss",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE) /\ PersistentCapacityLossAccrual5(PersistentCapacityLossQuantity104(objects),PersistentCapacityLossQuantity104(afterObjects),amount) DamageSufferedEvent104(frame,batchId,successors) == [tag |-> "DamageSuffered",packet |-> frame.packet.key,reference |-> frame.packet.reference,source |-> frame.packet.source, sourceCard |-> frame.packet.sourceCard,responsible |-> frame.packet.responsible,damageType |-> frame.packet.damageType, amount |-> frame.packet.amount,turnId |-> frame.packet.turnId,batchId |-> batchId, originalObjects |-> frame.selected,successors |-> successors,simultaneous |-> TRUE] ResolveDamageBatch104(before,after,objects,afterObjects,successors,usedIds,owners,addedCore,beforeHistory,afterHistory,batchId,events) == /\ before.phase="ReadyToRetire" /\ before.outcome="Playing" /\ objects=before.beforeObjects /\ before.packet.amount<=Cardinality(before.bHand) /\ Cardinality(before.selected)=before.packet.amount /\ LET cardsAfter==DamageOwnerMoveMap104( DamageOwnerMoveMap104(objects,{id \in before.selected : owners[objects[id].card]="SideB"}, [id \in {i \in before.selected : owners[objects[i].card]="SideB"} |-> successors[id]],"SideB"), {id \in before.selected : owners[objects[id].card]="SideA"}, [id \in {i \in before.selected : owners[objects[i].card]="SideA"} |-> successors[id]],"SideA") fresh=={successors[id] : id \in before.selected} movementEvents=={MovementEvent8(batchId,"Retire",before.selected)} damageEvent==DamageSufferedEvent104(before,batchId,successors) IN /\ DamageCardBatchTransfer104(objects,cardsAfter,before.selected,successors,usedIds,owners) /\ DamageCoreCounters104(before.packet,cardsAfter,afterObjects,addedCore,usedIds \cup fresh) /\ RecordMovement8(beforeHistory,afterHistory,batchId,"Retire",before.selected,"Complete",TRUE,movementEvents) /\ events=movementEvents \cup {damageEvent} /\ after=[before EXCEPT !.phase="Complete",!.finalObjects=afterObjects, !.completion=[batchId |-> batchId,damageEvent |-> damageEvent,movementEvent |-> MovementEvent8(batchId,"Retire",before.selected)]] DamageBatchReadyForConditionals104(frame,objects,event) == /\ frame.phase="Complete" /\ frame.outcome="Playing" /\ objects=frame.finalObjects /\ event=frame.completion.damageEvent /\ event=DamageSufferedEvent104(frame,frame.completion.batchId,event.successors) /\ frame.selected \cap DOMAIN objects={} /\ \A id \in frame.selected : event.successors[id] \in DOMAIN objects /\ objects[event.successors[id]].zone \in {"SideADiscard","SideBDiscard"} DamageNetMeatRetireObservation104(frame,objects,event,originalObject) == /\ DamageBatchReadyForConditionals104(frame,objects,event) /\ originalObject \in frame.selected /\ frame.packet.damageType \in {"HarmClassA","HarmClassB"} ExposureMarkerIds105(objects) == {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ExposureMarker" /\ objects[id].zone="SideBExposureMarkers" /\ objects[id].host=0} ExposureMarkerQuantity105(objects) == Cardinality(ExposureMarkerIds105(objects)) MovableExposureMarkerIds105(objects) == {id \in ExposureMarkerIds105(objects) : ~objects[id].virtual} ExposureMarkerStateView105(objects,declarations) == [quantity |-> ExposureMarkerQuantity105(objects),hasExposureMarkers |-> ExposureMarkerQuantity105(objects)>0 \/ DOMAIN declarations#{},movable |-> MovableExposureMarkerIds105(objects)] CurrentExposureMarkerState105(world,declarations,cardFacts,state) == /\ \A id \in DOMAIN declarations : LET d==declarations[id] IN /\ d.snapshotId=world.id /\ d.projection.property="HasExposureMarkers" /\ d.projection.target="SideB" /\ d.projection.value=TRUE /\ d.projection.mode="Continuous" /\ ~d.projection.resolving /\ ~d.projection.lingering /\ d.projection.source.kind="Object" /\ d.projection.source.object \in DOMAIN world.objects /\ d.sourceObject=world.objects[d.projection.source.object] /\ d.sourceObject.card \in DOMAIN cardFacts /\ d.sourceSHA=cardFacts[d.sourceObject.card].sourceSHA /\ d.projection.ability \in world.activeAbilities /\ DefaultActive(d.sourceObject,world.started,cardFacts) /\ state=ExposureMarkerStateView105(world.objects,declarations) ExposureMarkerCounterRow105 == [DamageCoreCounterRow104 EXCEPT !.kind="ExposureMarker",!.zone="SideBExposureMarkers"] TakeExposureMarkers105(context,reference,world,id,afterObjects,added,usedIds,event) == /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ LET effect==context.actualEffects[id] IN /\ effect.kind="ExposureMarkers" /\ effect.value \in Nat \ {0} /\ effect.actor \in SetupPlayers /\ effect.baseOrigin=reference.source /\ DOMAIN added \subseteq (Nat \ {0}) \ usedIds /\ \A token \in DOMAIN added : added[token]=ExposureMarkerCounterRow105 /\ BankMintProjection4(world.objects,afterObjects,added,effect.value,"ExposureMarker",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE) /\ event=[tag |-> "ExposureMarkersTaken",contextId |-> context.id,reference |-> reference,effectId |-> id,source |-> effect.baseOrigin,actor |-> effect.actor, player |-> "SideB",amount |-> effect.value,counters |-> DOMAIN added] ExposureMarkerActionActor105(kind) == IF kind="RetireResource" THEN "SideA" ELSE "SideB" ExposureMarkerActionRule105(kind) == IF kind="RetireResource" THEN "ProcedureCodeef666cf169ed" ELSE "ProcedureCode383141df25e9" ExposureMarkerActionKey105(kind) == BasicActionKey5(ExposureMarkerActionActor105(kind),kind) ExposureMarkerActionStatusGate105(kind,hasExposureMarkers) == kind="RemoveExposureMarker" \/ (kind="RetireResource" /\ hasExposureMarkers) ExposureMarkerSourceBound105(world,source,object,sourceSHA,cardFacts) == /\ source.kind="Object" /\ source.object \in DOMAIN world.objects /\ object=world.objects[source.object] /\ object.card \in DOMAIN cardFacts /\ sourceSHA=cardFacts[object.card].sourceSHA /\ source.object \in world.activeSources /\ DefaultActive(object,world.started,cardFacts) ExampleFamily094ExposureMarkerCostShape105(kind,sourceObject,chosenReduction,delta) == /\ sourceObject.card="Specimen0233" /\ IF sourceObject.front THEN delta=IF kind="RemoveExposureMarker" THEN 1 ELSE 0 ELSE delta=IF kind="RetireResource" /\ chosenReduction THEN -2 ELSE 0 ExposureMarkerCostModifiers105(world,kind,mods,cardFacts) == /\ mods=world.exposureMarkerCostModifiers[kind] /\ \A source \in world.activeSources \cap DOMAIN world.objects : IF world.objects[source].card="Specimen0233" /\ DefaultActive(world.objects[source],world.started,cardFacts) THEN /\ Cardinality({id \in DOMAIN mods : mods[id].source.object=source})<=1 /\ (world.objects[source].front /\ kind="RemoveExposureMarker" => Cardinality({id \in DOMAIN mods : mods[id].source.object=source})=1) ELSE TRUE /\ \A id \in DOMAIN mods : mods[id].snapshotId=world.id /\ mods[id].action=kind /\ mods[id].delta \in Int /\ ExposureMarkerSourceBound105(world,mods[id].source,mods[id].sourceObject,mods[id].sourceSHA,cardFacts) /\ (mods[id].sourceObject.card="Specimen0233" => ExampleFamily094ExposureMarkerCostShape105(kind,mods[id].sourceObject,mods[id].chosenReduction,mods[id].delta)) ExposureMarkerResourceUnitCost105(mods) == ModifiedCost(2,<0} |-> mods[id].delta])>>, < -mods[id].delta])>>) ExampleFamily011ExposureMarkerPermission105(world,kind,transaction,permission,cardFacts) == /\ kind="RemoveExposureMarker" /\ permission.action=kind /\ permission.player="SideB" /\ permission.paymentId=transaction /\ permission.snapshotId=world.id /\ permission.allowsPayment /\ permission.sourceObject.card="Specimen0058" /\ ExposureMarkerSourceBound105(world,permission.source,permission.sourceObject,permission.sourceSHA,cardFacts) /\ \A id \in permission.paidCounters : id \in DOMAIN world.objects /\ BankPhysicalToken4(world.objects[id]) /\ world.objects[id].kind="ResourceUnit" /\ world.objects[id].host=permission.source.object /\ world.controllers[id]="SideB" ExposureMarkerResourceUnitEligible105(world,player,permissions) == {id \in DOMAIN world.objects : BankPhysicalToken4(world.objects[id]) /\ world.objects[id].kind="ResourceUnit" /\ world.controllers[id]=player /\ ((world.objects[id].zone=player \o "ResourceUnits" /\ world.objects[id].host=0) \/ \E p \in DOMAIN permissions : id \in permissions[p].paidCounters)} ExposureMarkerPaymentPermissionSources105(payment,permissions) == CounterPermissionUseSources9(payment,[id \in DOMAIN permissions |-> [permissions[id] EXCEPT !.paidCounters=@ \cap payment.paidCounterIds]]) ReserveExposureMarkerAction105(beforeStack,afterStack,world,declarations,cardFacts,state,kind,option,legality,actionId,usedActions,frame) == /\ kind \in {"RetireResource","RemoveExposureMarker"} /\ CurrentExposureMarkerState105(world,declarations,cardFacts,state) /\ ExposureMarkerActionStatusGate105(kind,state.hasExposureMarkers) /\ OwnActionPhase5(world.turn,ExposureMarkerActionActor105(kind)) /\ world.outcome="Playing" /\ actionId \in (Nat \ {0}) \ usedActions /\ Len(beforeStack)>0 /\ LET w==WindowTop9(beforeStack) IN /\ w.kind="NeutralValue00001" /\ WindowSiteAllowed9("NeutralValue00001",w.site) /\ w.site=TurnPrioritySite9(world.turn,world.step,world.phaseId,world.actionPoints[ExposureMarkerActionActor105(kind)],[turn |-> world.turn,step |-> world.step]) /\ \A i \in 1..Len(beforeStack) : beforeStack[i].kind="NeutralValue00001" => beforeStack[i].busy.id=0 /\ option.kind="NeutralValue00001" /\ option.controller=ExposureMarkerActionActor105(kind) /\ option.source=RuleAbilitySource9(ExposureMarkerActionRule105(kind)) /\ option.target=0 /\ option.newStructures={} /\ BeginPriorityOption9(beforeStack,afterStack,option,world.objects,legality,[id \in {} |-> id]) /\ frame=[id |-> actionId,kind |-> kind,player |-> ExposureMarkerActionActor105(kind),windowId |-> w.id,option |-> option,transaction |-> legality.transactionId, activationSnapshot |-> 0,phase |-> "Reserved",action |-> [id |-> 0],target |-> 0,instruction |-> 0,effective |-> [mode |-> "NoValue"], nestedTransaction |-> 0,effectCosts |-> [id \in {} |-> id],payment |-> [complete |-> FALSE]] PayExposureMarkerAction105(before,after,stack,world,afterWorld,declarations,afterDeclarations,cardFacts,mods,permissions,selected,payment) == /\ before.phase="Reserved" /\ world.outcome="Playing" /\ Len(stack)>0 /\ OwnActionPhase5(world.turn,before.player) /\ WindowTop9(stack).id=before.windowId /\ WindowTop9(stack).busy=before.option /\ WindowTop9(stack).busyTransaction=before.transaction /\ WindowTop9(stack).stage="Resolving" /\ CurrentExposureMarkerState105(world,declarations,cardFacts,ExposureMarkerStateView105(world.objects,declarations)) /\ ExposureMarkerActionStatusGate105(before.kind,ExposureMarkerStateView105(world.objects,declarations).hasExposureMarkers) /\ ExposureMarkerCostModifiers105(world,before.kind,mods,cardFacts) /\ permissions=world.exposureMarkerSpendPermissions /\ \A p \in DOMAIN permissions : ExampleFamily011ExposureMarkerPermission105(world,before.kind,before.transaction,permissions[p],cardFacts) /\ selected \subseteq ExposureMarkerResourceUnitEligible105(world,before.player,permissions) /\ Cardinality(selected)=ExposureMarkerResourceUnitCost105(mods) /\ world.actionPoints[before.player]>=1 /\ afterWorld.id \in Nat \ {0} /\ afterWorld.id#world.id /\ BankSpendReturn4(world.objects,afterWorld.objects,selected,TRUE) /\ afterWorld=[world EXCEPT !.id=afterWorld.id,!.objects=afterWorld.objects,!.controllers=Without101(@,selected), !.actionPoints[before.player]=@-1,!.spent[before.player]=@+1] /\ CurrentExposureMarkerState105(afterWorld,afterDeclarations,cardFacts,ExposureMarkerStateView105(afterWorld.objects,afterDeclarations)) /\ ExposureMarkerActionStatusGate105(before.kind,ExposureMarkerStateView105(afterWorld.objects,afterDeclarations).hasExposureMarkers) /\ payment=[tag |-> "BasicExposureMarkerTriggerPayment",id |-> before.transaction,actionId |-> before.id,player |-> before.player, beforeSnapshot |-> world.id,afterSnapshot |-> afterWorld.id,actionPoints |-> 1,resourceUnits |-> ExposureMarkerResourceUnitCost105(mods),paidCounterIds |-> selected,complete |-> TRUE] /\ LET action==NewAction5(before.id,before.player,ExposureMarkerActionKey105(before.kind)) IN /\ ActionStart5(world.turn,before.player,TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1],[kind |-> "SpendResourceUnits",amount |-> ExposureMarkerResourceUnitCost105(mods)]>>, TRUE,TRUE,TRUE,before.id,ExposureMarkerActionKey105(before.kind),action) /\ after=[before EXCEPT !.phase="BaseCostCheckpoint",!.activationSnapshot=world.id,!.action=action,!.payment=payment] ExposureMarkerCheckpointCaller105(frame,scope) == [kind |-> "BasicExposureMarkerActionCheckpoint",action |-> frame.id,scope |-> scope, transaction |-> IF scope="BaseCost" THEN frame.transaction ELSE IF scope="AdditionalCost" THEN frame.nestedTransaction ELSE 0] DrainExposureMarkerAction105(before,after,world,cp,ledger,stack) == /\ before.phase \in {"BaseCostCheckpoint","AdditionalCostCheckpoint","EffectCheckpoint"} /\ world.outcome="Playing" /\ LET scope==CASE before.phase="BaseCostCheckpoint" -> "BaseCost" [] before.phase="AdditionalCostCheckpoint" -> "AdditionalCost" [] OTHER -> "Effect" IN /\ cp.caller=ExposureMarkerCheckpointCaller105(before,scope) /\ cp.snapshotId=world.id /\ CheckpointDrained103(cp,ledger,stack) /\ IF scope="BaseCost" THEN /\ ActionEffectsBegin5(before.action,after.action,TRUE) /\ after=[before EXCEPT !.phase="Targets",!.action=after.action] ELSE IF scope="AdditionalCost" THEN after=[before EXCEPT !.phase="EffectReady"] ELSE /\ ActionComplete5(before.action,after.action,TRUE) /\ after=[before EXCEPT !.phase="Complete",!.action=after.action] ResourceTargetIds105(world) == {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].zone="Play" /\ world.objects[id].deployed /\ BasicCardTarget5("SideA","RetireResource",world.objects[id].kind,world.objects[id].zone,world.objects[id].deployed) /\ world.owners[world.objects[id].card]="SideB"} ExposureMarkerActionTargets105(frame,world) == IF frame.kind="RetireResource" THEN ResourceTargetIds105(world) ELSE MovableExposureMarkerIds105(world.objects) AnnounceExposureMarkerTarget105(before,after,world,target,instructionId) == /\ before.phase="Targets" /\ before.action.status="Effects" /\ world.outcome="Playing" /\ instructionId \in Nat \ {0} /\ IF ExposureMarkerActionTargets105(before,world)={} THEN target=0 ELSE target \in ExposureMarkerActionTargets105(before,world) /\ after=[before EXCEPT !.phase="Targeted",!.target=target,!.instruction=instructionId] ResourceKnownCostSources105(world,target,cardFacts) == {source \in world.activeSources \cap DOMAIN world.objects : DefaultActive(world.objects[source],world.started,cardFacts) /\ ((world.objects[source].card="Specimen0212" /\ "SchemaAtom044" \in world.subtypes[target]) \/ (world.objects[source].card="Specimen0136" /\ source=target /\ ThreatFlagGate93(<<[category |-> "AbilityFlag",subtype |-> "Threat",value |-> 3]>>,world.points)))} ResourceKnownCostInventory105(world,target,costs,cardFacts) == LET required==ResourceKnownCostSources105(world,target,cardFacts) observed=={costs[id].source.object : id \in {id \in DOMAIN costs : costs[id].source.object \in DOMAIN world.objects /\ world.objects[costs[id].source.object].card \in {"Specimen0212","Specimen0136"}}} IN /\ observed=required /\ \A source \in required : Cardinality({id \in DOMAIN costs : costs[id].source=ObjectAbilitySource9(source)})=1 PrepareExposureMarkerEffect105(before,after,world,context,reference,id,cardFacts) == /\ before.phase="Targeted" /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ reference.id=before.instruction /\ reference.abilityInstance=before.id /\ reference.source=RuleAbilitySource9(ExposureMarkerActionRule105(before.kind)) /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates /\ context.templates[id].kind=IF before.kind="RetireResource" THEN "RetireCards" ELSE "RemoveExposureMarkers" /\ LET removed==id \notin DOMAIN context.actualEffects costs==IF before.kind="RetireResource" /\ ~removed /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions THEN world.additionalResourceCosts ELSE [key \in {} |-> key] IN /\ IF removed THEN TRUE ELSE context.actualEffects[id].kind=context.templates[id].kind /\ context.actualEffects[id].targetCard=before.target /\ context.actualEffects[id].actor=before.player /\ context.actualEffects[id].value=1 /\ (before.kind="RetireResource" /\ ~removed /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions => ResourceKnownCostInventory105(world,before.target,costs,cardFacts)) /\ after=[before EXCEPT !.effective=[mode |-> IF removed THEN "Removed" ELSE "Kept",reference |-> reference,effectId |-> id], !.effectCosts=costs,!.phase=IF DOMAIN costs={} THEN "EffectReady" ELSE "AdditionalCosts"] ResourceAdditionalCosts105(frame,world,cardFacts) == /\ frame.effectCosts=world.additionalResourceCosts /\ DOMAIN frame.effectCosts#{} /\ \A id \in DOMAIN frame.effectCosts : LET c==frame.effectCosts[id] IN /\ c.snapshotId=world.id /\ c.actionId=frame.id /\ c.target=frame.target /\ c.kind="RetireCentralA" /\ c.amount=1 /\ ExposureMarkerSourceBound105(world,c.source,c.sourceObject,c.sourceSHA,cardFacts) /\ c.eligible \subseteq {card \in DOMAIN world.objects : world.objects[card].form="Card" /\ world.objects[card].zone="SideAHand" /\ card \notin world.currentRetireProhibitions} /\ (c.sourceObject.card="Specimen0212" => "SchemaAtom044" \in world.subtypes[frame.target]) /\ (c.sourceObject.card="Specimen0136" => c.source.object=frame.target /\ ThreatFlagGate93(<<[category |-> "AbilityFlag",subtype |-> "Threat",value |-> 3]>>,world.points)) PayResourceAdditional105(before,after,world,afterWorld,cardFacts,assignments,successors,usedIds,transaction,eventIds,beforeHistory,afterHistory,events) == /\ before.phase="AdditionalCosts" /\ before.target \in ResourceTargetIds105(world) /\ before.target \notin world.currentRetireProhibitions /\ ResourceAdditionalCosts105(before,world,cardFacts) /\ transaction \in Nat \ {0} /\ transaction#before.transaction /\ DOMAIN assignments=DOMAIN before.effectCosts /\ \A cost \in DOMAIN assignments : assignments[cost] \subseteq before.effectCosts[cost].eligible /\ Cardinality(assignments[cost])=before.effectCosts[cost].amount /\ \A a,b \in DOMAIN assignments : a#b => assignments[a] \cap assignments[b]={} /\ DOMAIN eventIds=DOMAIN assignments /\ Cardinality({eventIds[cost] : cost \in DOMAIN eventIds})=Cardinality(DOMAIN eventIds) /\ \A cost \in DOMAIN eventIds : eventIds[cost] \in (Nat \ {0}) \ DOMAIN beforeHistory /\ LET selected==UNION {assignments[id] : id \in DOMAIN assignments} newEvents==[cost \in DOMAIN assignments |-> MovementEvent8(eventIds[cost],"Retire",assignments[cost])] IN /\ CardBatchTransfer8(world.objects,afterWorld.objects,selected,successors,usedIds,"SideADiscard","Down",[id \in selected |-> "discard"]) /\ afterWorld.id \in Nat \ {0} /\ afterWorld.id#world.id /\ afterWorld=[world EXCEPT !.id=afterWorld.id,!.objects=afterWorld.objects, !.controllers=[id \in (DOMAIN @ \ selected) \cup {successors[old] : old \in selected} |-> IF id \in DOMAIN @ \ selected THEN @[id] ELSE "SideA"],!.currentRetireProhibitions=afterWorld.currentRetireProhibitions] /\ before.target \notin afterWorld.currentRetireProhibitions /\ afterHistory=[id \in DOMAIN beforeHistory \cup {eventIds[cost] : cost \in DOMAIN eventIds} |-> IF id \in DOMAIN beforeHistory THEN beforeHistory[id] ELSE newEvents[CHOOSE cost \in DOMAIN eventIds : eventIds[cost]=id]] /\ \A cost \in DOMAIN assignments : RecordMovement8(beforeHistory,[id \in DOMAIN beforeHistory \cup {eventIds[cost]} |-> IF id=eventIds[cost] THEN newEvents[cost] ELSE beforeHistory[id]],eventIds[cost],"Retire",assignments[cost],"Complete",TRUE,{newEvents[cost]}) /\ events={newEvents[cost] : cost \in DOMAIN newEvents} /\ after=[before EXCEPT !.phase="AdditionalCostCheckpoint",!.nestedTransaction=transaction] SkipResourceAdditional105(before,after,world,reason) == /\ before.phase="AdditionalCosts" /\ reason \in {"Declined","Unpayable"} /\ world.outcome="Playing" /\ after=[before EXCEPT !.phase="EffectReady",!.effective.mode="Removed"] ResolveExposureMarkerAction105(before,after,world,afterObjects,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,beforeDepartures,afterDepartures,events) == /\ before.phase="EffectReady" /\ before.action.status="Effects" /\ world.outcome="Playing" /\ LET blocked==IF before.kind="RetireResource" THEN world.currentRetireProhibitions ELSE world.currentExposureMarkerRemovalProhibitions due==IF before.effective.mode="Kept" /\ before.target \in ExposureMarkerActionTargets105(before,world) /\ before.target \notin blocked THEN {before.target} ELSE {} cards=={id \in due : world.objects[id].card#"none"} IN /\ CheckpointRetirePost103(world.objects,afterObjects,due,successors,usedIds,printed,owners,visible) /\ IF cards={} THEN /\ BankSpendReturn4(world.objects,afterObjects,due,TRUE) /\ afterHistory=beforeHistory /\ afterDepartures=beforeDepartures ELSE /\ RecordMovement8(beforeHistory,afterHistory,batchId,"Retire",cards,"Complete",TRUE,{MovementEvent8(batchId,"Retire",cards)}) /\ IF before.kind="RetireResource" THEN RecordHostDeparture103(beforeDepartures,afterDepartures,batchId,world.objects,afterObjects,before.target,successors[before.target],[id \in {} |-> id]) ELSE afterDepartures=beforeDepartures /\ events=(IF cards={} THEN {} ELSE {MovementEvent8(batchId,"Retire",cards)}) \cup (IF before.kind="RemoveExposureMarker" /\ due#{} THEN {[tag |-> "ExposureMarkerRemoved",actionId |-> before.id,player |-> "SideB",counter |-> before.target]} ELSE {}) /\ after=[before EXCEPT !.phase="EffectCheckpoint"] ReturnExposureMarkerAction105(frame,beforeStack,afterStack,receipt) == /\ frame.phase="Complete" /\ frame.action.status="Complete" /\ Len(beforeStack)>0 /\ WindowTop9(beforeStack).id=frame.windowId /\ WindowTop9(beforeStack).busy=frame.option /\ WindowTop9(beforeStack).busyTransaction=frame.transaction /\ CompletePriorityOption9(beforeStack,afterStack,receipt) LiabilityMarkerIds106(objects) == {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="LiabilityMarker" /\ objects[id].zone="SideALiabilityMarker" /\ objects[id].host=0} LiabilityMarkerQuantity106(objects) == Cardinality(LiabilityMarkerIds106(objects)) MovableLiabilityMarkerIds106(objects) == {id \in LiabilityMarkerIds106(objects) : ~objects[id].virtual} LiabilityMarkerFundIds106(objects) == {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ResourceUnit" /\ objects[id].zone="Play" /\ objects[id].host=0 /\ objects[id].resourceUnitLocation="LiabilityMarkerFund"} BaseSideBPoolIds106(objects) == {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ResourceUnit" /\ objects[id].host=0 /\ (objects[id].zone="SideBResourceUnits" \/ (objects[id].zone="Play" /\ objects[id].resourceUnitLocation="SideBPool"))} LiabilityMarkerFundController106(object,ordinaryController) == IF LiabilityMarkerFundIds106([id \in {1} |-> object])={1} THEN "SideB" ELSE ordinaryController LiabilityMarkerCounterRow106 == [DamageCoreCounterRow104 EXCEPT !.kind="LiabilityMarker",!.zone="SideALiabilityMarker",!.placedBy="SideA"] LiabilityMarkerFundRow106 == ReplacementOverlay99(DamageCoreCounterRow104, [kind |-> "ResourceUnit",zone |-> "Play",resourceUnitLocation |-> "LiabilityMarkerFund",placedBy |-> "SideB"]) CurrentLiabilityMarker106(world,declarations,cardFacts,quantity) == /\ LET virtual==LiabilityMarkerIds106(world.objects) \ MovableLiabilityMarkerIds106(world.objects) IN /\ UNION {declarations[id].counters : id \in DOMAIN declarations}=virtual /\ \A a,b \in DOMAIN declarations : a#b => declarations[a].counters \cap declarations[b].counters={} /\ \A id \in DOMAIN declarations : LET d==declarations[id] IN /\ d.snapshotId=world.id /\ d.projection.property="AdditionalLiabilityMarker" /\ d.projection.target="SideA" /\ d.projection.mode="Continuous" /\ ~d.projection.resolving /\ ~d.projection.lingering /\ d.projection.value=Cardinality(d.counters) /\ d.counters \subseteq LiabilityMarkerIds106(world.objects) /\ d.projection.source.kind="Object" /\ d.projection.source.object \in DOMAIN world.objects /\ d.sourceObject=world.objects[d.projection.source.object] /\ d.sourceObject.card \in DOMAIN cardFacts /\ d.sourceSHA=cardFacts[d.sourceObject.card].sourceSHA /\ d.projection.ability \in world.activeAbilities /\ DefaultActive(d.sourceObject,world.started,cardFacts) /\ quantity=LiabilityMarkerQuantity106(world.objects) LiabilityMarkerPacket106(context,reference,world,id,cardFacts,packet) == /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates /\ LET original==context.templates[id] kept==id \in DOMAIN context.actualEffects actual==IF kept THEN context.actualEffects[id] ELSE original IN /\ original.kind="LiabilityMarker" /\ original.operation \in {"Take","Give","Remove"} /\ original.target="SideA" /\ actual.kind=original.kind /\ actual.operation=original.operation /\ actual.target="SideA" /\ actual.actor=original.actor /\ actual.actor \in SetupPlayers /\ (actual.operation="Take" => actual.actor="SideA") /\ (actual.operation="Give" => actual.actor="SideB") /\ original.baseOrigin=reference.source /\ actual.baseOrigin=reference.source /\ actual.sourceCard=original.sourceCard /\ actual.sourceSHA=original.sourceSHA /\ actual.sourceCard \in DOMAIN cardFacts /\ actual.sourceSHA=cardFacts[actual.sourceCard].sourceSHA /\ actual.value \in Int /\ packet=[contextId |-> context.id,reference |-> reference,effectId |-> id,snapshotId |-> world.id, source |-> actual.baseOrigin,sourceCard |-> actual.sourceCard,sourceSHA |-> actual.sourceSHA,operation |-> actual.operation,actor |-> actual.actor, amount |-> IF ~kept \/ actual.value<=0 THEN 0 ELSE actual.value] TakeLiabilityMarker106(context,reference,world,id,cardFacts,packet,afterObjects,added,usedIds,events) == /\ LiabilityMarkerPacket106(context,reference,world,id,cardFacts,packet) /\ packet.operation \in {"Take","Give"} /\ \A token \in DOMAIN added : added[token]=LiabilityMarkerCounterRow106 /\ BankMintProjection4(world.objects,afterObjects,added,packet.amount,"LiabilityMarker",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE) /\ events=IF packet.amount=0 THEN {} ELSE {[tag |-> "LiabilityMarkerTaken",player |-> "SideA",actor |-> packet.actor,packet |-> packet, counters |-> DOMAIN added,amount |-> packet.amount]} LiabilityMarkerCounterDeparture106(objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) == /\ CheckpointRetirePost103(objects,afterObjects,selected,successors,usedIds,printed,owners,visible) /\ LET cards=={id \in selected : objects[id].card#"none"} IN IF cards={} THEN BankSpendReturn4(objects,afterObjects,selected,TRUE) /\ afterHistory=beforeHistory /\ events={} ELSE RecordMovement8(beforeHistory,afterHistory,batchId,"Retire",cards,"Complete",TRUE,{MovementEvent8(batchId,"Retire",cards)}) /\ events={MovementEvent8(batchId,"Retire",cards)} RemoveLiabilityMarker106(context,reference,world,id,cardFacts,packet,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) == /\ LiabilityMarkerPacket106(context,reference,world,id,cardFacts,packet) /\ packet.operation="Remove" /\ selected \subseteq MovableLiabilityMarkerIds106(world.objects) /\ Cardinality(selected)=IF packet.amount<=Cardinality(MovableLiabilityMarkerIds106(world.objects)) THEN packet.amount ELSE Cardinality(MovableLiabilityMarkerIds106(world.objects)) /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) GrantLiabilityMarkerFund106(before,after,world,afterObjects,declarations,cardFacts,added,usedIds,events) == /\ world.traversal=before.traversal /\ TraversalTimingPresent6(before.traversal) /\ ~before.traversal.formalBegun /\ world.outcome="Playing" /\ CurrentLiabilityMarker106(world,declarations,cardFacts,LiabilityMarkerQuantity106(world.objects)) /\ AddInitiationLiabilityMarker6(before,after,Cardinality(LiabilityMarkerFundIds106(world.objects)),Cardinality(LiabilityMarkerFundIds106(afterObjects)),LiabilityMarkerQuantity106(world.objects)) /\ \A id \in DOMAIN added : added[id]=LiabilityMarkerFundRow106 /\ BankMintProjection4(world.objects,afterObjects,added,LiabilityMarkerQuantity106(world.objects),"ResourceUnit",usedIds,[kind |-> "Zone",zone |-> "Bank"],TRUE,TRUE) /\ events=IF DOMAIN added={} THEN {} ELSE {[tag |-> "LiabilityMarkerFundLoaded",traversalId |-> before.traversal.id,source |-> RuleAbilitySource9("ProcedureCode5da712559aad"), snapshotId |-> world.id,added |-> DOMAIN added,amount |-> LiabilityMarkerQuantity106(world.objects)]} SpendLiabilityMarkerFund106(world,afterObjects,cost,selected,payment,usedPayments,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) == /\ world.outcome="Playing" /\ DuringTraversal6(world.traversal) /\ TimingRef9("SchemaAtom138",world.traversal.id) \in world.inside /\ cost=world.resourceUnitCost /\ cost.tag="ResourceUnitCostContext" /\ cost.status="Paying" /\ cost.snapshotId=world.id /\ cost.traversalId=world.traversal.id /\ cost.player="SideB" /\ cost.amount \in Nat /\ cost.id \in (Nat \ {0}) \ usedPayments /\ selected \subseteq (LiabilityMarkerFundIds106(world.objects) \cup BaseSideBPoolIds106(world.objects)) /\ selected \subseteq CheckpointPhysicalIds103(world.objects) /\ Cardinality(selected)=cost.amount /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) /\ payment=[tag |-> "CompletedResourceUnitMethod",id |-> cost.id,source |-> cost.source,player |-> "SideB",traversalId |-> world.traversal.id, snapshotId |-> world.id,amount |-> cost.amount,paidCounterIds |-> selected,fundCounters |-> selected \cap LiabilityMarkerFundIds106(world.objects),complete |-> TRUE] LiabilityMarkerSpendSources106(payment) == CounterPermissionUseSources9(payment,[id \in {1} |-> [source |-> RuleAbilitySource9("ProcedureCode51c5eb4c9e6c"),paymentId |-> payment.id,allowsPayment |-> TRUE,paidCounters |-> payment.fundCounters]]) ReturnLiabilityMarkerFund106(before,after,world,afterObjects,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) == /\ world.traversal=before.traversal /\ world.outcome="Playing" /\ LiabilityMarkerFundIds106(world.objects) \subseteq CheckpointPhysicalIds103(world.objects) /\ ReturnLiabilityMarkerFund6(before,after,Cardinality(LiabilityMarkerFundIds106(world.objects)),Cardinality(LiabilityMarkerFundIds106(afterObjects)),0,Cardinality(LiabilityMarkerFundIds106(world.objects))) /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,LiabilityMarkerFundIds106(world.objects),successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,events) INSTANCE ConnectionFacts LinkDefinition107(world,object) == world.definitions[object.card] LinkBaseRead107(world,cardFacts,read) == /\ world.sideBProfile \in DOMAIN world.objects /\ world.sideBProfile \in DOMAIN world.properties /\ LET object==world.objects[world.sideBProfile] definition==LinkDefinition107(world,object) properties==SideBCharacteristics8(object,world.properties[world.sideBProfile]) IN /\ object.form="Card" /\ object.kind="Profile" /\ object.zone="Play" /\ object.side="SideB" /\ definition \in DOMAIN world.profileLinkFacts /\ definition \in DOMAIN cardFacts /\ cardFacts[definition].kind="Profile" /\ cardFacts[definition].side="SideB" /\ world.profileLinkFacts[definition].sourceSHA=cardFacts[definition].sourceSHA /\ "baseLink" \in DOMAIN properties /\ properties.baseLink \in Int /\ read=[tag |-> "CurrentBaseLink",snapshotId |-> world.id,object |-> world.sideBProfile,physical |-> object.card,definition |-> definition, sourceSHA |-> cardFacts[definition].sourceSHA,printedBase |-> world.profileLinkFacts[definition].baseLink,value |-> properties.baseLink] PrintedLinkObjectIds107(world) == {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].card \in DOMAIN world.definitions /\ LinkDefinition107(world,world.objects[id]) \in DOMAIN world.linkSymbolFacts} EligiblePrintedLinkSources107(world) == {id \in PrintedLinkObjectIds107(world) : world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.objects[id].face="Up" /\ world.controllers[id]="SideB" /\ world.printedLinkAbilities[id] \in world.activeAbilities} CurrentLinkDeclarations107(world,cardFacts,declarations) == /\ declarations=world.linkDeclarations /\ DOMAIN world.printedLinkAbilities=PrintedLinkObjectIds107(world) /\ \A id \in DOMAIN declarations : declarations[id].projection.source.kind="Object" /\ \A a,b \in DOMAIN declarations : a#b => <>#<> /\ \A a,b \in DOMAIN world.printedLinkAbilities : a#b => world.printedLinkAbilities[a]#world.printedLinkAbilities[b] /\ LET eligible==EligiblePrintedLinkSources107(world) printed=={id \in DOMAIN declarations : declarations[id].origin="PrintedLink"} IN /\ {declarations[id].projection.source.object : id \in printed}=eligible /\ \A source \in eligible : Cardinality({id \in printed : declarations[id].projection.source=ObjectAbilitySource9(source)})=1 /\ \A id \in DOMAIN declarations : LET d==declarations[id] source==d.projection.source.object object==world.objects[source] definition==LinkDefinition107(world,object) IN /\ d.origin \in {"PrintedLink","OtherCompiled"} /\ d.snapshotId=world.id /\ d.projection.property="Connection" /\ d.projection.target="SideB" /\ d.projection.mode="Continuous" /\ ~d.projection.resolving /\ ~d.projection.lingering /\ d.projection.value \in Int /\ d.projection.source.kind="Object" /\ source \in DOMAIN world.objects /\ d.sourceObject=object /\ object.form="Card" /\ object.side="SideB" /\ object.deployed /\ object.zone="Play" /\ world.controllers[source]="SideB" /\ SideBAbilityActivity8(object,d.projection.ability \in world.activeAbilities) /\ definition \in DOMAIN cardFacts /\ d.definition=definition /\ d.sourceSHA=cardFacts[definition].sourceSHA /\ IF d.origin="PrintedLink" THEN /\ definition \in DOMAIN world.linkSymbolFacts /\ world.linkSymbolFacts[definition].sourceSHA=d.sourceSHA /\ d.projection.ability=world.printedLinkAbilities[source] /\ d.projection.value=world.linkSymbolFacts[definition].link ELSE TRUE ReadSideBLink107(world,cardFacts,base,declarations,read) == /\ LinkBaseRead107(world,cardFacts,base) /\ CurrentLinkDeclarations107(world,cardFacts,declarations) /\ read=[tag |-> "CurrentSideBLink",snapshotId |-> world.id,profile |-> base.object,base |-> base.value, contributions |-> [id \in DOMAIN declarations |-> declarations[id].projection.value], value |-> base.value+SumMap([id \in DOMAIN declarations |-> declarations[id].projection.value])] LinkInstructionSnapshot107(world,cardFacts,base,declarations,read,snapshot) == /\ ReadSideBLink107(world,cardFacts,base,declarations,read) /\ snapshot=[tag |-> "CurrentLinkInstructionSnapshot",id |-> world.id,link |-> [player \in {"SideB"} |-> read.value]] EscalatingResourceContestSourceRead108(world,source,object,sourceSHA,ability,cardFacts) == /\ source.kind="Object" /\ source.object \in DOMAIN world.objects /\ object=world.objects[source.object] /\ object.card \in DOMAIN world.definitions /\ LinkDefinition107(world,object) \in DOMAIN cardFacts /\ sourceSHA=cardFacts[LinkDefinition107(world,object)].sourceSHA /\ ability \in world.activeAbilities /\ ability \in DOMAIN world.abilitySources /\ world.abilitySources[ability]=source /\ DefaultActive([object EXCEPT !.card=LinkDefinition107(world,object)],world.started,cardFacts) EscalatingResourceContestRoleIds108(world,role,definition) == {id \in world.activeAbilities \cap DOMAIN world.abilityRoles \cap DOMAIN world.abilitySources : world.abilityRoles[id]=role /\ world.abilitySources[id].kind="Object" /\ world.abilitySources[id].object \in DOMAIN world.objects /\ LinkDefinition107(world,world.objects[world.abilitySources[id].object])=definition} EscalatingResourceContestDuringTraversal108(world) == DuringTraversal6(world.traversal) /\ TimingRef9("SchemaAtom138",world.traversal.id) \in world.inside EscalatingResourceContestCurrent108(frame,world) == frame.id \in DOMAIN world.escalatingResourceContestFrames /\ world.escalatingResourceContestFrames[frame.id]=frame /\ ~frame.complete /\ ~frame.returned /\ world.outcome="Playing" /\ world.turn.id=frame.turnId EscalatingResourceContestOrder108(world,frame,cardFacts,order) == /\ DOMAIN world.escalatingResourceContestOrderPolicies=IF EscalatingResourceContestDuringTraversal108(world) THEN EscalatingResourceContestRoleIds108(world,"EscalatingResourceContestOrder","Specimen0231") ELSE {} /\ \A id \in DOMAIN world.escalatingResourceContestOrderPolicies : LET p==world.escalatingResourceContestOrderPolicies[id] IN /\ p.snapshotId=world.id /\ p.escalatingResourceContestId=frame.id /\ p.order= <<"SideB","SideA">> /\ p.ability=id /\ EscalatingResourceContestSourceRead108(world,p.source,p.sourceObject,p.sourceSHA,id,cardFacts) /\ world.controllers[p.source.object]="SideA" /\ LinkDefinition107(world,p.sourceObject)="Specimen0231" /\ order=IF DOMAIN world.escalatingResourceContestOrderPolicies={} THEN <<"SideA","SideB">> ELSE <<"SideB","SideA">> EscalatingResourceContestContextualLink108(frame,world,cardFacts,base,declarations,read,value) == /\ ReadSideBLink107(world,cardFacts,base,declarations,read) /\ DOMAIN world.escalatingResourceContestLinkPolicies=IF frame.ordinal=1 THEN EscalatingResourceContestRoleIds108(world,"EscalatingResourceContestLinkZero","Specimen0154") ELSE {} /\ \A id \in DOMAIN world.escalatingResourceContestLinkPolicies : LET p==world.escalatingResourceContestLinkPolicies[id] IN /\ p.snapshotId=world.id /\ p.escalatingResourceContestId=frame.id /\ p.value=0 /\ p.ability=id /\ EscalatingResourceContestSourceRead108(world,p.source,p.sourceObject,p.sourceSHA,id,cardFacts) /\ p.sourceObject.zone="SideAObjectiveCompletion" /\ LinkDefinition107(world,p.sourceObject)="Specimen0154" /\ value=IF DOMAIN world.escalatingResourceContestLinkPolicies={} THEN read.value ELSE 0 EscalatingResourceContestPacket108(context,reference,world,id,cardFacts,packet) == /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ id \in DOMAIN context.templates /\ context.templates[id].kind="EscalatingResourceContest" /\ LET effect==context.actualEffects[id] IN /\ effect.kind="EscalatingResourceContest" /\ effect.value \in Int /\ effect.actor="SideA" /\ effect.baseOrigin=reference.source /\ effect.sourceCard=context.templates[id].sourceCard /\ effect.sourceSHA=context.templates[id].sourceSHA /\ effect.sourceCard \in DOMAIN cardFacts /\ effect.sourceSHA=cardFacts[effect.sourceCard].sourceSHA /\ \A clause \in DOMAIN effect.associations : LET a==effect.associations[clause] IN /\ a.id=clause /\ a.trigger \in {"Successful","Unsuccessful","AnyResult"} /\ a.source=reference.source /\ a.sourceSHA=effect.sourceSHA /\ ConditionalDefinitionValid96(a.definition) /\ a.definition.syntax.source=reference.source /\ a.definition.primaryKind="Trigger" /\ a.definition.trigger.kinds={"EscalatingResourceContestAssociatedResult"} /\ a.definition.triggerRequirements=IF a.trigger="AnyResult" THEN {} ELSE {1} /\ a.bodyCondition.kind \in {"NoValue","EscalatingResourceContestStrengthAtLeast"} /\ (a.bodyCondition.kind="EscalatingResourceContestStrengthAtLeast" => a.bodyCondition.amount \in Int) /\ packet=[key |-> <>,contextId |-> context.id,reference |-> reference,effectId |-> id, source |-> effect.baseOrigin,sourceCard |-> effect.sourceCard,sourceSHA |-> effect.sourceSHA,base |-> effect.value,associations |-> effect.associations] EscalatingResourceContestOmitted108(context,reference,world,id) == context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates /\ context.templates[id].kind="EscalatingResourceContest" /\ id \notin DOMAIN context.actualEffects EscalatingResourceContestInitialFrame108(id,packet,turnId,ordinal) == [tag |-> "ActualEscalatingResourceContestProcedure",id |-> id,instance |-> packet.reference.abilityInstance,caller |-> packet.reference,packet |-> packet, turnId |-> turnId,ordinal |-> ordinal,phase |-> "InitialCheckpoint",point |-> "ProcedureCoded1e36ce96789",order |-> <<>>,nextPlayer |-> "NoValue",acted |-> {}, boosts |-> [p \in SetupPlayers |-> [mode |-> "NoValue",amount |-> 0,transaction |-> 0]], strengths |-> [p \in SetupPlayers |-> [set |-> FALSE,value |-> 0]],pendingPlayer |-> "NoValue",checkpoints |-> {}, result |-> "Undetermined",resultEvent |-> [id |-> 0],complete |-> FALSE,returned |-> FALSE] BeginEscalatingResourceContest108(context,reference,world,id,cardFacts,escalatingResourceContestId,eventId,packet,frame,afterFrames,afterHistory,event) == /\ EscalatingResourceContestPacket108(context,reference,world,id,cardFacts,packet) /\ escalatingResourceContestId \in (Nat \ {0}) \ (DOMAIN world.escalatingResourceContestFrames \cup DOMAIN world.escalatingResourceContestHistory) /\ \A old \in DOMAIN world.escalatingResourceContestHistory : world.escalatingResourceContestHistory[old].key#packet.key /\ eventId \in (Nat \ {0}) \ world.eventIds /\ LET ordinal==1+Cardinality({old \in DOMAIN world.escalatingResourceContestHistory : world.escalatingResourceContestHistory[old].turnId=world.turn.id}) IN /\ frame=EscalatingResourceContestInitialFrame108(escalatingResourceContestId,packet,world.turn.id,ordinal) /\ afterFrames=ReplacementOverlay99(world.escalatingResourceContestFrames,[i \in {escalatingResourceContestId} |-> frame]) /\ afterHistory=ReplacementOverlay99(world.escalatingResourceContestHistory,[i \in {escalatingResourceContestId} |-> [key |-> packet.key,turnId |-> world.turn.id,ordinal |-> ordinal]]) /\ event=[id |-> eventId,kind |-> "EscalatingResourceContestInitiated",escalatingResourceContestId |-> escalatingResourceContestId,actor |-> "SideA",source |-> packet.source,reference |-> reference,snapshotId |-> world.id] /\ InstructionPausePoint911([id |-> reference.abilityInstance],reference,context,"EscalatingResourceContest",frame,"ProcedureCoded1e36ce96789",id) EscalatingResourceContestCheckpointCaller108(frame) == IF frame.phase="InitialCheckpoint" THEN InstructionPauseCaller911([id |-> frame.instance],frame.caller,"EscalatingResourceContest",frame,"ProcedureCoded1e36ce96789") ELSE [kind |-> "EscalatingResourceContestBoostCostCheckpoint",escalatingResourceContestId |-> frame.id,instance |-> frame.instance,caller |-> frame.caller, player |-> frame.pendingPlayer,transactionId |-> frame.boosts[frame.pendingPlayer].transaction,point |-> frame.point] DrainEscalatingResourceContestCheckpoint108(before,after,world,cardFacts,cp,ledger,stack,order) == /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase \in {"InitialCheckpoint","BoostCheckpoint"} /\ cp.id \in DOMAIN world.checkpointFrames /\ world.checkpointFrames[cp.id]=cp /\ ledger=world.checkpointLedger /\ cp.caller=EscalatingResourceContestCheckpointCaller108(before) /\ cp.id \notin before.checkpoints /\ CheckpointDrained103(cp,ledger,stack) /\ IF before.phase="InitialCheckpoint" THEN /\ EscalatingResourceContestOrder108(world,before,cardFacts,order) /\ after=[before EXCEPT !.phase="ChooseBoost",!.point=IF order[1]="SideA" THEN "ProcedureCode083016920358" ELSE "ProcedureCode785a8b2e5de4",!.order=order,!.nextPlayer=order[1],!.checkpoints=@ \cup {cp.id}] ELSE /\ order=before.order /\ after=[before EXCEPT !.phase="SetStrength",!.checkpoints=@ \cup {cp.id}] EscalatingResourceContestPoolIds108(objects,player) == IF player="SideB" THEN BaseSideBPoolIds106(objects) ELSE {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind="ResourceUnit" /\ objects[id].host=0 /\ (objects[id].zone="SideAResourceUnits" \/ (objects[id].zone="Play" /\ objects[id].resourceUnitLocation="SideAPool"))} EscalatingResourceContestRecurringPermission108(frame,world,payer,transaction,p,cardFacts) == /\ EscalatingResourceContestCurrent108(frame,world) /\ p.escalatingResourceContestId=frame.id /\ p.snapshotId=world.id /\ p.player=payer /\ p.paymentId=transaction /\ p.purpose="EscalatingResourceContest" /\ EscalatingResourceContestSourceRead108(world,p.source,p.sourceObject,p.sourceSHA,p.ability,cardFacts) /\ world.controllers[p.source.object]=payer /\ world.abilityRoles[p.ability]="EscalatingResourceContestPermission" /\ LinkDefinition107(world,p.sourceObject)=IF payer="SideA" THEN "Specimen0184" ELSE "Specimen0056" /\ \A id \in p.counters : id \in DOMAIN world.objects /\ world.objects[id].form="Counter" /\ world.objects[id].kind="ResourceUnit" /\ ~world.objects[id].virtual /\ world.objects[id].host=p.source.object /\ world.controllers[id]=payer EscalatingResourceContestBoostRule108(player) == RuleAbilitySource9(IF player="SideA" THEN "ProcedureCode000048c944c1" ELSE "ProcedureCode306f617c02aa") DeclineEscalatingResourceContestBoost108(before,after,world,player,announcement) == /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="ChooseBoost" /\ before.nextPlayer=player /\ player \in SetupPlayers /\ player \notin before.acted /\ announcement=[tag |-> "EscalatingResourceContestBoostChoice",escalatingResourceContestId |-> before.id,player |-> player,mode |-> "Decline",amount |-> 0,viewers |-> SetupPlayers] /\ after=[before EXCEPT !.phase="SetStrength",!.pendingPlayer=player,!.acted=@ \cup {player},!.boosts[player]=[mode |-> "Decline",amount |-> 0,transaction |-> 0]] PayEscalatingResourceContestBoost108(before,after,world,afterObjects,player,amount,selected,transaction,payment,announcement,cardFacts,permissions,usedPayments, successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,movementEvents,spendEvents) == /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="ChooseBoost" /\ before.nextPlayer=player /\ player \in SetupPlayers /\ player \notin before.acted /\ usedPayments=world.usedPayments /\ usedIds=world.usedObjects /\ amount \in Nat /\ transaction \in (Nat \ {0}) \ usedPayments /\ world.resourceUnitCost=[tag |-> "EscalatingResourceContestBoostCostContext",id |-> transaction,escalatingResourceContestId |-> before.id,player |-> player,amount |-> amount, snapshotId |-> world.id,source |-> EscalatingResourceContestBoostRule108(player),parent |-> before.caller,status |-> "Paying"] /\ permissions=world.escalatingResourceContestSpendPermissions[player] /\ \A id \in DOMAIN permissions : EscalatingResourceContestRecurringPermission108(before,world,player,transaction,permissions[id],cardFacts) /\ LET fund==IF player="SideB" /\ EscalatingResourceContestDuringTraversal108(world) THEN LiabilityMarkerFundIds106(world.objects) ELSE {} hosted==UNION {permissions[id].counters : id \in DOMAIN permissions} IN /\ selected \subseteq {id \in (EscalatingResourceContestPoolIds108(world.objects,player) \cup fund \cup hosted) : LiabilityMarkerFundController106(world.objects[id],world.controllers[id])=player} /\ Cardinality(selected)=amount /\ selected \subseteq CheckpointPhysicalIds103(world.objects) /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,selected,successors,usedIds,printed,owners,visible,batchId,beforeHistory,afterHistory,movementEvents) /\ payment=[tag |-> "CompletedEscalatingResourceContestBoostCost",id |-> transaction,escalatingResourceContestId |-> before.id,player |-> player,amount |-> amount, snapshotId |-> world.id,source |-> EscalatingResourceContestBoostRule108(player),parent |-> before.caller,paidCounterIds |-> selected,complete |-> TRUE] /\ announcement=[tag |-> "EscalatingResourceContestBoostChoice",escalatingResourceContestId |-> before.id,player |-> player,mode |-> "Pay",amount |-> amount,viewers |-> SetupPlayers] /\ spendEvents=IF amount=0 THEN {} ELSE {[kind |-> "EscalatingResourceContestResourceUnitsSpent",escalatingResourceContestId |-> before.id,player |-> player,amount |-> amount, transactionId |-> transaction,escalatingResourceContestSource |-> before.packet.source,beforeSnapshotId |-> world.id]} /\ after=[before EXCEPT !.phase="BoostCheckpoint",!.pendingPlayer=player,!.acted=@ \cup {player},!.boosts[player]=[mode |-> "Pay",amount |-> amount,transaction |-> transaction]] EscalatingResourceContestPermissionUseSources108(payment,permissions) == CounterPermissionUseSources9(payment,[id \in DOMAIN permissions |-> [source |-> permissions[id].source,paymentId |-> permissions[id].paymentId,allowsPayment |-> TRUE,paidCounters |-> permissions[id].counters \cap payment.paidCounterIds]]) EstablishEscalatingResourceContestStrength108(before,after,world,cardFacts,base,declarations,linkRead,contextualLink) == /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="SetStrength" /\ before.pendingPlayer \in before.acted /\ LET player==before.pendingPlayer value==IF player="SideA" THEN before.packet.base+before.boosts[player].amount ELSE contextualLink+before.boosts[player].amount IN /\ ~before.strengths[player].set /\ IF player="SideB" THEN EscalatingResourceContestContextualLink108(before,world,cardFacts,base,declarations,linkRead,contextualLink) ELSE contextualLink=0 /\ after=[before EXCEPT !.strengths[player]=[set |-> TRUE,value |-> value],!.pendingPlayer="NoValue", !.phase=IF before.acted=SetupPlayers THEN "Determine" ELSE "ChooseBoost", !.nextPlayer=IF before.acted=SetupPlayers THEN "NoValue" ELSE before.order[2], !.point=IF before.acted=SetupPlayers THEN "ProcedureCode42d1fb0bb9d2" ELSE IF before.order[2]="SideA" THEN "ProcedureCode083016920358" ELSE "ProcedureCode785a8b2e5de4"] EscalatingResourceContestAssociatedMatches108(frame,a) == frame.result \in {"Successful","Unsuccessful"} /\ (a.trigger="AnyResult" \/ (a.trigger="Successful" /\ frame.result="Successful") \/ (a.trigger="Unsuccessful" /\ frame.result="Unsuccessful")) EscalatingResourceContestAssociatedBodyGate108(frame,a) == frame.result \in {"Successful","Unsuccessful"} /\ (a.bodyCondition.kind="NoValue" \/ (a.bodyCondition.kind="EscalatingResourceContestStrengthAtLeast" /\ frame.resultEvent.escalatingResourceContestStrength>=a.bodyCondition.amount)) DetermineEscalatingResourceContest108(before,after,world,afterObjects,eventId,event) == /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="Determine" /\ before.acted=SetupPlayers /\ \A p \in SetupPlayers : before.strengths[p].set /\ eventId \in (Nat \ {0}) \ world.eventIds /\ afterObjects=world.objects /\ LET result==IF before.strengths["SideA"].value>before.strengths["SideB"].value THEN "Successful" ELSE "Unsuccessful" IN /\ event=[id |-> eventId,kind |-> "EscalatingResourceContestResult",escalatingResourceContestId |-> before.id,actor |-> "SideA",source |-> before.packet.source,reference |-> before.caller, snapshotId |-> world.id,result |-> result,escalatingResourceContestStrength |-> before.strengths["SideA"].value,linkStrength |-> before.strengths["SideB"].value] /\ after=[before EXCEPT !.phase="Determined",!.point="ProcedureCode0cb35cf3f8e6",!.result=result,!.resultEvent=event] CompleteEscalatingResourceContest108(before,after,world) == /\ EscalatingResourceContestCurrent108(before,world) /\ before.phase="Determined" /\ before.result \in {"Successful","Unsuccessful"} /\ after=[before EXCEPT !.phase="Complete",!.complete=TRUE] ReturnEscalatingResourceContest108(before,after,world,completion) == /\ before.id \in DOMAIN world.escalatingResourceContestFrames /\ world.escalatingResourceContestFrames[before.id]=before /\ before.phase="Complete" /\ before.complete /\ ~before.returned /\ completion=[tag |-> "OwnedEscalatingResourceContestProcedureReturn",escalatingResourceContestId |-> before.id,instance |-> before.instance,caller |-> before.caller, operation |-> before.packet.effectId,resultEvent |-> before.resultEvent,complete |-> TRUE,unprocessedCheckpointRequests |-> {}] /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE] EscalatingResourceContestAssociatedStipulation108(frame,a,event) == [tag |-> "ConditionalTriggerStipulations",ability |-> a.definition.syntax.id,source |-> a.definition.syntax.source, occurrence |-> event.id,snapshotId |-> event.snapshot.id,results |-> [id \in a.definition.triggerRequirements |-> EscalatingResourceContestAssociatedMatches108(frame,a)]] EscalatingResourceContestAssociatedOccurrence108(frame,a,event,snapshot) == /\ a.id \in DOMAIN frame.packet.associations /\ a=frame.packet.associations[a.id] /\ frame.result \in {"Successful","Unsuccessful"} /\ event.id \in Nat \ {0} /\ event.rawResultId=frame.resultEvent.id /\ event.escalatingResourceContestId=frame.id /\ event.kind="EscalatingResourceContestAssociatedResult" /\ event.actor="SideA" /\ event.side="SideA" /\ event.snapshot=snapshot /\ snapshot.id=frame.resultEvent.snapshotId /\ event.scopeKind="Ability" /\ event.scopeDefinition=ConditionalKey96(a.definition) /\ event.escalatingResourceContestStrength=frame.resultEvent.escalatingResourceContestStrength /\ event.linkStrength=frame.resultEvent.linkStrength /\ event.result=frame.result /\ event.object=frame.packet.source.object EscalatingResourceContestAssociatedCandidate108(frame,a,event,stipulation) == /\ EscalatingResourceContestAssociatedOccurrence108(frame,a,event,event.snapshot) /\ stipulation=EscalatingResourceContestAssociatedStipulation108(frame,a,event) /\ TriggerPattern96(a.definition,event) /\ TriggerStipulations96(a.definition,event,stipulation) EscalatingResourceContestAssociatedInstructionCondition108(frame,a,event,instance,condition) == /\ EscalatingResourceContestAssociatedOccurrence108(frame,a,event,event.snapshot) /\ instance.occurrence=event.id /\ instance.definition=ConditionalKey96(a.definition) /\ instance.definitionCopy=a.definition /\ condition=[tag |-> "EscalatingResourceContestAssociatedInstructionCondition",escalatingResourceContestId |-> frame.id,occurrence |-> event.id, definition |-> instance.definition,instance |-> instance.member.id,holds |-> EscalatingResourceContestAssociatedBodyGate108(frame,a)] LoadedCounterToken109(kind,zone,host,actor) == [card |-> "none",form |-> "Counter",kind |-> kind,zone |-> zone,loc |-> host,deployed |-> FALSE,face |-> "Up",front |-> TRUE, activated |-> FALSE,host |-> host,placedBy |-> actor,virtual |-> FALSE,objectivePoints |-> 0,marks |-> {}] CounterInstructionDisposition109(effect) == IF effect.kind \notin {"LoadCounters","PlaceCounters","RemoveCounters"} THEN "UnsupportedCounterOperation" ELSE IF effect.value \notin Nat THEN "RequiresQuantityNormalization" ELSE IF Cardinality(effect.counterKinds)#1 THEN "UnsupportedCounterTypeOrMultiType" ELSE IF effect.counterKind \notin CounterKinds101 \/ effect.counterKinds#{effect.counterKind} THEN "UnsupportedCounterTypeOrMultiType" ELSE IF effect.kind="LoadCounters" /\ effect.value=0 THEN "UnsupportedZeroLoad" ELSE "Supported" CounterInstruction109(context,reference,world,id,cardFacts) == /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ id \in DOMAIN context.templates /\ LET e==context.actualEffects[id] IN /\ e.kind \in {"LoadCounters","PlaceCounters","RemoveCounters"} /\ e.kind=context.templates[id].kind /\ e.value \in Nat /\ CounterInstructionDisposition109(e)="Supported" /\ e.actor \in SetupPlayers /\ e.baseOrigin=reference.source /\ e.sourceCard=context.templates[id].sourceCard /\ e.sourceSHA=context.templates[id].sourceSHA /\ e.sourceCard \in DOMAIN cardFacts /\ e.sourceSHA=cardFacts[e.sourceCard].sourceSHA /\ e.target \in DOMAIN world.objects /\ world.objects[e.target].form="Card" /\ world.objects[e.target].zone \in {"Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ e.counterKinds=context.templates[id].counterKinds /\ e.counterKind=context.templates[id].counterKind /\ e.loadDefinition=context.templates[id].loadDefinition /\ IF e.kind="LoadCounters" THEN e.loadDefinition \in Nat \ {0} ELSE e.loadDefinition=0 /\ \A key \in DOMAIN world.loadLinks : LET link==world.loadLinks[key] IN (e.kind="LoadCounters" /\ e.target=link.host /\ e.baseOrigin=ObjectAbilitySource9(link.host) /\ e.loadDefinition=link.loadDefinition) => e.counterKind=link.kind CounterInstructionKey109(context,reference,id) == <> HostedCounterIds109(objects,host,kind) == {id \in DOMAIN objects : objects[id].form="Counter" /\ objects[id].kind=kind /\ objects[id].host=host /\ objects[id].zone=objects[host].zone} MovableHostedTokens109(objects,host,kind) == {id \in HostedCounterIds109(objects,host,kind) : BankPhysicalToken4(objects[id])} HostedCounterExecutionDisposition109(world,e) == IF CounterInstructionDisposition109(e)#"Supported" THEN CounterInstructionDisposition109(e) ELSE IF e.kind="RemoveCounters" /\ e.value>Cardinality(MovableHostedTokens109(world.objects,e.target,e.counterKind)) /\ {id \in HostedCounterIds109(world.objects,e.target,e.counterKind) : ~world.objects[id].virtual /\ world.objects[id].card#"none"}#{} THEN "RequiresConvertedCounterDeparture" ELSE "Supported" ExecuteBankHostedCounterInstruction109(context,reference,world,id,cardFacts,afterObjects,afterHistory,afterCompleted,selected,added,afterNext,eventId,event) == /\ CounterInstruction109(context,reference,world,id,cardFacts) /\ HostedCounterExecutionDisposition109(world,context.actualEffects[id])="Supported" /\ eventId \in (Nat \ {0}) \ (world.counterEventIds \cup DOMAIN world.loadHistory) /\ CounterInstructionKey109(context,reference,id) \notin world.completedCounterInstructions /\ LET e==context.actualEffects[id] first==world.nextCounterObject created==IF e.kind="RemoveCounters" THEN {} ELSE first..(first+e.value-1) history==[tag |-> "CompletedLoad",host |-> e.target,kind |-> e.counterKind,loadDefinition |-> e.loadDefinition, reference |-> reference,sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA,amount |-> e.value,createdCounterIds |-> created,snapshotId |-> world.id] IN /\ IF e.kind="RemoveCounters" THEN /\ added=[emptyId \in {} |-> emptyId] /\ afterNext=first /\ selected \subseteq MovableHostedTokens109(world.objects,e.target,e.counterKind) /\ Cardinality(selected)=MinOf(e.value,Cardinality(MovableHostedTokens109(world.objects,e.target,e.counterKind))) /\ BankSpendReturn4(world.objects,afterObjects,selected,TRUE) ELSE /\ selected={} /\ first \in Nat \ {0} /\ created \cap world.usedObjects={} /\ added=[i \in created |-> LoadedCounterToken109(e.counterKind,world.objects[e.target].zone,e.target,e.actor)] /\ afterNext=first+e.value /\ BankMintProjection4(world.objects,afterObjects,added,e.value,e.counterKind,world.usedObjects,BankDefaultSource4(IF e.kind="LoadCounters" THEN "Load" ELSE "Place",FALSE,[kind |-> "NoValue"]),TRUE,TRUE) /\ afterHistory=IF e.kind="LoadCounters" THEN ReplacementOverlay99(world.loadHistory,[i \in {eventId} |-> history]) ELSE world.loadHistory /\ afterCompleted=world.completedCounterInstructions \cup {CounterInstructionKey109(context,reference,id)} /\ event=[tag |-> "HostedCounterInstructionComplete",id |-> eventId,operation |-> e.kind,reference |-> reference,host |-> e.target, kind |-> e.counterKind,amount |-> e.value,selected |-> selected,created |-> created,snapshotId |-> world.id,complete |-> TRUE] EmptyLink109(world,cardFacts,link) == /\ link.id \in DOMAIN world.loadLinks /\ link=world.loadLinks[link.id] /\ link.kind \in CounterKinds101 /\ link.loadDefinition \in Nat \ {0} /\ link.host \in DOMAIN world.objects /\ world.objects[link.host].form="Card" /\ world.objects[link.host].card=link.physical /\ LinkDefinition107(world,world.objects[link.host])=link.card /\ link.card \in DOMAIN cardFacts /\ link.sourceSHA=cardFacts[link.card].sourceSHA /\ ConditionalDefinitionValid96(link.emptyDefinition) /\ link.emptyDefinition.primaryKind="Static" /\ link.emptyDefinition.syntax.source=ObjectAbilitySource9(link.host) LinkedLoadIds109(world,link) == {id \in DOMAIN world.loadHistory : LET h==world.loadHistory[id] IN h.tag="CompletedLoad" /\ h.host=link.host /\ h.kind=link.kind /\ h.loadDefinition=link.loadDefinition /\ h.amount>0 /\ h.reference.source=ObjectAbilitySource9(link.host) /\ h.sourceCard=link.card /\ h.sourceSHA=link.sourceSHA} ReadEmpty109(world,cardFacts,link,read) == /\ EmptyLink109(world,cardFacts,link) /\ read=[tag |-> "CurrentLinkedEmpty",snapshotId |-> world.id,linkId |-> link.id,host |-> link.host,physical |-> link.physical, kind |-> link.kind,loadDefinition |-> link.loadDefinition,linkedLoads |-> LinkedLoadIds109(world,link), effectiveCounterIds |-> HostedCounterIds109(world.objects,link.host,link.kind), empty |-> LinkedLoadIds109(world,link)#{} /\ HostedCounterIds109(world.objects,link.host,link.kind)={}] LoadState109(world) == [objects |-> world.objects,definitions |-> world.definitions,history |-> world.loadHistory,links |-> world.loadLinks] EmptyStaticTruth109(world,cardFacts,link,cp,read,truth) == /\ ReadEmpty109(world,cardFacts,link,read) /\ world.id=cp.beginSnapshot.id /\ cp.beginSnapshot.loadState=LoadState109(world) /\ ConditionalKey96(link.emptyDefinition) \in DOMAIN cp.beginSnapshot.definitions /\ cp.beginSnapshot.definitions[ConditionalKey96(link.emptyDefinition)]=link.emptyDefinition /\ truth=[tag |-> "ConditionalStaticTruth",ability |-> link.emptyDefinition.syntax.id,source |-> link.emptyDefinition.syntax.source, checkpointId |-> cp.id,snapshotId |-> cp.beginSnapshot.id,condition |-> link.emptyDefinition.primaryCondition,holds |-> read.empty] ChargePower1010(objects,id) == id \in DOMAIN objects /\ objects[id].form="Card" /\ objects[id].zone \in {"Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ HostedCounterIds109(objects,id,"Power")#{} ChargeSpecKey1010(reference) == WouldContextKey99(reference) ChargeSpec1010(world,reference,cardFacts,spec) == /\ ChargeSpecKey1010(reference) \in DOMAIN world.chargeSpecs /\ spec=world.chargeSpecs[ChargeSpecKey1010(reference)] /\ spec.tag="CurrentChargeSpec" /\ spec.reference=reference /\ spec.snapshotId=world.id /\ spec.sourceCard \in DOMAIN cardFacts /\ spec.sourceSHA=cardFacts[spec.sourceCard].sourceSHA /\ spec.source=reference.source /\ spec.actor \in SetupPlayers /\ spec.mode \in {"Chosen","Particular"} /\ spec.requested \in Nat /\ spec.ifAble \in BOOLEAN /\ spec.setRule \in {"YourDeployedCards","CompiledSet"} /\ spec.targetZone \in {"DefaultDeployed","Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} /\ spec.targetView="OrdinaryHosting" /\ spec.mode="Particular" => spec.requested=1 /\ spec.particular \in Nat \ {0} ChargeSet1010(world,spec) == LET indicated==IF spec.setRule="YourDeployedCards" THEN {id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.controllers[id]=spec.actor} ELSE spec.compiledSet IN {id \in indicated : id \in DOMAIN world.objects /\ world.objects[id].form="Card" /\ IF spec.targetZone="DefaultDeployed" THEN world.objects[id].deployed ELSE world.objects[id].zone=spec.targetZone} ChargeEligible1010(world,spec) == {id \in ChargeSet1010(world,spec) : ChargePower1010(world.objects,id)} ChargeSameMeaning1010(before,after) == /\ before.source=after.source /\ before.sourceCard=after.sourceCard /\ before.sourceSHA=after.sourceSHA /\ before.actor=after.actor /\ before.targetView=after.targetView /\ before.targetZone=after.targetZone /\ before.mode=after.mode /\ before.requested=after.requested /\ before.ifAble=after.ifAble /\ before.setRule=after.setRule /\ before.particular=after.particular ChargeTargetReceipt1010(plan,targets) == [tag |-> "InstructionTargets",instruction |-> plan.id,abilityInstance |-> plan.abilityInstance,source |-> plan.source, sourceZone |-> plan.sourceZone,index |-> plan.index,targets |-> targets,valid |-> TRUE] AnnounceChargeTargets1010(before,after,ability,world,cardFacts,spec,targets,receipt) == /\ ChargeSpec1010(world,InstructionWindowRef93(before),cardFacts,spec) /\ spec.mode="Chosen" /\ before.requiresTargets /\ targets \subseteq ChargeEligible1010(world,spec) /\ Cardinality(targets)=MinOf(spec.requested,Cardinality(ChargeEligible1010(world,spec))) /\ receipt=ChargeTargetReceipt1010(before,targets) /\ AnnounceInstructionTargets93(before,after,receipt,ability,"NoValue") CaptureChargeImminence1010(plan,ability,world,cardFacts,spec,admission) == /\ InstructionImminentAtOrigin93(plan,ability,"NoValue") /\ ChargeSpec1010(world,InstructionWindowRef93(plan),cardFacts,spec) /\ IF spec.mode="Chosen" THEN /\ plan.requiresTargets /\ plan.announced /\ plan.targets \subseteq ChargeEligible1010(world,spec) /\ Cardinality(plan.targets)=MinOf(spec.requested,Cardinality(ChargeEligible1010(world,spec))) ELSE /\ ~plan.requiresTargets /\ plan.targets={} /\ LET refs==IF spec.mode="Chosen" THEN plan.targets ELSE {spec.particular} IN admission=[tag |-> "ChargeAtImminence",reference |-> InstructionWindowRef93(plan),snapshotId |-> world.id,spec |-> spec, announced |-> plan.targets,initialPower |-> [id \in refs |-> ChargePower1010(world.objects,id)], physical |-> [id \in refs \cap DOMAIN world.objects |-> world.objects[id].card]] ChargeAdmissionKey1010(context,id) == <> ChargePacket1010(context,world,id,cardFacts,admission,currentSpec) == /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.actualEffects /\ id \in DOMAIN context.templates /\ ChargeAdmissionKey1010(context,id) \in DOMAIN world.chargeAdmissions /\ admission=world.chargeAdmissions[ChargeAdmissionKey1010(context,id)] /\ admission.tag="ChargeAtImminence" /\ admission.reference=context.initialRef /\ WouldContextKey99(context.initialRef)=WouldContextKey99(context.currentRef) /\ ChargeSpec1010(world,context.currentRef,cardFacts,currentSpec) /\ ChargeSameMeaning1010(admission.spec,currentSpec) /\ LET e==context.actualEffects[id] IN /\ e.kind="Charge" /\ context.templates[id].kind="Charge" /\ e.value=1 /\ e.counterKind="Power" /\ e.actor=currentSpec.actor /\ e.baseOrigin=context.currentRef.source /\ e.sourceCard=currentSpec.sourceCard /\ e.sourceSHA=currentSpec.sourceSHA /\ e.sourceCard=context.templates[id].sourceCard /\ e.sourceSHA=context.templates[id].sourceSHA /\ e.admissionKey=ChargeAdmissionKey1010(context,id) ChargeOmitted1010(context,world,id,afterObjects,afterHistory) == /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ id \in DOMAIN context.templates /\ context.templates[id].kind="Charge" /\ id \notin DOMAIN context.actualEffects /\ afterObjects=world.objects /\ afterHistory=world.loadHistory CurrentChargeTargets1010(world,admission,spec) == LET candidates==IF spec.mode="Chosen" THEN admission.announced \cap ChargeSet1010(world,spec) ELSE {spec.particular} legal=={id \in candidates : id \in DOMAIN admission.physical /\ id \in DOMAIN world.objects /\ world.objects[id].card=admission.physical[id] /\ ChargePower1010(world.objects,id)} initial==IF spec.mode="Particular" THEN {id \in legal : admission.initialPower[id]} ELSE legal IN IF spec.ifAble /\ Cardinality(initial) "NoValue"]),TRUE,TRUE) /\ afterHistory=world.loadHistory /\ afterCompleted=world.completedCharges \cup {ChargeAdmissionKey1010(context,id)} /\ completion=[tag |-> "ChargeInstructionComplete",id |-> eventId,reference |-> context.currentRef,admission |-> ChargeAdmissionKey1010(context,id),charged |-> targets,complete |-> TRUE] /\ events={[tag |-> "PowerCounterPlacedByCharge",instruction |-> context.currentRef,host |-> target,counter |-> CHOOSE i \in DOMAIN added : added[i].host=target, source |-> context.currentRef.source,snapshotId |-> world.id] : target \in targets} NextChargeAfterCheckpoint1010(beforeAbility,afterAbility,beforePlan,afterPlan,world,cp,ledger,stack,cohort,entry) == /\ cohort.ability=beforeAbility /\ cohort.id=beforeAbility.id /\ cohort.source=beforeAbility.source /\ cp.id \in DOMAIN world.instructionCheckpoints /\ world.instructionCheckpoints[cp.id]=cp /\ ledger=world.conditionalLedger /\ cp.caller=PlayInstructionCaller97(cohort) /\ CheckpointDrained103(cp,ledger,stack) /\ entry.checkpointAndAllNewerChainsComplete /\ EnterNextAbilityInstruction93(beforeAbility,afterAbility,beforePlan,afterPlan,entry) ExampleFamily049DeployedReference1010(beforeObjects,afterObjects,old,new,successors,used,source,deployReference,reference) == /\ deployReference.source=source /\ old \in DOMAIN beforeObjects /\ beforeObjects[old].zone="SideBHand" /\ successors=[id \in {old} |-> new] /\ CardBatchTransfer8(beforeObjects,afterObjects,{old},successors,used,"Play","Up",[id \in {old} |-> 0]) /\ reference=[tag |-> "InstructionDeployedObject",source |-> source,fromInstruction |-> deployReference,oldObject |-> old,object |-> new,physical |-> beforeObjects[old].card] MarkEffectIds1011(registry) == {id \in DOMAIN registry.effects : registry.effects[id].definitionId=101101 /\ registry.effects[id].choiceKey="GlobalMark"} LiveMarkIds1011(registry,world) == MarkEffectIds1011(registry) \cap ActiveLingeringIds910(registry,world) MarkRegistryValid1011(registry,world) == /\ Cardinality(LiveMarkIds1011(registry,world))<=1 /\ \A id \in MarkEffectIds1011(registry) : LET e==registry.effects[id] IN /\ e.kind="Ordinary" /\ e.choicePolicy="NoValue" /\ e.value.targetSite \in CentralTargetSites4 /\ e.value.cutoff \in Nat \ {0} /\ e.value.turn=e.creationTurn /\ e.baseDuration=[kind |-> "Timing",ref |-> TimingRef9("Turn",e.creationTurn)] /\ e.durationClass="Turn" MarkJournalValid1011(world) == /\ world.eventSerial \in Nat /\ \A id \in DOMAIN world.history : world.history[id].id=id /\ world.history[id].serial \in 1..world.eventSerial /\ \A a,b \in DOMAIN world.history : a#b => world.history[a].serial#world.history[b].serial MarkWorldBound1011(world,registry,a) == /\ LifetimeWorldProjection910(world)=a.current /\ world.lingering=registry /\ LifetimeReady910(registry,a) /\ MarkRegistryValid1011(registry,a.current) /\ MarkJournalValid1011(world) /\ \A id \in LiveMarkIds1011(registry,a.current) : LET e==registry.effects[id] IN \E event \in DOMAIN world.history : /\ world.history[event].kind="MarkDesignated" /\ world.history[event].effectId=id /\ world.history[event].targetSite=e.value.targetSite /\ world.history[event].serial=e.value.cutoff /\ world.history[event].turn=e.value.turn /\ world.history[event].reference=e.creation[2] /\ world.history[event].source=e.source MarkRead1011(world,a,player,read) == /\ player \in SetupPlayers /\ MarkWorldBound1011(world,world.lingering,a) /\ ReadActiveLingering910(world.lingering,a,[tag |-> "CurrentActiveLingeringEffects",worldId |-> a.current.id,ids |-> ActiveLingeringIds910(world.lingering,a.current)]) /\ LET ids==LiveMarkIds1011(world.lingering,a.current) IN read=IF ids={} THEN [tag |-> "CurrentGlobalMark",worldId |-> world.id,present |-> FALSE,effectId |-> 0,targetSite |-> "NoValue",cutoff |-> 0,turn |-> world.turn.id] ELSE LET id==CHOOSE id \in ids : TRUE value==world.lingering.effects[id].value IN [tag |-> "CurrentGlobalMark",worldId |-> world.id,present |-> TRUE,effectId |-> id,targetSite |-> value.targetSite,cutoff |-> value.cutoff,turn |-> value.turn] MarkBalancedSampler1011(sampler) == /\ sampler.tag="UniformFiniteAtoms" /\ sampler.space#{} /\ IsFiniteSet(sampler.space) /\ DOMAIN sampler.mapping=sampler.space /\ {sampler.mapping[atom] : atom \in sampler.space} \subseteq CentralTargetSites4 /\ sampler.weights=[atom \in sampler.space |-> 1] /\ sampler.totalWeight=Cardinality(sampler.space) /\ \A targetSite \in CentralTargetSites4 : 3*Cardinality({atom \in sampler.space : sampler.mapping[atom]=targetSite})=Cardinality(sampler.space) MarkDraw1011(world,context,operation,draw,sampler,targetSite) == /\ draw.id \in Nat \ {0} /\ draw.id \in DOMAIN world.pendingRandomDraws /\ draw=world.pendingRandomDraws[draw.id] /\ draw.id \notin DOMAIN world.draws /\ draw.tag="UniformMarkDraw" /\ draw.phase="InstructionResolution" /\ draw.snapshotId=world.id /\ draw.reference=context.currentRef /\ draw.operation=operation /\ MarkBalancedSampler1011(sampler) /\ draw.sampler=sampler /\ draw.atom \in sampler.space /\ targetSite=sampler.mapping[draw.atom] /\ draw.targetSite=targetSite MarkBlueprint1011(source,originKind,targetSite,cutoff,turn) == [kind |-> "Ordinary",source |-> source,originKind |-> originKind,target |-> 0,value |-> [targetSite |-> targetSite,cutoff |-> cutoff,turn |-> turn], baseDuration |-> [kind |-> "Timing",ref |-> TimingRef9("Turn",turn)],durationMode |-> "Specified",durationClass |-> "Turn",choiceKey |-> "GlobalMark", lingeringConsumers |-> {},otherConsumers |-> {},definitionId |-> 101101,whenYourTurnBegins |-> FALSE,onlyChoice |-> FALSE] MarkInstruction1011(context,origin,world,operation,cardFacts) == /\ cardFacts=world.cardFacts /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ origin.kind="Instruction" /\ origin.plan.phase="Resolving" /\ context.currentRef=InstructionWindowRef93(origin.plan) /\ ConditionalCreationInstruction96(origin.plan,origin.parent,origin.ruleStep) /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \in DOMAIN context.actualEffects /\ operation \in DOMAIN context.templates /\ LET e==context.actualEffects[operation] IN /\ e.kind="CreateLingering" /\ e.semantic="IdentifyMark" /\ e.actor \in SetupPlayers /\ e.sourceCard=context.templates[operation].sourceCard /\ e.sourceSHA=context.templates[operation].sourceSHA /\ e.sourceCard \in DOMAIN cardFacts /\ e.sourceSHA=cardFacts[e.sourceCard].sourceSHA /\ e.baseOrigin=context.currentRef.source /\ context.currentRef.source.kind="Object" /\ IF context.currentRef.source.object \in DOMAIN world.objects THEN world.sourceDefinitions[world.objects[context.currentRef.source.object].card]=e.sourceCard ELSE TRUE IdentifyMark1011(before,after,a,context,origin,operation,cardFacts,read,draw,sampler,effectId,eventId,execution,completion,events) == /\ MarkInstruction1011(context,origin,before,operation,cardFacts) /\ MarkRead1011(before,a,context.actualEffects[operation].actor,read) /\ IF read.present THEN /\ context.actualEffects[operation].blueprints=[emptyId \in {} |-> emptyId] /\ draw=[tag |-> "NoDraw"] /\ after=before /\ events={} /\ completion=[tag |-> "IdentifyMarkComplete",reference |-> context.currentRef,operation |-> operation,created |-> FALSE,effectId |-> read.effectId,targetSite |-> read.targetSite] ELSE /\ ~before.turn.formalEnded /\ eventId \in (Nat \ {0}) \ DOMAIN before.history /\ LET targetSite==draw.targetSite cutoff==before.eventSerial+1 blueprint==MarkBlueprint1011(context.currentRef.source,IF origin.plan.origin="Rule" THEN "Rule" ELSE origin.parent.kind,targetSite,cutoff,before.turn.id) event==[id |-> eventId,kind |-> "MarkDesignated",serial |-> cutoff,turn |-> before.turn.id,targetSite |-> targetSite,effectId |-> effectId,reference |-> context.currentRef,source |-> context.currentRef.source] IN /\ MarkDraw1011(before,context,operation,draw,sampler,targetSite) /\ context.actualEffects[operation].blueprints=[id \in {effectId} |-> blueprint] /\ CreateObservedLingeringEffects910(before.lingering,after.lingering,context,origin,operation,execution,a) /\ after=[before EXCEPT !.lingering=after.lingering,!.eventSerial=cutoff,!.history=ReplacementOverlay99(@,[id \in {eventId} |-> event]), !.draws=ReplacementOverlay99(@,[id \in {draw.id} |-> draw]),!.pendingRandomDraws=Without101(@,{draw.id})] /\ completion=[tag |-> "IdentifyMarkComplete",reference |-> context.currentRef,operation |-> operation,created |-> TRUE,effectId |-> effectId,targetSite |-> targetSite] /\ events={event} MarkRelatedEvents1011(world,mark,kind) == IF ~mark.present THEN {} ELSE {id \in DOMAIN world.history : LET e==world.history[id] IN e.kind=kind /\ e.targetSite=mark.targetSite /\ e.turn=mark.turn /\ e.serial>mark.cutoff} FirstMarkEvent1011(world,mark,kind,event) == event \in MarkRelatedEvents1011(world,mark,kind) /\ \A earlier \in MarkRelatedEvents1011(world,mark,kind) : world.history[earlier].serial>=world.history[event].serial MarkHistoryRead1011(world,a,player,kind,mark,receipt) == /\ MarkRead1011(world,a,player,mark) /\ receipt=[tag |-> "CurrentMarkHistory",worldId |-> world.id,effectId |-> mark.effectId,kind |-> kind,events |-> MarkRelatedEvents1011(world,mark,kind), first |-> {id \in MarkRelatedEvents1011(world,mark,kind) : FirstMarkEvent1011(world,mark,kind,id)}] MarkTraversalRelation1011(world,a,mark,receipt) == /\ MarkRead1011(world,a,"SideB",mark) /\ receipt=[tag |-> "OngoingTraversalOnMark",worldId |-> world.id,traversalId |-> world.control.traversal.id,holds |-> mark.present /\ DuringTraversal6(world.control.traversal) /\ TimingRef9("SchemaAtom138",world.control.traversal.id) \in world.inside /\ world.control.traversal.attacked=mark.targetSite] MarkProtectionRelation1011(world,a,mark,barrierCard,protection,receipt) == /\ MarkRead1011(world,a,"SideB",mark) /\ protection=world.barrierProtection /\ receipt=[tag |-> "BarrierProtectingMark",worldId |-> world.id,barrierCard |-> barrierCard,holds |-> mark.present /\ barrierCard \in DOMAIN world.objects /\ world.objects[barrierCard].form="Card" /\ world.objects[barrierCard].kind="Barrier" /\ barrierCard \in DOMAIN protection /\ protection[barrierCard]=mark.targetSite] CaptureMarkEvent1011(before,after,a,event,mark) == /\ MarkRead1011(before,a,event.actor,mark) /\ event.id \in (Nat \ {0}) \ DOMAIN before.history /\ event.id \in DOMAIN before.sourceOccurrences /\ event=before.sourceOccurrences[event.id] /\ event.snapshot.id=before.id /\ event.snapshot.objects=before.objects /\ event.kind \in {"TraversalSuccessful","TraversalEnded","Inspection","EncounterBarrier"} /\ event.journalSerial=before.eventSerial+1 /\ event.turnId=before.turn.id /\ event.kind \in {"TraversalSuccessful","TraversalEnded","EncounterBarrier"} => event.targetSite=event.traversal.attacked /\ event.kind="EncounterBarrier" => event.traversal=before.control.traversal /\ DuringTraversal6(event.traversal) /\ TimingRef9("SchemaAtom138",event.traversal.id) \in before.inside /\ after=[before EXCEPT !.eventSerial=@+1,!.history=ReplacementOverlay99(@,[id \in {event.id} |-> [id |-> event.id,kind |-> event.kind,serial |-> event.journalSerial,turn |-> event.turnId,targetSite |-> event.targetSite,traversalId |-> event.traversal.id, actor |-> event.actor,mark |-> mark,occurrence |-> event]])] HistoricalMark1011(world,mark) == mark.tag="CurrentGlobalMark" /\ mark.present /\ \E id \in DOMAIN world.history : LET e==world.history[id] IN e.kind="MarkDesignated" /\ e.effectId=mark.effectId /\ e.targetSite=mark.targetSite /\ e.turn=mark.turn /\ e.serial=mark.cutoff MarkRole1011(card) == CASE card \in {"Specimen0165","Specimen0259"} -> "FirstSuccess" [] card="Specimen0119" -> "FirstTraversalEnd" [] card="Specimen0026" -> "EncounterDuringMarkTraversal" [] OTHER -> "Unsupported" MarkConditionalStipulation1011(world,a,d,event,rule,receipt) == /\ MarkWorldBound1011(world,world.lingering,a) /\ ConditionalDefinitionValid96(d) /\ d.primaryKind="Trigger" /\ d.triggerRequirements={1} /\ ConditionalKey96(d) \in DOMAIN world.markRules /\ rule=world.markRules[ConditionalKey96(d)] /\ rule.definition=d /\ rule.card \in DOMAIN world.cardFacts /\ rule.sourceSHA=world.cardFacts[rule.card].sourceSHA /\ rule.role=MarkRole1011(rule.card) /\ rule.role#"Unsupported" /\ d.syntax.source.kind="Object" /\ rule.physical \in DOMAIN world.sourceDefinitions /\ world.sourceDefinitions[rule.physical]=rule.card /\ IF d.syntax.source.object \in DOMAIN world.objects THEN world.objects[d.syntax.source.object].card=rule.physical ELSE TRUE /\ event.id \in DOMAIN world.history /\ event=world.history[event.id].occurrence /\ LET row==world.history[event.id] mark==row.mark kind==CASE rule.role="FirstSuccess" -> "TraversalSuccessful" [] rule.role="FirstTraversalEnd" -> "TraversalEnded" [] OTHER -> "EncounterBarrier" matches==HistoricalMark1011(world,mark) /\ event.kind=kind /\ event.actor="SideB" /\ IF rule.role="EncounterDuringMarkTraversal" THEN event.id \in MarkRelatedEvents1011(world,mark,"EncounterBarrier") ELSE FirstMarkEvent1011(world,mark,kind,event.id) IN receipt=[tag |-> "ConditionalTriggerStipulations",ability |-> d.syntax.id,source |-> d.syntax.source,occurrence |-> event.id,snapshotId |-> event.snapshot.id, results |-> [id \in {1} |-> matches]] MarkSpecimen0119Body1011(world,event,receipt) == /\ event.kind="TraversalEnded" /\ event.id \in DOMAIN world.history /\ event=world.history[event.id].occurrence /\ LET row==world.history[event.id] mark==row.mark siteInspections=={id \in MarkRelatedEvents1011(world,mark,"Inspection") : world.history[id].traversalId=row.traversalId /\ world.history[id].serial<=row.serial} IN receipt=[tag |-> "Specimen0119InstructionCondition",occurrence |-> event.id,traversalId |-> row.traversalId,holds |-> HistoricalMark1011(world,mark) /\ siteInspections#{}] MarkSpecimen0259Branch1011(world,event,branch) == /\ event.kind="TraversalSuccessful" /\ event.id \in DOMAIN world.history /\ event=world.history[event.id].occurrence /\ HistoricalMark1011(world,world.history[event.id].mark) /\ branch=[tag |-> "Specimen0259InstructionBranch",occurrence |-> event.id,branch |-> IF world.history[event.id].mark.targetSite="SchemaAtom082" THEN "AdditionalCentralAItemInspection" ELSE "InspectionCentralAAfterTraversal"] SabotageSources1012 == {"Specimen0159","Specimen0242","Specimen0025","Specimen0083","Specimen0041","Specimen0141","Specimen0048"} SabotageKey1012(context,operation) == <> SabotageZones1012(world) == /\ DeckObjectOrder8(world.objects,"SideA",world.aDrawPile) /\ world.aHand={id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].zone="SideAHand"} /\ world.aHand \cap SetupRange(world.aDrawPile)={} /\ DOMAIN world.objects \subseteq world.usedObjects /\ DOMAIN world.owners=DOMAIN world.objects /\ \A id \in world.aHand \cup SetupRange(world.aDrawPile) : world.objects[id].side="SideA" /\ world.owners[id]="SideA" /\ ~world.objects[id].deployed /\ world.objects[id].host=0 SabotageScope1012(world) == [id |-> world.id,objects |-> world.objects,aHand |-> world.aHand,aDrawPile |-> world.aDrawPile,usedObjects |-> world.usedObjects,owners |-> world.owners,known |-> world.sideAKnowledge] SabotagePacket1012(context,world,operation,packet) == /\ world.outcome="Playing" /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ context.id \in DOMAIN world.expectedInstructions /\ context=world.expectedInstructions[context.id] /\ ExpectedEffectsValid99(context.state.effects) /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \in DOMAIN context.actualEffects /\ operation \in DOMAIN context.templates /\ SabotageKey1012(context,operation) \in DOMAIN world.sabotagePackets /\ packet=world.sabotagePackets[SabotageKey1012(context,operation)] /\ LET e==context.actualEffects[operation] IN /\ e.id=operation /\ e.kind="SchemaAtom139" /\ context.templates[operation].kind="SchemaAtom139" /\ e.value \in Int /\ e.actor="SideA" /\ e.abilityController="SideB" /\ e.baseOrigin=context.currentRef.source /\ e.sourceCard \in SabotageSources1012 /\ e.sourceCard=context.templates[operation].sourceCard /\ e.sourceSHA=context.templates[operation].sourceSHA /\ e.sourceCard \in DOMAIN world.cardFacts /\ e.sourceSHA=world.cardFacts[e.sourceCard].sourceSHA /\ packet=[tag |-> "CurrentSabotagePacket",key |-> SabotageKey1012(context,operation),reference |-> context.currentRef,snapshotId |-> world.id, sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA,amount |-> e.value,actor |-> "SideA",abilityController |-> "SideB",sourcePhysical |-> packet.sourcePhysical, choicePolicy |-> packet.choicePolicy,trashProfile |-> packet.trashProfile] /\ context.currentRef.source.kind="Object" /\ packet.sourcePhysical \in DOMAIN world.sourceDefinitions /\ world.sourceDefinitions[packet.sourcePhysical]=e.sourceCard /\ IF context.currentRef.source.object \in DOMAIN world.objects THEN world.objects[context.currentRef.source.object].card=packet.sourcePhysical ELSE context.currentRef.source.object \in DOMAIN world.historicalPhysical /\ world.historicalPhysical[context.currentRef.source.object]=packet.sourcePhysical SabotageSupport1012(packet) == CASE packet.choicePolicy#"InternalResolutionChoice" -> "RequiresTargetTimingAdapter" [] packet.trashProfile#"OrdinaryUnreplaced" -> "RequiresOwningRetireAdapter" [] OTHER -> "SupportedResolutionComponent" SabotageTotal1012(world,amount) == MinOf(MaxOf(0,amount),Cardinality(world.aHand)+Len(world.aDrawPile)) SideASabotageView1012(world,packet) == [tag |-> "SideASabotageDecisionView",actor |-> "SideA",amount |-> packet.amount, aHand |-> [id \in HandVisibleCards4(world.aHand,"SideA","SideA",{}) |-> world.objects[id].card],aDrawPileCount |-> DeckCount4(world.aDrawPile),previousKnowledge |-> world.sideAKnowledge] OpenSabotageFrame1012(id,context,operation,world,packet) == [tag |-> "SabotageResolution",id |-> id,contextId |-> context.id,operation |-> operation,reference |-> context.currentRef,packet |-> packet, scope |-> SabotageScope1012(world),phase |-> "Choose",choiceSealed |-> FALSE,aHandChosen |-> {},aDrawPileCount |-> 0,successors |-> [x \in {} |-> x],complete |-> FALSE,afterWorld |-> 0] OpenSabotage1012(id,context,operation,world,packet,frame) == /\ SabotagePacket1012(context,world,operation,packet) /\ SabotageSupport1012(packet)="SupportedResolutionComponent" /\ SabotageZones1012(world) /\ id \in (Nat \ {0}) \ world.usedProcedures /\ packet.key \notin world.completedSabotage /\ frame=OpenSabotageFrame1012(id,context,operation,world,packet) SabotageFrameBound1012(frame,context,operation,world,packet) == /\ SabotagePacket1012(context,world,operation,packet) /\ SabotageSupport1012(packet)="SupportedResolutionComponent" /\ SabotageZones1012(world) /\ frame.tag="SabotageResolution" /\ frame.id \in (Nat \ {0}) \ world.usedProcedures /\ ~frame.complete /\ frame.contextId=context.id /\ frame.operation=operation /\ frame.reference=context.currentRef /\ frame.packet=packet /\ frame.scope=SabotageScope1012(world) /\ packet.key \notin world.completedSabotage ChooseSabotageCentralA1012(before,after,context,operation,world,packet,decision) == /\ SabotageFrameBound1012(before,context,operation,world,packet) /\ before.phase="Choose" /\ ~before.choiceSealed /\ decision.tag="SideASabotageCentralAChoice" /\ decision.actor="SideA" /\ decision.frameId=before.id /\ decision.snapshotId=world.id /\ decision.view=SideASabotageView1012(world,packet) /\ decision.aHand \subseteq world.aHand /\ LET total==SabotageTotal1012(world,packet.amount) count==Cardinality(decision.aHand) IN /\ MaxOf(0,total-Len(world.aDrawPile))<=count /\ count<=MinOf(total,Cardinality(world.aHand)) /\ after=[before EXCEPT !.phase="ReadyRetire",!.choiceSealed=TRUE,!.aHandChosen=decision.aHand,!.aDrawPileCount=total-count] SabotageSelected1012(frame,world) == frame.aHandChosen \cup SetupRange(SubSeq(world.aDrawPile,1,frame.aDrawPileCount)) SabotageRetireEvent1012(id,frame,world,afterId,successors) == [id |-> id,kind |-> "CardsRetireed",actor |-> "SideA",abilityController |-> frame.packet.abilityController,source |-> frame.reference.source, sourceCard |-> frame.packet.sourceCard,sourceSHA |-> frame.packet.sourceSHA,reference |-> frame.reference,operation |-> frame.operation, objects |-> SabotageSelected1012(frame,world),fromCentralA |-> frame.aHandChosen,fromADrawPile |-> SubSeq(world.aDrawPile,1,frame.aDrawPileCount),successors |-> successors, beforeSnapshot |-> world.id,afterSnapshot |-> afterId,destination |-> "SideADiscard",face |-> "Down",simultaneous |-> TRUE] SabotageRetireMap1012(objects,successors) == ReplacementOverlay99(Without101(objects,DOMAIN successors),[new \in {successors[old] : old \in DOMAIN successors} |-> [objects[CHOOSE old \in DOMAIN successors : successors[old]=new] EXCEPT !.zone="SideADiscard",!.face="Down",!.loc=0,!.host=0,!.deployed=FALSE,!.activated=FALSE,!.marks={}]]) ResolveSabotage1012(before,after,context,operation,world,next,packet,successors,afterId,eventId,eventMap,completion) == /\ SabotageFrameBound1012(before,context,operation,world,packet) /\ before.phase="ReadyRetire" /\ before.choiceSealed /\ before.aHandChosen \subseteq world.aHand /\ before.aDrawPileCount=SabotageTotal1012(world,packet.amount)-Cardinality(before.aHandChosen) /\ before.aDrawPileCount \in 0..Len(world.aDrawPile) /\ Cardinality(before.aHandChosen)<=SabotageTotal1012(world,packet.amount) /\ afterId \in (Nat \ {0}) \ world.usedWorlds /\ eventId \in (Nat \ {0}) \ world.eventIds /\ LET selected==SabotageSelected1012(before,world) event==SabotageRetireEvent1012(eventId,before,world,afterId,successors) IN /\ next.objects=SabotageRetireMap1012(world.objects,successors) /\ CardBatchTransfer8(world.objects,next.objects,selected,successors,world.usedObjects,"SideADiscard","Down",[id \in selected |-> 0]) /\ eventMap=IF selected={} THEN [id \in {} |-> id] ELSE [id \in {eventId} |-> event] /\ next=[world EXCEPT !.id=afterId,!.objects=next.objects,!.aHand=@ \ before.aHandChosen,!.aDrawPile=SubSeq(@,before.aDrawPileCount+1,Len(@)), !.owners=ReplacementOverlay99(Without101(@,selected),[id \in {successors[old] : old \in selected} |-> world.owners[CHOOSE old \in selected : successors[old]=id]]), !.usedObjects=@ \cup {successors[old] : old \in selected},!.usedProcedures=@ \cup {before.id},!.usedWorlds=@ \cup {afterId}, !.completedSabotage=@ \cup {packet.key},!.eventIds=@ \cup DOMAIN eventMap,!.sabotageEvents=ReplacementOverlay99(@,eventMap)] /\ SabotageZones1012(next) /\ after=[before EXCEPT !.phase="Complete",!.successors=successors,!.complete=TRUE,!.afterWorld=afterId] /\ completion=[tag |-> "SabotageBodyComplete",reference |-> before.reference,operation |-> operation,snapshotId |-> afterId,frameId |-> before.id, actor |-> "SideA",trashed |-> selected,events |-> DOMAIN eventMap,complete |-> TRUE] SabotagePublicSummary1012(event) == [tag |-> "SabotageRetireSummary",actor |-> event.actor,aHandCount |-> Cardinality(event.fromCentralA),aDrawPileCount |-> Len(event.fromADrawPile),destination |-> "SchemaAtom018",face |-> "Down"] ReadSabotageDiscardSite1012(frame,world,viewer,currentVisibleIds,read) == /\ viewer \in SetupPlayers /\ currentVisibleIds=world.currentLookIds[viewer] /\ frame.packet.key \in world.completedSabotage /\ frame.id \in world.usedProcedures /\ frame.complete /\ frame.phase="Complete" /\ frame.choiceSealed /\ frame.afterWorld=world.id /\ LET moved=={frame.successors[id] : id \in DOMAIN frame.successors} IN /\ moved \subseteq DOMAIN world.objects /\ \A id \in moved : world.objects[id].zone="SideADiscard" /\ world.objects[id].face="Down" /\ read=[tag |-> "SabotageArchiveLook",viewer |-> viewer,snapshotId |-> world.id, visible |-> DiscardSiteVisibleCards4(moved,[id \in moved |-> world.objects[id].face],viewer,currentVisibleIds)] SabotageOmitted1012(context,operation,world,afterObjects,afterCentralA,afterADrawPile,events) == /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.id \in DOMAIN world.expectedInstructions /\ context=world.expectedInstructions[context.id] /\ operation \in DOMAIN context.templates /\ context.templates[operation].kind="SchemaAtom139" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \notin DOMAIN context.actualEffects /\ afterObjects=world.objects /\ afterCentralA=world.aHand /\ afterADrawPile=world.aDrawPile /\ events={} NewSabotageOccurrence1012(id,batch,unit,snapshot,beforeSnapshot) == [id |-> id,kind |-> IF unit=0 THEN "CardsRetireed" ELSE "CardRetireed",object |-> unit,actor |-> batch.actor,side |-> "SideA",snapshot |-> snapshot,effectId |-> batch.id, movement |-> [tag |-> IF unit=0 THEN "BatchRetire" ELSE "Retire",oldObject |-> unit,newObject |-> IF unit=0 THEN 0 ELSE batch.successors[unit],beforeSnapshot |-> beforeSnapshot], scopeKind |-> "Global",scopeDefinition |-> [ability |-> 0,source |-> RuleAbilitySource9("NoValue")],structure |-> NoTimingRef9,step |-> "NoValue",traversal |-> NoTraversal6,siteInspection |-> [traversalId |-> 0,origin |-> "NoValue"], batchId |-> batch.id,batch |-> batch,unit |-> unit] PublishSabotageOccurrences1012(world,batch,allocation,snapshot,beforeSnapshot,occurrences) == /\ batch.id \in DOMAIN world.sabotageEvents /\ batch=world.sabotageEvents[batch.id] /\ batch.objects#{} /\ snapshot.id=world.id /\ snapshot.objects=world.objects /\ batch.afterSnapshot=world.id /\ beforeSnapshot.id=batch.beforeSnapshot /\ DOMAIN allocation={0} \cup batch.objects /\ {allocation[unit] : unit \in DOMAIN allocation} \subseteq (Nat \ {0}) \ world.usedOccurrenceIds /\ Cardinality({allocation[unit] : unit \in DOMAIN allocation})=Cardinality(DOMAIN allocation) /\ occurrences=[id \in {allocation[unit] : unit \in DOMAIN allocation} |-> LET unit==CHOOSE unit \in DOMAIN allocation : allocation[unit]=id IN NewSabotageOccurrence1012(id,batch,unit,snapshot,beforeSnapshot)] SabotageObserverRole1012(card) == CASE card="Specimen0024" -> [actor |-> "SideA",scope |-> "CentralABatch"] [] card \in {"Specimen0072","Specimen0110","Specimen0041"} -> [actor |-> "SideB",scope |-> "SideACard"] [] OTHER -> [actor |-> "NoValue",scope |-> "Unsupported"] SabotageTriggerStipulation1012(world,d,event,rule,receipt) == /\ ConditionalDefinitionValid96(d) /\ d.primaryKind="Trigger" /\ d.triggerRequirements={1} /\ ConditionalKey96(d) \in DOMAIN world.trashRules /\ rule=world.trashRules[ConditionalKey96(d)] /\ rule.definition=d /\ rule.card \in DOMAIN world.cardFacts /\ rule.sourceSHA=world.cardFacts[rule.card].sourceSHA /\ rule.role=SabotageObserverRole1012(rule.card) /\ rule.role.scope#"Unsupported" /\ d.syntax.source.kind="Object" /\ d.syntax.source.object \in DOMAIN world.objects /\ world.sourceDefinitions[world.objects[d.syntax.source.object].card]=rule.card /\ event.id \in DOMAIN world.sabotageOccurrences /\ event=world.sabotageOccurrences[event.id] /\ event.batchId \in DOMAIN world.sabotageEvents /\ event.batch=world.sabotageEvents[event.batchId] /\ event.batch.id=event.batchId /\ (event.unit=0 \/ event.unit \in event.batch.objects) /\ event.kind=(IF event.unit=0 THEN "CardsRetireed" ELSE "CardRetireed") /\ event.object=event.unit /\ event.actor=event.batch.actor /\ event.batch.objects#{} /\ event.batch.actor="SideA" /\ LET matched==event.actor=rule.role.actor /\ (IF rule.role.scope="CentralABatch" THEN event.unit=0 /\ event.batch.fromCentralA#{} ELSE event.unit \in event.batch.objects) IN receipt=[tag |-> "ConditionalTriggerStipulations",ability |-> d.syntax.id,source |-> d.syntax.source,occurrence |-> event.id,snapshotId |-> event.snapshot.id,results |-> [part \in {1} |-> matched]] DividendFacts1013 == INSTANCE SettlementFacts DividendSources1013 == DOMAIN DividendFacts1013!DividendPrintedFacts1013 DividendFact1013(card,cardFacts) == card \in DividendSources1013 /\ card \in DOMAIN cardFacts /\ DividendFacts1013!DividendPrintedFacts1013[card].sourceSHA=cardFacts[card].sourceSHA ReadDividendExampleFamily052Requirement1013(world,objective,read) == /\ objective \in DOMAIN world.objects /\ world.objects[objective].form="Card" /\ world.objects[objective].kind="Objective" /\ world.requirementProfile="PrintedAndExampleFamily052Only" /\ LET card==world.definitions[world.objects[objective].card] sources=={id \in DOMAIN world.objects : world.objects[id].form="Card" /\ world.objects[id].kind="Attachment" /\ world.objects[id].deployed /\ world.objects[id].zone="Play" /\ world.objects[id].activated /\ world.objects[id].face="Up" /\ world.definitions[world.objects[id].card]="Specimen0208" /\ world.objects[id].area="Root" /\ world.objects[id].targetSite=world.objects[objective].targetSite /\ world.objects[objective].deployed /\ world.objects[objective].area="Root"} IN /\ DividendFact1013(card,world.cardFacts) /\ read=[tag |-> "CurrentExampleFamily052ObjectiveRequirement",snapshotId |-> world.id,object |-> objective,sourceIds |-> sources,sourceSHA |-> world.cardFacts["Specimen0208"].sourceSHA, value |-> DividendFacts1013!DividendPrintedFacts1013[card].requirement-Cardinality(sources)] /\ world.requirements[objective]=read.value DividendPhysicalProgress1013(world,host) == {id \in DOMAIN world.objects : world.objects[id].form="Counter" /\ world.objects[id].kind="Progress" /\ world.objects[id].host=host /\ world.objects[id].zone=world.objects[host].zone} DividendBeginSupport1013(begin) == CASE begin.mode="Replay" -> "RequiresAsIfObjectiveCompletionCaptureAdapter" [] begin.mode#"ObjectiveCompletion" -> "NotAnOrdinaryObjectiveCompletion" [] begin.costProfile#"OrdinaryCostlessObjectiveCompletion" -> "RequiresAdditionalCostCapturePointAdapter" [] OTHER -> "SupportedObjectiveCompletionBegin" CaptureDividendBegin1013(world,begin,cardFacts,capture) == /\ begin.id \in DOMAIN world.objectiveCompletionBeginnings /\ begin=world.objectiveCompletionBeginnings[begin.id] /\ DividendBeginSupport1013(begin)="SupportedObjectiveCompletionBegin" /\ begin.actor="SideA" /\ begin.point="ObjectiveCompletionBegins" /\ begin.snapshotId=world.id /\ begin.object \in DOMAIN world.objects /\ world.objects[begin.object].form="Card" /\ world.objects[begin.object].kind="Objective" /\ world.objects[begin.object].zone="Play" /\ world.objects[begin.object].deployed /\ world.objects[begin.object].side="SideA" /\ world.objects[begin.object].card \in DOMAIN world.definitions /\ begin.sourceCard=world.definitions[world.objects[begin.object].card] /\ DividendFact1013(begin.sourceCard,cardFacts) /\ cardFacts=world.cardFacts /\ begin.object \in DOMAIN world.requirements /\ world.requirements[begin.object] \in Int /\ begin.object \in DOMAIN world.consideredProgress /\ world.consideredProgress[begin.object] \in Nat /\ \A id \in DividendPhysicalProgress1013(world,begin.object) : ~world.objects[id].virtual /\ LET fact==DividendFacts1013!DividendPrintedFacts1013[begin.sourceCard] physical==DividendPhysicalProgress1013(world,begin.object) count==Cardinality(physical)+world.consideredProgress[begin.object] IN capture=[tag |-> "DividendObjectiveCompletionBegin",objectiveCompletionId |-> begin.id,beginSnapshot |-> world.id,oldObject |-> begin.object,physical |-> world.objects[begin.object].card, sourceCard |-> begin.sourceCard,sourceSHA |-> fact.sourceSHA,requirement |-> world.requirements[begin.object],progress |-> count, physicalProgress |-> physical,considered |-> world.consideredProgress[begin.object],multiplier |-> fact.multiplier,excess |-> MaxOf(0,count-world.requirements[begin.object]),beforeObjects |-> world.objects] DividendCleanupSupport1013(world,capture) == IF \E id \in DOMAIN world.objects : world.objects[id].host=capture.oldObject /\ world.objects[id].kind#"Progress" THEN "RequiresOtherHostedCleanupAdapter" ELSE IF \E id \in capture.physicalProgress : ~BankPhysicalToken4(world.objects[id]) THEN "RequiresConvertedCounterCleanupAdapter" ELSE "SupportedNativeProgressCleanup" DividendObjectiveCompletionMap1013(objects,old,new) == ReplacementOverlay99(Without101(objects,{old}),[id \in {new} |-> [objects[old] EXCEPT !.zone="SideAObjectiveCompletion",!.deployed=FALSE,!.face="Up",!.loc=0,!.host=0,!.activated=FALSE,!.marks={},!.area="NoValue",!.targetSite="NoValue"]]) MoveDividendObjective1013(world,next,begin,capture,new,moved,binding,eventId,event) == /\ world.outcome="Playing" /\ CaptureDividendBegin1013(world,begin,world.cardFacts,capture) /\ begin.id \in DOMAIN world.dividendCaptures /\ capture=world.dividendCaptures[begin.id] /\ capture.beforeObjects=world.objects /\ DividendCleanupSupport1013(world,capture)="SupportedNativeProgressCleanup" /\ moved=DividendObjectiveCompletionMap1013(world.objects,capture.oldObject,new) /\ CardBatchTransfer8(world.objects,moved,{capture.oldObject},[old \in {capture.oldObject} |-> new],world.usedObjects,"SideAObjectiveCompletion","Up",[old \in {capture.oldObject} |-> 0]) /\ NormalObjectiveCompletionClaimObjectivePost4(moved[new],"SideA","Scored",TRUE) /\ LiabilityMarkerCounterDeparture106(moved,next.objects,capture.physicalProgress,[id \in {} |-> id],world.usedObjects \cup {new},world.printed,world.owners,world.visible,eventId,world.movementHistory,next.movementHistory,{}) /\ eventId \in (Nat \ {0}) \ world.objectiveCompletionEventIds /\ next.id \in (Nat \ {0}) \ world.usedWorlds /\ binding=[tag |-> "DividendObjectiveCompletionBinding",objectiveCompletionId |-> begin.id,oldObject |-> capture.oldObject,newObject |-> new,physical |-> capture.physical,beforeSnapshot |-> world.id,afterSnapshot |-> next.id] /\ event=[id |-> eventId,kind |-> "ObjectivePlacementd",actor |-> "SideA",object |-> new,objectiveCompletionId |-> begin.id,binding |-> binding] /\ next=[world EXCEPT !.id=next.id,!.objects=next.objects,!.movementHistory=next.movementHistory,!.usedObjects=@ \cup {new},!.usedWorlds=@ \cup {next.id}, !.requirements=ReplacementOverlay99(Without101(@,{capture.oldObject}),[id \in {new} |-> DividendFacts1013!DividendPrintedFacts1013[capture.sourceCard].requirement]), !.consideredProgress=ReplacementOverlay99(Without101(@,{capture.oldObject}),[id \in {new} |-> 0]),!.historicalPhysical=ReplacementOverlay99(@,[id \in {capture.oldObject} |-> capture.physical]), !.dividendBindings=ReplacementOverlay99(@,[id \in {begin.id} |-> binding]),!.objectiveCompletionEventIds=@ \cup {eventId},!.objectiveCompletionEvents=ReplacementOverlay99(@,[id \in {eventId} |-> event])] DividendEventSupport1013(event) == IF event.kind#"ObjectivePlacementd" THEN "NotAScoredOccurrence" ELSE IF event.scopeKind="Ability" THEN "RequiresAsIfObjectiveCompletionCaptureAdapter" ELSE "SupportedOrdinaryObjectiveCompletion" DividendBasis1013(world,instance,event,basis) == /\ DividendEventSupport1013(event)="SupportedOrdinaryObjectiveCompletion" /\ instance.member.id \in DOMAIN world.conditionalLedger.instances /\ instance=world.conditionalLedger.instances[instance.member.id] /\ instance.occurrence=event.id /\ instance.definition.source=ObjectAbilitySource9(event.object) /\ instance.definitionCopy.syntax.source=ObjectAbilitySource9(event.object) /\ event.id \in DOMAIN world.objectiveCompletionEvents /\ event.scored=world.objectiveCompletionEvents[event.id] /\ event.object=event.scored.object /\ instance.definition \in DOMAIN world.dividendDefinitions /\ world.dividendDefinitions[instance.definition].definition=instance.definitionCopy /\ "WhenScored" \in ConditionalClasses96(instance.definitionCopy) /\ event.scored.objectiveCompletionId \in DOMAIN world.dividendBindings /\ event.scored.binding=world.dividendBindings[event.scored.objectiveCompletionId] /\ LET binding==world.dividendBindings[event.scored.objectiveCompletionId] capture==world.dividendCaptures[event.scored.objectiveCompletionId] IN /\ capture.tag="DividendObjectiveCompletionBegin" /\ capture.objectiveCompletionId=binding.objectiveCompletionId /\ capture.oldObject=binding.oldObject /\ capture.physical=binding.physical /\ world.dividendDefinitions[instance.definition].card=capture.sourceCard /\ world.dividendDefinitions[instance.definition].sourceSHA=capture.sourceSHA /\ capture.beginSnapshot=binding.beforeSnapshot /\ binding.newObject=event.object /\ event.scored.kind="ObjectivePlacementd" /\ event.scored.actor="SideA" /\ basis=[tag |-> "DividendCapturedBasis",instance |-> instance.member.id,occurrence |-> event.id,objectiveCompletionId |-> capture.objectiveCompletionId,target |-> binding.newObject, physical |-> binding.physical,sourceCard |-> capture.sourceCard,sourceSHA |-> capture.sourceSHA,requirement |-> capture.requirement,progress |-> capture.progress, repetitions |-> capture.excess,multiplier |-> capture.multiplier] OpenDividendPlan1013(world,instance,event,basis,plan) == /\ world.outcome="Playing" /\ instance.status="Resolving" /\ DividendBasis1013(world,instance,event,basis) /\ instance.member.id \notin DOMAIN world.dividendBodyAnchors /\ plan=[tag |-> "DividendInstructionPlan",instance |-> instance.member.id,reference |-> InstructionWindowRef93(OpenInstruction93(instance.definitionCopy.instructions[1],"Ability",instance.member.id,instance.definition.source,"SideAObjectiveCompletion",1,"NoValue",<<"RepeatedObjectivePlacement">>,FALSE)), basis |-> basis,cursor |-> 1,applied |-> {},skipped |-> {},totalPlaced |-> 0,complete |-> FALSE] PublishDividendPlan1013(before,next,instance,event,basis,plan) == /\ OpenDividendPlan1013(before,instance,event,basis,plan) /\ next=[before EXCEPT !.dividendBodyAnchors=ReplacementOverlay99(@,[id \in {plan.instance} |-> [basis |-> basis,reference |-> plan.reference]])] DividendPlanBound1013(world,plan) == /\ plan.instance \in DOMAIN world.dividendBodyAnchors /\ world.dividendBodyAnchors[plan.instance]=[basis |-> plan.basis,reference |-> plan.reference] /\ plan.reference.source=ObjectAbilitySource9(plan.basis.target) DividendEffects1013(plan) == [id \in 1..plan.basis.repetitions |-> [id |-> id,kind |-> "PlaceCounters",actor |-> "SideA",value |-> plan.basis.multiplier,target |-> plan.basis.target,counterKind |-> "Objective",counterKinds |-> {"Objective"}, loadDefinition |-> 0,sourceCard |-> plan.basis.sourceCard,sourceSHA |-> plan.basis.sourceSHA,baseOrigin |-> plan.reference.source,dividendInstance |-> plan.instance,application |-> id]] DividendTargetStatus1013(world,plan) == IF plan.basis.target \notin DOMAIN world.objects THEN "ReferencedObjectGone" ELSE IF world.objects[plan.basis.target].form#"Card" \/ world.objects[plan.basis.target].zone \notin {"Play","SideAObjectiveCompletion","SideBObjectiveCompletion"} THEN "UnhostableReferencedObject" ELSE IF world.objects[plan.basis.target].card#plan.basis.physical THEN "DifferentPhysicalObject" ELSE "SupportedPlacementTarget" DividendApplicationSupport1013(plan,context) == IF context.templates#DividendEffects1013(plan) THEN "RequiresDividendsCompilerAdapter" ELSE IF context.state.effects#DividendEffects1013(plan) \/ context.actualEffects#ActualExpectedEffects99(context.state.effects) THEN "RequiresModifiedPlacementAdapter" ELSE "SupportedOrdinaryPlacementApplications" ApplyDividendPlacement1013(before,after,context,world,next,selected,added,eventId,event) == /\ world.outcome="Playing" /\ DividendPlanBound1013(world,before) /\ ~before.complete /\ before.cursor \in 1..before.basis.repetitions /\ DividendTargetStatus1013(world,before)="SupportedPlacementTarget" /\ context.id=before.instance /\ context.phase="Resolving" /\ context.currentWorld=world.id /\ context.currentRef=before.reference /\ DividendApplicationSupport1013(before,context)="SupportedOrdinaryPlacementApplications" /\ context.actualEffects[before.cursor].value=before.basis.multiplier /\ ExecuteBankHostedCounterInstruction109(context,before.reference,world,before.cursor,world.cardFacts,next.objects,next.loadHistory,next.completedCounterInstructions,selected,added,next.nextCounterObject,eventId,event) /\ next.id \in (Nat \ {0}) \ world.usedWorlds /\ next=[world EXCEPT !.id=next.id,!.objects=next.objects,!.loadHistory=next.loadHistory,!.completedCounterInstructions=next.completedCounterInstructions,!.nextCounterObject=next.nextCounterObject, !.usedObjects=@ \cup DOMAIN added,!.usedWorlds=@ \cup {next.id},!.counterEventIds=@ \cup {eventId},!.dividendPlacementEvents=ReplacementOverlay99(@,[id \in {eventId} |-> event])] /\ after=[before EXCEPT !.cursor=@+1,!.applied=@ \cup {before.cursor},!.totalPlaced=@+before.basis.multiplier] SkipDividendRemainder1013(before,after,world) == /\ world.outcome="Playing" /\ DividendPlanBound1013(world,before) /\ ~before.complete /\ DividendTargetStatus1013(world,before) \in {"ReferencedObjectGone","UnhostableReferencedObject"} /\ after=[before EXCEPT !.skipped=@ \cup (before.cursor..before.basis.repetitions),!.cursor=before.basis.repetitions+1] CompleteDividendPlan1013(before,after,world,completion) == /\ world.outcome="Playing" /\ DividendPlanBound1013(world,before) /\ ~before.complete /\ before.cursor=before.basis.repetitions+1 /\ \A i \in before.applied : <> \in world.completedCounterInstructions /\ before.applied \cap before.skipped={} /\ before.applied \cup before.skipped=1..before.basis.repetitions /\ before.totalPlaced=before.basis.multiplier*Cardinality(before.applied) /\ after=[before EXCEPT !.complete=TRUE] /\ completion=[tag |-> "DividendInstructionComplete",instance |-> before.instance,reference |-> before.reference,objectiveCompletionId |-> before.basis.objectiveCompletionId,applications |-> before.applied, skipped |-> before.skipped,totalPlaced |-> before.totalPlaced,complete |-> TRUE] BidExampleFamily022Ids1014(world,cardFacts) == {id \in DOMAIN world.bidValueRestrictions : LET r==world.bidValueRestrictions[id] IN /\ r.tag="CurrentBidValueRestriction" /\ r.snapshotId=world.id /\ r.forbidden=2 /\ r.ability \in world.activeAbilities /\ world.abilitySources[r.ability]=r.source /\ world.abilityRoles[r.ability]="BidForbidTwo" /\ r.source.kind="Object" /\ r.source.object \in DOMAIN world.objects /\ r.sourceObject=world.objects[r.source.object] /\ r.sourceSHA=cardFacts["Specimen0102"].sourceSHA /\ LinkDefinition107(world,r.sourceObject)="Specimen0102" /\ DefaultActive([r.sourceObject EXCEPT !.card="Specimen0102"],world.gameStarted,cardFacts)} BidExampleFamily022ProjectionValid1014(world,cardFacts) == LET sources=={world.abilitySources[id].object : id \in EscalatingResourceContestRoleIds108(world,"BidForbidTwo","Specimen0102")} IN /\ DOMAIN world.bidValueRestrictions=sources /\ BidExampleFamily022Ids1014(world,cardFacts)=sources /\ \A id \in sources : world.bidValueRestrictions[id].source=ObjectAbilitySource9(id) BidWalletFresh1014(world) == /\ world.bidWalletProfile="PoolFundAndExampleFamily019" /\ LifetimeWorldProjection910(world)=world.lifetimeAuthority.current /\ LifetimeReady910(world.lingering,world.lifetimeAuthority) /\ world.traversal=world.control.traversal /\ BidExampleFamily022ProjectionValid1014(world,world.cardFacts) BidTraversalLive1014(world) == EscalatingResourceContestDuringTraversal108(world) /\ ~world.traversal.complete BidEffectIds1014(world,key,definition) == {id \in ActiveLingeringIds910(world.lingering,world.lifetimeAuthority.current) : LET e==world.lingering.effects[id] IN /\ e.kind="Ordinary" /\ e.choicePolicy="NoValue" /\ e.choiceKey=key /\ e.definitionId=definition /\ e.baseDuration=[kind |-> "Timing",ref |-> TimingRef9("SchemaAtom138",world.traversal.id)] /\ e.durationClass="SchemaAtom138" /\ e.value.traversalId=world.traversal.id} BidHostedPermission1014(world,effectId,cardFacts) == LET e==world.lingering.effects[effectId] host==e.value.host IN /\ BidTraversalLive1014(world) /\ effectId \in BidEffectIds1014(world,"ExampleFamily019Spend",141401) /\ e.source=ObjectAbilitySource9(host) /\ e.target=host /\ e.value.kind="SpendHostedResourceUnits" /\ e.value.player="SideB" /\ host \in DOMAIN world.objects /\ world.objects[host].form="Card" /\ world.objects[host].zone="Play" /\ LinkDefinition107(world,world.objects[host])="Specimen0089" /\ world.controllers[host]="SideB" /\ e.value.sourceSHA=cardFacts["Specimen0089"].sourceSHA BidExampleFamily050Lock1014(world,cardFacts) == BidTraversalLive1014(world) /\ \E id \in BidEffectIds1014(world,"ExampleFamily050SpendLock",141402) : LET e==world.lingering.effects[id] IN /\ e.value.kind="CannotSpendResourceUnits" /\ e.value.player="SideB" /\ e.value.sourceCard="Specimen0205" /\ e.value.sourceSHA=cardFacts["Specimen0205"].sourceSHA BidEligibleResourceUnits1014(world,player,cardFacts) == LET hosted==IF player="SideB" THEN UNION {{id \in DOMAIN world.objects : world.objects[id].form="Counter" /\ world.objects[id].kind="ResourceUnit" /\ ~world.objects[id].virtual /\ world.objects[id].host=world.lingering.effects[e].value.host /\ world.objects[id].zone="Play"} : e \in {e \in DOMAIN world.lingering.effects : BidHostedPermission1014(world,e,cardFacts)}} ELSE {} fund==IF player="SideB" /\ BidTraversalLive1014(world) THEN LiabilityMarkerFundIds106(world.objects) ELSE {} candidates==EscalatingResourceContestPoolIds108(world.objects,player) \cup fund \cup hosted IN {id \in candidates : id \in CheckpointPhysicalIds103(world.objects) /\ SetupMayUseForCost(player,world.objects[id],LiabilityMarkerFundController106(world.objects[id],world.controllers[id]),FALSE)} BidPaymentPlans1014(world,player,amount,cardFacts) == IF amount=0 THEN {{}} ELSE IF amount \notin Nat \/ (player="SideB" /\ BidExampleFamily050Lock1014(world,cardFacts)) \/ (amount=2 /\ BidExampleFamily022Ids1014(world,cardFacts)#{}) THEN {} ELSE {selected \in SUBSET BidEligibleResourceUnits1014(world,player,cardFacts) : Cardinality(selected)=amount} BidPaymentScope1014(world) == [id |-> world.id,objects |-> world.objects,controllers |-> world.controllers,traversal |-> world.traversal,inside |-> world.inside, lingering |-> world.lingering,authority |-> world.lifetimeAuthority,restrictions |-> world.bidValueRestrictions, definitions |-> world.definitions,facts |-> world.cardFacts,abilities |-> world.activeAbilities,abilitySources |-> world.abilitySources,roles |-> world.abilityRoles, printed |-> world.printed,owners |-> world.owners,visible |-> world.visible,usedObjects |-> world.usedObjects,history |-> world.movementHistory] BidInstructionSupport1014(effect) == IF effect.costProfile="UnmodifiedNestedResourceUnits" THEN "Supported" ELSE "RequiresModifiedNestedCostAdapter" BidPacket1014(context,reference,world,operation,cardFacts,packet) == /\ cardFacts=world.cardFacts /\ context.phase="Resolving" /\ context.currentRef=reference /\ context.currentWorld=world.id /\ world.outcome="Playing" /\ context.actualEffects=ActualExpectedEffects99(context.state.effects) /\ operation \in DOMAIN context.actualEffects /\ operation \in DOMAIN context.templates /\ LET e==context.actualEffects[operation] t==context.templates[operation] IN /\ BidInstructionSupport1014(e)="Supported" /\ e.kind \in {"SimultaneousBidComparisonGame","SecretBid"} /\ t.kind=e.kind /\ e.baseOrigin=reference.source /\ e.sourceCard=t.sourceCard /\ e.sourceSHA=t.sourceSHA /\ e.sourceCard \in DOMAIN cardFacts /\ e.sourceSHA=cardFacts[e.sourceCard].sourceSHA /\ e.participants \subseteq SetupPlayers /\ e.participants#{} /\ DOMAIN e.allowed=e.participants /\ \A p \in e.participants : e.allowed[p] \subseteq Nat /\ 0 \in e.allowed[p] /\ (e.kind="SimultaneousBidComparisonGame" => e.participants=SetupPlayers /\ e.allowed=[p \in SetupPlayers |-> {0,1,2}] /\ e.reveal="Immediate") /\ e.rangeMode \in {"SchemaAtom127","AtMost","AnyAffordable"} /\ (e.kind="SimultaneousBidComparisonGame")=(e.rangeMode="SchemaAtom127") /\ e.reveal \in {"Immediate","LaterInstruction"} /\ e.classification \in {"PrintedSimultaneousBidComparison","LegacyPairedSimultaneousBidComparison","GeneralBid"} /\ (e.kind="SimultaneousBidComparisonGame")=(e.classification \in {"PrintedSimultaneousBidComparison","LegacyPairedSimultaneousBidComparison"}) /\ packet=[key |-> <>,reference |-> reference,sourceCard |-> e.sourceCard,sourceSHA |-> e.sourceSHA, participants |-> e.participants,allowed |-> e.allowed,rangeMode |-> e.rangeMode,kind |-> e.kind,reveal |-> e.reveal,classification |-> e.classification] BidInitial1014(id,packet,world) == [tag |-> "OwnedBiddingProcedure",id |-> id,packet |-> packet,caller |-> packet.reference,turnId |-> world.turn.id,active |-> world.turn.owner, phase |-> "Selecting",revealCaller |-> packet.reference,generalStages |-> {},generalCheckpoints |-> {},selections |-> [p \in {} |-> p],revealed |-> {},plans |-> [p \in {} |-> p],choiceOrder |-> <<>>, guess |-> "NoValue",paymentWorld |-> 0,paymentScope |-> [tag |-> "NoValue"],costs |-> [p \in {} |-> p],transactions |-> [p \in {} |-> p],result |-> "Undetermined",paid |-> FALSE,complete |-> FALSE,returned |-> FALSE] BeginBid1014(context,reference,world,operation,cardFacts,id,packet,frame,frames,usedFrames) == /\ BidPacket1014(context,reference,world,operation,cardFacts,packet) /\ BidWalletFresh1014(world) /\ id \in (Nat \ {0}) \ (DOMAIN world.bidFrames \cup world.usedBidFrames) /\ ~\E previous \in DOMAIN world.bidFrames : world.bidFrames[previous].packet.key=packet.key /\ usedFrames=world.usedBidFrames \cup {id} /\ frame=BidInitial1014(id,packet,world) /\ frames=ReplacementOverlay99(world.bidFrames,[key \in {id} |-> frame]) BidCurrent1014(frame,world) == /\ frame.id \in DOMAIN world.bidFrames /\ world.bidFrames[frame.id]=frame /\ ~frame.returned /\ world.outcome="Playing" /\ world.turn.id=frame.turnId /\ world.turn.owner=frame.active /\ world.bidOwners[frame.id]=frame.caller /\ BidWalletFresh1014(world) SelectSecretBid1014(before,after,world,player,amount,cardFacts) == /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase="Selecting" /\ player \in before.packet.participants \ DOMAIN before.selections /\ (IF before.packet.rangeMode="AnyAffordable" THEN amount \in Nat ELSE amount \in before.packet.allowed[player]) /\ BidPaymentPlans1014(world,player,amount,cardFacts)#{} /\ LET selections==ReplacementOverlay99(before.selections,[p \in {player} |-> amount]) IN after=[before EXCEPT !.selections=selections,!.phase=IF DOMAIN selections=before.packet.participants THEN IF before.packet.reveal="Immediate" THEN "RevealDue" ELSE "WaitingReveal" ELSE "Selecting"] BidView1014(frame,player) == [id |-> frame.id,phase |-> frame.phase,committed |-> DOMAIN frame.selections,guess |-> frame.guess, knownValues |-> [p \in {p \in DOMAIN frame.selections : p=player \/ p \in frame.revealed} |-> frame.selections[p]], sourceChoices |-> IF frame.revealed=frame.packet.participants THEN frame.plans ELSE [p \in {} |-> p]] RecordBidGuess1014(before,after,world,player,guess,continuation) == /\ BidCurrent1014(before,world) /\ before.phase="WaitingReveal" /\ before.packet.participants={"SideB"} /\ player="SideA" /\ before.guess="NoValue" /\ "Selection" \in before.generalStages /\ guess \in {"Even","Odd"} /\ continuation=world.bidContinuations[before.id] /\ continuation.tag="AuthorizedBidGuess" /\ continuation.bidId=before.id /\ continuation.instance=before.caller.abilityInstance /\ continuation.player=player /\ continuation.snapshotId=world.id /\ after=[before EXCEPT !.guess=guess] GeneralBidInstructionCheckpoint1014(before,after,world,checkpoint,ledger) == /\ BidCurrent1014(before,world) /\ before.phase="WaitingReveal" /\ ~before.paid /\ checkpoint.id \in DOMAIN world.checkpoints /\ world.checkpoints[checkpoint.id]=checkpoint /\ world.conditionalLedger=ledger /\ LET stage==IF before.guess="NoValue" THEN "Selection" ELSE "Guess" IN /\ checkpoint.caller=[kind |-> "GeneralBiddingInstructionEnd",bidId |-> before.id,caller |-> before.caller,stage |-> stage] /\ stage \notin before.generalStages /\ CheckpointDrained103(checkpoint,ledger,<<>>) /\ after=[before EXCEPT !.generalStages=@ \cup {stage},!.generalCheckpoints=@ \cup {checkpoint.id}] BidRevealSupport1014(frame,world,cardFacts) == IF \A p \in frame.packet.participants : BidPaymentPlans1014(world,p,frame.selections[p],cardFacts)#{} THEN "OrdinaryFullPayment" ELSE "RequiresChangedPayabilityAdapter" BidNestedSpecification1014(frame,player) == <<[category |-> "Nested",kind |-> "ResourceUnit",amount |-> frame.selections[player],eventId |-> <>]>> BidNestedCost1014(frame,world,player,transaction) == [tag |-> "BidNestedResourceUnitCost",id |-> transaction,transaction |-> transaction,instance |-> frame.caller.abilityInstance,instruction |-> frame.revealCaller, source |-> frame.caller.source,payer |-> player,specification |-> BidNestedSpecification1014(frame,player),bidId |-> frame.id, sourceRule |-> "ProcedureCode3b2e1996810a",snapshotId |-> world.id,amount |-> frame.selections[player],status |-> "Paying",optionalInterrupts |-> {}, resourceUnitHosts |-> [id \in DOMAIN world.objects |-> world.objects[id].host]] BidReservedCosts1014(world) == world.usedCostTransactions \cup UNION {{world.bidFrames[id].transactions[p] : p \in DOMAIN world.bidFrames[id].transactions} : id \in DOMAIN world.bidFrames} RevealBids1014(before,after,world,cardFacts,transactions,continuation) == /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase \in {"RevealDue","WaitingReveal"} /\ DOMAIN before.selections=before.packet.participants /\ BidRevealSupport1014(before,world,cardFacts)="OrdinaryFullPayment" /\ continuation=world.bidContinuations[before.id] /\ continuation.tag="AuthorizedBidReveal" /\ continuation.bidId=before.id /\ continuation.instance=before.caller.abilityInstance /\ continuation.snapshotId=world.id /\ continuation.source=before.caller.source /\ (before.phase="RevealDue" => continuation.instruction=before.caller) /\ (before.phase="WaitingReveal" => "Selection" \in before.generalStages /\ continuation.instruction#before.caller) /\ (before.packet.sourceCard \in {"Specimen0191","Specimen0200"} => before.guess#"NoValue" /\ "Guess" \in before.generalStages) /\ DOMAIN transactions=before.packet.participants /\ \A p \in DOMAIN transactions : transactions[p] \in (Nat \ {0}) \ BidReservedCosts1014(world) /\ \A p,q \in DOMAIN transactions : p#q => transactions[p]#transactions[q] /\ after=[before EXCEPT !.phase="ChoosePayment",!.revealed=before.packet.participants,!.paymentWorld=world.id,!.paymentScope=BidPaymentScope1014(world), !.transactions=transactions,!.revealCaller=continuation.instruction,!.costs=[p \in before.packet.participants |-> BidNestedCost1014([before EXCEPT !.revealCaller=continuation.instruction],world,p,transactions[p])]] BidMultipleChoicePlayers1014(frame,world,cardFacts) == {p \in frame.packet.participants : Cardinality(BidPaymentPlans1014(world,p,frame.selections[p],cardFacts))>1} ChooseBidPaymentSources1014(before,after,world,player,selected,cardFacts) == /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase="ChoosePayment" /\ before.revealed=before.packet.participants /\ world.id=before.paymentWorld /\ BidPaymentScope1014(world)=before.paymentScope /\ player \in before.packet.participants \ DOMAIN before.plans /\ selected \in BidPaymentPlans1014(world,player,before.selections[player],cardFacts) /\ (BidMultipleChoicePlayers1014(before,world,cardFacts)=SetupPlayers /\ DOMAIN before.plans={} => player=before.active) /\ after=[before EXCEPT !.plans=ReplacementOverlay99(@,[p \in {player} |-> selected]),!.choiceOrder=Append(@,player)] BidCompletedCost1014(cost,selected) == [tag |-> "CompletedCostTransaction",id |-> cost.id,instance |-> cost.instance,instruction |-> cost.instruction,source |-> cost.source,payer |-> cost.payer, specification |-> cost.specification,allCostsPaid |-> TRUE,announced |-> TRUE,selected |-> selected,bidId |-> cost.bidId, permissionSources |-> {ObjectAbilitySource9(cost.resourceUnitHosts[id]) : id \in {id \in selected : cost.resourceUnitHosts[id]#0}}] BidPaidFrame1014(frame) == [frame EXCEPT !.phase="PaidCheckpointDue",!.paid=TRUE, !.result=IF frame.packet.kind="SimultaneousBidComparisonGame" THEN IF frame.selections["SideA"]=frame.selections["SideB"] THEN "Equal" ELSE "Different" ELSE "SingleBid"] CommitBidPayments1014(before,after,world,cardFacts,afterObjects,successors,batchId,afterHistory,events,receipts) == /\ cardFacts=world.cardFacts /\ BidCurrent1014(before,world) /\ before.phase="ChoosePayment" /\ world.id=before.paymentWorld /\ BidPaymentScope1014(world)=before.paymentScope /\ before.revealed=before.packet.participants /\ DOMAIN before.plans=before.packet.participants /\ \A p \in before.packet.participants : /\ before.plans[p] \in BidPaymentPlans1014(world,p,before.selections[p],cardFacts) /\ before.costs[p]=BidNestedCost1014(before,world,p,before.transactions[p]) /\ before.costs[p].optionalInterrupts={} /\ EffectiveCosts(before.costs[p].specification,{},FALSE,FALSE)=BidNestedSpecification1014(before,p) /\ AlternatePaymentPreservesValue(before.selections[p],Cardinality(before.plans[p])) /\ \A p,q \in before.packet.participants : p#q => before.plans[p] \cap before.plans[q]={} /\ LiabilityMarkerCounterDeparture106(world.objects,afterObjects,UNION {before.plans[p] : p \in before.packet.participants},successors,world.usedObjects, world.printed,world.owners,world.visible,batchId,world.movementHistory,afterHistory,events) /\ receipts=[p \in before.packet.participants |-> BidCompletedCost1014(before.costs[p],before.plans[p])] /\ after=BidPaidFrame1014(before) BidPaymentEvent1014(frame,world,eventId,snapshot) == [id |-> eventId,kind |-> "BidsRevealedAndPaid",bidId |-> frame.id,source |-> frame.caller.source,sourceCard |-> frame.packet.sourceCard, sourceSHA |-> frame.packet.sourceSHA,participants |-> frame.packet.participants,amounts |-> frame.selections,result |-> frame.result,turnId |-> frame.turnId, duringTraversal |-> BidTraversalLive1014(world),serial |-> world.bidEventSerial+1,reference |-> frame.caller,snapshot |-> snapshot,transactionIds |-> frame.transactions] BidPublish1014(frame,world,afterWorld,cardFacts,afterObjects,successors,batchId,history,events,receipts,event,eventId,snapshot) == /\ frame.phase="PaidCheckpointDue" /\ frame.paid /\ frame.id \in DOMAIN world.bidFrames /\ world.bidFrames[frame.id].phase="ChoosePayment" /\ CommitBidPayments1014(world.bidFrames[frame.id],frame,world,cardFacts,afterObjects,successors,batchId,history,events,receipts) /\ snapshot.objects=afterObjects /\ snapshot.id \in (Nat \ {0}) \ world.usedWorlds /\ event=BidPaymentEvent1014(frame,world,eventId,snapshot) /\ eventId \in (Nat \ {0}) \ DOMAIN world.bidEvents /\ afterWorld=[world EXCEPT !.id=snapshot.id,!.objects=afterObjects,!.movementHistory=history,!.bidFrames[frame.id]=frame, !.usedWorlds=@ \cup {snapshot.id},!.usedObjects=@ \cup DOMAIN afterObjects, !.controllers=[id \in DOMAIN afterObjects |-> IF id \in DOMAIN world.controllers THEN world.controllers[id] ELSE world.owners[afterObjects[id].card]], !.bidEventSerial=@+1,!.usedCostTransactions=@ \cup {frame.transactions[p] : p \in frame.packet.participants},!.bidCosts=ReplacementOverlay99(@,[id \in {frame.transactions[p] : p \in frame.packet.participants} |-> receipts[CHOOSE p \in frame.packet.participants : frame.transactions[p]=id]]),!.bidEvents=ReplacementOverlay99(@,[id \in {eventId} |-> event])] BidCheckpointSite1014(frame) == [kind |-> "BidBatchPaymentCheckpoint",bidId |-> frame.id,caller |-> frame.caller,paymentInstruction |-> frame.revealCaller,transactions |-> frame.transactions,cause |-> "CostPaid",simultaneousBidComparison |-> frame.packet.kind="SimultaneousBidComparisonGame"] BidCheckpointReady1014(frame,world,checkpoint,ledger) == /\ world.outcome="Playing" /\ world.bidOwners[frame.id]=frame.caller /\ frame.phase="PaidCheckpointDue" /\ frame.paid /\ frame.id \in DOMAIN world.bidFrames /\ world.bidFrames[frame.id]=frame /\ checkpoint.id \in DOMAIN world.checkpoints /\ world.checkpoints[checkpoint.id]=checkpoint /\ checkpoint.site=BidCheckpointSite1014(frame) /\ checkpoint.caller=BidCheckpointSite1014(frame) /\ checkpoint.returned /\ CheckpointDrained103(checkpoint,ledger,<<>>) /\ world.conditionalLedger=ledger /\ \A p \in frame.packet.participants : /\ frame.transactions[p] \in DOMAIN world.bidCosts /\ world.bidCosts[frame.transactions[p]]=BidCompletedCost1014(frame.costs[p],frame.plans[p]) /\ {e \in DOMAIN world.bidEvents : world.bidEvents[e].bidId=frame.id}#{} FinishBid1014(before,after,world,checkpoint,ledger,completion) == /\ BidCheckpointReady1014(before,world,checkpoint,ledger) /\ completion=[tag |-> "BiddingInstructionComplete",bidId |-> before.id,caller |-> before.revealCaller,result |-> before.result,checkpoint |-> checkpoint.id,paid |-> TRUE] /\ after=[before EXCEPT !.phase="Complete",!.complete=TRUE] ReturnBid1014(before,after,completion,caller) == /\ completion.tag="BiddingInstructionComplete" /\ completion.result=before.result /\ before.complete /\ ~before.returned /\ caller=before.revealCaller /\ completion.bidId=before.id /\ completion.caller=caller /\ completion.paid /\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE] BidObserverCondition1014(rule,event,priorEvents,cardFacts) == CASE rule="BothReveal" -> event.participants=SetupPlayers [] rule="FirstReveal" -> "SideA" \in event.participants /\ ~\E id \in DOMAIN priorEvents : priorEvents[id].turnId=event.turnId /\ "SideA" \in priorEvents[id].participants [] rule="SideBSpentFromSideATraversalAbility" -> "SideB" \in event.participants /\ event.amounts["SideB"]>0 /\ event.duringTraversal /\ event.sourceCard \in DOMAIN cardFacts /\ cardFacts[event.sourceCard].side="SideA" [] OTHER -> FALSE BidPublished1014(event,world) == /\ event.id \in DOMAIN world.bidEvents /\ world.bidEvents[event.id]=event /\ event.bidId \in DOMAIN world.bidFrames /\ world.bidFrames[event.bidId].paid /\ LET f==world.bidFrames[event.bidId] IN /\ event.kind="BidsRevealedAndPaid" /\ event.source=f.caller.source /\ event.sourceCard=f.packet.sourceCard /\ event.sourceSHA=f.packet.sourceSHA /\ event.reference=f.caller /\ event.turnId=f.turnId /\ event.amounts=f.selections /\ event.participants=f.packet.participants /\ event.transactionIds=f.transactions /\ event.result=f.result /\ \A p \in event.participants : f.transactions[p] \in DOMAIN world.bidCosts /\ world.bidCosts[f.transactions[p]]=BidCompletedCost1014(f.costs[p],f.plans[p]) BidObserverRule1014(card) == CASE card \in {"Specimen0161","Specimen0096"} -> "BothReveal" [] card="Specimen0113" -> "FirstReveal" [] card="Specimen0097" -> "SideBSpentFromSideATraversalAbility" [] OTHER -> "UnsupportedObserver" PublishBidOccurrence1014(world,event,definition,card,priorEvents,occurrence,cardFacts) == /\ cardFacts=world.cardFacts /\ BidPublished1014(event,world) /\ card \in DOMAIN cardFacts /\ BidObserverRule1014(card)#"UnsupportedObserver" /\ priorEvents=[id \in {id \in DOMAIN world.bidEvents : world.bidEvents[id].serial world.bidEvents[id]] /\ definition.syntax.source.object \in DOMAIN world.objects /\ LinkDefinition107(world,world.objects[definition.syntax.source.object])=card /\ ConditionalDefinitionValid96(definition) /\ definition.primaryKind="Trigger" /\ definition.trigger.kinds={"BidsRevealedAndPaid"} /\ definition.triggerRequirements={} /\ BidObserverCondition1014(BidObserverRule1014(card),event,priorEvents,cardFacts) /\ occurrence.kind="BidsRevealedAndPaid" /\ occurrence.effectId=event.id /\ occurrence.snapshot=event.snapshot /\ occurrence.bidId=event.bidId /\ occurrence.amounts=event.amounts /\ occurrence.result=event.result /\ occurrence.scopeKind="Ability" /\ occurrence.scopeDefinition=ConditionalKey96(definition) BidGuessCorrect1014(frame) == frame.packet.participants={"SideB"} /\ frame.guess \in {"Even","Odd"} /\ frame.paid /\ IF frame.guess="Even" THEN frame.selections["SideB"] % 2=0 ELSE frame.selections["SideB"] % 2=1 =============================================================================