---------------- MODULE PersistentChecksMC ---------------- EXTENDS AdditionalContracts,SpecimenFactsA Empty9 == [id \in {} |-> id] CardObject9(card,zone,deployed,face) == [card |-> card,form |-> "Card",kind |-> CardFacts9[card].kind,side |-> CardFacts9[card].side, zone |-> zone,loc |-> zone,host |-> 0,deployed |-> deployed,face |-> face,activated |-> FALSE, area |-> "NoValue",targetSite |-> "NoValue",targetSiteKind |-> "NoValue",position |-> "NoValue",marks |-> {}] TurnFixture92(player) == [OpenTurn5(player,1,[p \in SetupPlayers |-> 0]) EXCEPT !.phase = "NeutralValue00001"] TraversalFixture92(step) == [OpenTraversal6(2,20,"action") EXCEPT !.formalBegun = TRUE,!.phase = TraversalStepInfo6(step).phase,!.step = step, !.attacked = "SchemaAtom082",!.position = "outer"] UnitFixture93(id,category,subtype,primary) == TextUnit93(id,category,subtype,primary,0) InstructionFixture93 == UnitFixture93(10,"Instruction","NoValue",FALSE) DeclarationFixture93 == UnitFixture93(10,"Declaration","NoValue",FALSE) SyntaxFixture93(id,kind,side,cardKind,units) == [id |-> id,kind |-> kind,side |-> side,controller |-> side,cardKind |-> cardKind,source |-> ObjectAbilitySource9(1), units |-> units,arrowAfterFlags |-> TRUE,barrierInstructionPrefix |-> kind="BarrierInstruction", paidPrefix |-> [present |-> kind="Paid",bold |-> TRUE,colon |-> TRUE]] ConditionalDefinitionFixture96(id,card,primary,eventKind,subject,actor,side) == LET syntax == SyntaxFixture93(id,"Conditional",CardFacts9[card].side,CardFacts9[card].kind, <>) IN [syntax |-> syntax,activity |-> AbilityDefinition9(id,"Conditional",syntax.source,"Printed"), primaryKind |-> primary,primaryCondition |-> 1,instructions |-> <<700>>,instructionHasWould |-> FALSE, trigger |-> [kinds |-> {eventKind},subject |-> subject,actor |-> actor,side |-> side],triggerRequirements |-> {}, effectChoices |-> {{1}},optionalParts |-> {},partsByInstruction |-> [i \in {700} |-> {1}],delayedEffect |-> 0,thisTraversal |-> FALSE] ConditionalCardActivityFixture96(o) == IF o.form="Counter" THEN o.kind="SchemaAtom043" ELSE o.zone \in {"SideAObjectiveCompletion","SideBObjectiveCompletion","SideAProfile","SideBProfile"} \/ (o.zone="Play" /\ o.deployed /\ (IF o.side="SideB" THEN o.face="Up" ELSE ActivationStatus8(o)="ItemActivated")) ConditionalSnapshotFixture96(id,checkpointId,point,definitions,objects) == [id |-> id,checkpointId |-> checkpointId,point |-> point,definitions |-> definitions,objects |-> objects, present |-> {definitions[key].syntax.id : key \in DOMAIN definitions}, ordinaryActivity |-> [key \in DOMAIN definitions |-> IF definitions[key].syntax.source.kind="Object" THEN IF definitions[key].syntax.source.object \in DOMAIN objects THEN ConditionalCardActivityFixture96(objects[definitions[key].syntax.source.object]) ELSE FALSE ELSE FALSE], cardActivity |-> [object \in DOMAIN objects |-> ConditionalCardActivityFixture96(objects[object])], activationEpoch |-> [key \in DOMAIN definitions |-> 0],activationSerial |-> 0,activity |-> ActivityContext9,points |-> [p \in SetupPlayers |-> 0], progress |-> [object \in DOMAIN objects |-> 0],link |-> [p \in SetupPlayers |-> IF p="SideB" THEN 1 ELSE 0], exposureMarkers |-> [p \in SetupPlayers |-> 0],objectiveCompletionEvents |-> {},usedObjects |-> DOMAIN objects,holds |-> Empty9,effects |-> Empty9] ConditionalEventFixture96(id,kind,object,actor,side,snapshot,effectId) == [id |-> id,kind |-> kind,object |-> object,actor |-> actor,side |-> side,snapshot |-> snapshot,effectId |-> effectId, movement |-> [tag |-> "NoValue",oldObject |-> 0,newObject |-> 0,beforeSnapshot |-> snapshot], scopeKind |-> "Global",scopeDefinition |-> [ability |-> 0,source |-> RuleAbilitySource9("NoValue")],structure |-> NoTimingRef9, step |-> "NoValue",traversal |-> NoTraversal6,siteInspection |-> [traversalId |-> 0,origin |-> "NoValue"]] ConditionalTriggerReceiptFixture96(d,event) == [tag |-> "ConditionalTriggerStipulations",ability |-> d.syntax.id,source |-> d.syntax.source,occurrence |-> event.id, snapshotId |-> event.snapshot.id,results |-> [id \in d.triggerRequirements |-> TRUE]] ConditionalCheckpointFixture96(before,id,beginSnapshot,processingSnapshot,events) == [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> id,previousCheckpoint |-> before.lastCheckpoint,serial |-> before.serial+1, previousSnapshot |-> before.lastSnapshot,beginSnapshot |-> beginSnapshot,processingSnapshot |-> processingSnapshot, stepSerial |-> before.stepSerial,occurrences |-> events,caller |-> [kind |-> "Observation"]] ConditionalCommittedFixture96(before,definitions,cp,allocation,bindings,holds) == LET stable == ConditionalActivityLedger96(before,definitions,cp.processingSnapshot) ids == {allocation[key] : key \in DOMAIN allocation} IN [stable EXCEPT !.activationEpoch=cp.processingSnapshot.activationEpoch,!.lastCheckpoint=cp.id,!.checkpointIds=@ \cup {cp.id}, !.checkpoints=[id \in DOMAIN @ \cup {cp.id} |-> IF id=cp.id THEN [caller |-> cp.caller] ELSE @[id]],!.serial=cp.serial,!.lastSnapshot=cp.processingSnapshot, !.processed=@ \cup DOMAIN cp.occurrences,!.holds=[key \in DOMAIN @ \cup DOMAIN holds |-> IF key \in DOMAIN holds THEN holds[key] ELSE @[key]], !.instances=[id \in DOMAIN @ \cup ids |-> IF id \in ids THEN LET key == CHOOSE k \in DOMAIN allocation : allocation[k]=id IN NewConditionalInstance96(id,definitions[key.definition],cp,key.occurrence,bindings[key].windowId,bindings[key].group) ELSE @[id]]] LexicalMentionFixture99(d,word,unit,role) == [word |-> word,unit |-> unit,owner |-> AbilityKey99(d),role |-> role] LexicalReceiptFixture99(d,card,mentions,facts) == [tag |-> "NormalizedAbilityLexemes",definition |-> d,source |-> d.syntax.source, card |-> card,sourceSHA |-> facts[card].sourceSHA,mentions |-> mentions, origin |-> [tag |-> "AbilityTextOrigin",recipientSource |-> d.syntax.source,provider |-> d.activity.provider, card |-> card,sourceSHA |-> facts[card].sourceSHA,rule |-> "NoValue"]] LexicalSingleFixture99(d,card,word,unit,role,facts) == LexicalReceiptFixture99(d,card,[id \in {1} |-> LexicalMentionFixture99(d,word,unit,role)],facts) LifetimeWorldFixture910 == LET e == [OpenEncounter6(20,2,0,TRUE,700,<<>>) EXCEPT !.stage="Paid"] IN [id |-> 1,objects |-> [id \in {1,2,3} |-> IF id=1 THEN CardObject9("Specimen0088","Play",TRUE,"Up") ELSE IF id=2 THEN [CardObject9("NeutralValue00016","Play",TRUE,"Up") EXCEPT !.activated=TRUE] ELSE [CardObject9("Specimen0100","Play",TRUE,"Up") EXCEPT !.host=1]], gameStarted |-> TRUE,cardFacts |-> CardFacts9,playActivated |-> {}, turn |-> OpenTurn5("SideB",10,[p \in SetupPlayers |-> 0]),turnPhase |-> [id |-> 11,ended |-> FALSE], control |-> [traversal |-> NoTraversal6,phaseEndedIds |-> {}],encounters |-> [id \in {20} |-> e],currentEncounter |-> 20, siteInspections |-> Empty9,itemInspections |-> Empty9,finishedInstances |-> {},finishedDelayedEffects |-> {},statedDurations |-> Empty9, durationComparisons |-> Empty9,extenders |-> Empty9,present |-> {},activity |-> ActivityContext9,points |-> [p \in SetupPlayers |-> 0],barrierResponseCards |-> {1}] ObservedWithFrontier910(registry,a,position) == ReplacementOverlay99(registry,[frontier |-> LifetimeFrontier910(a,position)]) PersistentExampleFamily002DefinitionFixture912 == LET d == ConditionalDefinitionFixture96(19000,"Specimen0010","Trigger","TraversalEnds","SchemaAtom016","SideB","SideB") IN [d EXCEPT !.syntax.units= <> \o @,!.triggerRequirements={2}] PersistentDoppelDefinitionFixture912 == LET d == ConditionalDefinitionFixture96(19001,"Specimen0076","Trigger","TraversalEnds","SchemaAtom016","SideB","SideB") IN [d EXCEPT !.syntax.source=ObjectAbilitySource9(2),!.activity.source=ObjectAbilitySource9(2), !.syntax.units= <> \o @,!.triggerRequirements={3},!.optionalParts={1}] PersistentBirthProposedFixture912(registry,inventory,trash,effectIds,world) == LET cohort == PersistentBirthCohort912(inventory,world) records == [key \in cohort |-> PersistentRecord912(inventory.definitions[key],inventory.lexemes[key],effectIds[key],trash,world)] effects == [id \in {effectIds[key] : key \in cohort} |-> LET key == CHOOSE key \in cohort : effectIds[key]=id IN PersistentEffect912(id,inventory.definitions[key],inventory.lexemes[key],trash,trash.itemInspection.traversalId,world)] IN [registry EXCEPT !.persistent=ReplacementOverlay99(@,records),!.effects=ReplacementOverlay99(@,effects), !.usedEffects=@ \cup DOMAIN effects,!.creations=@ \cup {effects[id].creation : id \in DOMAIN effects},!.persistentRetireIds=@ \cup {trash.id}] PersistentBirthForSourceFixture912(withTraversal,sourceCard,d,doppelDeployed) == LET dg == PersistentDoppelDefinitionFixture912 key == AbilityKey99(d) definitions == [k \in (IF d.syntax.kind="Conditional" THEN {key,ConditionalKey96(dg)} ELSE {ConditionalKey96(dg)}) |-> IF k=key THEN d ELSE dg] sourceLex == LexicalSingleFixture99(d,sourceCard,IF d.syntax.kind="Conditional" THEN "whenever" ELSE "pay",2, IF d.syntax.kind="Conditional" THEN "ActualOccurrenceTrigger" ELSE "StaticDeclaration",CardFacts9) lexemes == [k \in DOMAIN definitions |-> IF k=key THEN sourceLex ELSE LexicalSingleFixture99(dg,"Specimen0076","when",2,"ActualOccurrenceTrigger",CardFacts9)] objects == [id \in {1,2} |-> IF id=1 THEN [CardObject9(sourceCard,"Play",TRUE,"Up") EXCEPT !.activated=TRUE, !.targetSite="SchemaAtom082",!.targetSiteKind="SchemaAtom033",!.area="Root",!.loc= <<"Root","SchemaAtom082">>] ELSE CardObject9("Specimen0076",IF doppelDeployed THEN "Play" ELSE "SideBDiscard",doppelDeployed,"Up")] traversal == IF withTraversal THEN [TraversalFixture92("ProcedureCoded75d879e00ff") EXCEPT !.reachedSuccess=TRUE,!.successful=TRUE,!.position="NoValue"] ELSE NoTraversal6 itemInspection == [OpenItemInspection7(200,1,objects[1],traversal.id,201,"siteInspection",{}) EXCEPT !.active=TRUE,!.beginMet=TRUE,!.step="ProcedureCode1dd0e8f05be2"] beforeWorld == [LifetimeWorldFixture910 EXCEPT !.objects=objects,!.present={19000,19001},!.turn=TurnFixture92("SideB"), !.control=[traversal |-> traversal,phaseEndedIds |-> {}],!.encounters=Empty9,!.currentEncounter=0,!.barrierResponseCards={}, !.itemInspections=[id \in {200} |-> itemInspection]] beforeAuthority == NewLifetimeAuthority910(beforeWorld) beforeRegistry == NewPersistentRegistry912(ObservedWithFrontier910(NewLingeringRegistry910,beforeAuthority,1)) beforeSnapshot == [ConditionalSnapshotFixture96(1,0,"BeforeItemInspectionRetire",definitions,objects) EXCEPT !.present=beforeWorld.present] beforeLedger == NewConditionalLedger96(beforeSnapshot) inventory == [tag |-> "AuthoritativeSourceAbilityInventory",worldId |-> 1,source |-> d.syntax.source, card |-> sourceCard,sourceSHA |-> CardFacts9[sourceCard].sourceSHA, definitions |-> [k \in {key} |-> d],lexemes |-> [k \in {key} |-> sourceLex]] movement == [tag |-> "CardMovement",kind |-> "Retire",id |-> 210,disposition |-> "Complete",sources |-> {1},successors |-> [id \in {1} |-> 3]] trashEvent == MovementEvent8(210,"Retire",{1}) trash == [tag |-> "ActualSideBItemInspectionRetire",id |-> 210,actor |-> "SideB",source |-> 1,successor |-> 3,itemInspection |-> itemInspection,movement |-> movement, historyBefore |-> Empty9,historyAfter |-> [id \in {210} |-> trashEvent],events |-> {trashEvent}] effectIds == [k \in {key} |-> 55000] created == PersistentBirthProposedFixture912(beforeRegistry,inventory,trash,effectIds,beforeWorld) afterObjects == [id \in {2,3} |-> IF id=2 THEN objects[2] ELSE [objects[1] EXCEPT !.zone="SideADiscard",!.loc="SideADiscard", !.deployed=FALSE,!.activated=FALSE,!.face="Up",!.host=0,!.marks={}]] base == [beforeWorld EXCEPT !.id=2,!.objects=afterObjects,!.present={19001}] afterWorld == PersistentWorld912(base,created) execution == [tag |-> "ActualObjectTransition",id |-> 210,snapshotId |-> 2,source |-> RuleAbilitySource9("ProcedureCode17f2a65162fb"),trash |-> trash] afterAuthority == LifetimeAuthorityAfter910(beforeAuthority,LifetimeKernelTransition910(beforeWorld,afterWorld,execution)) afterRegistry == [created EXCEPT !.frontier=LifetimeFrontier910(afterAuthority,2)] afterLedger == IF withTraversal \/ key \notin DOMAIN beforeLedger.activationEpoch THEN beforeLedger ELSE [beforeLedger EXCEPT !.activationEpoch[key]=1,!.activationSerial=1] afterSnapshot == [ConditionalSnapshotFixture96(2,0,"AfterItemInspectionRetire",definitions,afterObjects) EXCEPT !.present=afterWorld.present,!.activity=afterWorld.activity,!.usedObjects={1,2,3},!.activationEpoch=afterLedger.activationEpoch, !.activationSerial=afterLedger.activationSerial] IN [d |-> d,dg |-> dg,key |-> key,definitions |-> definitions,lexemes |-> lexemes,objects |-> objects,traversal |-> traversal,itemInspection |-> itemInspection, beforeWorld |-> beforeWorld,beforeAuthority |-> beforeAuthority,beforeRegistry |-> beforeRegistry,beforeSnapshot |-> beforeSnapshot,beforeLedger |-> beforeLedger, inventory |-> inventory,trash |-> trash,effectIds |-> effectIds,created |-> created,afterObjects |-> afterObjects,afterWorld |-> afterWorld, execution |-> execution,afterAuthority |-> afterAuthority,afterRegistry |-> afterRegistry,afterLedger |-> afterLedger,afterSnapshot |-> afterSnapshot] PersistentBirthFixture912(withTraversal) == PersistentBirthForSourceFixture912(withTraversal,"Specimen0010",PersistentExampleFamily002DefinitionFixture912,TRUE) PersistentSpecimen0198DefinitionFixture912 == LET syntax == SyntaxFixture93(19000,"Static","SideA","Attachment",<>) IN [syntax |-> syntax,activity |-> AbilityDefinition9(19000,"Static",syntax.source,"Printed"),instructions |-> <<>>] PersistentBirthValid912(f) == CreatePersistentOnRetire912(f.beforeRegistry,f.afterRegistry,f.beforeLedger,f.afterLedger,<<>>,<<>>,f.beforeSnapshot,f.afterSnapshot, f.inventory,f.trash,f.effectIds,{1,2},f.beforeAuthority,f.afterAuthority,CardFacts9) PersistentTraversalSnapshotFixture912(f,w,r,l,checkpoint,point) == LingeringConditionalSnapshot910([f.afterSnapshot EXCEPT !.id=w.id,!.checkpointId=checkpoint,!.point=point, !.objects=w.objects,!.present=w.present,!.activity=w.activity,!.activationEpoch=l.activationEpoch, !.activationSerial=l.activationSerial],r,l,w) PersistentTraversalStateFixture912(f,r,l,w,a,stack) == [f |-> f,r |-> r,l |-> l,w |-> w,a |-> a,stack |-> stack, s |-> PersistentTraversalSnapshotFixture912(f,w,r,l,l.lastCheckpoint,"PersistentCurrent")] PersistentTraversalMoveFixture912(b,base,execution) == LET w == PersistentWorld912(base,b.r) a == LifetimeAuthorityAfter910(b.a,LifetimeKernelTransition910(b.w,w,execution)) r == [b.r EXCEPT !.effects=ObserveLingeringEffects910(@,w),!.frontier=LifetimeFrontier910(a,Len(a.order))] IN PersistentTraversalStateFixture912(b.f,r,b.l,w,a,b.stack) PersistentTraversalMoveValid912(b,a,base,execution) == ObservePersistentKernel912(b.r,a.r,b.l,a.l,b.stack,a.stack,b.s,a.s,base,execution,b.a,a.a) PersistentTraversalCPFixture912(b,caller,events) == LET id == b.l.lastCheckpoint+1 begin == [b.s EXCEPT !.checkpointId=id,!.point="CheckpointBeginning"] current == [begin EXCEPT !.point="ProcedureCodee605a78f5d5e"] IN [ConditionalCheckpointFixture96(b.l,id,begin,current,events) EXCEPT !.caller=caller] PersistentTraversalEndFixture912(f,targetSiteMatches) == LET initial == PersistentTraversalStateFixture912(f,f.afterRegistry,f.afterLedger,f.afterWorld,f.afterAuthority,<<>>) preTraversal == [f.traversal EXCEPT !.phase="TraversalEnds",!.step="ProcedureCode9606a4cd52b4",!.ending=TRUE,!.phaseId=21,!.usedPhaseIds=@ \cup {21}] preEnd == [traversal |-> preTraversal,phaseEndedIds |-> {},windows |-> <<>>,windowsDone |-> TRUE, fundReturned |-> TRUE,resultDeclared |-> TRUE,returned |-> FALSE] beforeBase == [initial.w EXCEPT !.id=3,!.control=[traversal |-> preTraversal,phaseEndedIds |-> {}]] beforeExecution == [tag |-> "ActualTimingTransition",id |-> 19500,snapshotId |-> 3,source |-> RuleAbilitySource9("NormalizedPriorTraversalEndSteps")] before == PersistentTraversalMoveFixture912(initial,beforeBase,beforeExecution) ended == [preEnd EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds={21}] events6 == {[tag |-> "TraversalEnds",traversalId |-> 2],TraversalPhaseEndEvent6(preTraversal)} endBase == [before.w EXCEPT !.id=4,!.control=[traversal |-> ended.traversal,phaseEndedIds |-> ended.phaseEndedIds]] endExecution == [tag |-> "ActualTimingTransition",id |-> 19501,snapshotId |-> 4,source |-> RuleAbilitySource9("ProcedureCode9606a4cd52b4"), before |-> preEnd,after |-> ended,events |-> events6] end == PersistentTraversalMoveFixture912(before,endBase,endExecution) event == [ConditionalEventFixture96(19502,"TraversalEnds",0,"SideB","SideB",end.s,19501) EXCEPT !.traversal=ended.traversal,!.structure=TimingRef9("SchemaAtom138",2),!.step="ProcedureCode9606a4cd52b4"] fullEvent == ReplacementOverlay99(event,[actualEvent |-> [tag |-> "TraversalEnds",traversalId |-> 2]]) events == [id \in {19502} |-> fullEvent] cp == PersistentTraversalCPFixture912(end,PersistentTraversalEndCaller912(2),events) conditions == [key \in DOMAIN f.definitions |-> [id \in {19502} |-> [ConditionalTriggerReceiptFixture96(f.definitions[key],fullEvent) EXCEPT !.results=[i \in f.definitions[key].triggerRequirements |-> IF i=2 THEN targetSiteMatches ELSE ended.traversal.successful]]]] keys == (IF targetSiteMatches /\ f.d.syntax.kind="Conditional" THEN {[definition |-> f.key,occurrence |-> 19502]} ELSE {}) \cup (IF ConditionalActive96(f.dg,end.s) THEN {[definition |-> ConditionalKey96(f.dg),occurrence |-> 19502]} ELSE {}) allocation == [key \in keys |-> IF key.definition=f.key THEN 19510 ELSE 19511] bindings == [key \in keys |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> 19520,group |-> 1952]] ledger == ConditionalCommittedFixture96(end.l,f.definitions,cp,allocation,bindings,Empty9) boundary == [tag |-> "PersistentLastCreationCheckpoint",traversal |-> ended.traversal,checkpointId |-> cp.id,caller |-> cp.caller, windowId |-> IF keys={} THEN 0 ELSE 19520,completion |-> PersistentCheckpointCompletion912(ledger,cp,end.w)] cut == [end.r EXCEPT !.persistent[f.key].creationOpen=FALSE,!.persistent[f.key].endCheckpoint=cp.id, !.persistent[f.key].endWindow=boundary.windowId,!.persistent[f.key].endMembers={}] finalCut == [cut EXCEPT !.persistent[f.key].endMembers={allocation[key] : key \in keys}] after == PersistentTraversalStateFixture912(f,finalCut,ledger,end.w,end.a,<<>>) IN [f |-> f,initial |-> initial,preEnd |-> preEnd,ended |-> ended,events6 |-> events6,beforeBase |-> beforeBase, beforeExecution |-> beforeExecution,before |-> before,endBase |-> endBase,endExecution |-> endExecution,end |-> end, cp |-> cp,conditions |-> conditions,allocation |-> allocation,bindings |-> bindings,boundary |-> boundary,after |-> after] PersistentPassFixture912(b) == LET w == WindowTop9(b.stack) passed == PassPriorityFrame9(w) stack == ReplaceWindowTop9(b.stack,passed) candidate == ConditionalPendingAfterWindows96(b.l,stack) keys == IF passed.open THEN {} ELSE PersistentEndWindows912(b.r,w.id) changed == PersistentExpirationRegistry912(b.r,keys) base == [b.w EXCEPT !.id=@+1,!.activity.instances=PersistentInstanceRows912(@,candidate)] world == PersistentWorld912(base,changed) execution == [tag |-> "CurrentCharacteristicsEvaluation",id |-> w.id,snapshotId |-> world.id,source |-> RuleAbilitySource9("ProcedureCode17f2a65162fb"), closedWindow |-> IF passed.open THEN 0 ELSE passed.id] authority == LifetimeAuthorityAfter910(b.a,LifetimeKernelTransition910(b.w,world,execution)) registry == [changed EXCEPT !.effects=ObserveLingeringEffects910(@,world),!.frontier=LifetimeFrontier910(authority,Len(authority.order))] losses == IF keys={} \/ b.f.key \notin DOMAIN b.s.definitions THEN {} ELSE {b.f.key} ledger == [candidate EXCEPT !.activationEpoch=[key \in DOMAIN @ |-> @[key]+IF key \in losses THEN 1 ELSE 0], !.activationSerial=@+IF losses={} THEN 0 ELSE 1] after == PersistentTraversalStateFixture912(b.f,registry,ledger,world,authority,stack) IN [b |-> b,candidate |-> candidate,candidateStack |-> stack,after |-> after] PersistentPassValid912(p) == PassPersistentPriority912(p.b.r,p.after.r,p.b.l,p.candidate,p.after.l,p.b.stack,p.candidateStack,p.after.stack, WindowTop9(p.b.stack).priority,Empty9,p.b.s,p.after.s,p.b.a,p.after.a) PersistentSource103(kind) == IF kind="ExampleFamily002" THEN PersistentBirthFixture912(TRUE) ELSE PersistentBirthForSourceFixture912(TRUE,"Specimen0198",PersistentSpecimen0198DefinitionFixture912,kind#"NoReaction") PersistentRecognitionValid103(g) == /\ PersistentBirthValid912(g.f) /\ PersistentTraversalMoveValid912(g.initial,g.before,g.beforeBase,g.beforeExecution) /\ CompleteTraversal6(g.preEnd,g.ended,TRUE,g.events6,{2}) /\ PersistentTraversalMoveValid912(g.before,g.end,g.endBase,g.endExecution) /\ ProcessPersistentCheckpoint912(g.end.r,g.end.l,g.after.l,<<>>,<<>>,g.f.definitions,g.f.lexemes,g.cp,g.conditions,g.allocation,g.bindings, Empty9,Empty9,[tag |-> "PersistentCheckpointTraversalScope",checkpointId |-> g.cp.id,caller |-> g.cp.caller,traversalId |-> 2],{},CardFacts9,g.end.w,g.end.a) PersistentCleanupFixture103(g) == LET old==PersistentTraversalStateFixture912(g.f,g.end.r,g.after.l,g.end.w,g.end.a,<<>>) key==ConditionalKey96(g.f.dg) lostIds=={i \in DOMAIN old.l.instances : old.l.instances[i].member.source=ObjectAbilitySource9(2)} candidate==[old.l EXCEPT !.activationEpoch[key]=@+1,!.activationSerial=@+1, !.instances=[i \in DOMAIN @ |-> IF i \in lostIds THEN [@[i] EXCEPT !.status="Lost"] ELSE @[i]]] objects==[i \in (DOMAIN old.w.objects \ {2}) \cup {4} |-> IF i=4 THEN [old.w.objects[2] EXCEPT !.zone="SideBDiscard",!.loc="SideBDiscard",!.deployed=FALSE, !.host=0,!.face="Up",!.activated=FALSE] ELSE old.w.objects[i]] base==[old.w EXCEPT !.id=5,!.objects=objects,!.present=@ \ {19001}, !.activity.instances=PersistentInstanceRows912(@,candidate)] world==PersistentWorld912(base,old.r) execution==[tag |-> "ActualObjectTransition",id |-> 19530,snapshotId |-> 5, source |-> RuleAbilitySource9("ProcedureCodea488e1ba6ca3"),component |-> "NormalizedCleanupControl"] authority==LifetimeAuthorityAfter910(old.a,LifetimeKernelTransition910(old.w,world,execution)) registry==[old.r EXCEPT !.effects=ObserveLingeringEffects910(@,world),!.frontier=LifetimeFrontier910(authority,Len(authority.order))] snapshot==[old.s EXCEPT !.id=world.id,!.objects=world.objects,!.present=world.present,!.activity=world.activity, !.activationEpoch=candidate.activationEpoch,!.activationSerial=candidate.activationSerial] rawSnapshot==SnapshotWithConditionalRegistry96(snapshot,old.l) after==PersistentTraversalStateFixture912(g.f,registry,candidate,world,authority,<<>>) IN [g |-> g,old |-> old,lost |-> lostIds,base |-> base,world |-> world,execution |-> execution, authority |-> authority,registry |-> registry,rawSnapshot |-> rawSnapshot,after |-> after] PersistentCleanupComponentsValid103(f) == /\ CommitLifetimeKernelCore910(f.old.a,f.authority,f.world,f.execution) /\ ObserveLingering910(f.old.r,[f.registry EXCEPT !.frontier=f.old.r.frontier],f.world) /\ LingeringConditionalWorld910(f.old.s,f.old.l,f.old.w) /\ LingeringConditionalWorld910(f.rawSnapshot,f.old.l,f.world) /\ ObserveConditionalActivity96(f.old.l,f.old.l,f.after.l,<<>>,<<>>,f.old.s,f.rawSnapshot) /\ PersistentRegistryWorldBound912(f.registry,f.world) /\ LingeringConditionalWorld910(f.after.s,f.after.l,f.world) /\ PersistentRecognizedIds912(f.old.l,f.g.cp.id)=PersistentRecognizedIds912(f.after.l,f.g.cp.id) /\ \A i \in f.lost : f.after.l.instances[i].status="Lost" /\ f.after.l.instances[i].member=f.old.l.instances[i].member PersistentCases103 == {<<"ExampleFamily002",FALSE>>,<<"ExampleFamily002",TRUE>>,<<"Static",FALSE>>,<<"Static",TRUE>>,<<"NoReaction",FALSE>>} PersistentStepCap103(n) == IF n<12 THEN n ELSE 12 PersistentScenario103(which) == LET g==PersistentTraversalEndFixture912(PersistentSource103(which[1]),TRUE) ordinary==PersistentTraversalStateFixture912(g.f,g.end.r,g.after.l,g.end.w,g.end.a,<<>>) IN [g |-> g,ordinary |-> ordinary,cleanup |-> IF which[2] THEN PersistentCleanupFixture103(g) ELSE [after |-> ordinary]] PersistentInside103 == {TimingRef9("Turn",1),TimingRef9("TurnPhase",10)} PersistentStageAfter103(f,snapshot) == LET rest==Tail(f.owed) IN [f EXCEPT !.owed=rest,!.done=@ \cup {f.owed[1]},!.snapshotId=snapshot, !.point=IF rest= <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE rest[1],!.phase=IF rest= <<>> THEN "Completed" ELSE "Steps"] PersistentFrame103(which,n) == LET g==PersistentScenario103(which).g base==NewCheckpoint103(g.cp.id,g.cp.caller,g.cp.beginSnapshot.id,PersistentInside103) IN [base EXCEPT !.owed=SubSeq(CheckpointStages103,n+1,12),!.done={CheckpointStages103[i] : i \in 1..n}, !.snapshotId=IF which[2] /\ n>=5 THEN 5 ELSE g.end.w.id, !.point=IF n=12 THEN "ProcedureCodeb74d673a0fc6" ELSE CheckpointStages103[n+1],!.phase=IF n=12 THEN "Completed" ELSE "Steps", !.recognition=IF n=0 THEN base.recognition ELSE g.cp, !.recognized=IF n=0 THEN Empty9 ELSE CheckpointMemberMap103(g.after.l,g.cp.id)] PersistentCurrent103(which,n) == LET s==PersistentScenario103(which) IN IF n=0 THEN s.g.end ELSE IF which[2] /\ n>=5 THEN s.cleanup.after ELSE s.ordinary PersistentRecognizeInput103(g) == [route |-> "Persistent",registry |-> g.end.r,definitions |-> g.f.definitions,lexemes |-> g.f.lexemes, cp |-> g.cp,conditions |-> g.conditions,allocation |-> g.allocation,bindings |-> g.bindings, departures |-> Empty9,holds |-> Empty9, scope |-> [tag |-> "PersistentCheckpointTraversalScope",checkpointId |-> g.cp.id,caller |-> g.cp.caller,traversalId |-> 2], usedWindows |-> {},cardFacts |-> CardFacts9,world |-> g.end.w,authority |-> g.end.a] PersistentCompletion103(which) == LET b==PersistentCurrent103(which,12) IN PersistentCheckpointCompletion912(b.l,PersistentScenario103(which).g.cp,b.w) PersistentCutRegistry103(which) == LET b==PersistentCurrent103(which,12) f==PersistentFrame103(which,12) key==PersistentScenario103(which).g.f.key IN [b.r EXCEPT !.persistent[key].creationOpen=FALSE,!.persistent[key].endCheckpoint=f.id, !.persistent[key].endWindow=CheckpointRecognizedWindow103(f),!.persistent[key].endMembers=DOMAIN f.recognized] PersistentBoundary103(which) == LET f==PersistentFrame103(which,12) IN [tag |-> "PersistentLastCreationCheckpoint",traversal |-> PersistentScenario103(which).g.ended.traversal, checkpointId |-> f.id,caller |-> f.caller,windowId |-> CheckpointRecognizedWindow103(f),completion |-> PersistentCompletion103(which)] PersistentSite103(which) == LET s==PersistentScenario103(which) IN TraversalPrioritySite9(s.ordinary.w.turn,s.g.ended.traversal,[id |-> 0,traversalId |-> 0,begun |-> FALSE],[slots |-> Empty9],s.g.ended) PersistentOpening103(which) == LET f==PersistentFrame103(which,12) IN [tag |-> "PriorityWindowOpening",windowId |-> CheckpointRecognizedWindow103(f),kind |-> "Reaction", site |-> PersistentSite103(which),members |-> DOMAIN f.recognized,instances |-> f.recognized,group |-> 1952, beginning |-> NoTimingRef9,instruction |-> [id |-> 0,abilityInstance |-> 0,index |-> 0],effectRevision |-> 0, modifiersExist |-> FALSE,preparation |-> <<"ConditionsMet","PendingGroup">>,checkpointId |-> f.id,caller |-> f.caller, completion |-> PersistentCompletion103(which)] PersistentOpenedStack103(which) == LET f==PersistentFrame103(which,12) b==PersistentCurrent103(which,12) o==PersistentOpening103(which) raw==NewPriorityWindow9(o.windowId,"Reaction",o.site,f.recognized,o.group,o.beginning,o.instruction,o.effectRevision) pending==PersistentGeneratedIds912(b.l,f.id) IN <<[raw EXCEPT !.pending=pending,!.lostPending=DOMAIN f.recognized \ pending]>> PersistentOpenValid103(which) == LET f==PersistentFrame103(which,12) b==PersistentCurrent103(which,12) IN OpenCheckpointReaction103(f,[f EXCEPT !.phase="Reaction",!.windowId=CheckpointRecognizedWindow103(f)], b.l,<<>>,PersistentOpenedStack103(which),PersistentSite103(which),PersistentOpening103(which),{}) PersistentCutValid103(which) == LET s==PersistentScenario103(which) b==PersistentCurrent103(which,12) IN CutoffPersistentAtCheckpoint103(b.r,PersistentCutRegistry103(which),b.l,PersistentFrame103(which,12), PersistentCompletion103(which),s.g.preEnd,s.g.ended,s.g.events6,{2},PersistentBoundary103(which)) PersistentNoReactionReturn103(which) == LET f==PersistentFrame103(which,12) b==PersistentCurrent103(which,12) IN ReturnCheckpointWithoutReaction103(f,[f EXCEPT !.phase="Returned",!.returned=TRUE],b.l,b.w,PersistentCompletion103(which),f.caller) PersistentStepValid103(which,n) == LET s==PersistentScenario103(which) IN IF n=0 THEN /\ PersistentRecognitionValid103(s.g) /\ RecognizeCheckpoint103(PersistentFrame103(which,0),PersistentFrame103(which,1),s.g.end.l,s.g.after.l, <<>>,<<>>,PersistentRecognizeInput103(s.g)) ELSE /\ CheckpointStageAdvance103(PersistentFrame103(which,n),PersistentFrame103(which,n+1),CheckpointStages103[n+1], PersistentCurrent103(which,n+1).w.id) /\ IF n=4 /\ which[2] THEN LET c==s.cleanup IN /\ PersistentCleanupComponentsValid103(c) /\ ObserveCheckpointKernel103(PersistentFrame103(which,n),c.old.r,c.after.r,c.old.l,c.after.l, <<>>,<<>>,c.old.s,c.rawSnapshot,c.base,c.execution,c.old.a,c.after.a) ELSE TRUE PersistentFrontierBindings103(which) == LET f==PersistentFrame103(which,12) b==PersistentCurrent103(which,12) completion==PersistentCompletion103(which) fakeEarly==[f EXCEPT !.done=@ \ {"ProcedureCode0811ebc5f40e"}] changedMember==IF DOMAIN f.recognized={} THEN b.l ELSE LET id==CHOOSE i \in DOMAIN f.recognized : TRUE IN [b.l EXCEPT !.instances[id].member.source=ObjectAbilitySource9(999)] forgedReceipt==PersistentCheckpointCompletion912(changedMember,f.recognition,b.w) IN /\ CheckpointCompletion103(f,b.l,b.w,completion) /\ \A n \in 0..11 : ~CheckpointCompletion103(PersistentFrame103(which,n),PersistentCurrent103(which,n).l, PersistentCurrent103(which,n).w,completion) /\ ~CheckpointCompletion103(fakeEarly,b.l,b.w,completion) /\ ~CheckpointCompletion103(f,b.l,[b.w EXCEPT !.id=999],PersistentCheckpointCompletion912(b.l,f.recognition,[b.w EXCEPT !.id=999])) /\ IF DOMAIN f.recognized={} THEN TRUE ELSE ~CheckpointCompletion103(f,changedMember,b.w,forgedReceipt) PersistentPriorityFrame103(cp,ledger,n) == LET base==NewCheckpoint103(cp.id,cp.caller,cp.beginSnapshot.id,PersistentInside103) IN [base EXCEPT !.owed=SubSeq(CheckpointStages103,n+1,12),!.done={CheckpointStages103[i] : i \in 1..n}, !.point=IF n=12 THEN "ProcedureCodeb74d673a0fc6" ELSE CheckpointStages103[n+1],!.phase=IF n=12 THEN "Completed" ELSE "Steps", !.recognition=IF n=0 THEN base.recognition ELSE cp, !.recognized=IF n=0 THEN Empty9 ELSE CheckpointMemberMap103(ledger,cp.id)] PersistentReceiveFixture103(b) == LET w==WindowTop9(b.stack) cp==PersistentTraversalCPFixture912(b,ConditionalPriorityCaller96(w),Empty9) ledger==ConditionalCommittedFixture96(b.l,b.f.definitions,cp,Empty9,Empty9,Empty9) ready==[w EXCEPT !.stage="Ready",!.checkpoint=cp.id] after==PersistentTraversalStateFixture912(b.f,b.r,ledger,b.w,b.a,<>) completion==PersistentCheckpointCompletion912(ledger,cp,b.w) full==PersistentPriorityFrame103(cp,ledger,12) priority==[tag |-> "NormalPriorityCheckpoint",id |-> cp.id,windowId |-> w.id,reception |-> w.reception, player |-> w.priority,complete |-> TRUE,reactionsDrained |-> TRUE] input==[route |-> "Persistent",registry |-> b.r,definitions |-> b.f.definitions,lexemes |-> b.f.lexemes, cp |-> cp,conditions |-> Empty9,allocation |-> Empty9,bindings |-> Empty9,departures |-> Empty9,holds |-> Empty9, scope |-> [tag |-> "PersistentCheckpointTraversalScope",checkpointId |-> cp.id,caller |-> cp.caller,traversalId |-> 2], usedWindows |-> {w.id},cardFacts |-> CardFacts9,world |-> b.w,authority |-> b.a] IN [b |-> b,cp |-> cp,after |-> after,completion |-> completion,full |-> full,priority |-> priority,input |-> input] PersistentReceiveValid103(f) == /\ RecognizeCheckpoint103(PersistentPriorityFrame103(f.cp,f.b.l,0),PersistentPriorityFrame103(f.cp,f.after.l,1), f.b.l,f.after.l,f.b.stack,f.b.stack,f.input) /\ \A n \in 1..11 : CheckpointStageAdvance103(PersistentPriorityFrame103(f.cp,f.after.l,n), PersistentPriorityFrame103(f.cp,f.after.l,n+1),CheckpointStages103[n+1],f.b.w.id) /\ CheckpointCompletion103(f.full,f.after.l,f.b.w,f.completion) /\ ReturnCheckpointWithoutReaction103(f.full,[f.full EXCEPT !.phase="Returned",!.returned=TRUE], f.after.l,f.b.w,f.completion,f.cp.caller) /\ CheckpointPriorityWithConditionals96(f.after.l,f.b.stack,f.after.stack,f.priority) PersistentLostClosure103 == LET which== <<"Static",TRUE>> s==PersistentScenario103(which) b==PersistentCurrent103(which,12) opened==PersistentTraversalStateFixture912(s.g.f,PersistentCutRegistry103(which),b.l,b.w,b.a,PersistentOpenedStack103(which)) firstReady==PersistentReceiveFixture103(opened) firstPass==PersistentPassFixture912(firstReady.after) secondReady==PersistentReceiveFixture103(firstPass.after) secondPass==PersistentPassFixture912(secondReady.after) parent==[PersistentFrame103(which,12) EXCEPT !.phase="Reaction",!.windowId=19520] IN /\ PersistentCutValid103(which) /\ PersistentOpenValid103(which) /\ PersistentReceiveValid103(firstReady) /\ PersistentPassValid912(firstPass) /\ PersistentReceiveValid103(secondReady) /\ PersistentPassValid912(secondPass) /\ ~WindowTop9(secondPass.after.stack).open /\ secondPass.after.r.persistent[s.g.f.key].phase="Expired" /\ secondPass.after.r.effects[55000].status="Expired" /\ 19000 \notin secondPass.after.w.present /\ ReturnCheckpointAfterReaction103(parent,[parent EXCEPT !.phase="Returned",!.returned=TRUE], secondPass.after.l,secondPass.after.stack,<<>>,parent.caller) /\ ~ReturnCheckpointAfterReaction103(parent,[parent EXCEPT !.phase="Returned",!.returned=TRUE], firstPass.after.l,firstPass.after.stack,<<>>,parent.caller) PersistentZeroExpiry103 == LET which== <<"NoReaction",FALSE>> s==PersistentScenario103(which) b0==PersistentCurrent103(which,12) b==PersistentTraversalStateFixture912(s.g.f,PersistentCutRegistry103(which),b0.l,b0.w,b0.a,<<>>) changed==PersistentExpirationRegistry912(b.r,{s.g.f.key}) world==PersistentWorld912([b.w EXCEPT !.id=@+1],changed) clearance==[tag |-> "NormalCheckpointNoReactionWindow",checkpointId |-> s.g.cp.id,caller |-> s.g.cp.caller, pendingInstances |-> {},point |-> "ProcedureCodeb74d673a0fc6"] execution==[tag |-> "CurrentCharacteristicsEvaluation",id |-> s.g.cp.id,snapshotId |-> world.id, source |-> RuleAbilitySource9("ProcedureCode17f2a65162fb"),noWindow |-> clearance] authority==LifetimeAuthorityAfter910(b.a,LifetimeKernelTransition910(b.w,world,execution)) registry==[changed EXCEPT !.effects=ObserveLingeringEffects910(@,world),!.frontier=LifetimeFrontier910(authority,Len(authority.order))] after==PersistentTraversalStateFixture912(s.g.f,registry,b.l,world,authority,<<>>) IN /\ PersistentCutValid103(which) /\ PersistentNoReactionReturn103(which) /\ ExpirePersistentNoReaction912(b.r,registry,b.l,after.l,<<>>,<<>>,b.s,after.s,s.g.cp,clearance,b.a,authority) /\ registry.effects[55000].status="Expired" /\ 19000 \notin world.present VARIABLE p103 InitPersistent103 == \E which \in PersistentCases103 : p103=[which |-> which,step |-> 0] WorkPersistent103 == /\ p103.step<14 /\ CASE p103.step<12 -> PersistentStepValid103(p103.which,p103.step) [] p103.step=12 -> PersistentCutValid103(p103.which) [] OTHER -> IF DOMAIN PersistentFrame103(p103.which,12).recognized={} THEN PersistentNoReactionReturn103(p103.which) ELSE PersistentOpenValid103(p103.which) /\ p103'=[p103 EXCEPT !.step=@+1] NextPersistent103 == WorkPersistent103 \/ UNCHANGED p103 SpecPersistent103 == InitPersistent103 /\ [][NextPersistent103]_p103 /\ WF_p103(WorkPersistent103) DeliveredPersistent103 == <>(p103.step=14) PersistentFrontierAssertions103 == /\ p103.which \in PersistentCases103 /\ p103.step \in 0..14 /\ PersistentFrontierBindings103(p103.which) /\ PersistentFrame103(p103.which,PersistentStepCap103(p103.step)).inside=PersistentInside103 /\ TimingRef9("SchemaAtom138",2) \notin PersistentInside103 /\ TimingRef9("TraversalPhase",21) \notin PersistentInside103 /\ (p103.step>=1 => DOMAIN PersistentFrame103(p103.which,PersistentStepCap103(p103.step)).recognized= PersistentRecognizedIds912(PersistentCurrent103(p103.which,PersistentStepCap103(p103.step)).l,1)) /\ (p103.step>=12 => PersistentCutValid103(p103.which)) /\ (p103.step=14 /\ p103.which= <<"Static",TRUE>> => PersistentLostClosure103) /\ (p103.step=14 /\ p103.which= <<"NoReaction",FALSE>> => PersistentZeroExpiry103) /\ (p103.step=14 => IF p103.which[1]="NoReaction" THEN /\ DOMAIN PersistentFrame103(p103.which,12).recognized={} /\ PersistentNoReactionReturn103(p103.which) ELSE LET w==WindowTop9(PersistentOpenedStack103(p103.which)) b==PersistentCurrent103(p103.which,12) IN /\ w.members=PersistentFrame103(p103.which,12).recognized /\ w.pending=PersistentGeneratedIds912(b.l,1) /\ w.lostPending=DOMAIN w.members \ w.pending /\ ~PersistentNoReactionReturn103(p103.which)) =============================================================================