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

AdditionalProceduresMC¶

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 16 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.

ActiveWork10p · operator

reference-profile · input revision 2 · CC0 1.0

ActiveWork10p == Work10p /\ UNCHANGED block10

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block10, Work10p

AuxiliarySite10p · operator

reference-profile · input revision 2 · CC0 1.0

AuxiliarySite10p ==
 LET targetSites==Without101(q10p.targetSites,{"r1"})
 IN /\ CheckpointAuxiliarySiteCleanup103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.targetSites,targetSites,q10p.objects,Empty10p,q10p.frame.snapshotId)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),!.targetSites=targetSites]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointAuxiliarySiteCleanup103, Without101, Empty10p, q10p

CP10p · operator

reference-profile · input revision 2 · CC0 1.0

CP10p == [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> 1,caller |-> Caller10p,
 previousCheckpoint |-> 0,serial |-> 1,previousSnapshot |-> InitialSnapshot10p,
 beginSnapshot |-> [Processing10p EXCEPT !.point="CheckpointBeginning"],processingSnapshot |-> Processing10p,
 stepSerial |-> 0,occurrences |-> Empty10p]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Caller10p, Empty10p, InitialSnapshot10p, Processing10p

Caller10p · operator

reference-profile · input revision 2 · CC0 1.0

Caller10p == [kind |-> "AbilityInstruction",abilityInstance |-> 55,instruction |-> 77]

Exact module download · Source bundle and reproduction instructions

Cleanup10p · operator

reference-profile · input revision 2 · CC0 1.0

Cleanup10p ==
 LET world==World10p(q10p)
     f==LingeringCheckpointFrame910(q10p.ledger,CP10p,world)
     cleanup==[tag |-> "LingeringCheckpointCleanup",frame |-> f,expired |-> {9},complete |-> TRUE]
     registry==[q10p.registry EXCEPT !.effects=Empty10p,!.cleanupIds={1}]
 IN /\ CheckpointCleanupEffects103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.registry,registry,
         q10p.ledger,q10p.ledger,q10p.ledger,<<>>,<<>>,Processing10p,Processing10p,world,f,[f EXCEPT !.returned=TRUE,!.point="ProcedureCodeb681cc249a04"],cleanup)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100),!.registry=registry]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LingeringCheckpointFrame910, CheckpointNextFrame103, CheckpointCleanupEffects103, CP10p, Empty10p, Processing10p, World10p, q10p

Counters10p · operator

reference-profile · input revision 2 · CC0 1.0

Counters10p ==
 LET objects==Without101(q10p.objects,{5})
 IN /\ CheckpointReturnDiscardCounters103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.objects,objects,q10p.frame.snapshotId)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),!.objects=objects]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointReturnDiscardCounters103, Without101, q10p

Empty10p · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

EventuallyReturned10p · operator

reference-profile · input revision 2 · CC0 1.0

EventuallyReturned10p == <>q10p.frame.returned

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q10p

Hosted10p · operator

reference-profile · input revision 2 · CC0 1.0

Hosted10p ==
 LET due==CheckpointHostedTargets103(q10p.objects,q10p.departures,q10p.frame.point,Empty10p,Empty10p)
     cards=={id \in due : q10p.objects[id].card#"none"}
     successors==[id \in cards |-> 10+id]
     objects==CheckpointRetireMap103(q10p.objects,due,successors,CheckpointPrinted103,CheckpointOwners103,DOMAIN q10p.objects)
     history==MergeCheckpointDepartures103(q10p.departures,CheckpointNewUninstallDepartures103(q10p.objects,due))
     snapshot==q10p.frame.snapshotId+(IF due={} THEN 0 ELSE 1)
     frame==IF q10p.frame.point="ProcedureCode96bfa1b6a970" /\ due#{} THEN [q10p.frame EXCEPT !.snapshotId=snapshot,!.hostPasses=@+1]
            ELSE CheckpointNextFrame103(q10p.frame,snapshot)
 IN /\ CheckpointHostedCleanup103(q10p.frame,frame,q10p.objects,objects,q10p.departures,history,Empty10p,Empty10p,
         successors,q10p.used,CheckpointPrinted103,CheckpointOwners103,DOMAIN q10p.objects,snapshot)
    /\ q10p'=[q10p EXCEPT !.frame=frame,!.objects=objects,!.departures=history,!.used=@ \cup {successors[id] : id \in cards}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointOwners103, CheckpointPrinted103, CheckpointHostedCleanup103, CheckpointHostedTargets103, CheckpointNewUninstallDepartures103, CheckpointRetireMap103, MergeCheckpointDepartures103, Empty10p, q10p

Illegal10p · operator

reference-profile · input revision 2 · CC0 1.0

Illegal10p ==
 /\ CheckpointIllegalRetire103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.objects,q10p.objects,{},Legal10p,
       Empty10p,"SideB",q10p.targetSites,[applies |-> FALSE],"NoValue",{},Empty10p,q10p.used,CheckpointPrinted103,CheckpointOwners103,{},100)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointOwners103, CheckpointPrinted103, CheckpointIllegalRetire103, Empty10p, Legal10p, q10p

Init10p · operator

reference-profile · input revision 2 · CC0 1.0

Init10p ==
 /\ block10=3
 /\ q10p=[frame |-> NewCheckpoint103(1,Caller10p,100,{TimingRef9("Turn",1)}),objects |-> Objects10p,
     ledger |-> NewConditionalLedger96(InitialSnapshot10p),registry |-> InitialRegistry10p,used |-> 1..5,
     departures |-> [key \in {<<"Movement",90>>} |-> [source |-> 9,objectiveCompletionLeft |-> FALSE,uninstalled |-> TRUE,hostRemoved |-> TRUE,children |-> {1}]],
     targetSites |-> [s \in CentralTargetSites4 \cup {"r1"} |-> [kind |-> IF s \in CentralTargetSites4 THEN "SchemaAtom033" ELSE "SchemaAtom132"]],
     layout |-> [slots |-> Empty10p,orders |-> [s \in {"r1"} |-> <<>>]],
     capacity |-> [siteInspectionId |-> 8,admittedRoots |-> {},pendingRoots |-> {},deniedRoots |-> {}],
     conversions |-> [id \in {4} |-> [mode |-> "Counter",card |-> "Specimen0046",owner |-> "SideA",createdBy |-> 55,gained |-> [kind |-> "SchemaAtom043"]]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, TimingRef9, block10, NewCheckpoint103, Caller10p, Empty10p, InitialRegistry10p, InitialSnapshot10p, Objects10p, q10p, CentralTargetSites4

InitialRegistry10p · operator

reference-profile · input revision 2 · CC0 1.0

InitialRegistry10p == [NewLingeringRegistry910 EXCEPT !.effects=[id \in {9} |-> [kind |-> "Ordinary",status |-> "Expired"]],!.usedEffects={9}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewLingeringRegistry910

InitialSnapshot10p · operator

reference-profile · input revision 2 · CC0 1.0

InitialSnapshot10p ==
 [id |-> 100,point |-> "BeforeCheckpoint",checkpointId |-> 0,definitions |-> Empty10p,present |-> {},
  objects |-> Objects10p,points |-> [p \in SetupPlayers |-> 0],holds |-> Empty10p,effects |-> Empty10p,
  activity |-> [instances |-> Empty10p],activationEpoch |-> Empty10p,activationSerial |-> 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Empty10p, Objects10p, SetupPlayers

Legal10p · operator

reference-profile · input revision 2 · CC0 1.0

Legal10p(selected) == selected={}

Exact module download · Source bundle and reproduction instructions

Next10p · operator

reference-profile · input revision 2 · CC0 1.0

Next10p == ActiveWork10p \/ (q10p.frame.returned /\ UNCHANGED vars10p)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActiveWork10p, vars10p, q10p

Objects10p · operator

reference-profile · input revision 2 · CC0 1.0

Objects10p == [id \in 1..5 |->
 CASE id=1 -> CheckpointObject103("NeutralValue00007","Play",FALSE,0)
   [] id=2 -> CheckpointCounter103("SchemaAtom043","Play",1)
   [] id=3 -> CheckpointCounter103("Power","Play",2)
   [] id=4 -> [CheckpointCounter103("SchemaAtom043","SideADiscard",0) EXCEPT !.card="Specimen0046"]
   [] OTHER -> CheckpointCounter103("SchemaAtom180","SideBDiscard",0)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointCounter103, CheckpointObject103

Position10p · operator

reference-profile · input revision 2 · CC0 1.0

Position10p ==
 /\ CheckpointPositionCleanup103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.layout,q10p.layout,"NoValue",Empty10p,q10p.frame.snapshotId)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointPositionCleanup103, Empty10p, q10p

Processing10p · operator

reference-profile · input revision 2 · CC0 1.0

Processing10p == [InitialSnapshot10p EXCEPT !.point="ProcedureCodee605a78f5d5e",!.checkpointId=1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitialSnapshot10p

Recognition10p · operator

reference-profile · input revision 2 · CC0 1.0

Recognition10p == [route |-> "Ordinary",cp |-> CP10p,definitions |-> Empty10p,lexemes |-> Empty10p,
 conditions |-> Empty10p,allocation |-> Empty10p,bindings |-> Empty10p,departures |-> Empty10p,holds |-> Empty10p,
 usedWindows |-> {},cardFacts |-> CardFacts10]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CP10p, Empty10p, CardFacts10

Recognize10p · operator

reference-profile · input revision 2 · CC0 1.0

Recognize10p ==
 LET ledger==[q10p.ledger EXCEPT !.lastCheckpoint=1,!.checkpointIds={1},!.checkpoints=[id \in {1} |-> [caller |-> Caller10p]],
                !.serial=1,!.lastSnapshot=Processing10p]
     frame==[CheckpointNextFrame103(q10p.frame,100) EXCEPT !.recognition=CP10p,!.recognized=Empty10p]
 IN /\ RecognizeCheckpoint103(q10p.frame,frame,q10p.ledger,ledger,<<>>,<<>>,Recognition10p)
    /\ q10p'=[q10p EXCEPT !.frame=frame,!.ledger=ledger]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, RecognizeCheckpoint103, CP10p, Caller10p, Empty10p, Processing10p, Recognition10p, q10p

Restore10p · operator

reference-profile · input revision 2 · CC0 1.0

Restore10p ==
 LET objects==[q10p.objects EXCEPT ![4].form="Card",![4].kind="Plan",![4].properties=CheckpointPrinted103["Specimen0046"]]
 IN /\ CheckpointRestoreDiscard103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.objects,objects,q10p.conversions,Empty10p,CheckpointPrinted103,q10p.frame.snapshotId)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),!.objects=objects,!.conversions=Empty10p]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointPrinted103, CheckpointRestoreDiscard103, Empty10p, q10p

Return10p · operator

reference-profile · input revision 2 · CC0 1.0

Return10p ==
 /\ ReturnCheckpointWithoutReaction103(q10p.frame,[q10p.frame EXCEPT !.phase="Returned",!.returned=TRUE],q10p.ledger,
       World10p(q10p),PersistentCheckpointCompletion912(q10p.ledger,CP10p,World10p(q10p)),Caller10p)
 /\ q10p'=[q10p EXCEPT !.frame.phase="Returned",!.frame.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointCompletion912, ReturnCheckpointWithoutReaction103, CP10p, Caller10p, World10p, q10p

Root10p · operator

reference-profile · input revision 2 · CC0 1.0

Root10p ==
 /\ CheckpointRootAdmissions103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.capacity,q10p.capacity,
       [id |-> 0,active |-> FALSE,complete |-> FALSE,targetSite |-> "NoValue"],q10p.objects,Empty10p,0,10,{},"NoValue",q10p.frame.snapshotId)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointRootAdmissions103, Empty10p, q10p

Safety10p · operator

reference-profile · input revision 2 · CC0 1.0

Safety10p ==
 /\ block10=3 /\ q10p.frame.done \subseteq CheckpointStageSet103
 /\ ("ProcedureCodeb681cc249a04" \in q10p.frame.done => DOMAIN q10p.registry.effects={})
 /\ ("ProcedureCode2d73b20aa788" \in q10p.frame.done => {1,2,3} \cap DOMAIN q10p.objects={})
 /\ ("ProcedureCode0811ebc5f40e" \in q10p.frame.done => q10p.objects[4].form="Card" /\ 5 \notin DOMAIN q10p.objects)
 /\ (q10p.frame.returned => q10p.frame.done=CheckpointStageSet103 /\ q10p.frame.hostPasses=3 /\ DOMAIN q10p.objects={4,11})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block10, CheckpointStageSet103, q10p

Spec10p · operator

reference-profile · input revision 2 · CC0 1.0

Spec10p == Init10p /\ [][Next10p]_vars10p /\ WF_vars10p(ActiveWork10p)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActiveWork10p, Init10p, Next10p, vars10p

Unique10p · operator

reference-profile · input revision 2 · CC0 1.0

Unique10p ==
 /\ CheckpointUniqueRetire103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.objects,q10p.objects,
       [id \in DOMAIN q10p.objects |-> q10p.objects[id].card],{},{},{},[id \in DOMAIN q10p.objects |-> "SideB"],Empty10p,
       Empty10p,q10p.used,CheckpointPrinted103,CheckpointOwners103,{},100)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointOwners103, CheckpointPrinted103, CheckpointUniqueRetire103, Empty10p, q10p

Victory10p · operator

reference-profile · input revision 2 · CC0 1.0

Victory10p ==
 /\ CheckpointVictory103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.objects,[id \in DOMAIN q10p.objects |-> 0],100)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointNextFrame103, CheckpointVictory103, q10p

Work10p · operator

reference-profile · input revision 2 · CC0 1.0

Work10p ==
 /\ q10p.frame.phase#"Returned"
 /\ CASE q10p.frame.point="ProcedureCodee605a78f5d5e" -> Recognize10p [] q10p.frame.point="ProcedureCode88eda145024f" -> Cleanup10p
     [] q10p.frame.point="ProcedureCodeb681cc249a04" -> Victory10p [] q10p.frame.point="ProcedureCodefe50c31480ea" -> Unique10p
     [] q10p.frame.point="ProcedureCodea488e1ba6ca3" -> Illegal10p [] q10p.frame.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} -> Hosted10p
     [] q10p.frame.point="ProcedureCode2d73b20aa788" -> AuxiliarySite10p [] q10p.frame.point="ProcedureCode2d6279f9d639" -> Position10p
     [] q10p.frame.point="ProcedureCode7f181ce21011" -> Root10p [] q10p.frame.point="ProcedureCodeda83a77a1f12" -> Restore10p
     [] q10p.frame.point="ProcedureCode0811ebc5f40e" -> Counters10p [] q10p.frame.point="ProcedureCodeb74d673a0fc6" -> Return10p [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AuxiliarySite10p, Cleanup10p, Counters10p, Hosted10p, Illegal10p, Position10p, Recognize10p, Restore10p, Return10p, Root10p, Unique10p, Victory10p, q10p

World10p · operator

reference-profile · input revision 2 · CC0 1.0

World10p(q) == [id |-> q.frame.snapshotId,objects |-> q.objects,points |-> [p \in SetupPlayers |-> 0],
 present |-> {},activity |-> [instances |-> Empty10p]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Empty10p, SetupPlayers

vars10p · operator

reference-profile · input revision 2 · CC0 1.0

vars10p == <<q10p,block10>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block10, q10p

q10p · variable

reference-profile · input revision 2 · CC0 1.0

q10p

Exact module download · Source bundle and reproduction instructions