r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

PersistentChecksMC¶

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

This model/fact module also contains 161 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

CardObject9 · operator

reference-profile · input revision 2 · CC0 1.0

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 |-> {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardFacts9

ConditionalCardActivityFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

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"))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivationStatus8

ConditionalCheckpointFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

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"]]

Exact module download · Source bundle and reproduction instructions

ConditionalCommittedFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

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]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActivityLedger96, NewConditionalInstance96

ConditionalDefinitionFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

ConditionalDefinitionFixture96(id,card,primary,eventKind,subject,actor,side) ==
 LET syntax == SyntaxFixture93(id,"Conditional",CardFacts9[card].side,CardFacts9[card].kind,
                 <<TextUnit93(1,"SchemaAtom043",primary,TRUE,0),InstructionFixture93>>)
 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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityDefinition9, TextUnit93, InstructionFixture93, SyntaxFixture93, CardFacts9

ConditionalEventFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

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"]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoTimingRef9, RuleAbilitySource9, NoTraversal6

ConditionalSnapshotFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivityContext9, ConditionalCardActivityFixture96, Empty9, SetupPlayers

ConditionalTriggerReceiptFixture96 · operator

reference-profile · input revision 2 · CC0 1.0

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]]

Exact module download · Source bundle and reproduction instructions

DeclarationFixture93 · operator

reference-profile · input revision 2 · CC0 1.0

DeclarationFixture93 == UnitFixture93(10,"Declaration","NoValue",FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: UnitFixture93

DeliveredPersistent103 · operator

reference-profile · input revision 2 · CC0 1.0

DeliveredPersistent103 == <>(p103.step=14)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p103

Empty9 · operator

reference-profile · input revision 2 · CC0 1.0

Empty9 == [id \in {} |-> id]

Exact module download · Source bundle and reproduction instructions

InitPersistent103 · operator

reference-profile · input revision 2 · CC0 1.0

InitPersistent103 == \E which \in PersistentCases103 : p103=[which |-> which,step |-> 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCases103, p103

InstructionFixture93 · operator

reference-profile · input revision 2 · CC0 1.0

InstructionFixture93 == UnitFixture93(10,"Instruction","NoValue",FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: UnitFixture93

LexicalMentionFixture99 · operator

reference-profile · input revision 2 · CC0 1.0

LexicalMentionFixture99(d,word,unit,role) ==
 [word |-> word,unit |-> unit,owner |-> AbilityKey99(d),role |-> role]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityKey99

LexicalReceiptFixture99 · operator

reference-profile · input revision 2 · CC0 1.0

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"]]

Exact module download · Source bundle and reproduction instructions

LexicalSingleFixture99 · operator

reference-profile · input revision 2 · CC0 1.0

LexicalSingleFixture99(d,card,word,unit,role,facts) ==
 LexicalReceiptFixture99(d,card,[id \in {1} |-> LexicalMentionFixture99(d,word,unit,role)],facts)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LexicalMentionFixture99, LexicalReceiptFixture99

LifetimeWorldFixture910 · operator

reference-profile · input revision 2 · CC0 1.0

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}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivityContext9, CardObject9, Empty9, SetupPlayers, CardFacts9, NoTraversal6, OpenEncounter6, OpenTurn5

NextPersistent103 · operator

reference-profile · input revision 2 · CC0 1.0

NextPersistent103 == WorkPersistent103 \/ UNCHANGED p103

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WorkPersistent103, p103

ObservedWithFrontier910 · operator

reference-profile · input revision 2 · CC0 1.0

ObservedWithFrontier910(registry,a,position) == ReplacementOverlay99(registry,[frontier |-> LifetimeFrontier910(a,position)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LifetimeFrontier910, ReplacementOverlay99

PersistentBirthFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentBirthFixture912(withTraversal) == PersistentBirthForSourceFixture912(withTraversal,"Specimen0010",PersistentExampleFamily002DefinitionFixture912,TRUE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentBirthForSourceFixture912, PersistentExampleFamily002DefinitionFixture912

PersistentBirthForSourceFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityKey99, ConditionalKey96, LifetimeAuthorityAfter910, LifetimeFrontier910, LifetimeKernelTransition910, NewConditionalLedger96, NewLifetimeAuthority910, NewLingeringRegistry910, NewPersistentRegistry912, PersistentWorld912, RuleAbilitySource9, OpenItemInspection7, MovementEvent8, CardObject9, ConditionalSnapshotFixture96, Empty9, LexicalSingleFixture99, LifetimeWorldFixture910, ObservedWithFrontier910, PersistentBirthProposedFixture912, PersistentDoppelDefinitionFixture912, TraversalFixture92, TurnFixture92, CardFacts9, NoTraversal6

PersistentBirthProposedFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentBirthCohort912, PersistentEffect912, PersistentRecord912, ReplacementOverlay99

PersistentBirthValid912 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CreatePersistentOnRetire912, CardFacts9

PersistentBoundary103 · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointRecognizedWindow103, PersistentCompletion103, PersistentFrame103, PersistentScenario103

PersistentCases103 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentCases103 == {<<"ExampleFamily002",FALSE>>,<<"ExampleFamily002",TRUE>>,<<"Static",FALSE>>,<<"Static",TRUE>>,<<"NoReaction",FALSE>>}

Exact module download · Source bundle and reproduction instructions

PersistentCleanupComponentsValid103 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CommitLifetimeKernelCore910, LingeringConditionalWorld910, ObserveConditionalActivity96, ObserveLingering910, PersistentRecognizedIds912, PersistentRegistryWorldBound912

PersistentCleanupFixture103 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, LifetimeAuthorityAfter910, LifetimeFrontier910, LifetimeKernelTransition910, ObjectAbilitySource9, ObserveLingeringEffects910, PersistentInstanceRows912, PersistentWorld912, RuleAbilitySource9, SnapshotWithConditionalRegistry96, PersistentTraversalStateFixture912

PersistentCompletion103 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentCompletion103(which) ==
 LET b==PersistentCurrent103(which,12)
 IN PersistentCheckpointCompletion912(b.l,PersistentScenario103(which).g.cp,b.w)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointCompletion912, PersistentCurrent103, PersistentScenario103

PersistentCurrent103 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentScenario103

PersistentCutRegistry103 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointRecognizedWindow103, PersistentCurrent103, PersistentFrame103, PersistentScenario103

PersistentCutValid103 · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CutoffPersistentAtCheckpoint103, PersistentBoundary103, PersistentCompletion103, PersistentCurrent103, PersistentCutRegistry103, PersistentFrame103, PersistentScenario103

PersistentDoppelDefinitionFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentDoppelDefinitionFixture912 ==
 LET d == ConditionalDefinitionFixture96(19001,"Specimen0076","Trigger","TraversalEnds","SchemaAtom016","SideB","SideB")
 IN [d EXCEPT !.syntax.source=ObjectAbilitySource9(2),!.activity.source=ObjectAbilitySource9(2),
      !.syntax.units= <<TextUnit93(91,"AbilityFlag","OncePerTurn",FALSE,0)>> \o @,!.triggerRequirements={3},!.optionalParts={1}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, TextUnit93, ConditionalDefinitionFixture96

PersistentExampleFamily002DefinitionFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentExampleFamily002DefinitionFixture912 ==
 LET d == ConditionalDefinitionFixture96(19000,"Specimen0010","Trigger","TraversalEnds","SchemaAtom016","SideB","SideB")
 IN [d EXCEPT !.syntax.units= <<TextUnit93(90,"AbilityFlag","Persistent",FALSE,0)>> \o @,!.triggerRequirements={2}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TextUnit93, ConditionalDefinitionFixture96

PersistentFrame103 · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointMemberMap103, CheckpointStages103, NewCheckpoint103, Empty9, PersistentInside103, PersistentScenario103

PersistentFrontierAssertions103 · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentGeneratedIds912, PersistentRecognizedIds912, TimingRef9, WindowTop9, PersistentCases103, PersistentCurrent103, PersistentCutValid103, PersistentFrame103, PersistentFrontierBindings103, PersistentInside103, PersistentLostClosure103, PersistentNoReactionReturn103, PersistentOpenedStack103, PersistentStepCap103, PersistentZeroExpiry103, p103

PersistentFrontierBindings103 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9, PersistentCheckpointCompletion912, CheckpointCompletion103, PersistentCompletion103, PersistentCurrent103, PersistentFrame103

PersistentInside103 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentInside103 == {TimingRef9("Turn",1),TimingRef9("TurnPhase",10)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9

PersistentLostClosure103 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, ReturnCheckpointAfterReaction103, PersistentCurrent103, PersistentCutRegistry103, PersistentCutValid103, PersistentFrame103, PersistentOpenValid103, PersistentOpenedStack103, PersistentPassFixture912, PersistentPassValid912, PersistentReceiveFixture103, PersistentReceiveValid103, PersistentScenario103, PersistentTraversalStateFixture912

PersistentNoReactionReturn103 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReturnCheckpointWithoutReaction103, PersistentCompletion103, PersistentCurrent103, PersistentFrame103

PersistentOpenValid103 · operator

reference-profile · input revision 2 · CC0 1.0

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),{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointRecognizedWindow103, OpenCheckpointReaction103, PersistentCurrent103, PersistentFrame103, PersistentOpenedStack103, PersistentOpening103, PersistentSite103

PersistentOpenedStack103 · operator

reference-profile · input revision 2 · CC0 1.0

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]>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, PersistentGeneratedIds912, PersistentCurrent103, PersistentFrame103, PersistentOpening103

PersistentOpening103 · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoTimingRef9, CheckpointRecognizedWindow103, PersistentCompletion103, PersistentFrame103, PersistentSite103

PersistentPassFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalPendingAfterWindows96, LifetimeAuthorityAfter910, LifetimeFrontier910, LifetimeKernelTransition910, ObserveLingeringEffects910, PassPriorityFrame9, PersistentEndWindows912, PersistentExpirationRegistry912, PersistentInstanceRows912, PersistentWorld912, ReplaceWindowTop9, RuleAbilitySource9, WindowTop9, PersistentTraversalStateFixture912

PersistentPassValid912 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PassPersistentPriority912, WindowTop9, Empty9

PersistentPriorityFrame103 · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointMemberMap103, CheckpointStages103, NewCheckpoint103, Empty9, PersistentInside103

PersistentReceiveFixture103 · operator

reference-profile · input revision 2 · CC0 1.0

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,<<ready>>)
     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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalPriorityCaller96, PersistentCheckpointCompletion912, WindowTop9, ConditionalCommittedFixture96, Empty9, PersistentPriorityFrame103, PersistentTraversalCPFixture912, PersistentTraversalStateFixture912, CardFacts9

PersistentReceiveValid103 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriorityWithConditionals96, CheckpointCompletion103, CheckpointStageAdvance103, CheckpointStages103, RecognizeCheckpoint103, ReturnCheckpointWithoutReaction103, PersistentPriorityFrame103

PersistentRecognitionValid103 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProcessPersistentCheckpoint912, Empty9, PersistentBirthValid912, PersistentTraversalMoveValid912, CardFacts9, CompleteTraversal6

PersistentRecognizeInput103 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Empty9, CardFacts9

PersistentScenario103 · operator

reference-profile · input revision 2 · CC0 1.0

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]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCleanupFixture103, PersistentSource103, PersistentTraversalEndFixture912, PersistentTraversalStateFixture912

PersistentSite103 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalPrioritySite9, Empty9, PersistentScenario103

PersistentSource103 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentSource103(kind) ==
 IF kind="ExampleFamily002" THEN PersistentBirthFixture912(TRUE)
 ELSE PersistentBirthForSourceFixture912(TRUE,"Specimen0198",PersistentSpecimen0198DefinitionFixture912,kind#"NoReaction")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentBirthFixture912, PersistentBirthForSourceFixture912, PersistentSpecimen0198DefinitionFixture912

PersistentSpecimen0198DefinitionFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentSpecimen0198DefinitionFixture912 ==
 LET syntax == SyntaxFixture93(19000,"Static","SideA","Attachment",<<TextUnit93(90,"AbilityFlag","Persistent",FALSE,0),DeclarationFixture93>>)
 IN [syntax |-> syntax,activity |-> AbilityDefinition9(19000,"Static",syntax.source,"Printed"),instructions |-> <<>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityDefinition9, TextUnit93, DeclarationFixture93, SyntaxFixture93

PersistentStageAfter103 · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

PersistentStepCap103 · operator

reference-profile · input revision 2 · CC0 1.0

PersistentStepCap103(n) == IF n<12 THEN n ELSE 12

Exact module download · Source bundle and reproduction instructions

PersistentStepValid103 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointStageAdvance103, CheckpointStages103, ObserveCheckpointKernel103, RecognizeCheckpoint103, PersistentCleanupComponentsValid103, PersistentCurrent103, PersistentFrame103, PersistentRecognitionValid103, PersistentRecognizeInput103, PersistentScenario103

PersistentTraversalCPFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalCheckpointFixture96

PersistentTraversalEndFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ConditionalKey96, PersistentCheckpointCompletion912, PersistentTraversalEndCaller912, ReplacementOverlay99, RuleAbilitySource9, TimingRef9, ConditionalCommittedFixture96, ConditionalEventFixture96, ConditionalTriggerReceiptFixture96, Empty9, PersistentTraversalCPFixture912, PersistentTraversalMoveFixture912, PersistentTraversalStateFixture912, TraversalPhaseEndEvent6

PersistentTraversalMoveFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LifetimeAuthorityAfter910, LifetimeFrontier910, LifetimeKernelTransition910, ObserveLingeringEffects910, PersistentWorld912, PersistentTraversalStateFixture912

PersistentTraversalMoveValid912 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObservePersistentKernel912

PersistentTraversalSnapshotFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LingeringConditionalSnapshot910

PersistentTraversalStateFixture912 · operator

reference-profile · input revision 2 · CC0 1.0

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")]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentTraversalSnapshotFixture912

PersistentZeroExpiry103 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExpirePersistentNoReaction912, LifetimeAuthorityAfter910, LifetimeFrontier910, LifetimeKernelTransition910, ObserveLingeringEffects910, PersistentExpirationRegistry912, PersistentWorld912, RuleAbilitySource9, PersistentCurrent103, PersistentCutRegistry103, PersistentCutValid103, PersistentNoReactionReturn103, PersistentScenario103, PersistentTraversalStateFixture912

SpecPersistent103 · operator

reference-profile · input revision 2 · CC0 1.0

SpecPersistent103 == InitPersistent103 /\ [][NextPersistent103]_p103 /\ WF_p103(WorkPersistent103)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitPersistent103, NextPersistent103, WorkPersistent103, p103

SyntaxFixture93 · operator

reference-profile · input revision 2 · CC0 1.0

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]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectAbilitySource9

TraversalFixture92 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalFixture92(step) ==
 [OpenTraversal6(2,20,"action") EXCEPT !.formalBegun = TRUE,!.phase = TraversalStepInfo6(step).phase,!.step = step,
   !.attacked = "SchemaAtom082",!.position = "outer"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenTraversal6, TraversalStepInfo6

TurnFixture92 · operator

reference-profile · input revision 2 · CC0 1.0

TurnFixture92(player) == [OpenTurn5(player,1,[p \in SetupPlayers |-> 0]) EXCEPT !.phase = "NeutralValue00001"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, OpenTurn5

UnitFixture93 · operator

reference-profile · input revision 2 · CC0 1.0

UnitFixture93(id,category,subtype,primary) == TextUnit93(id,category,subtype,primary,0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TextUnit93

WorkPersistent103 · operator

reference-profile · input revision 2 · CC0 1.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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCutValid103, PersistentFrame103, PersistentNoReactionReturn103, PersistentOpenValid103, PersistentStepValid103, p103

p103 · variable

reference-profile · input revision 2 · CC0 1.0

p103

Exact module download · Source bundle and reproduction instructions