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

ActionAdapters¶

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.

trigger · operator

reference-profile · input revision 2 · CC0 1.0

trigger==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
       allTriggerCostsPaid |-> AActionPaid(q),costCheckpointAndReactionsDrained |-> AActionCostDrained(q,ACostCaller(q))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: w, AActionCostDrained, AActionPaid, ACostCaller

w · operator

reference-profile · input revision 2 · CC0 1.0

w==WindowTop9(q.stack)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9

bodyComplete · operator

reference-profile · input revision 2 · CC0 1.0

bodyComplete==p.ability.complete /\ q.childPlan.phase="Complete" /\ q.childPlan.completedSteps=q.childPlan.steps /\ p.id \in q.noUseChildren

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p

drained · operator

reference-profile · input revision 2 · CC0 1.0

drained==CheckpointDrained103(q.frames[p.checkpoint],q.ledger,q.stack)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p, CheckpointDrained103

noTriggerCost · operator

reference-profile · input revision 2 · CC0 1.0

noTriggerCost==~(\E u \in {p.definition.syntax.units[i] : i \in 1..Len(p.definition.syntax.units)} : u.category="SchemaAtom043" /\ u.subtype="Cost")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p

p · operator

reference-profile · input revision 2 · CC0 1.0

p==q.child

Exact module download · Source bundle and reproduction instructions

payment · operator

reference-profile · input revision 2 · CC0 1.0

payment==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> p.transaction,
        allTriggerCostsPaid |-> noTriggerCost,costCheckpointAndReactionsDrained |-> drained]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: drained, noTriggerCost, p, w

w · operator

reference-profile · input revision 2 · CC0 1.0

w==WindowTop9(q.stack)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9

s · operator

reference-profile · input revision 2 · CC0 1.0

s==ProtocolP!Syntax9p(301,"Conditional","ActionCompletionReactionControl")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Syntax9p

s · operator

reference-profile · input revision 2 · CC0 1.0

s==ProtocolP!Syntax9p(300,"Conditional","ActionCostReactionControl")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Syntax9p

chosen · operator

reference-profile · input revision 2 · CC0 1.0

chosen==CHOOSE candidate \in DOMAIN f.recognized : TRUE

Exact module download · Source bundle and reproduction instructions

d · operator

reference-profile · input revision 2 · CC0 1.0

d==q.ledger.instances[chosen].definitionCopy

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: chosen

A2Permissions · operator

reference-profile · input revision 2 · CC0 1.0

A2Permissions(scenario) == CASE scenario="cost-reaction" -> APermissions
 [] scenario="completion-reaction" -> RPermissions \cup {"ActionCompletionReactionControl"} [] OTHER -> RPermissions

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: APermissions, RPermissions

AActionCostDrained · operator

reference-profile · input revision 2 · CC0 1.0

AActionCostDrained(q,caller) ==
 IF q.costCP=0 THEN FALSE ELSE
 /\ caller=ACostCaller(q) /\ q.frames[q.costCP].caller=caller
 /\ CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack) /\ ANativeCommitted(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACostCaller, ANativeCommitted, CheckpointDrained103

AActionPaid · operator

reference-profile · input revision 2 · CC0 1.0

AActionPaid(q) ==
 /\ AReservation(q) /\ ANativeCommitted(q) /\ AActionCostDrained(q,ACostCaller(q))
 /\ q.actionPointWorld=[q.payment.after EXCEPT !.checkpointDue=FALSE] /\ q.costDrained

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AActionCostDrained, ACostCaller, ANativeCommitted, AReservation

AActionReturn · operator

reference-profile · input revision 2 · CC0 1.0

AActionReturn(q) ==
 LET w==WindowTop9(q.stack)
     trigger==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
       allTriggerCostsPaid |-> AActionPaid(q),costCheckpointAndReactionsDrained |-> AActionCostDrained(q,ACostCaller(q))]
 IN [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
  triggerPayment |-> trigger,allCostsPaid |-> AActionPaid(q),optionComplete |-> ActionReadyToContinue5(q.action),
  childrenReturned |-> "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete,
  reactionsDrained |-> AActionCostDrained(q,ACostCaller(q)) /\ "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: trigger, w, AActionCostDrained, AActionPaid, ACostCaller, ActionReadyToContinue5

AAddCapture · operator

reference-profile · input revision 2 · CC0 1.0

AAddCapture(q,snapshot) == AJoin(q.captures,[key \in {<<snapshot.id,snapshot.point>>} |-> ACapture(q,snapshot)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACapture, AJoin

AAdmit · operator

reference-profile · input revision 2 · CC0 1.0

AAdmit(q,ledger,snapshot) == AdmitConditionalSnapshotSA(q.catalog,ABasis(q),ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
 ATemplate(q,snapshot.id,snapshot.point,snapshot.checkpointId),snapshot,MinimalCaptureSA(ABasis(q)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitConditionalSnapshotSA, MinimalCaptureSA, ABasis, ATemplate

ABasis · operator

reference-profile · input revision 2 · CC0 1.0

ABasis(q) == BasisSA(q.abilityRevision,q.abilityRegistry,q.objects,q.rulePermissions)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA

ACapture · operator

reference-profile · input revision 2 · CC0 1.0

ACapture(q,snapshot) == [basis |-> MinimalCaptureSA(ABasis(q)),snapshot |-> snapshot]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, ABasis

ACaptureFrame · operator

reference-profile · input revision 2 · CC0 1.0

ACaptureFrame(before,after) ==
 /\ DOMAIN before.captures \subseteq DOMAIN after.captures
 /\ \A key \in DOMAIN before.captures : after.captures[key]=before.captures[key]

Exact module download · Source bundle and reproduction instructions

ACatalog · operator

reference-profile · input revision 2 · CC0 1.0

ACatalog == AJoin(AJoin(RCatalog(0),[id \in {3} |-> [kind |-> "Conditional",nativeId |-> 300,
 source |-> ACostDefinition.syntax.source,definition |-> ACostDefinition]]),
 [id \in {4} |-> [kind |-> "Conditional",nativeId |-> 301,source |-> ACompletionDefinition.syntax.source,definition |-> ACompletionDefinition]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACompletionDefinition, ACostDefinition, AJoin, RCatalog

AChildReturnReceipt · operator

reference-profile · input revision 2 · CC0 1.0

AChildReturnReceipt(q) ==
 LET w==WindowTop9(q.stack) p==q.child
     drained==CheckpointDrained103(q.frames[p.checkpoint],q.ledger,q.stack)
     noTriggerCost==~(\E u \in {p.definition.syntax.units[i] : i \in 1..Len(p.definition.syntax.units)} : u.category="SchemaAtom043" /\ u.subtype="Cost")
     bodyComplete==p.ability.complete /\ q.childPlan.phase="Complete" /\ q.childPlan.completedSteps=q.childPlan.steps /\ p.id \in q.noUseChildren
     payment==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> p.transaction,
        allTriggerCostsPaid |-> noTriggerCost,costCheckpointAndReactionsDrained |-> drained]
 IN [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> p.transaction,
   triggerPayment |-> payment,allCostsPaid |-> noTriggerCost /\ bodyComplete,optionComplete |-> bodyComplete,
   childrenReturned |-> drained,reactionsDrained |-> drained,finalCheckpointId |-> p.checkpoint]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: bodyComplete, drained, noTriggerCost, p, payment, w

ACompletionCommitted · operator

reference-profile · input revision 2 · CC0 1.0

ACompletionCommitted(q) ==
 IF q.nativeCompletion=EmptyT11 THEN FALSE ELSE
 /\ q.completionCommitCount=1 /\ q.nativeCompletion.operationId=2
 /\ q.nativeCompletion.before.status="Effects" /\ q.nativeCompletion.after=[q.nativeCompletion.before EXCEPT !.status="Complete"]
 /\ q.nativeCompletion.after=q.action /\ q.nativeCompletion.windowId=q.NeutralValue00003.opened.id
 /\ q.nativeCompletion.turnId=q.flow.turn.id /\ q.nativeCompletion.phaseId=q.actionPhaseId
 /\ q.completionEvent.nativeCompletion=q.nativeCompletion /\ q.completionEvent.rawEvent=[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]
 /\ q.rawEvents[q.nativeCompletion.rawIndex]={q.completionEvent.rawEvent}
 /\ q.completionOccurrence.actualEvent=q.completionEvent /\ q.completionOccurrence.nativeCompletion=q.nativeCompletion

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11

ACompletionDefinition · operator

reference-profile · input revision 2 · CC0 1.0

ACompletionDefinition ==
 LET s==ProtocolP!Syntax9p(301,"Conditional","ActionCompletionReactionControl")
 IN [ACostDefinition EXCEPT !.syntax=s,!.activity=AbilityDefinition9(301,"Conditional",s.source,"Printed"),
  !.instructions= <<721>>,!.trigger.kinds={"OriginalActionCompletes"},!.partsByInstruction=[i \in {721} |-> {1}]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityDefinition9, s, ACostDefinition

ACostCaller · operator

reference-profile · input revision 2 · CC0 1.0

ACostCaller(q) == [kind |-> "ActionTriggerCost",actionId |-> q.action.id,windowId |-> q.payment.window,
 transactionId |-> q.payment.transaction,turnId |-> q.flow.turn.id]

Exact module download · Source bundle and reproduction instructions

ACostDefinition · operator

reference-profile · input revision 2 · CC0 1.0

ACostDefinition ==
 LET s==ProtocolP!Syntax9p(300,"Conditional","ActionCostReactionControl")
 IN [RChildDefinition EXCEPT !.syntax=s,!.activity=AbilityDefinition9(300,"Conditional",s.source,"Printed"),
  !.instructions= <<720>>,!.trigger.kinds={"ActionActionPointCostPaid"},!.partsByInstruction=[i \in {720} |-> {1}]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityDefinition9, s, RChildDefinition

ADefinitions · operator

reference-profile · input revision 2 · CC0 1.0

ADefinitions(q) == ConditionalDefinitionsSA(q.abilityRegistry)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionsSA

AInside · operator

reference-profile · input revision 2 · CC0 1.0

AInside(q) == {TimingRef9("Turn",q.flow.turn.id),TimingRef9("TurnPhase",q.actionPhaseId)} \cup
 (IF TraversalTimingPresent6(q.control.traversal) THEN {TimingRef9("SchemaAtom138",q.control.traversal.id)} ELSE {}) \cup
 (IF IInsideInspectionT11(q) THEN {TimingRef9("Inspection",IBT11(q).id)} ELSE {}) \cup
 (IF IInsideItemInspectionT11(q) THEN {TimingRef9("ItemInspection",IAT11(q).id)} ELSE {})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, IAT11, IBT11, IInsideInspectionT11, IInsideItemInspectionT11, TraversalTimingPresent6

AInspection · operator

reference-profile · input revision 2 · CC0 1.0

AInspection(q) == IF IInsideInspectionT11(q) THEN IBT11(q) ELSE [active |-> FALSE,complete |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IBT11, IInsideInspectionT11

AInstanceDefinition · operator

reference-profile · input revision 2 · CC0 1.0

AInstanceDefinition(id) == IF id=301 THEN ACostDefinition ELSE ACompletionDefinition

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACompletionDefinition, ACostDefinition

AInstanceWindow · operator

reference-profile · input revision 2 · CC0 1.0

AInstanceWindow(id) == IF id=301 THEN 20 ELSE 21

Exact module download · Source bundle and reproduction instructions

AJoin · operator

reference-profile · input revision 2 · CC0 1.0

AJoin(base,extra) == RJoin(base,extra)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RJoin

ALatchAfterSteps · operator

reference-profile · input revision 2 · CC0 1.0

ALatchAfterSteps(q) ==
 /\ "AE" \in q.stepConsumed /\ q.stepContinuations["AE"].after=q.flow
 /\ q.stepReturnReceipts["AE"].checkpointId=q.stepCP["AE"]
 /\ CheckpointDrained103(q.frames[q.stepCP["AE"]],q.ledger,q.stack)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103

ANativeCommitted · operator

reference-profile · input revision 2 · CC0 1.0

ANativeCommitted(q) ==
 IF q.native=EmptyT11 THEN FALSE ELSE
 /\ q.native.operationId=1 /\ q.native.command=IActionPointCommandT11
 /\ q.native.before=IActionPointWorldT11 /\ q.native.after=IActionPointAfterT11(q.native.before)
 /\ q.native.payment=q.payment /\ q.payment.before=q.native.before /\ q.payment.after=q.native.after
 /\ q.native.actionId=q.action.id /\ q.native.turnId=q.flow.turn.id
 /\ q.payment.transaction=200 /\ q.payment.option=IActionOptionT11
 /\ q.payment.window=q.NeutralValue00003.opened.id /\ q.native.after.event="SpendActionPoints"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IActionOptionT11, IActionPointAfterT11, IActionPointCommandT11, IActionPointWorldT11, EmptyT11

ANativeObjects · operator

reference-profile · input revision 2 · CC0 1.0

ANativeObjects == IInitialT11.objects

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IInitialT11

ANativeProjection · operator

reference-profile · input revision 2 · CC0 1.0

ANativeProjection(objects) == [id \in DOMAIN ANativeObjects |-> [field \in DOMAIN ANativeObjects[id] |-> objects[id][field]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ANativeObjects

AObjects · operator

reference-profile · input revision 2 · CC0 1.0

AObjects == [id \in DOMAIN ANativeObjects |-> AJoin(ANativeObjects[id],
 [virtual |-> FALSE,properties |-> [kind |-> ANativeObjects[id].kind],area |-> "NoValue",targetSite |-> "NoValue"])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AJoin, ANativeObjects

AOwners · operator

reference-profile · input revision 2 · CC0 1.0

AOwners == [card \in {"SyntheticItemInspectionPhysical1"} |-> "SideA"]

Exact module download · Source bundle and reproduction instructions

APermissions · operator

reference-profile · input revision 2 · CC0 1.0

APermissions == RPermissions \cup {"ActionCostReactionControl"}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RPermissions

APlacement · operator

reference-profile · input revision 2 · CC0 1.0

APlacement(q,role) ==
 /\ q.stack= <<>> /\ q.flow.step=AStepName(role) /\ q.action.status="Complete"
 /\ IF role="AF" THEN "AF" \in DOMAIN q.poppedWindows /\ q.poppedWindows["AF"]=q.closedWindows["AF"] /\ ACompletionCommitted(q)
    ELSE IF role="AE" THEN "AE" \in DOMAIN q.poppedWindows /\ q.poppedWindows["AE"]=q.closedWindows["AE"]
    ELSE "AF" \in q.stepConsumed

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACompletionCommitted, AStepName

APrinted · operator

reference-profile · input revision 2 · CC0 1.0

APrinted == [card \in {"SyntheticItemInspectionPhysical1"} |-> [kind |-> "Plan"]]

Exact module download · Source bundle and reproduction instructions

AReactionContext · operator

reference-profile · input revision 2 · CC0 1.0

AReactionContext(q,f) ==
 LET chosen==CHOOSE candidate \in DOMAIN f.recognized : TRUE d==q.ledger.instances[chosen].definitionCopy
 IN [instanceId |-> chosen,definition |-> d,windowId |-> f.recognized[chosen].windowId,transaction |-> 2600+chosen-301,
  instructionId |-> d.instructions[1],work |-> IF chosen=301 THEN "ActionCostReaction" ELSE "ActionCompletionReaction"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: chosen, d

AReactionSite · operator

reference-profile · input revision 2 · CC0 1.0

AReactionSite(q) == IF Len(q.stack)=0 THEN ITurnSiteT11(q) ELSE WindowTop9(q.stack).site

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, ITurnSiteT11

ARequireStep · operator

reference-profile · input revision 2 · CC0 1.0

ARequireStep(q,role,f,flow) ==
 /\ role \notin q.stepConsumed /\ role \in DOMAIN q.stepReturnReceipts
 /\ flow=q.flow /\ AStepDrained(q,role,f)
 /\ q.stepReturnReceipts[role]=AStepReceipt(q,role,f,q.revision)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepDrained, AStepReceipt

AReservation · operator

reference-profile · input revision 2 · CC0 1.0

AReservation(q) ==
 /\ Len(q.stack)=1 /\ q.NeutralValue00003.ready=PriorityReadyT11(q.NeutralValue00003.opened)
 /\ q.NeutralValue00003.ready.site=[ITurnSiteT11(q) EXCEPT !.actionPoints=q.NeutralValue00003.opened.site.actionPoints]
 /\ q.NeutralValue00003.ready.kind="NeutralValue00001" /\ q.NeutralValue00003.option=IActionOptionT11
 /\ WindowTop9(q.stack)=StartPriorityOptionFrame9(q.NeutralValue00003.ready,IActionOptionT11,200)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StartPriorityOptionFrame9, WindowTop9, IActionOptionT11, ITurnSiteT11, PriorityReadyT11

ASnapshot · operator

reference-profile · input revision 2 · CC0 1.0

ASnapshot(q,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,ABasis(q),ledger,ATemplate(q,id,point,checkpoint))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, ABasis, ATemplate

AStepCaller · operator

reference-profile · input revision 2 · CC0 1.0

AStepCaller(q,role,windowId) == [kind |-> "ActionTimingStep",role |-> role,step |-> AStepName(role),
 turnId |-> q.flow.turn.id,phaseId |-> q.actionPhaseId,actionId |-> q.action.id,windowId |-> windowId,transactionId |-> q.payment.transaction]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepName

AStepDrained · operator

reference-profile · input revision 2 · CC0 1.0

AStepDrained(q,role,f) ==
 /\ role \in DOMAIN q.stepEvents /\ q.stepCP[role]>0 /\ f=q.frames[q.stepCP[role]]
 /\ f.caller=AStepCaller(q,role,AStepWindow(q,role)) /\ f.caller=q.stepEvents[role].caller
 /\ f.inside=AInside(q) /\ CheckpointDrained103(f,q.ledger,q.stack)
 /\ q.flow.step=AStepName(role) /\ APlacement(q,role)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInside, APlacement, AStepCaller, AStepName, AStepWindow, CheckpointDrained103

AStepEvent · operator

reference-profile · input revision 2 · CC0 1.0

AStepEvent(q,role,id,windowId,source,complete) == [id |-> id,tag |-> "InstructionFinished",origin |-> "TimingStep",
 instruction |-> AStepName(role),caller |-> AStepCaller(q,role,windowId),source |-> source,complete |-> complete]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepCaller, AStepName

AStepLower · operator

reference-profile · input revision 2 · CC0 1.0

AStepLower(role) == CASE role="AF" -> "af" [] role="AG" -> "ag" [] OTHER -> "ae"

Exact module download · Source bundle and reproduction instructions

AStepName · operator

reference-profile · input revision 2 · CC0 1.0

AStepName(role) == CASE role="AF" -> "ProcedureCode989abc27e0c6" [] role="AG" -> "ProcedureCodea439ce381bba" [] OTHER -> "ProcedureCode484be3e50aa9"

Exact module download · Source bundle and reproduction instructions

AStepReceipt · operator

reference-profile · input revision 2 · CC0 1.0

AStepReceipt(q,role,f,revision) == [checkpointId |-> f.id,caller |-> f.caller,eventId |-> q.stepEvents[role].id,
 flow |-> q.flow,revision |-> revision,worldId |-> f.snapshotId,basis |-> MinimalCaptureSA(ABasis(q))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, ABasis

AStepRoles · operator

reference-profile · input revision 2 · CC0 1.0

AStepRoles == {"AF","AG","AE"}

Exact module download · Source bundle and reproduction instructions

AStepStage · operator

reference-profile · input revision 2 · CC0 1.0

AStepStage(role) == CASE role="AF" -> "TurnAdvance" [] role="AG" -> "TurnLoop" [] OTHER -> "TurnContinue"

Exact module download · Source bundle and reproduction instructions

AStepWindow · operator

reference-profile · input revision 2 · CC0 1.0

AStepWindow(q,role) == IF role="AE" THEN q.poppedWindows["AE"].id ELSE q.NeutralValue00003.opened.id

Exact module download · Source bundle and reproduction instructions

ATemplate · operator

reference-profile · input revision 2 · CC0 1.0

ATemplate(q,id,point,checkpoint) == [q.ledger.lastSnapshot EXCEPT !.id=id,!.point=point,!.checkpointId=checkpoint]

Exact module download · Source bundle and reproduction instructions

AWorld · operator

reference-profile · input revision 2 · CC0 1.0

AWorld(q,f) == [id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,
 present |-> ConditionalPresentSA(q.abilityRegistry),activity |-> CommonActivitySA(ABasis(q),q.ledger)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CommonActivitySA, ConditionalPresentSA, ABasis, ZeroCountsT11

AWorldBound · operator

reference-profile · input revision 2 · CC0 1.0

AWorldBound(q,f,world) ==
 /\ BasisValidSA(q.catalog,ABasis(q)) /\ LedgerDomainSA(q.ledger)
 /\ UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)
 /\ world=AWorld(q,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, LedgerDomainSA, UseProvenanceValidSA, ABasis, AWorld