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

ActionCompositionMC¶

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.

a · operator

reference-profile · input revision 2 · CC0 1.0

a==NewAction5(30,"SideB",BasicActionKey5("SideB","SchemaAtom138"))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasicActionKey5, NewAction5

after · operator

reference-profile · input revision 2 · CC0 1.0

after==IActionPointAfterT11(q.actionPointWorld)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, IActionPointAfterT11

committed · operator

reference-profile · input revision 2 · CC0 1.0

committed==[q EXCEPT !.actionPointWorld=after,!.payment=payment,!.action=a,!.native=native]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: a, after, native, payment, q

event · operator

reference-profile · input revision 2 · CC0 1.0

event==[id |-> 1,tag |-> "CostPaid",caller |-> ACostCaller(committed),transactionId |-> 200,
       operationId |-> 1,nativePayment |-> native,complete |-> ANativeCommitted(committed)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACostCaller, ANativeCommitted, committed, native

native · operator

reference-profile · input revision 2 · CC0 1.0

native==[operationId |-> 1,command |-> IActionPointCommandT11,before |-> q.actionPointWorld,after |-> after,payment |-> payment,actionId |-> a.id,turnId |-> q.flow.turn.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: a, after, payment, q, IActionPointCommandT11

occurrence · operator

reference-profile · input revision 2 · CC0 1.0

occurrence==[id |-> 1,kind |-> "ActionActionPointCostPaid",object |-> 0,actor |-> "SideB",side |-> "SideB",
       snapshot |-> snapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(ACostDefinition),
       actualEvent |-> event,nativeOperation |-> native,turnId |-> q.flow.turn.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, ACostDefinition, event, native, q, snapshot

payment · operator

reference-profile · input revision 2 · CC0 1.0

payment==[before |-> q.actionPointWorld,after |-> after,window |-> WindowTop9(q.stack).id,option |-> IActionOptionT11,transaction |-> 200]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, after, q, IActionOptionT11

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

snapshot · operator

reference-profile · input revision 2 · CC0 1.0

snapshot==ASnapshot(committed,q.ledger,q.nextWorld,"ActionPaymentOccurrence",q.ledger.lastCheckpoint)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ASnapshot, committed, q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.flow EXCEPT !.step=CASE role="AF" -> "ProcedureCodea439ce381bba" [] role="AG" -> "ProcedureCode484be3e50aa9" [] OTHER -> "ProcedureCode989abc27e0c6",!.decision="NoValue"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

event · operator

reference-profile · input revision 2 · CC0 1.0

event==AStepEvent(g,"AG",q.nextEvent,q.NeutralValue00003.opened.id,source,after.step="ProcedureCodea439ce381bba" /\ "AF" \in next.stepConsumed)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepEvent, after, g, next, q, source

f · operator

reference-profile · input revision 2 · CC0 1.0

f==q.frames[q.stepCP[role]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

g · operator

reference-profile · input revision 2 · CC0 1.0

g==IRecordT11(next,"ProcedureCodea439ce381bba",{},"TurnLoop")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: next, IRecordT11

next · operator

reference-profile · input revision 2 · CC0 1.0

next==[q EXCEPT !.flow=after,!.stepConsumed=@ \cup {role},
       !.stepContinuations=AJoin(@,[key \in {role} |-> [before |-> q.flow,after |-> after,receipt |-> q.stepReturnReceipts[role]]]),
       !.lifecycle=Append(@,ALife(q,"StepConsume",role,f.id,0)),!.stage=IF role="AF" THEN "Drain" ELSE IF role="AG" THEN "OpenPR" ELSE "LatchNew"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AJoin, after, f, q, ALife

proof · operator

reference-profile · input revision 2 · CC0 1.0

proof==ARequireStep(q,role,suppliedFrame,suppliedFlow)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ARequireStep, q, suppliedFlow, suppliedFrame

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

source · operator

reference-profile · input revision 2 · CC0 1.0

source==[kind |-> "NativeStepAdvance",before |-> q.flow,after |-> after,from |-> role,checkpointId |-> f.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, f, q

suppliedFlow · operator

reference-profile · input revision 2 · CC0 1.0

suppliedFlow==IF role="AG" /\ AMutation="stale-ag-flow" THEN [q.flow EXCEPT !.step="ProcedureCode989abc27e0c6"] ELSE q.flow

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, AMutation

suppliedFrame · operator

reference-profile · input revision 2 · CC0 1.0

suppliedFrame==IF AMutation="unreturned-" \o AStepLower(role) THEN [f EXCEPT !.returned=FALSE,!.phase="Completed"] ELSE f

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepLower, f, AMutation

f · operator

reference-profile · input revision 2 · CC0 1.0

f==AFrame(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, AFrame

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

returned · operator

reference-profile · input revision 2 · CC0 1.0

returned==[f EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f

world · operator

reference-profile · input revision 2 · CC0 1.0

world==AWorld(q,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AWorld, f, q

b · operator

reference-profile · input revision 2 · CC0 1.0

b==ASnapshot(q,q.ledger,f.snapshotId,"CheckpointBeginning",f.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ASnapshot

rest · operator

reference-profile · input revision 2 · CC0 1.0

rest==SubSeq(f.owed,2,Len(f.owed))

Exact module download · Source bundle and reproduction instructions

cp · operator

reference-profile · input revision 2 · CC0 1.0

cp==q.recognitionHistory[id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[next EXCEPT !.recognition=cp,!.recognized=CheckpointMemberMap103(ledger,f.id)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cp, f, ledger, next, CheckpointMemberMap103

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[f EXCEPT !.phase="Reaction",!.windowId=context.windowId]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: context, f

allocation · operator

reference-profile · input revision 2 · CC0 1.0

allocation==[k \in IF AMutation="omit-cost-recognition" /\ q.cpRole="ActionCost" THEN {} ELSE eligible |->
          IF k.definition=ConditionalKey96(ACostDefinition) THEN 301 ELSE 302]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, ACostDefinition, eligible, q, AMutation

bindings · operator

reference-profile · input revision 2 · CC0 1.0

bindings==[k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> AInstanceWindow(allocation[k]),group |-> 4]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInstanceWindow, allocation, cp

cleanup · operator

reference-profile · input revision 2 · CC0 1.0

cleanup==[tag |-> "LingeringCheckpointCleanup",frame |-> cursor,expired |-> {},complete |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: cursor

conditions · operator

reference-profile · input revision 2 · CC0 1.0

conditions==[k \in DOMAIN ADefinitions(q) |-> [id \in DOMAIN cp.occurrences |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> ADefinitions(q)[k].syntax.id,source |-> ADefinitions(q)[k].syntax.source,
          occurrence |-> id,snapshotId |-> cp.occurrences[id].snapshot.id,results |-> EmptyT11]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ADefinitions, cp, q, EmptyT11

context · operator

reference-profile · input revision 2 · CC0 1.0

context==AReactionContext(q,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AReactionContext, f, q

cp · operator

reference-profile · input revision 2 · CC0 1.0

cp==ACPData(q,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f, q, ACPData

cursor · operator

reference-profile · input revision 2 · CC0 1.0

cursor==LingeringCheckpointFrame910(q.ledger,f.recognition,world)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LingeringCheckpointFrame910, f, q, world

eligible · operator

reference-profile · input revision 2 · CC0 1.0

eligible=={k \in keys : TriggerPattern96(ADefinitions(q)[k.definition],cp.occurrences[k.occurrence])}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TriggerPattern96, ADefinitions, cp, keys, q

f · operator

reference-profile · input revision 2 · CC0 1.0

f==AFrame(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, AFrame

keys · operator

reference-profile · input revision 2 · CC0 1.0

keys=={[definition |-> key,occurrence |-> id] : key \in {k \in DOMAIN ADefinitions(q) :
         ConditionalActive96(ADefinitions(q)[k],cp.processingSnapshot)},id \in DOMAIN cp.occurrences}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ADefinitions, cp, q

ledger · operator

reference-profile · input revision 2 · CC0 1.0

ledger==ProtocolP!CPAfter9p(q.ledger,cp,allocation,bindings)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: allocation, bindings, cp, q, ProtocolP!CPAfter9p

members · operator

reference-profile · input revision 2 · CC0 1.0

members==f.recognized

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f

next · operator

reference-profile · input revision 2 · CC0 1.0

next==ACPNext(f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f, ACPNext

opening · operator

reference-profile · input revision 2 · CC0 1.0

opening==AJoin(IOpeningT11(context.windowId,"Reaction",site),
           [members |-> DOMAIN members,instances |-> members,group |-> 4,modifiersExist |-> FALSE,
            preparation |-> <<"ConditionsMet","PendingGroup">>,checkpointId |-> f.id,caller |-> f.caller,
            completion |-> PersistentCheckpointCompletion912(q.ledger,f.recognition,world)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointCompletion912, AJoin, context, f, members, q, site, world, IOpeningT11

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

registry · operator

reference-profile · input revision 2 · CC0 1.0

registry==[q.registry EXCEPT !.cleanupIds=@ \cup {f.id}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f, q

returned · operator

reference-profile · input revision 2 · CC0 1.0

returned==[f EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f

site · operator

reference-profile · input revision 2 · CC0 1.0

site==AReactionSite(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AReactionSite, q

snapshot · operator

reference-profile · input revision 2 · CC0 1.0

snapshot==ASnapshot(q,q.ledger,f.snapshotId,"CleanupCurrent",f.id)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ASnapshot, f, q

window · operator

reference-profile · input revision 2 · CC0 1.0

window==NewPriorityWindow9(context.windowId,"Reaction",site,members,4,NoTimingRef9,[id |-> 0],0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, context, members, site

world · operator

reference-profile · input revision 2 · CC0 1.0

world==AWorld(q,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AWorld, f, q

x · operator

reference-profile · input revision 2 · CC0 1.0

x==[route |-> "Ordinary",cp |-> cp,definitions |-> ADefinitions(q),lexemes |-> ALexemes(q),conditions |-> conditions,
         allocation |-> allocation,bindings |-> bindings,departures |-> EmptyT11,holds |-> EmptyT11,
         usedWindows |-> q.usedWindows,cardFacts |-> CardFacts10]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ADefinitions, allocation, bindings, conditions, cp, q, ALexemes, EmptyT11, CardFacts10

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.action EXCEPT !.status="Complete"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

completed · operator

reference-profile · input revision 2 · CC0 1.0

completed==IRecordT11([q EXCEPT !.action=after],"5.7.1f:return",{raw},"TurnAdvance")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, q, raw, IRecordT11

event · operator

reference-profile · input revision 2 · CC0 1.0

event==[id |-> q.nextEvent,tag |-> "OriginalActionCompletes",rawEvent |-> raw,nativeCompletion |-> native]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: native, q, raw

events · operator

reference-profile · input revision 2 · CC0 1.0

events==IF AMutation="repeated-completion-publication" THEN [id \in {event.id,event.id+1} |-> [event EXCEPT !.id=id]] ELSE [id \in {event.id} |-> event]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: event, AMutation

native · operator

reference-profile · input revision 2 · CC0 1.0

native==[operationId |-> 2,before |-> q.action,after |-> after,windowId |-> WindowTop9(q.stack).id,
       turnId |-> q.flow.turn.id,phaseId |-> q.actionPhaseId,rawIndex |-> Len(q.rawEvents)+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, after, q

occurrence · operator

reference-profile · input revision 2 · CC0 1.0

occurrence==[id |-> event.id,kind |-> "OriginalActionCompletes",object |-> 0,actor |-> "SideB",side |-> "SideB",snapshot |-> snapshot,
       scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(ACompletionDefinition),actualEvent |-> event,nativeCompletion |-> native]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, ACompletionDefinition, event, native, snapshot

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

raw · operator

reference-profile · input revision 2 · CC0 1.0

raw==[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

siteEvent · operator

reference-profile · input revision 2 · CC0 1.0

siteEvent==AStepEvent(completed,"AF",event.id,q.NeutralValue00003.opened.id,source,ActionReadyToContinue5(after))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepEvent, after, completed, event, q, source, ActionReadyToContinue5

snapshot · operator

reference-profile · input revision 2 · CC0 1.0

snapshot==ASnapshot(completed,q.ledger,q.nextWorld,"ActionCompletionOccurrence",q.ledger.lastCheckpoint)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ASnapshot, completed, q

source · operator

reference-profile · input revision 2 · CC0 1.0

source==[kind |-> "NativeActionComplete",native |-> native,event |-> event]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: event, native

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.action EXCEPT !.status="Effects"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

cp · operator

reference-profile · input revision 2 · CC0 1.0

cp==q.recognitionHistory[instance.checkpointId]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: instance, q

instance · operator

reference-profile · input revision 2 · CC0 1.0

instance==q.ledger.instances[id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

original · operator

reference-profile · input revision 2 · CC0 1.0

original==NewConditionalInstance96(id,AInstanceDefinition(id),cp,instance.occurrence,AInstanceWindow(id),4)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalInstance96, AInstanceDefinition, AInstanceWindow, cp, instance

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

basis · operator

reference-profile · input revision 2 · CC0 1.0

basis==BasisSA(0,ACatalog,AObjects,permissions)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA, ACatalog, AObjects, permissions

permissions · operator

reference-profile · input revision 2 · CC0 1.0

permissions==A2Permissions(scenario)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: A2Permissions

seed · operator

reference-profile · input revision 2 · CC0 1.0

seed==NewConditionalLedger96(PInitialSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, PInitialSnapshot

snapshot · operator

reference-profile · input revision 2 · CC0 1.0

snapshot==ConditionalSnapshotFromRegistrySA(ACatalog,basis,seed,PInitialSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, ACatalog, basis, seed, PInitialSnapshot

caller · operator

reference-profile · input revision 2 · CC0 1.0

caller==IF role="ActionCost" /\ AMutation="wrong-cost-caller" THEN [originalCaller EXCEPT !.transactionId=201] ELSE originalCaller

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AMutation

event · operator

reference-profile · input revision 2 · CC0 1.0

event==CASE kind="Cost" -> [q.costEvent EXCEPT !.caller=caller]
        [] kind="SchemaAtom126" -> [id |-> q.nextEvent,caller |-> caller,complete |-> WindowTop9(q.stack).stage="NeedCheckpoint",
             tag |-> "PriorityAboutToBeReceived",player |-> WindowTop9(q.stack).priority]
        [] OTHER -> [id |-> q.nextEvent,caller |-> caller,complete |-> q.childPlan.phase="Complete",
             tag |-> "InstructionFinished",origin |-> "Ability",instruction |-> IF q.reactionContext.instanceId=301 THEN "AbilityInstruction720" ELSE "AbilityInstruction721",
             instructionRef |-> InstructionWindowRef93(q.childPlan),finishedPlan |-> q.childPlan]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, WindowTop9, caller, q

frame · operator

reference-profile · input revision 2 · CC0 1.0

frame==NewCheckpoint103(id,caller,worldId,AInside(q))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInside, caller, id, q, worldId, NewCheckpoint103

frames · operator

reference-profile · input revision 2 · CC0 1.0

frames==AJoin(q.frames,[k \in {id} |-> frame])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AJoin, frame, id, q

id · operator

reference-profile · input revision 2 · CC0 1.0

id==q.ledger.lastCheckpoint+1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

site · operator

reference-profile · input revision 2 · CC0 1.0

site==[kind |-> kind,caller |-> caller,eventId |-> event.id,snapshotId |-> worldId,inside |-> AInside(q)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInside, caller, event, q, worldId

worldId · operator

reference-profile · input revision 2 · CC0 1.0

worldId==q.nextWorld

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

caller · operator

reference-profile · input revision 2 · CC0 1.0

caller==IF role="AF" /\ AMutation="wrong-af-caller" THEN [original.caller EXCEPT !.step="ProcedureCodea439ce381bba"]
       ELSE IF role="AE" /\ AMutation="wrong-ae-window" THEN [original.caller EXCEPT !.windowId=@+1] ELSE original.caller

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: original, AMutation

event · operator

reference-profile · input revision 2 · CC0 1.0

event==[original EXCEPT !.caller=caller]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: caller, original

f · operator

reference-profile · input revision 2 · CC0 1.0

f==NewCheckpoint103(id,caller,world,AInside(q))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInside, caller, id, q, world, NewCheckpoint103

frames · operator

reference-profile · input revision 2 · CC0 1.0

frames==AJoin(q.frames,[key \in {id} |-> f])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AJoin, f, id, q

id · operator

reference-profile · input revision 2 · CC0 1.0

id==q.ledger.lastCheckpoint+1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

original · operator

reference-profile · input revision 2 · CC0 1.0

original==q.stepEvents[role]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

site · operator

reference-profile · input revision 2 · CC0 1.0

site==[kind |-> "Instruction",caller |-> caller,eventId |-> event.id,snapshotId |-> world,inside |-> AInside(q)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInside, caller, event, q, world

world · operator

reference-profile · input revision 2 · CC0 1.0

world==q.nextWorld

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.flow EXCEPT !.decision="NeutralValue00001"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

b · operator

reference-profile · input revision 2 · CC0 1.0

b==IBT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, IBT11

next · operator

reference-profile · input revision 2 · CC0 1.0

next==IWithItemInspectionT11(q,after)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, q, IWithItemInspectionT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.action EXCEPT !.status="Nested",!.nested="Traversal7"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

b · operator

reference-profile · input revision 2 · CC0 1.0

b==IBT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, IBT11

next · operator

reference-profile · input revision 2 · CC0 1.0

next==IWithInspectionT11(q,after)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, q, IWithInspectionT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[a EXCEPT !.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: a

next · operator

reference-profile · input revision 2 · CC0 1.0

next==[q EXCEPT !.control=after]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: after, q

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: b

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[b EXCEPT !.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: b

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[c EXCEPT !.siteInspectionFinished=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: c

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[c EXCEPT !.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: c

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.flow EXCEPT !.decision="NeutralValue00001"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

a · operator

reference-profile · input revision 2 · CC0 1.0

a==IAT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, IAT11

c · operator

reference-profile · input revision 2 · CC0 1.0

c==q.control

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

closed · operator

reference-profile · input revision 2 · CC0 1.0

closed==CompletePriorityOptionFrame9(w)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOptionFrame9, w

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

traversal · operator

reference-profile · input revision 2 · CC0 1.0

traversal==OpenTraversal6(7,1000,ITraversalCallerT11(q.action))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, ITraversalCallerT11, OpenTraversal6

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, q

ledger · operator

reference-profile · input revision 2 · CC0 1.0

ledger==[q.ledger EXCEPT !.instances[q.reactionContext.instanceId].status="Imminent"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

p · operator

reference-profile · input revision 2 · CC0 1.0

p==OpenConditionalProcedure96(id,d,w,option,context.transaction,"Rule")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenConditionalProcedure96, w, context, d, id, option

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==OpenInstruction93(context.instructionId,"Ability",id,d.syntax.source,"Rule",1,"NoValue",<<context.work>>,FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenInstruction93, context, d, id

receipt · operator

reference-profile · input revision 2 · CC0 1.0

receipt==[tag |-> "ConditionalInstructionCheckpoint",id |-> q.currentCP,abilityInstance |-> q.child.id,
        transactionId |-> q.child.transaction,source |-> q.child.ability.source,instruction |-> q.childPlan.id,index |-> 1,
        complete |-> CheckpointDrained103(AFrame(q),q.ledger,q.stack),
        allNewerChainsComplete |-> CheckpointDrained103(AFrame(q),q.ledger,q.stack)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, AFrame, CheckpointDrained103

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, q

ledger · operator

reference-profile · input revision 2 · CC0 1.0

ledger==[q.ledger EXCEPT !.instances[q.reactionContext.instanceId].status="Resolving",!.instances[q.reactionContext.instanceId].expected=[i \in {1} |->
         [instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, q

p · operator

reference-profile · input revision 2 · CC0 1.0

p==[q.child EXCEPT !.phase="Resolve",!.ability.phase="Resolving"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==[q.childPlan EXCEPT !.phase="Resolving"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

receipt · operator

reference-profile · input revision 2 · CC0 1.0

receipt==AChildReturnReceipt(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AChildReturnReceipt, q

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, q

ledger · operator

reference-profile · input revision 2 · CC0 1.0

ledger==[q.ledger EXCEPT !.instances[q.reactionContext.instanceId].status="Complete"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

p · operator

reference-profile · input revision 2 · CC0 1.0

p==[q.child EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ability, q

plan · operator

reference-profile · input revision 2 · CC0 1.0

plan==ProtocolP!FinishedPlan9p(q.childPlan)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, ProtocolP!FinishedPlan9p

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, q

p · operator

reference-profile · input revision 2 · CC0 1.0

p==[q.child EXCEPT !.phase="Complete",!.checkpoint=q.currentCP]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

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, q

p · operator

reference-profile · input revision 2 · CC0 1.0

p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

ability · operator

reference-profile · input revision 2 · CC0 1.0

ability==ProtocolP!FinishedAbility9p(q.child.ability,q.childPlan)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, ProtocolP!FinishedAbility9p

after · operator

reference-profile · input revision 2 · CC0 1.0

after==PassPriorityFrame9(w)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PassPriorityFrame9, w

afterSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

afterSnapshot==ASnapshot(q,ledger,q.nextWorld+1,"InstructionAfter",q.ledger.lastCheckpoint)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ASnapshot, ledger, q

announced · operator

reference-profile · input revision 2 · CC0 1.0

announced==[plan EXCEPT !.phase="Imminent",!.announced=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: plan

beforeId · operator

reference-profile · input revision 2 · CC0 1.0

beforeId==IF AMutation="reuse-world-id" THEN q.costOccurrence.snapshot.id ELSE q.nextWorld

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, AMutation

beforeSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

beforeSnapshot==ASnapshot(q,q.ledger,beforeId,"InstructionBefore",q.ledger.lastCheckpoint)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ASnapshot, beforeId, q

busy · operator

reference-profile · input revision 2 · CC0 1.0

busy==StartPriorityOptionFrame9(w,option,context.transaction)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StartPriorityOptionFrame9, w, context, option

captures · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AAddCapture, ACapture, AJoin, afterSnapshot, beforeSnapshot, q

context · operator

reference-profile · input revision 2 · CC0 1.0

context==q.reactionContext

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

d · operator

reference-profile · input revision 2 · CC0 1.0

d==context.definition

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: context

expected · operator

reference-profile · input revision 2 · CC0 1.0

expected==[tag |-> "ConditionalExpectedEffects",point |-> "ExpectedEffectsBeforeInterrupt",instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, q

f · operator

reference-profile · input revision 2 · CC0 1.0

f==q.frames[q.reactionOwner.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

id · operator

reference-profile · input revision 2 · CC0 1.0

id==context.instanceId

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: context

imminent · operator

reference-profile · input revision 2 · CC0 1.0

imminent==[p EXCEPT !.phase="Imminent",!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.detached=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p

option · operator

reference-profile · input revision 2 · CC0 1.0

option==PriorityOption9(70,"Conditional","SideB",d.syntax.id,id,d.syntax.source,0,{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PriorityOption9, d, id

publishedCaptures · operator

reference-profile · input revision 2 · CC0 1.0

publishedCaptures==IF AMutation="history-rewrite" THEN [captures EXCEPT ![<<1,PInitialSnapshot.point>>].basis.revision=1] ELSE captures

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: captures, AMutation, PInitialSnapshot

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

ready · operator

reference-profile · input revision 2 · CC0 1.0

ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: w, q

rest · operator

reference-profile · input revision 2 · CC0 1.0

rest==SubSeq(q.stack,1,Len(q.stack)-1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

returned · operator

reference-profile · input revision 2 · CC0 1.0

returned==[f EXCEPT !.phase="Returned",!.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: f

snapshot · operator

reference-profile · input revision 2 · CC0 1.0

snapshot==ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Pass",q.ledger.lastCheckpoint)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, ACurrentSnapshot

step · operator

reference-profile · input revision 2 · CC0 1.0

step==[ProtocolP!Step9p(q.childPlan) EXCEPT !.complete=AMutation#"blocked-child-carry"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, AMutation, ProtocolP!Step9p

a · operator

reference-profile · input revision 2 · CC0 1.0

a==IAT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IAT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[a EXCEPT !.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: a

b · operator

reference-profile · input revision 2 · CC0 1.0

b==IBT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IBT11

a · operator

reference-profile · input revision 2 · CC0 1.0

a==IAT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IAT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: b

b · operator

reference-profile · input revision 2 · CC0 1.0

b==IBT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IBT11

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[b EXCEPT !.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: b

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[c EXCEPT !.returned=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: c

after · operator

reference-profile · input revision 2 · CC0 1.0

after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"]

Exact module download · Source bundle and reproduction instructions

after · operator

reference-profile · input revision 2 · CC0 1.0

after==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOptionFrame9, ReplaceWindowTop9, WindowTop9

c · operator

reference-profile · input revision 2 · CC0 1.0

c==q.control

Exact module download · Source bundle and reproduction instructions

oldId · operator

reference-profile · input revision 2 · CC0 1.0

oldId==q.NeutralValue00003.opened.id

Exact module download · Source bundle and reproduction instructions

site · operator

reference-profile · input revision 2 · CC0 1.0

site==ITurnSiteT11(q)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ITurnSiteT11

w · operator

reference-profile · input revision 2 · CC0 1.0

w==NewPriorityWindow9(oldId,"NeutralValue00001",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, oldId, site, EmptyT11

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

drain · operator

reference-profile · input revision 2 · CC0 1.0

drain==[step |-> q.lastWork,insideItemInspection |-> IInsideItemInspectionT11(q),insideInspection |-> IInsideInspectionT11(q),duringTraversal |-> DuringTraversal6(q.control.traversal)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, IInsideInspectionT11, IInsideItemInspectionT11, DuringTraversal6

f · operator

reference-profile · input revision 2 · CC0 1.0

f==q.frames[q.stepCP[role]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, role

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

role · operator

reference-profile · input revision 2 · CC0 1.0

role==q.activeStepRole

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

event · operator

reference-profile · input revision 2 · CC0 1.0

event==AStepEvent(next,"AE",q.nextEvent,w.id,source,~w.open /\ w.stage="Closed" /\ q.flow.step="ProcedureCode484be3e50aa9")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepEvent, next, q, source, w

next · operator

reference-profile · input revision 2 · CC0 1.0

next==IRecordT11([q EXCEPT !.stack=rest],"ProcedureCode484be3e50aa9",{},"TurnContinue")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, rest, IRecordT11

passed · operator

reference-profile · input revision 2 · CC0 1.0

passed==PassPriorityFrame9(w)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PassPriorityFrame9, w

q · operator

reference-profile · input revision 2 · CC0 1.0

q==qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

rest · operator

reference-profile · input revision 2 · CC0 1.0

rest==SubSeq(q.stack,1,Len(q.stack)-1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q

source · operator

reference-profile · input revision 2 · CC0 1.0

source==[kind |-> "NativeTurnPRPop",window |-> w,afterStack |-> rest,flow |-> q.flow]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q, rest, 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, q

AMutation · constant

reference-profile · input revision 2 · CC0 1.0

AMutation

Exact module download · Source bundle and reproduction instructions

AScenario · constant

reference-profile · input revision 2 · CC0 1.0

AScenario

Exact module download · Source bundle and reproduction instructions

AActionPay · operator

reference-profile · input revision 2 · CC0 1.0

AActionPay ==
 LET q==qT11 after==IActionPointAfterT11(q.actionPointWorld) a==NewAction5(30,"SideB",BasicActionKey5("SideB","SchemaAtom138"))
     payment==[before |-> q.actionPointWorld,after |-> after,window |-> WindowTop9(q.stack).id,option |-> IActionOptionT11,transaction |-> 200]
     native==[operationId |-> 1,command |-> IActionPointCommandT11,before |-> q.actionPointWorld,after |-> after,payment |-> payment,actionId |-> a.id,turnId |-> q.flow.turn.id]
     committed==[q EXCEPT !.actionPointWorld=after,!.payment=payment,!.action=a,!.native=native]
     snapshot==ASnapshot(committed,q.ledger,q.nextWorld,"ActionPaymentOccurrence",q.ledger.lastCheckpoint)
     event==[id |-> 1,tag |-> "CostPaid",caller |-> ACostCaller(committed),transactionId |-> 200,
       operationId |-> 1,nativePayment |-> native,complete |-> ANativeCommitted(committed)]
     occurrence==[id |-> 1,kind |-> "ActionActionPointCostPaid",object |-> 0,actor |-> "SideB",side |-> "SideB",
       snapshot |-> snapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(ACostDefinition),
       actualEvent |-> event,nativeOperation |-> native,turnId |-> q.flow.turn.id]
 IN /\ AReservation(q) /\ BasicActionLocalGate5("SideB","SchemaAtom138",FALSE)
    /\ q.nativeCommitCount=0 /\ q.native=EmptyT11 /\ q.nextWorld \notin q.issuedWorlds
    /\ BasicAction5("SideB","SchemaAtom138").effect="SchemaAtom138" /\ BasicAction5("SideB","SchemaAtom138").actionPoints=1 /\ BasicAction5("SideB","SchemaAtom138").resourceUnits=0
    /\ ActionStart5(q.flow.turn,"SideB",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,AReservation(q),TRUE,q.action.status="Idle",a.id,a.key,a)
    /\ AAdmit(committed,q.ledger,snapshot)
    /\ qT11'=[committed EXCEPT !.costEvent=event,!.costOccurrence=occurrence,!.nativeEvents=[id \in {1} |-> event],
       !.nativeCommitCount=1,!.issuedEvents=@ \cup {1},!.captures=AAddCapture(q,snapshot),!.issuedWorlds=@ \cup {snapshot.id},!.nextWorld=@+1,!.stage="ActionCostDrain"]
    /\ IntegrationActionPointsT11!DoActionPoints(IActionPointCommandT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AAddCapture, AAdmit, AReservation, a, committed, event, occurrence, q, snapshot, IActionPointCommandT11, IntegrationActionPointsT11!DoActionPoints, EmptyT11, qT11, ActionStart5, BasicAction5, BasicActionLocalGate5

AActionPaymentSafety · operator

reference-profile · input revision 2 · CC0 1.0

AActionPaymentSafety ==
 LET q==qT11 IN
 /\ q.nativeCommitCount \in {0,1}
 /\ IF q.nativeCommitCount=0 THEN q.native=EmptyT11 /\ q.nativeEvents=EmptyT11 ELSE
      /\ ANativeCommitted(q) /\ DOMAIN q.nativeEvents={1} /\ q.nativeEvents[1]=q.costEvent
      /\ q.costEvent.id=1 /\ q.costEvent.operationId=1 /\ q.costEvent.nativePayment=q.native
      /\ q.costOccurrence.id=1 /\ q.costOccurrence.actualEvent=q.costEvent /\ q.costOccurrence.nativeOperation=q.native
      /\ q.actionPointWorld=(IF q.costDrained THEN [q.payment.after EXCEPT !.checkpointDue=FALSE] ELSE q.payment.after)
      /\ (q.costDrained => AActionCostDrained(q,ACostCaller(q)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AActionCostDrained, ACostCaller, ANativeCommitted, q, EmptyT11

AAdmitOccurrences · operator

reference-profile · input revision 2 · CC0 1.0

AAdmitOccurrences(q,cp) ==
 /\ ANativeCommitted(q) /\ q.nativeCommitCount=1 /\ DOMAIN q.nativeEvents={1}
 /\ cp.occurrences=(IF cp.id=q.costCP THEN [id \in {1} |-> q.costOccurrence]
      ELSE IF cp.id=q.stepCP["AF"] THEN [id \in {q.completionOccurrence.id} |-> q.completionOccurrence] ELSE EmptyT11)
 /\ (cp.id=q.stepCP["AF"] => ACompletionCommitted(q))
 /\ q.costOccurrence.id=1 /\ q.costOccurrence.nativeOperation=q.native /\ q.costOccurrence.actualEvent=q.costEvent

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACompletionCommitted, ANativeCommitted, EmptyT11

AAdmitSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

AAdmitSnapshot(q,objects,ledger,view) == objects=q.objects /\ AAdmit(q,ledger,view)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AAdmit

AAdvanceStep · operator

reference-profile · input revision 2 · CC0 1.0

AAdvanceStep(role) ==
 LET q==qT11 f==q.frames[q.stepCP[role]]
     suppliedFrame==IF AMutation="unreturned-" \o AStepLower(role) THEN [f EXCEPT !.returned=FALSE,!.phase="Completed"] ELSE f
     suppliedFlow==IF role="AG" /\ AMutation="stale-ag-flow" THEN [q.flow EXCEPT !.step="ProcedureCode989abc27e0c6"] ELSE q.flow
     after==[q.flow EXCEPT !.step=CASE role="AF" -> "ProcedureCodea439ce381bba" [] role="AG" -> "ProcedureCode484be3e50aa9" [] OTHER -> "ProcedureCode989abc27e0c6",!.decision="NoValue"]
     proof==ARequireStep(q,role,suppliedFrame,suppliedFlow)
     next==[q EXCEPT !.flow=after,!.stepConsumed=@ \cup {role},
       !.stepContinuations=AJoin(@,[key \in {role} |-> [before |-> q.flow,after |-> after,receipt |-> q.stepReturnReceipts[role]]]),
       !.lifecycle=Append(@,ALife(q,"StepConsume",role,f.id,0)),!.stage=IF role="AF" THEN "Drain" ELSE IF role="AG" THEN "OpenPR" ELSE "LatchNew"]
     g==IRecordT11(next,"ProcedureCodea439ce381bba",{},"TurnLoop")
     source==[kind |-> "NativeStepAdvance",before |-> q.flow,after |-> after,from |-> role,checkpointId |-> f.id]
     event==AStepEvent(g,"AG",q.nextEvent,q.NeutralValue00003.opened.id,source,after.step="ProcedureCodea439ce381bba" /\ "AF" \in next.stepConsumed)
 IN /\ proof /\ SideBStepAdvance5(q.flow,after,proof)
    /\ qT11'=IF role="AF" THEN [g EXCEPT !.stepEvents=AJoin(@,[key \in {"AG"} |-> event]),!.issuedEvents=@ \cup {event.id},!.nextEvent=@+1]
      ELSE next

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AJoin, after, event, g, next, proof, q, qT11, SideBStepAdvance5

ABypassReaction · operator

reference-profile · input revision 2 · CC0 1.0

ABypassReaction ==
 LET q==qT11 f==AFrame(q) returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] world==AWorld(q,f) IN
 /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
 /\ qT11'=[ASetFrame(q,returned) EXCEPT !.stage="AStepReturn"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointCompletion912, f, q, returned, world, ASetFrame, ReturnCheckpointWithoutReaction103, qT11

ACPData · operator

reference-profile · input revision 2 · CC0 1.0

ACPData(q,f) ==
 LET b==ASnapshot(q,q.ledger,f.snapshotId,"CheckpointBeginning",f.id)
 IN [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> f.id,previousCheckpoint |-> q.ledger.lastCheckpoint,
  serial |-> q.ledger.serial+1,previousSnapshot |-> q.ledger.lastSnapshot,beginSnapshot |-> b,
  processingSnapshot |-> [b EXCEPT !.point="ProcedureCodee605a78f5d5e"],stepSerial |-> q.ledger.stepSerial,
  occurrences |-> IF q.cpRole="ActionCost" THEN [id \in {1} |-> q.costOccurrence]
    ELSE IF q.cpRole="AF" THEN [id \in {q.completionOccurrence.id} |-> q.completionOccurrence]
    ELSE IF AMutation="remint-cost-occurrence" /\ q.childReturned /\ q.cpRole="ChildPriority"
    THEN [id \in {2} |-> [q.costOccurrence EXCEPT !.id=2]] ELSE EmptyT11,caller |-> f.caller]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: b, AMutation, EmptyT11

ACPNext · operator

reference-profile · input revision 2 · CC0 1.0

ACPNext(f) ==
 LET rest==SubSeq(f.owed,2,Len(f.owed)) IN
 [f EXCEPT !.owed=rest,!.done=@ \cup {f.point},!.point=IF rest= <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE rest[1],!.phase=IF rest= <<>> THEN "Completed" ELSE "Steps"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: rest

ACheckpointSafety · operator

reference-profile · input revision 2 · CC0 1.0

ACheckpointSafety ==
 LET q==qT11 IN
 /\ DOMAIN q.checkpointEvents=DOMAIN q.frames /\ DOMAIN q.basisHistory=DOMAIN q.frames
 /\ q.registry.cleanupIds={id \in DOMAIN q.frames : "ProcedureCode88eda145024f" \in q.frames[id].done}
 /\ (q.costCP>0 => q.frames[q.costCP].caller=ACostCaller(q))
 /\ \A id \in DOMAIN q.recognitionHistory :
     LET cp==q.recognitionHistory[id] IN
     /\ cp.beginSnapshot.id=cp.processingSnapshot.id /\ cp.id=id /\ cp.caller=q.frames[id].caller
     /\ cp.beginSnapshot.objects=q.basisHistory[id].objects
     /\ IF id=q.costCP THEN cp.occurrences=[k \in {1} |-> q.costOccurrence]
         ELSE IF id=q.stepCP["AF"] THEN cp.occurrences=[k \in {q.completionOccurrence.id} |-> q.completionOccurrence] ELSE cp.occurrences=EmptyT11
 /\ (q.done =>
     /\ DOMAIN q.frames=(IF q.scenario="empty" THEN 1..4 ELSE 1..8)
     /\ \A id \in DOMAIN q.frames : q.frames[id].returned /\ q.frames[id].done=CheckpointStageSet103 /\ q.frames[id].owed= <<>>
     /\ (IF q.scenario="empty" THEN q.child=EmptyT11 /\ q.ledger.instances=EmptyT11 /\ q.noUseCount=0 /\ q.work= <<>>
          ELSE q.childReturned /\ q.child.phase="Returned" /\ q.child.ability.returned /\ q.ledger.instances[q.reactionContext.instanceId].status="Complete" /\ ~q.ledger.instances[q.reactionContext.instanceId].used /\ q.noUseCount=1 /\ q.work= <<IF q.scenario="cost-reaction" THEN "ActionCostReaction" ELSE "ActionCompletionReaction">>))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACostCaller, cp, q, CheckpointStageSet103, EmptyT11

ACheckpointWork · operator

reference-profile · input revision 2 · CC0 1.0

ACheckpointWork ==
 LET q==qT11 f==AFrame(q) next==ACPNext(f) world==AWorld(q,f) IN
 CASE f.point="ProcedureCodee605a78f5d5e" ->
   LET cp==ACPData(q,f)
       keys=={[definition |-> key,occurrence |-> id] : key \in {k \in DOMAIN ADefinitions(q) :
         ConditionalActive96(ADefinitions(q)[k],cp.processingSnapshot)},id \in DOMAIN cp.occurrences}
       eligible=={k \in keys : TriggerPattern96(ADefinitions(q)[k.definition],cp.occurrences[k.occurrence])}
       allocation==[k \in IF AMutation="omit-cost-recognition" /\ q.cpRole="ActionCost" THEN {} ELSE eligible |->
          IF k.definition=ConditionalKey96(ACostDefinition) THEN 301 ELSE 302]
       bindings==[k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> AInstanceWindow(allocation[k]),group |-> 4]]
       conditions==[k \in DOMAIN ADefinitions(q) |-> [id \in DOMAIN cp.occurrences |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> ADefinitions(q)[k].syntax.id,source |-> ADefinitions(q)[k].syntax.source,
          occurrence |-> id,snapshotId |-> cp.occurrences[id].snapshot.id,results |-> EmptyT11]]]
       ledger==ProtocolP!CPAfter9p(q.ledger,cp,allocation,bindings)
       after==[next EXCEPT !.recognition=cp,!.recognized=CheckpointMemberMap103(ledger,f.id)]
       x==[route |-> "Ordinary",cp |-> cp,definitions |-> ADefinitions(q),lexemes |-> ALexemes(q),conditions |-> conditions,
         allocation |-> allocation,bindings |-> bindings,departures |-> EmptyT11,holds |-> EmptyT11,
         usedWindows |-> q.usedWindows,cardFacts |-> CardFacts10]
   IN /\ AAdmitOccurrences(q,cp)
      /\ AAdmitSnapshot(q,q.objects,q.ledger,cp.beginSnapshot)
      /\ AAdmitSnapshot(q,q.objects,q.ledger,cp.processingSnapshot)
      /\ x.definitions=ConditionalDefinitionsSA(q.abilityRegistry)
      /\ RecognizeCheckpoint103(f,after,q.ledger,ledger,q.stack,q.stack,x)
      /\ qT11'=[ASetFrame(q,after) EXCEPT !.ledger=ledger,
        !.recognitionHistory=AJoin(@,[id \in {cp.id} |-> cp]),
        !.captures=AJoin(AAddCapture(q,cp.beginSnapshot),[captureKey \in {<<cp.processingSnapshot.id,cp.processingSnapshot.point>>} |-> ACapture(q,cp.processingSnapshot)])]
 [] f.point="ProcedureCode88eda145024f" ->
   LET cursor==LingeringCheckpointFrame910(q.ledger,f.recognition,world)
       cleanup==[tag |-> "LingeringCheckpointCleanup",frame |-> cursor,expired |-> {},complete |-> TRUE]
       registry==[q.registry EXCEPT !.cleanupIds=@ \cup {f.id}]
       snapshot==ASnapshot(q,q.ledger,f.snapshotId,"CleanupCurrent",f.id)
   IN /\ AWorldBound(q,f,world)
      /\ AAdmitSnapshot(q,q.objects,q.ledger,snapshot)
      /\ CheckpointCleanupEffects103(f,next,q.registry,registry,q.ledger,q.ledger,q.ledger,q.stack,q.stack,
        snapshot,snapshot,world,cursor,[cursor EXCEPT !.returned=TRUE,!.point="ProcedureCodeb681cc249a04"],cleanup)
      /\ qT11'=[ASetFrame(q,next) EXCEPT !.registry=registry]
 [] f.point="ProcedureCodeb681cc249a04" ->
   /\ CheckpointVictory103(f,next,q.objects,[id \in DOMAIN q.objects |-> 0],f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodefe50c31480ea" ->
   /\ CheckpointUniqueRetire103(f,next,q.objects,q.objects,[id \in DOMAIN q.objects |-> q.objects[id].card],{},{},{},
        [id \in DOMAIN q.objects |-> "SideA"],EmptyT11,EmptyT11,DOMAIN q.objects,APrinted,AOwners,{},f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodea488e1ba6ca3" ->
   /\ CheckpointIllegalRetire103(f,next,q.objects,q.objects,{},ALegal,[id \in DOMAIN q.objects |-> "SideA"],q.flow.turn.owner,
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],[applies |-> FALSE],"NoValue",{},EmptyT11,DOMAIN q.objects,APrinted,AOwners,{},f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} ->
   /\ CheckpointHostedCleanup103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,
        EmptyT11,EmptyT11,DOMAIN q.objects,APrinted,AOwners,{},f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode2d73b20aa788" ->
   /\ CheckpointAuxiliarySiteCleanup103(f,next,[s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],q.objects,EmptyT11,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode2d6279f9d639" ->
   /\ CheckpointPositionCleanup103(f,next,q.layout,q.layout,q.control.traversal.position,EmptyT11,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode7f181ce21011" ->
   /\ CheckpointRootAdmissions103(f,next,q.capacity,q.capacity,AInspection(q),q.objects,EmptyT11,0,q.ledger.stepSerial,{},IF IInsideInspectionT11(q) THEN "SideB" ELSE "NoValue",f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodeda83a77a1f12" ->
   /\ CheckpointRestoreDiscard103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,APrinted,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCode0811ebc5f40e" ->
   /\ CheckpointReturnDiscardCounters103(f,next,q.objects,q.objects,f.snapshotId)
   /\ qT11'=ASetFrame(q,next)
 [] f.point="ProcedureCodeb74d673a0fc6" ->
   IF DOMAIN f.recognized={} THEN
     LET returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] IN
     /\ AWorldBound(q,f,world)
     /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
     /\ qT11'=[ASetFrame(q,returned) EXCEPT !.stage=q.cpResume,
         !.checkpointHistory=Append(@,[id |-> f.id,role |-> q.cpRole,caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
   ELSE
     LET members==f.recognized site==AReactionSite(q) context==AReactionContext(q,f)
         opening==AJoin(IOpeningT11(context.windowId,"Reaction",site),
           [members |-> DOMAIN members,instances |-> members,group |-> 4,modifiersExist |-> FALSE,
            preparation |-> <<"ConditionsMet","PendingGroup">>,checkpointId |-> f.id,caller |-> f.caller,
            completion |-> PersistentCheckpointCompletion912(q.ledger,f.recognition,world)])
         window==NewPriorityWindow9(context.windowId,"Reaction",site,members,4,NoTimingRef9,[id |-> 0],0)
         after==[f EXCEPT !.phase="Reaction",!.windowId=context.windowId]
     IN /\ AWorldBound(q,f,world)
        /\ OpenCheckpointReaction103(f,after,q.ledger,q.stack,Append(q.stack,window),site,opening,q.usedWindows)
        /\ qT11'=[ASetFrame(q,after) EXCEPT !.stack=Append(@,window),!.usedWindows=@ \cup {context.windowId},!.childWindow=context.windowId,!.reactionContext=context,!.childReturned=FALSE,!.child=EmptyT11,!.childPlan=EmptyT11,
          !.reactionOwner=[id |-> f.id,role |-> q.cpRole,resume |-> q.cpResume],!.stage="AReceive"]
 [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PersistentCheckpointCompletion912, ConditionalDefinitionsSA, AAddCapture, ACapture, AInspection, AJoin, AOwners, APrinted, AWorldBound, after, after, cleanup, context, cp, cursor, f, ledger, next, opening, q, registry, returned, site, snapshot, window, world, x, AAdmitOccurrences, AAdmitSnapshot, ALegal, ASetFrame, CheckpointAuxiliarySiteCleanup103, CheckpointCleanupEffects103, CheckpointHostedCleanup103, CheckpointIllegalRetire103, CheckpointPositionCleanup103, CheckpointRestoreDiscard103, CheckpointReturnDiscardCounters103, CheckpointRootAdmissions103, CheckpointUniqueRetire103, CheckpointVictory103, OpenCheckpointReaction103, RecognizeCheckpoint103, ReturnCheckpointWithoutReaction103, IInsideInspectionT11, CentralTargetSites4, EmptyT11, qT11

AChildTurnUses · operator

reference-profile · input revision 2 · CC0 1.0

AChildTurnUses(q) == FamilyTurnUsesSA(q.catalog,q.useIndex,q.turnUses,"Conditional",q.reactionContext.definition.syntax.source)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FamilyTurnUsesSA

ACompleteAction · operator

reference-profile · input revision 2 · CC0 1.0

ACompleteAction ==
 LET q==qT11 after==[q.action EXCEPT !.status="Complete"] raw==[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]
     completed==IRecordT11([q EXCEPT !.action=after],"5.7.1f:return",{raw},"TurnAdvance")
     native==[operationId |-> 2,before |-> q.action,after |-> after,windowId |-> WindowTop9(q.stack).id,
       turnId |-> q.flow.turn.id,phaseId |-> q.actionPhaseId,rawIndex |-> Len(q.rawEvents)+1]
     event==[id |-> q.nextEvent,tag |-> "OriginalActionCompletes",rawEvent |-> raw,nativeCompletion |-> native]
     snapshot==ASnapshot(completed,q.ledger,q.nextWorld,"ActionCompletionOccurrence",q.ledger.lastCheckpoint)
     occurrence==[id |-> event.id,kind |-> "OriginalActionCompletes",object |-> 0,actor |-> "SideB",side |-> "SideB",snapshot |-> snapshot,
       scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(ACompletionDefinition),actualEvent |-> event,nativeCompletion |-> native]
     source==[kind |-> "NativeActionComplete",native |-> native,event |-> event]
     siteEvent==AStepEvent(completed,"AF",event.id,q.NeutralValue00003.opened.id,source,ActionReadyToContinue5(after))
     events==IF AMutation="repeated-completion-publication" THEN [id \in {event.id,event.id+1} |-> [event EXCEPT !.id=id]] ELSE [id \in {event.id} |-> event]
 IN /\ q.completionCommitCount=0 /\ "AF" \notin DOMAIN q.stepEvents
    /\ q.nextEvent \notin q.issuedEvents /\ q.nextWorld \notin q.issuedWorlds
    /\ ActionComplete5(q.action,after,"SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete)
    /\ AAdmit(completed,q.ledger,snapshot)
    /\ qT11'=[completed EXCEPT !.stage="ActionWindowReturn",!.nativeCompletion=native,!.completionEvent=event,!.completionOccurrence=occurrence,
       !.completionEvents=events,!.completionCommitCount=1,!.stepEvents=AJoin(@,[role \in {"AF"} |-> siteEvent]),
       !.captures=AAddCapture(q,snapshot),!.issuedWorlds=@ \cup {snapshot.id},!.nextWorld=@+1,
       !.issuedEvents=@ \cup DOMAIN events,!.nextEvent=@+IF AMutation="repeated-completion-publication" THEN 2 ELSE 1,
       !.lifecycle=Append(@,ALife(q,"ActionComplete","AF",0,Len(q.stack)))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AAddCapture, AAdmit, AJoin, after, completed, event, events, native, occurrence, q, siteEvent, snapshot, AMutation, ALife, qT11, ActionComplete5

ACompletion · operator

reference-profile · input revision 2 · CC0 1.0

ACompletion(q) == [tag |-> "ActionCompletion",scenario |-> q.scenario,trace |-> q.trace,objects |-> ANativeProjection(q.objects),
 enrichedObjects |-> q.objects,actionPointWorld |-> q.actionPointWorld,payment |-> q.payment,native |-> q.native,nativeCommitCount |-> q.nativeCommitCount,
 nativeEvents |-> q.nativeEvents,costEvent |-> q.costEvent,costOccurrence |-> q.costOccurrence,
 nativeCompletion |-> q.nativeCompletion,completionEvent |-> q.completionEvent,completionOccurrence |-> q.completionOccurrence,completionEvents |-> q.completionEvents,
 completionCommitCount |-> q.completionCommitCount,stepEvents |-> q.stepEvents,stepCP |-> q.stepCP,stepConsumed |-> q.stepConsumed,
 stepReturnReceipts |-> q.stepReturnReceipts,stepContinuations |-> q.stepContinuations,stepOpenRecords |-> q.stepOpenRecords,
 closedWindows |-> q.closedWindows,poppedWindows |-> q.poppedWindows,lifecycle |-> q.lifecycle,
 returnOrder |-> q.returnOrder,consumed |-> q.consumed,rawEvents |-> q.rawEvents,windowHistory |-> q.windowHistory,drains |-> q.drains,
 finalAction |-> q.action,finalWindow |-> WindowTop9(q.stack),frames |-> q.frames,frameRoles |-> q.frameRoles,recognitionHistory |-> q.recognitionHistory,
 uses |-> q.uses,turnUses |-> q.turnUses,useIndex |-> q.useIndex,procedures |-> q.procedures,
 child |-> q.child,childPlan |-> q.childPlan,childReturned |-> q.childReturned,instances |-> q.ledger.instances,
 reactionOwner |-> q.reactionOwner,reactionContext |-> q.reactionContext,noUseCount |-> q.noUseCount,work |-> q.work,
 checkpointHistory |-> q.checkpointHistory,captures |-> q.captures,issuedWorlds |-> q.issuedWorlds,issuedEvents |-> q.issuedEvents]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, ANativeProjection

ACompletionSafety · operator

reference-profile · input revision 2 · CC0 1.0

ACompletionSafety ==
 LET q==qT11 IN
 /\ q.completionCommitCount \in {0,1}
 /\ (q.completionCommitCount=0 => q.completionEvents=EmptyT11 /\ q.nativeCompletion=EmptyT11)
 /\ (q.completionCommitCount=1 => ACompletionCommitted(q) /\ DOMAIN q.completionEvents={q.completionEvent.id} /\ q.completionEvents[q.completionEvent.id]=q.completionEvent)
 /\ (q.done => q.completionCommitCount=1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACompletionCommitted, q, EmptyT11

ACurrentSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

ACurrentSnapshot(q,objects,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,BasisSA(q.abilityRevision,q.abilityRegistry,objects,q.rulePermissions),ledger,ATemplate(q,id,point,checkpoint))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA, ConditionalSnapshotFromRegistrySA, ATemplate

AEffects · operator

reference-profile · input revision 2 · CC0 1.0

AEffects ==
 LET q==qT11 after==[q.action EXCEPT !.status="Effects"] IN
 /\ AActionPaid(q) /\ ActionEffectsBegin5(q.action,after,AActionPaid(q))
 /\ qT11'=[q EXCEPT !.action=after,!.trace=Append(@,"ProcedureCode989abc27e0c6"),!.revision=@+1,!.stage="TraversalStart"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AActionPaid, after, q, qT11, ActionEffectsBegin5

AEventuallyReturns · operator

reference-profile · input revision 2 · CC0 1.0

AEventuallyReturns == <>qT11.done

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

AFrame · operator

reference-profile · input revision 2 · CC0 1.0

AFrame(q) == q.frames[q.currentCP]

Exact module download · Source bundle and reproduction instructions

AHistoryFrame · operator

reference-profile · input revision 2 · CC0 1.0

AHistoryFrame(before,after) ==
 /\ ACaptureFrame(before,after) /\ before.issuedWorlds \subseteq after.issuedWorlds
 /\ DOMAIN before.recognitionHistory \subseteq DOMAIN after.recognitionHistory
 /\ \A id \in DOMAIN before.recognitionHistory : before.recognitionHistory[id]=after.recognitionHistory[id]
 /\ before.issuedEvents \subseteq after.issuedEvents
 /\ \A field \in {"stepEvents","stepReturnReceipts","stepContinuations","closedWindows","poppedWindows"} :
      /\ DOMAIN before[field] \subseteq DOMAIN after[field]
      /\ \A key \in DOMAIN before[field] : before[field][key]=after[field][key]
 /\ (before.completionCommitCount>0 => before.nativeCompletion=after.nativeCompletion /\ before.completionEvent=after.completionEvent /\ before.completionOccurrence=after.completionOccurrence)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ACaptureFrame

AHistorySafety · operator

reference-profile · input revision 2 · CC0 1.0

AHistorySafety ==
 LET q==qT11 IN
 /\ \A key \in DOMAIN q.captures :
    /\ q.captures[key].basis=MinimalCaptureSA(ABasis(q)) /\ q.captures[key].snapshot.id \in q.issuedWorlds
    /\ key= <<q.captures[key].snapshot.id,q.captures[key].snapshot.point>>
 /\ DOMAIN q.ledger.instances \subseteq {301,302}
 /\ \A id \in DOMAIN q.ledger.instances :
     LET instance==q.ledger.instances[id] cp==q.recognitionHistory[instance.checkpointId]
         original==NewConditionalInstance96(id,AInstanceDefinition(id),cp,instance.occurrence,AInstanceWindow(id),4) IN
     /\ AInstanceCapture(q.ledger.instances[id])=AInstanceCapture(original)
 /\ (q.child#EmptyT11 => ConditionalProcedureBound96(q.ledger,q.child) /\ q.child.definition=q.reactionContext.definition)
 /\ (q.costCP>0 => \A id \in DOMAIN q.frames : q.frames[id].snapshotId \in q.issuedWorlds)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalProcedureBound96, MinimalCaptureSA, ABasis, original, q, AInstanceCapture, EmptyT11

AInit · operator

reference-profile · input revision 2 · CC0 1.0

AInit == guideCaseT11=0 /\ AScenario \in {"empty","cost-reaction","completion-reaction"} /\ qT11=AInitial(AScenario)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AScenario, AInitial, guideCaseT11, qT11

AInitial · operator

reference-profile · input revision 2 · CC0 1.0

AInitial(scenario) ==
 LET permissions==A2Permissions(scenario)
     basis==BasisSA(0,ACatalog,AObjects,permissions)
     seed==NewConditionalLedger96(PInitialSnapshot)
     snapshot==ConditionalSnapshotFromRegistrySA(ACatalog,basis,seed,PInitialSnapshot)
 IN AJoin([IInitialT11 EXCEPT !.objects=AObjects],
 [scenario |-> scenario,actionPhaseId |-> 4000,catalog |-> ACatalog,abilityRegistry |-> ACatalog,abilityRevision |-> 0,
  rulePermissions |-> permissions,ledger |-> NewConditionalLedger96(snapshot),registry |-> NewLingeringRegistry910,
  uses |-> EmptyT11,turnUses |-> EmptyT11,useIndex |-> EmptyT11,procedures |-> EmptyT11,
  nativeCompletion |-> EmptyT11,completionEvent |-> EmptyT11,completionOccurrence |-> EmptyT11,completionEvents |-> EmptyT11,completionCommitCount |-> 0,
  stepEvents |-> EmptyT11,stepCP |-> [role \in AStepRoles |-> 0],activeStepRole |-> "NoValue",stepReturnReceipts |-> EmptyT11,
  stepConsumed |-> {},stepContinuations |-> EmptyT11,stepOpenRecords |-> EmptyT11,closedWindows |-> EmptyT11,poppedWindows |-> EmptyT11,
  lifecycle |-> <<>>,frameRoles |-> EmptyT11,reactionContext |-> EmptyT11,reactionOwner |-> EmptyT11,noUseChildren |-> {},issuedEvents |-> {},
  native |-> EmptyT11,nativeEvents |-> EmptyT11,nativeCommitCount |-> 0,costEvent |-> EmptyT11,costOccurrence |-> EmptyT11,
  child |-> EmptyT11,childPlan |-> EmptyT11,childReturned |-> FALSE,childWindow |-> 20,work |-> <<>>,noUseCount |-> 0,
  frames |-> EmptyT11,sites |-> {},checkpointEvents |-> EmptyT11,currentCP |-> 0,costCP |-> 0,
  cpResume |-> "NoValue",cpRole |-> "NoValue",checkpointHistory |-> <<>>,basisHistory |-> EmptyT11,recognitionHistory |-> EmptyT11,
  captures |-> [key \in {<<snapshot.id,snapshot.point>>} |-> [basis |-> MinimalCaptureSA(basis),snapshot |-> snapshot]],
  issuedWorlds |-> {1},nextWorld |-> 2001,nextEvent |-> 2])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, NewLingeringRegistry910, MinimalCaptureSA, ACatalog, AJoin, AObjects, AStepRoles, basis, permissions, snapshot, IInitialT11, EmptyT11

AInstanceCapture · operator

reference-profile · input revision 2 · CC0 1.0

AInstanceCapture(i) == [member |-> i.member,definition |-> i.definition,definitionCopy |-> i.definitionCopy,
 activationEpoch |-> i.activationEpoch,checkpointId |-> i.checkpointId,occurrence |-> i.occurrence,hadSnapshot |-> i.hadSnapshot]

Exact module download · Source bundle and reproduction instructions

ALegal · operator

reference-profile · input revision 2 · CC0 1.0

ALegal(selected) == selected={}

Exact module download · Source bundle and reproduction instructions

ALegality · operator

reference-profile · input revision 2 · CC0 1.0

ALegality(w,option,transaction) == [LegalityT11(w,option) EXCEPT !.transactionId=transaction]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LegalityT11

ALexemes · operator

reference-profile · input revision 2 · CC0 1.0

ALexemes(q) == [key \in DOMAIN ADefinitions(q) |-> RLex(ADefinitions(q)[key])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ADefinitions, RLex

ALife · operator

reference-profile · input revision 2 · CC0 1.0

ALife(q,tag,role,cp,depth) == [tag |-> tag,role |-> role,checkpointId |-> cp,step |-> q.flow.step,
 stackDepth |-> depth,revision |-> q.revision,windowId |-> IF role="AE" /\ "AE" \in DOMAIN q.closedWindows THEN q.closedWindows["AE"].id ELSE q.NeutralValue00003.opened.id]

Exact module download · Source bundle and reproduction instructions

ANext · operator

reference-profile · input revision 2 · CC0 1.0

ANext == AWork /\ AHistoryFrame(qT11,qT11')

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AHistoryFrame, AWork, qT11

AObservation · operator

reference-profile · input revision 2 · CC0 1.0

AObservation(q) == [tag |-> "ActionStage",scenario |-> q.scenario,stage |-> q.stage,NeutralValue00012 |-> ASpecimen0139(q),done |-> q.done,
 paymentCommitted |-> ANativeCommitted(q),completionCommitted |-> ACompletionCommitted(q),nativeCommitCount |-> q.nativeCommitCount,
 nativeOperationId |-> IF q.native=EmptyT11 THEN 0 ELSE q.native.operationId,completionCommitCount |-> q.completionCommitCount,
 checkpointDue |-> q.actionPointWorld.checkpointDue,costDrained |-> q.costDrained,cpRole |-> q.cpRole,currentCP |-> q.currentCP,costCP |-> q.costCP,
 point |-> IF q.currentCP=0 THEN "NoValue" ELSE AFrame(q).point,phase |-> IF q.currentCP=0 THEN "NoValue" ELSE AFrame(q).phase,
 childStatus |-> IF AObservedChild(q) \in DOMAIN q.ledger.instances THEN q.ledger.instances[AObservedChild(q)].status ELSE "Absent",
 childPhase |-> IF q.child=EmptyT11 THEN "NoValue" ELSE q.child.phase,childReturned |-> q.childReturned,noUseCount |-> q.noUseCount,
 useCount |-> Cardinality(DOMAIN q.uses),indexCount |-> Cardinality(DOMAIN q.useIndex),actionStatus |-> q.action.status,
 controlActive |-> ConditionalActive96(ACostDefinition,ASnapshot(q,q.ledger,q.nextWorld,"ObservedCurrent",q.ledger.lastCheckpoint)),
 completionControlActive |-> ConditionalActive96(ACompletionDefinition,ASnapshot(q,q.ledger,q.nextWorld,"ObservedCurrent",q.ledger.lastCheckpoint)),
 stepRole |-> AObservedRole(q),stepWasConsumed |-> AObservedRole(q) \in q.stepConsumed,
 stepReceiptPublished |-> AObservedRole(q) \in DOMAIN q.stepReturnReceipts,stepCP |-> q.stepCP,stepConsumed |-> q.stepConsumed,
 stepEvents |-> q.stepEvents,stepReturnReceipts |-> q.stepReturnReceipts,stepContinuations |-> q.stepContinuations,
 closedWindows |-> q.closedWindows,poppedWindows |-> q.poppedWindows,lifecycle |-> q.lifecycle,
 stackDepth |-> Len(q.stack),stack |-> q.stack,topKind |-> IF Len(q.stack)=0 THEN "NoValue" ELSE WindowTop9(q.stack).kind,
 topOpen |-> IF Len(q.stack)=0 THEN FALSE ELSE WindowTop9(q.stack).open,currentFlow |-> q.flow,
 objects |-> ANativeProjection(q.objects),actionPoints |-> q.actionPointWorld.actionPoints,spent |-> q.actionPointWorld.spent,
 frames |-> [id \in DOMAIN q.frames |-> [caller |-> q.frames[id].caller,done |-> q.frames[id].done,point |-> q.frames[id].point,phase |-> q.frames[id].phase,returned |-> q.frames[id].returned]],
 returnOrder |-> q.returnOrder,consumed |-> q.consumed,work |-> q.work]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, WindowTop9, ACompletionCommitted, ACompletionDefinition, ACostDefinition, ANativeCommitted, ANativeProjection, ASnapshot, AFrame, AObservedChild, AObservedRole, ASpecimen0139, EmptyT11

AObservedChild · operator

reference-profile · input revision 2 · CC0 1.0

AObservedChild(q) == IF q.reactionContext#EmptyT11 THEN q.reactionContext.instanceId ELSE IF 302 \in DOMAIN q.ledger.instances THEN 302 ELSE 301

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11

AObservedRole · operator

reference-profile · input revision 2 · CC0 1.0

AObservedRole(q) ==
 IF q.stage \in {"ActionWindowReturn","PopAction","TurnAdvance"} \/ (q.stage="Drain" /\ q.lastWork="ProcedureCodea439ce381bba") THEN "AF"
 ELSE IF q.stage \in {"TurnLoop","OpenPR"} THEN "AG"
 ELSE IF q.stage \in {"TurnContinue","LatchNew"} THEN "AE" ELSE q.activeStepRole

Exact module download · Source bundle and reproduction instructions

AOpenCheckpoint · operator

reference-profile · input revision 2 · CC0 1.0

AOpenCheckpoint(kind,originalCaller,resume,role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 worldId==q.nextWorld
     caller==IF role="ActionCost" /\ AMutation="wrong-cost-caller" THEN [originalCaller EXCEPT !.transactionId=201] ELSE originalCaller
     event==CASE kind="Cost" -> [q.costEvent EXCEPT !.caller=caller]
        [] kind="SchemaAtom126" -> [id |-> q.nextEvent,caller |-> caller,complete |-> WindowTop9(q.stack).stage="NeedCheckpoint",
             tag |-> "PriorityAboutToBeReceived",player |-> WindowTop9(q.stack).priority]
        [] OTHER -> [id |-> q.nextEvent,caller |-> caller,complete |-> q.childPlan.phase="Complete",
             tag |-> "InstructionFinished",origin |-> "Ability",instruction |-> IF q.reactionContext.instanceId=301 THEN "AbilityInstruction720" ELSE "AbilityInstruction721",
             instructionRef |-> InstructionWindowRef93(q.childPlan),finishedPlan |-> q.childPlan]
     site==[kind |-> kind,caller |-> caller,eventId |-> event.id,snapshotId |-> worldId,inside |-> AInside(q)]
     frame==NewCheckpoint103(id,caller,worldId,AInside(q)) frames==AJoin(q.frames,[k \in {id} |-> frame])
 IN /\ id<=32 /\ event.id<=64 /\ worldId<=2256 /\ worldId \notin q.issuedWorlds
    /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,frame,id,site,event,AInside(q))
    /\ (kind="Cost" => ANativeCommitted(q) /\ q.actionPointWorld.checkpointDue /\ q.nativeCommitCount=1)
    /\ (kind="SchemaAtom126" => originalCaller=ConditionalPriorityCaller96(WindowTop9(q.stack)))
    /\ (kind="Instruction" => originalCaller=ConditionalInstructionCaller96(q.child) /\ q.childPlan.phase="Complete")
    /\ qT11'=[q EXCEPT !.frames=frames,!.frameRoles=AJoin(@,[k \in {id} |-> role]),!.sites=@ \cup {CheckpointSiteKey103(site)},!.currentCP=id,
       !.checkpointEvents=AJoin(@,[k \in {id} |-> event]),!.basisHistory=AJoin(@,[k \in {id} |-> MinimalCaptureSA(ABasis(q))]),
       !.costCP=IF role="ActionCost" THEN id ELSE @,!.cpResume=resume,!.cpRole=role,!.stage="ACP",
       !.issuedWorlds=@ \cup {worldId},!.nextWorld=@+1,!.nextEvent=IF kind="Cost" THEN @ ELSE @+1,!.issuedEvents=@ \cup {event.id}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalInstructionCaller96, ConditionalPriorityCaller96, WindowTop9, MinimalCaptureSA, ABasis, AInside, AJoin, ANativeCommitted, event, frame, frames, id, q, site, worldId, BeginCheckpointSite103, CheckpointSiteKey103, qT11

AOpenStep · operator

reference-profile · input revision 2 · CC0 1.0

AOpenStep(role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 world==q.nextWorld original==q.stepEvents[role]
     caller==IF role="AF" /\ AMutation="wrong-af-caller" THEN [original.caller EXCEPT !.step="ProcedureCodea439ce381bba"]
       ELSE IF role="AE" /\ AMutation="wrong-ae-window" THEN [original.caller EXCEPT !.windowId=@+1] ELSE original.caller
     event==[original EXCEPT !.caller=caller]
     site==[kind |-> "Instruction",caller |-> caller,eventId |-> event.id,snapshotId |-> world,inside |-> AInside(q)]
     f==NewCheckpoint103(id,caller,world,AInside(q)) frames==AJoin(q.frames,[key \in {id} |-> f])
 IN /\ role \in DOMAIN q.stepEvents /\ q.stepCP[role]=0 /\ APlacement(q,role)
    /\ id<=32 /\ world<=2256 /\ world \notin q.issuedWorlds /\ event.id \in q.issuedEvents
    /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,f,id,site,event,AInside(q))
    /\ qT11'=[q EXCEPT !.frames=frames,!.frameRoles=AJoin(@,[key \in {id} |-> role]),!.sites=@ \cup {CheckpointSiteKey103(site)},
       !.checkpointEvents=AJoin(@,[key \in {id} |-> event]),!.basisHistory=AJoin(@,[key \in {id} |-> MinimalCaptureSA(ABasis(q))]),
       !.stepCP[role]=id,!.activeStepRole=role,!.currentCP=id,!.cpRole=role,!.cpResume="AStepReturn",!.stage="ACP",
       !.issuedWorlds=@ \cup {world},!.nextWorld=@+1,
       !.stepOpenRecords=AJoin(@,[key \in {role} |-> [checkpointId |-> id,stack |-> q.stack,flow |-> q.flow,event |-> event]]),
       !.lifecycle=Append(@,ALife(q,"StepOpen",role,id,0))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, ABasis, AInside, AJoin, APlacement, event, f, frames, id, q, site, world, ALife, BeginCheckpointSite103, CheckpointSiteKey103, qT11

AOuterSafety · operator

reference-profile · input revision 2 · CC0 1.0

AOuterSafety ==
 LET q==qT11 IN
 /\ SideBProcedureValid5(q.flow) /\ TraversalFrameValid6(q.control.traversal)
 /\ AReturnGuardChecks(q)
 /\ IActionWindowOrderT11(q)
 /\ \A i \in 1..Len(q.windowHistory) : IWindowClassT11(q.windowHistory[i])=IntegrationOracleWindowClasses11[q.windowHistory[i].at] /\ ~PaidWindowOptions9(q.windowHistory[i].site).score
 /\ (q.action.status#"Complete" => \A i \in 1..Len(q.windowHistory) : q.windowHistory[i].at#"5.7.1f:new")
 /\ q.objects=AObjects /\ ANativeProjection(q.objects)=IInitialT11.objects /\ q.fund=0 /\ q.bank=0
 /\ q.actionPointWorld.actionPoints["SideB"] \in {IntegrationOracleStartActionPoints11,IntegrationOracleEndActionPoints11}
 /\ q.trace=SubSeq(IntegrationOracleTrace11,1,Len(q.trace))
 /\ IEventNamesT11(q) \cap IntegrationOracleAbsent11={}
 /\ \A i \in 1..Len(q.stack) : PriorityWindowValid9(q.stack[i])
 /\ \A id \in DOMAIN q.control.itemInspections : ItemInspectionProcedureValid7(q.control.itemInspections[id],q.objects)
 /\ \A id \in DOMAIN q.control.siteInspections : InspectionProcedureValid7(q.control.siteInspections[id])
 /\ (q.action.status="Nested" => q.waitTraversal.handle=q.action.nested /\ q.waitTraversal.id=q.control.traversal.id)
 /\ (q.action.status="Nested" => Len(q.stack)>0 /\ q.stack[1].kind="NeutralValue00001" /\ q.stack[1].open
       /\ q.stack[1].stage="Resolving" /\ q.stack[1].busy=IActionOptionT11)
 /\ ("ItemInspection" \in q.consumed => IAT11(q).returned)
 /\ ("Inspection" \in q.consumed => IBT11(q).returned)
 /\ ("SchemaAtom138" \in q.consumed => q.control.returned)
 /\ (q.done =>
       /\ q.trace=IntegrationOracleTrace11 /\ q.returnOrder=IntegrationOracleReturnOrder11
       /\ q.actionPointWorld.actionPoints["SideB"]=IntegrationOracleEndActionPoints11 /\ q.actionPointWorld.spent["SideB"]=1
       /\ q.action.status="Complete" /\ q.control.returned /\ q.control.traversal.complete /\ q.control.traversal.successful /\ ~q.control.traversal.unsuccessful
       /\ InspectionCentralChoices7(IBT11(q))=IntegrationOracleCentralChoices11
       /\ Cardinality(ActualItemInspectionesInInspection7(q.itemInspectionHistory,20))=IntegrationOracleActualItemInspectiones11
       /\ \A name \in IntegrationOracleEvents11 : IEventCountT11(q,name)=1
       /\ Len(q.stack)=1 /\ WindowTop9(q.stack).kind="NeutralValue00001" /\ WindowTop9(q.stack).stage="Ready" /\ WindowTop9(q.stack).priority="SideB"
       /\ WindowTop9(q.stack).id#q.NeutralValue00003.opened.id /\ WindowTop9(q.stack).busy=NoPriorityOption9
       /\ ~CanPassPriority9(WindowTop9(q.stack),EmptyT11))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanPassPriority9, NoPriorityOption9, PaidWindowOptions9, PriorityWindowValid9, WindowTop9, ANativeProjection, AObjects, q, AReturnGuardChecks, IntegrationOracleAbsent11, IntegrationOracleActualItemInspectiones11, IntegrationOracleCentralChoices11, IntegrationOracleEndActionPoints11, IntegrationOracleEvents11, IntegrationOracleReturnOrder11, IntegrationOracleStartActionPoints11, IntegrationOracleTrace11, IntegrationOracleWindowClasses11, IAT11, IActionOptionT11, IActionWindowOrderT11, IBT11, IEventCountT11, IEventNamesT11, IInitialT11, IWindowClassT11, ActualItemInspectionesInInspection7, InspectionCentralChoices7, InspectionProcedureValid7, ItemInspectionProcedureValid7, EmptyT11, TraversalFrameValid6, SideBProcedureValid5

AOuterStep · operator

reference-profile · input revision 2 · CC0 1.0

AOuterStep ==
 LET q==qT11 c==q.control IN
 /\ UNCHANGED guideCaseT11
 /\ CASE q.stage="LatchStart" ->
        LET after==[q.flow EXCEPT !.decision="NeutralValue00001"] IN
        /\ SideBLatchDecision5(q.flow,after,q.actionPointWorld.actionPoints["SideB"],TRUE)
        /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenAction"]
   [] q.stage="OpenAction" -> IOpenWindowT11("NeutralValue00001",ITurnSiteT11(q),"StartAction","ActionPay")
   [] q.stage="Window" -> AWindowWork
   [] q.stage="ActionPay" -> AActionPay
   [] q.stage="ActionCostDrain" -> AOpenCheckpoint("Cost",ACostCaller(q),"ACostResume","ActionCost")
   [] q.stage="ActionEffects" -> AEffects
   [] q.stage="TraversalStart" ->
        LET after==[q.action EXCEPT !.status="Nested",!.nested="Traversal7"] traversal==OpenTraversal6(7,1000,ITraversalCallerT11(q.action)) IN
        /\ ActionNestedBegin5(q.action,after,"Traversal7")
        /\ qT11'=[q EXCEPT !.action=after,!.waitTraversal=[id |-> traversal.id,handle |-> "Traversal7",action |-> q.action.id],!.control=TraversalControlT11(traversal),!.stage="TraversalWork"]
   [] q.stage="TraversalWork" -> ITraversalWorkT11
   [] q.stage="TraversalAdvance" -> ITraversalAdvanceT11
   [] q.stage="InspectionWork" -> IInspectionWorkT11
   [] q.stage="InspectionAdvance" -> IInspectionAdvanceT11
   [] q.stage="ItemInspectionWork" -> IItemInspectionWorkT11
   [] q.stage="ItemInspectionAdvance" -> IItemInspectionAdvanceT11
   [] q.stage="Drain" ->
        qT11'=[q EXCEPT !.drains=Append(@,[step |-> q.lastWork,insideItemInspection |-> IInsideItemInspectionT11(q),insideInspection |-> IInsideInspectionT11(q),duringTraversal |-> DuringTraversal6(c.traversal)]),!.revision=@+1,!.stage=q.resume]
   [] q.stage="ItemInspectionReturn" ->
        LET a==IAT11(q) after==[a EXCEPT !.returned=TRUE] next==IWithItemInspectionT11(q,after) IN
        /\ ReturnItemInspectionToCaller7(a,after,TRUE,InspectionItemInspectionCaller7(IBT11(q)))
        /\ qT11'=IRecordReturnT11(next,"ItemInspection",after,IBT11(q).id,"InspectionResume")
   [] q.stage="InspectionResume" ->
        LET b==IBT11(q) after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
        /\ IItemInspectionReturnReadyT11(q) /\ FinishInspectionItemInspectionInstruction7(b,after,IItemInspectionReturnReadyT11(q))
        /\ qT11'=IRecordT11([IWithInspectionT11(q,after) EXCEPT !.consumed=@ \cup {"ItemInspection"}],"7.5.5:return",{},"InspectionAdvance")
   [] q.stage="InspectionReturn" ->
        LET b==IBT11(q) after==[b EXCEPT !.returned=TRUE] next==IWithInspectionT11(q,after) IN
        /\ ReturnInspectionToCaller7(b,after,TRUE,IInspectionCallerT11(c.traversal))
        /\ qT11'=IRecordReturnT11(next,"Inspection",after,c.traversal.id,"TraversalResume")
   [] q.stage="TraversalResume" ->
        LET after==[c EXCEPT !.siteInspectionFinished=TRUE] IN
        /\ IInspectionReturnReadyT11(q) /\ FinishRulesInspectionInstruction6(c,after,IInspectionReturnReadyT11(q))
        /\ qT11'=IRecordT11([q EXCEPT !.control=after,!.consumed=@ \cup {"Inspection"}],"6.9.5b:return",{},"TraversalAdvance")
   [] q.stage="TraversalReturn" ->
        LET after==[c EXCEPT !.returned=TRUE] next==[q EXCEPT !.control=after] IN
        /\ ReturnTraversalToCaller6(c,after,TRUE,ITraversalCallerT11(q.action))
        /\ qT11'=IRecordReturnT11(next,"SchemaAtom138",after,q.action.id,"ActionResume")
   [] q.stage="ActionResume" ->
        LET after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"] IN
        /\ ITraversalReturnReadyT11(q) /\ ActionNestedReturn5(q.action,after,q.waitTraversal.handle,ITraversalReturnReadyT11(q))
        /\ qT11'=[q EXCEPT !.action=after,!.consumed=@ \cup {"SchemaAtom138"},!.stage="ActionComplete"]
   [] q.stage="ActionComplete" -> ACompleteAction
   [] q.stage="ActionWindowReturn" ->
        LET w==WindowTop9(q.stack) closed==CompletePriorityOptionFrame9(w) IN
        /\ CompletePriorityOption9(q.stack,ReplaceWindowTop9(q.stack,closed),AActionReturn(q))
        /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,closed),!.closedWindows=AJoin(@,[role \in {"AF"} |-> closed]),
           !.lifecycle=Append(@,ALife(q,"ActionClose","AF",0,1)),!.returnOrder=Append(@,"NeutralValue00001"),!.stage="PopAction"]
   [] q.stage="PopAction" ->
        /\ PopClosedPriorityWindow9(q.stack,<<>>) /\ WindowTop9(q.stack)=q.closedWindows["AF"]
        /\ qT11'=[q EXCEPT !.poppedWindows=AJoin(@,[role \in {"AF"} |-> WindowTop9(q.stack)]),!.stack= <<>>,
           !.lifecycle=Append(@,ALife(q,"ActionPop","AF",0,0)),!.stage="Drain"]
   [] q.stage="TurnAdvance" -> AAdvanceStep("AF")
   [] q.stage="TurnLoop" -> AAdvanceStep("AG")
   [] q.stage="OpenPR" -> IOpenWindowT11("Paid",ITurnSiteT11(q),"TurnPR","TurnContinue")
   [] q.stage="TurnContinue" -> AAdvanceStep("AE")
   [] q.stage="LatchNew" ->
        LET after==[q.flow EXCEPT !.decision="NeutralValue00001"] IN
        /\ SideBLatchDecision5(q.flow,after,q.actionPointWorld.actionPoints["SideB"],ALatchAfterSteps(q)) /\ qT11'=[q EXCEPT !.flow=after,!.stage="OpenNewAction"]
   [] q.stage="OpenNewAction" ->
        /\ q.stack= <<>> /\ ActionReadyToContinue5(q.action) /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"}
        /\ IOpenWindowT11("NeutralValue00001",ITurnSiteT11(q),"NewAction","Done")
   [] q.stage="Done" -> UNCHANGED qT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOption9, PopClosedPriorityWindow9, ReplaceWindowTop9, WindowTop9, AActionReturn, ACostCaller, AJoin, ALatchAfterSteps, after, b, next, after, b, next, after, next, after, after, after, after, after, after, a, c, closed, q, traversal, AActionPay, AAdvanceStep, ACompleteAction, AEffects, ALife, AOpenCheckpoint, AWindowWork, IBT11, IInsideInspectionT11, IInsideItemInspectionT11, IInspectionAdvanceT11, IInspectionCallerT11, IInspectionReturnReadyT11, IInspectionWorkT11, IItemInspectionAdvanceT11, IItemInspectionReturnReadyT11, IItemInspectionWorkT11, IOpenWindowT11, IRecordReturnT11, IRecordT11, ITraversalAdvanceT11, ITraversalCallerT11, ITraversalReturnReadyT11, ITraversalWorkT11, ITurnSiteT11, IWithInspectionT11, FinishInspectionItemInspectionInstruction7, InspectionItemInspectionCaller7, ReturnInspectionToCaller7, ReturnItemInspectionToCaller7, guideCaseT11, qT11, DuringTraversal6, FinishRulesInspectionInstruction6, ReturnTraversalToCaller6, TraversalControlT11, ActionNestedBegin5, ActionNestedReturn5, ActionReadyToContinue5, SideBLatchDecision5

AProtocolWork · operator

reference-profile · input revision 2 · CC0 1.0

AProtocolWork ==
 LET q==qT11 IN
 CASE q.stage="AReceive" -> AOpenCheckpoint("SchemaAtom126",ConditionalPriorityCaller96(WindowTop9(q.stack)),"AChildReady","ChildPriority")
 [] q.stage="AChildReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(AFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),AReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage=IF q.childReturned THEN "APass" ELSE "ASelect"]
 [] q.stage="ASelect" ->
   LET w==WindowTop9(q.stack) context==q.reactionContext id==context.instanceId d==context.definition
       option==PriorityOption9(70,"Conditional","SideB",d.syntax.id,id,d.syntax.source,0,{})
       busy==StartPriorityOptionFrame9(w,option,context.transaction) p==OpenConditionalProcedure96(id,d,w,option,context.transaction,"Rule")
       plan==OpenInstruction93(context.instructionId,"Ability",id,d.syntax.source,"Rule",1,"NoValue",<<context.work>>,FALSE)
       imminent==[p EXCEPT !.phase="Imminent",!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.detached=TRUE]
       announced==[plan EXCEPT !.phase="Imminent",!.announced=TRUE] ledger==[q.ledger EXCEPT !.instances[q.reactionContext.instanceId].status="Imminent"]
   IN /\ q.nextWorld \notin q.issuedWorlds /\ q.nextWorld<=2256
      /\ AAdmitSnapshot(q,q.objects,q.ledger,ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint))
      /\ BeginConditionalResolution96(q.ledger,ledger,q.stack,ReplaceWindowTop9(q.stack,busy),p,imminent,d,
        ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint),id,option,ALegality(w,option,context.transaction),EmptyT11,plan,announced,
        ATargets(plan,{}),ProtocolP!Entry9p(plan,0),AChildTurnUses(q),
        [tag |-> "AbilityRestrictions",ability |-> d.syntax.id,source |-> d.syntax.source,results |-> EmptyT11])
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.stack=ReplaceWindowTop9(@,busy),!.child=imminent,!.childPlan=announced,!.captures=AAddCapture(q,ASnapshot(q,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint)),!.issuedWorlds=@ \cup {q.nextWorld},!.nextWorld=@+1,!.stage="AChildBegin"]
 [] q.stage="AChildBegin" ->
   LET p==[q.child EXCEPT !.phase="Resolve",!.ability.phase="Resolving"] plan==[q.childPlan EXCEPT !.phase="Resolving"]
       expected==[tag |-> "ConditionalExpectedEffects",point |-> "ExpectedEffectsBeforeInterrupt",instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]
       ledger==[q.ledger EXCEPT !.instances[q.reactionContext.instanceId].status="Resolving",!.instances[q.reactionContext.instanceId].expected=[i \in {1} |->
         [instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]]]
   IN /\ ResolveConditionalWithoutInterrupt96(q.ledger,ledger,q.stack,q.child,p,q.childPlan,plan,
        ProtocolP!NoModifiers9p(q.childPlan),ProtocolP!Clearance9p(q.childPlan),expected)
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.stage="AChildWork"]
 [] q.stage="AChildWork" ->
   LET ability==ProtocolP!FinishedAbility9p(q.child.ability,q.childPlan)
       p==[q.child EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0]
       plan==ProtocolP!FinishedPlan9p(q.childPlan) ledger==[q.ledger EXCEPT !.instances[q.reactionContext.instanceId].status="Complete"]
       beforeId==IF AMutation="reuse-world-id" THEN q.costOccurrence.snapshot.id ELSE q.nextWorld
       beforeSnapshot==ASnapshot(q,q.ledger,beforeId,"InstructionBefore",q.ledger.lastCheckpoint)
       afterSnapshot==ASnapshot(q,ledger,q.nextWorld+1,"InstructionAfter",q.ledger.lastCheckpoint)
       captures==AJoin(AAddCapture(q,beforeSnapshot),[key \in {<<afterSnapshot.id,afterSnapshot.point>>} |-> ACapture(q,afterSnapshot)])
       step==[ProtocolP!Step9p(q.childPlan) EXCEPT !.complete=AMutation#"blocked-child-carry"]
       publishedCaptures==IF AMutation="history-rewrite" THEN [captures EXCEPT ![<<1,PInitialSnapshot.point>>].basis.revision=1] ELSE captures
   IN /\ AAdmit(q,q.ledger,beforeSnapshot) /\ AAdmit(q,ledger,afterSnapshot)
      /\ RecordConditionalExecutionUse96(q.ledger,q.ledger,q.child,q.childPlan,
        [tag |-> "ConditionalEffectExecution",instruction |-> InstructionWindowRef93(q.childPlan),abilityInstance |-> q.child.id,
         source |-> q.child.ability.source,partIds |-> {1}],q.uses,q.uses,q.turnUses,q.turnUses,2,{})
      /\ CarryConditionalInstruction96(q.ledger,ledger,ledger,q.stack,q.stack,q.child,p,q.childPlan,plan,step,beforeSnapshot,afterSnapshot)
      /\ beforeId \notin q.issuedWorlds /\ q.nextWorld+1 \notin q.issuedWorlds /\ q.nextWorld+1<=2256
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.noUseCount=@+1,!.noUseChildren=@ \cup {q.child.id},
        !.captures=publishedCaptures,!.issuedWorlds=@ \cup {q.nextWorld,q.nextWorld+1},!.nextWorld=@+2,
        !.work=Append(@,q.reactionContext.work),!.stage="AChildCPOpen"]
 [] q.stage="AChildCPOpen" -> AOpenCheckpoint("Instruction",ConditionalInstructionCaller96(q.child),"AChildCPDone","ChildFinal")
 [] q.stage="AChildCPDone" ->
   LET p==[q.child EXCEPT !.phase="Complete",!.checkpoint=q.currentCP]
       receipt==[tag |-> "ConditionalInstructionCheckpoint",id |-> q.currentCP,abilityInstance |-> q.child.id,
        transactionId |-> q.child.transaction,source |-> q.child.ability.source,instruction |-> q.childPlan.id,index |-> 1,
        complete |-> CheckpointDrained103(AFrame(q),q.ledger,q.stack),
        allNewerChainsComplete |-> CheckpointDrained103(AFrame(q),q.ledger,q.stack)]
   IN /\ ResumeConditionalInstructionAfterCheckpoint103(AFrame(q),q.ledger,q.stack,q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stage="AChildReturn"]
 [] q.stage="AChildReturn" ->
   LET p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE] w==WindowTop9(q.stack)
       receipt==AChildReturnReceipt(q)
   IN /\ FinishConditionalProcedure96(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(w)),q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.childReturned=TRUE,!.stage="AReceive"]
 [] q.stage="APass" ->
   LET w==WindowTop9(q.stack) after==PassPriorityFrame9(w)
       snapshot==ACurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Pass",q.ledger.lastCheckpoint)
   IN /\ q.nextWorld \notin q.issuedWorlds /\ q.nextWorld<=2256
      /\ AAdmitSnapshot(q,q.objects,q.ledger,snapshot)
      /\ PassConditionalPriority96(q.ledger,q.ledger,q.ledger,q.stack,ReplaceWindowTop9(q.stack,after),w.priority,EmptyT11,snapshot,snapshot)
      /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,after),!.captures=AAddCapture(q,snapshot),!.issuedWorlds=@ \cup {snapshot.id},!.nextWorld=@+1,!.stage=IF after.open THEN "AReceive" ELSE "AReactionReturn"]
 [] q.stage="AReactionReturn" ->
   LET f==q.frames[q.reactionOwner.id] returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] rest==SubSeq(q.stack,1,Len(q.stack)-1)
   IN /\ ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,IF AMutation="wrong-reaction-return" THEN [f.caller EXCEPT !.transactionId=201] ELSE f.caller)
      /\ qT11'=[ASetFrame(q,returned) EXCEPT !.stack=rest,!.currentCP=q.reactionOwner.id,!.cpRole=q.reactionOwner.role,!.cpResume=q.reactionOwner.resume,!.stage=q.reactionOwner.resume,
        !.checkpointHistory=Append(@,[id |-> f.id,role |-> q.reactionOwner.role,caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
 [] q.stage="ACostResume" ->
   /\ AActionCostDrained(q,ACostCaller(q)) /\ q.actionPointWorld=q.payment.after
   /\ qT11'=[q EXCEPT !.actionPointWorld.checkpointDue=FALSE,!.costDrained=TRUE,!.currentCP=q.costCP,!.stage="ActionEffects",
       !.native=IF AMutation="native-payment-rewrite" THEN [@ EXCEPT !.before.actionPoints["SideB"]=3] ELSE @,
       !.nativeEvents=IF AMutation="sticky-payment-alias" THEN AJoin(@,[id \in {2} |-> [q.costEvent EXCEPT !.id=2]]) ELSE @]
 [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginConditionalResolution96, CarryConditionalInstruction96, CompletePriorityOptionFrame9, ConditionalInstructionCaller96, ConditionalPriorityCaller96, FinishConditionalProcedure96, InstructionWindowRef93, PassConditionalPriority96, RecordConditionalExecutionUse96, ReplaceWindowTop9, ResolveConditionalWithoutInterrupt96, WindowTop9, AActionCostDrained, AAddCapture, AAdmit, ACostCaller, AJoin, ASnapshot, ledger, p, plan, receipt, ledger, p, plan, receipt, w, ledger, p, plan, w, p, w, p, after, afterSnapshot, announced, beforeId, beforeSnapshot, busy, context, d, expected, f, id, imminent, option, publishedCaptures, q, ready, rest, returned, snapshot, step, AMutation, AAdmitSnapshot, AChildTurnUses, ACurrentSnapshot, AFrame, ALegality, AOpenCheckpoint, AReadyCP, ASetFrame, ATargets, ReceivePriorityAfterCheckpoint103, ResumeConditionalInstructionAfterCheckpoint103, ReturnCheckpointAfterReaction103, ProtocolP!Clearance9p, ProtocolP!Entry9p, ProtocolP!NoModifiers9p, EmptyT11, qT11

AReadyCP · operator

reference-profile · input revision 2 · CC0 1.0

AReadyCP(q) == [ProtocolP!PriorityCP9p(WindowTop9(q.stack),q.currentCP) EXCEPT
 !.complete=CheckpointDrained103(AFrame(q),q.ledger,q.stack),!.reactionsDrained=CheckpointDrained103(AFrame(q),q.ledger,q.stack)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, AFrame, CheckpointDrained103, ProtocolP!PriorityCP9p

AReturnGuardChecks · operator

reference-profile · input revision 2 · CC0 1.0

AReturnGuardChecks(q) ==
 /\ (q.stage="ItemInspectionReturn" =>
       LET a==IAT11(q) after==[a EXCEPT !.returned=TRUE] IN
       /\ ReturnItemInspectionToCaller7(a,after,TRUE,InspectionItemInspectionCaller7(IBT11(q)))
       /\ ~ReturnItemInspectionToCaller7(a,after,FALSE,InspectionItemInspectionCaller7(IBT11(q)))
       /\ ~ReturnItemInspectionToCaller7(a,after,TRUE, <<"InspectionItemInspection",21>>))
 /\ (q.stage="InspectionResume" =>
       LET a==IAT11(q) b==IBT11(q) after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
       /\ IItemInspectionReturnReadyT11(q)
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].parent=21])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].revision=q.revision-1])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].frame=[a EXCEPT !.returned=FALSE]])
       /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.consumed=@ \cup {"ItemInspection"}])
       /\ ItemInspectionProcedureValid7([a EXCEPT !.id=78],q.objects) /\ ~InspectionChildReturnedT11(b,[a EXCEPT !.id=78])
       /\ ~InspectionChildReturnedT11(b,[a EXCEPT !.caller= <<"InspectionItemInspection",21>>])
       /\ ~FinishInspectionItemInspectionInstruction7(b,after,FALSE)
       /\ ~ReturnItemInspectionToCaller7(a,a,TRUE,InspectionItemInspectionCaller7(b)))
 /\ (q.stage="InspectionReturn" =>
       LET b==IBT11(q) after==[b EXCEPT !.returned=TRUE] IN
       /\ ~ReturnInspectionToCaller7(b,after,FALSE,IInspectionCallerT11(q.control.traversal))
       /\ ~ReturnInspectionToCaller7(b,after,TRUE, <<"TraversalInspectionInstruction",8,"ProcedureCoded75d879e00ff">>))
 /\ (q.stage="TraversalResume" =>
       /\ IInspectionReturnReadyT11(q)
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].revision=q.revision-1])
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].frame.choices= <<>>])
       /\ ~IInspectionReturnReadyT11([q EXCEPT !.consumed=@ \cup {"Inspection"}])
       /\ ~ReturnInspectionToCaller7(IBT11(q),IBT11(q),TRUE,IInspectionCallerT11(q.control.traversal)))
 /\ (q.stage="TraversalReturn" =>
       LET c==q.control after==[c EXCEPT !.returned=TRUE] IN
       /\ ~ReturnTraversalToCaller6(c,after,FALSE,ITraversalCallerT11(q.action))
       /\ ~ReturnTraversalToCaller6(c,after,TRUE, <<"BasicTraversalAction",31>>)
       /\ ~CompletePriorityOption9(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))),AActionReturn(q)))
 /\ (q.stage="ActionResume" =>
       LET after==[q.action EXCEPT !.status="Effects",!.nested="NoValue"] IN
       /\ ITraversalReturnReadyT11(q)
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].revision=q.revision-1])
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].frame.itemInspections[77].returned=FALSE])
       /\ ~ITraversalReturnReadyT11([q EXCEPT !.consumed=@ \cup {"SchemaAtom138"}])
       /\ ~ActionNestedReturn5(q.action,after,"SiblingTraversal",TRUE)
       /\ ~ActionNestedReturn5(q.action,after,q.waitTraversal.handle,FALSE)
       /\ ~ReturnTraversalToCaller6(q.control,q.control,TRUE,ITraversalCallerT11(q.action)))
 /\ (q.stage="ItemInspectionWork" /\ "ItemInspection" \notin DOMAIN q.receipts =>
       /\ ~IItemInspectionReturnReadyT11(q)
       /\ ~ReturnInspectionToCaller7(IBT11(q),[IBT11(q) EXCEPT !.returned=TRUE],TRUE,IInspectionCallerT11(q.control.traversal))
       /\ ~ReturnTraversalToCaller6(q.control,[q.control EXCEPT !.returned=TRUE],TRUE,ITraversalCallerT11(q.action))
       /\ ~ReturnItemInspectionToCaller7(IAT11(q),[IAT11(q) EXCEPT !.returned=TRUE],TRUE,InspectionItemInspectionCaller7(IBT11(q))))
 /\ (q.stage="OpenNewAction" =>
       LET site==ITurnSiteT11(q) oldId==q.NeutralValue00003.opened.id w==NewPriorityWindow9(oldId,"NeutralValue00001",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0) IN
       /\ ~OpenPriorityWindow9(q.stack,Append(q.stack,w),oldId,"NeutralValue00001",site,EmptyT11,IOpeningT11(oldId,"NeutralValue00001",site),q.usedWindows)
       /\ q.action.status="Complete" /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"})
 /\ (q.stage \in {"ActionComplete","ActionWindowReturn"} =>
       LET after==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
       /\ (CompletePriorityOption9(q.stack,after,AActionReturn(q)) = (q.stage="ActionWindowReturn"))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.action.status="Effects"]))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.control.returned=FALSE]))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.consumed=@ \ {"SchemaAtom138"}]))
       /\ ~CompletePriorityOption9(q.stack,after,AActionReturn([q EXCEPT !.costDrained=FALSE])))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOption9, CompletePriorityOptionFrame9, OpenPriorityWindow9, ReplaceWindowTop9, WindowTop9, AActionReturn, a, after, b, a, after, b, after, after, after, after, c, oldId, site, w, IAT11, IBT11, IInspectionCallerT11, IInspectionReturnReadyT11, IItemInspectionReturnReadyT11, IOpeningT11, ITraversalCallerT11, ITraversalReturnReadyT11, FinishInspectionItemInspectionInstruction7, InspectionItemInspectionCaller7, ItemInspectionProcedureValid7, ReturnInspectionToCaller7, ReturnItemInspectionToCaller7, InspectionChildReturnedT11, EmptyT11, ReturnTraversalToCaller6, ActionNestedReturn5

ASetFrame · operator

reference-profile · input revision 2 · CC0 1.0

ASetFrame(q,f) == [q EXCEPT !.frames[f.id]=f]

Exact module download · Source bundle and reproduction instructions

ASourceSafety · operator

reference-profile · input revision 2 · CC0 1.0

ASourceSafety ==
 LET q==qT11 IN
 /\ q.catalog=ACatalog /\ q.abilityRegistry=q.catalog /\ q.abilityRevision=0
 /\ q.rulePermissions=A2Permissions(q.scenario)
 /\ q.actionPhaseId=4000 /\ q.flow.turn.id=2 /\ q.flow.turn.phase="NeutralValue00001"
 /\ BasisValidSA(q.catalog,ABasis(q)) /\ LedgerDomainSA(q.ledger)
 /\ q.uses=EmptyT11 /\ q.turnUses=EmptyT11 /\ q.useIndex=EmptyT11 /\ q.procedures=EmptyT11
 /\ UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)
 /\ q.objects=AObjects /\ ANativeProjection(q.objects)=ANativeObjects

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, LedgerDomainSA, UseProvenanceValidSA, A2Permissions, ABasis, ACatalog, ANativeObjects, ANativeProjection, AObjects, q, EmptyT11

ASpec · operator

reference-profile · input revision 2 · CC0 1.0

ASpec == AInit /\ [][ANext]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(ANext)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInit, ANext, guideCaseT11, qT11

ASpecimen0139 · operator

reference-profile · input revision 2 · CC0 1.0

ASpecimen0139(q) ==
 IF q.stage="PopAction" THEN "af-closed-before-pop"
 ELSE IF q.stage="ActionWindowReturn" THEN "af-before-pop"
 ELSE IF q.stage="AStepReturn" THEN "step-return-ready"
 ELSE IF q.stage \in {"TurnAdvance","TurnLoop","TurnContinue"} THEN "step-before-advance"
 ELSE IF (q.stage="Drain" /\ q.lastWork="ProcedureCodea439ce381bba") \/ q.stage \in {"OpenPR","LatchNew"} THEN "step-after-consume"
 ELSE IF q.stage="ACP" /\ q.cpRole="AF" /\ AFrame(q).point="ProcedureCodeb74d673a0fc6" /\ DOMAIN AFrame(q).recognized#{} THEN "af-reaction-pending"
 ELSE IF q.stage="ACP" /\ q.cpRole="ActionCost" THEN "cost-frame-open"
 ELSE IF q.stage="ACostResume" THEN "cost-returned"
 ELSE IF q.stage="ACP" /\ q.cpRole="ChildPriority" /\ q.childReturned /\ AFrame(q).point="ProcedureCodee605a78f5d5e" THEN "post-child-reception"
 ELSE IF q.stage="AChildWork" THEN "child-instruction"
 ELSE IF q.stage="AReactionReturn" THEN "reaction-return" ELSE "other"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AFrame

AStepReturn · operator

reference-profile · input revision 2 · CC0 1.0

AStepReturn ==
 LET q==qT11 role==q.activeStepRole f==q.frames[q.stepCP[role]]
     drain==[step |-> q.lastWork,insideItemInspection |-> IInsideItemInspectionT11(q),insideInspection |-> IInsideInspectionT11(q),duringTraversal |-> DuringTraversal6(q.control.traversal)]
 IN /\ role \notin DOMAIN q.stepReturnReceipts /\ role \notin q.stepConsumed /\ AStepDrained(q,role,f)
    /\ qT11'=[q EXCEPT !.drains=Append(@,drain),!.revision=@+1,!.stage=AStepStage(role),
       !.stepReturnReceipts=AJoin(@,[key \in {role} |-> AStepReceipt(q,role,f,q.revision+1)]),
       !.lifecycle=Append(@,ALife(q,"StepReturn",role,f.id,0))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AJoin, AStepDrained, AStepReceipt, AStepStage, drain, f, q, role, ALife, qT11

AStepSafety · operator

reference-profile · input revision 2 · CC0 1.0

AStepSafety ==
 LET q==qT11 IN
 /\ DOMAIN q.stepEvents \subseteq AStepRoles /\ q.stepConsumed \subseteq DOMAIN q.stepReturnReceipts
 /\ \A role \in {r \in AStepRoles : q.stepCP[r]>0} :
      /\ q.frames[q.stepCP[role]].caller=AStepCaller(q,role,AStepWindow(q,role))
      /\ q.stepOpenRecords[role].stack= <<>> /\ q.stepOpenRecords[role].flow.step=AStepName(role)
      /\ q.checkpointEvents[q.stepCP[role]].origin="TimingStep" /\ q.checkpointEvents[q.stepCP[role]].instruction=AStepName(role)
 /\ \A role \in DOMAIN q.stepContinuations :
      /\ role \in q.stepConsumed /\ q.stepContinuations[role].receipt=q.stepReturnReceipts[role]
      /\ q.stepContinuations[role].before.step=AStepName(role)
 /\ (q.stage \in {"ActionWindowReturn","PopAction"} => q.stepCP["AF"]=0)
 /\ \A row \in {q.lifecycle[i] : i \in 1..Len(q.lifecycle)} :
      /\ (row.tag \in {"TurnPRClose","TurnPRPop"} => "AE" \in DOMAIN q.closedWindows /\ row.windowId=q.closedWindows["AE"].id)
      /\ (row.tag \in {"StepOpen","StepReturn","StepConsume"} => row.windowId=AStepWindow(q,row.role))
 /\ ("AF" \in DOMAIN q.poppedWindows => q.poppedWindows["AF"]=q.closedWindows["AF"] /\ ~q.poppedWindows["AF"].open /\ q.poppedWindows["AF"].kind="NeutralValue00001")
 /\ ("AE" \in DOMAIN q.poppedWindows => q.poppedWindows["AE"]=q.closedWindows["AE"] /\ ~q.poppedWindows["AE"].open /\ q.poppedWindows["AE"].kind="Paid")
 /\ (q.done => \A role \in AStepRoles : \A tag \in {"StepOpen","StepReturn","StepConsume"} :
      Cardinality({i \in 1..Len(q.lifecycle) : q.lifecycle[i].role=role /\ q.lifecycle[i].tag=tag})=1)
 /\ (q.done => q.stepConsumed=AStepRoles /\ DOMAIN q.stepReturnReceipts=AStepRoles /\ DOMAIN q.stepContinuations=AStepRoles)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AStepCaller, AStepName, AStepRoles, AStepWindow, q

ATargets · operator

reference-profile · input revision 2 · CC0 1.0

ATargets(plan,targets) == [ProtocolP!Targets9p(plan) EXCEPT !.targets=targets]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Targets9p

AWindowWork · operator

reference-profile · input revision 2 · CC0 1.0

AWindowWork ==
 LET q==qT11 w==WindowTop9(q.stack) IN
 IF q.windowRole="TurnPR" /\ w.kind="Paid" /\ w.stage="Ready" THEN
   LET passed==PassPriorityFrame9(w) IN
   /\ PassPriority9(q.stack,ReplaceWindowTop9(q.stack,passed),w.priority,EmptyT11)
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,passed),
       !.closedWindows=IF ~passed.open THEN AJoin(@,[key \in {"AE"} |-> passed]) ELSE @,
       !.lifecycle=IF ~passed.open THEN Append(@,[ALife(q,"TurnPRClose","AE",0,Len(q.stack)) EXCEPT !.windowId=passed.id]) ELSE @]
 ELSE IF q.windowRole="TurnPR" /\ w.stage="Closed" THEN
   LET rest==SubSeq(q.stack,1,Len(q.stack)-1) next==IRecordT11([q EXCEPT !.stack=rest],"ProcedureCode484be3e50aa9",{},"TurnContinue")
       source==[kind |-> "NativeTurnPRPop",window |-> w,afterStack |-> rest,flow |-> q.flow]
       event==AStepEvent(next,"AE",q.nextEvent,w.id,source,~w.open /\ w.stage="Closed" /\ q.flow.step="ProcedureCode484be3e50aa9")
   IN /\ w=q.closedWindows["AE"] /\ "AE" \notin DOMAIN q.stepEvents /\ q.nextEvent \notin q.issuedEvents
      /\ PopClosedPriorityWindow9(q.stack,rest)
      /\ qT11'=[next EXCEPT !.stepEvents=AJoin(@,[key \in {"AE"} |-> event]),!.poppedWindows=AJoin(@,[key \in {"AE"} |-> w]),
         !.issuedEvents=@ \cup {event.id},!.nextEvent=@+1,!.lifecycle=Append(@,ALife(q,"TurnPRPop","AE",0,Len(rest)))]
 ELSE IWindowStepT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PassPriority9, PopClosedPriorityWindow9, ReplaceWindowTop9, AJoin, event, next, passed, q, rest, w, ALife, IWindowStepT11, EmptyT11, qT11

AWork · operator

reference-profile · input revision 2 · CC0 1.0

AWork ==
 /\ UNCHANGED guideCaseT11
 /\ IF (qT11.stage="ActionWindowReturn" /\ AMutation="early-af-open") \/ (qT11.stage="PopAction" /\ AMutation="af-before-pop") THEN AOpenStep("AF")
    ELSE IF qT11.stage="TurnAdvance" /\ AMutation="duplicate-step-return" THEN AStepReturn
    ELSE IF qT11.stage="Drain" /\ qT11.lastWork="ProcedureCodea439ce381bba" /\ AMutation="duplicate-af" THEN AAdvanceStep("AF")
    ELSE IF qT11.stage="OpenPR" /\ AMutation="duplicate-ag" THEN AAdvanceStep("AG")
    ELSE IF qT11.stage="LatchNew" /\ AMutation="duplicate-ae" THEN AAdvanceStep("AE")
    ELSE IF qT11.stage="Drain" /\ qT11.lastWork \in {"5.7.1f:return","ProcedureCodea439ce381bba","ProcedureCode484be3e50aa9"}
       THEN AOpenStep(CASE qT11.lastWork="5.7.1f:return" -> "AF" [] qT11.lastWork="ProcedureCodea439ce381bba" -> "AG" [] OTHER -> "AE")
    ELSE IF qT11.stage="AStepReturn" THEN AStepReturn
    ELSE IF qT11.stage="ACP" THEN
       IF qT11.cpRole="ActionCost" /\ AFrame(qT11).point="ProcedureCode88eda145024f" /\ AMutation="skip-cost-stage"
       THEN CheckpointVictory103(AFrame(qT11),ACPNext(AFrame(qT11)),qT11.objects,[id \in DOMAIN qT11.objects |-> 0],AFrame(qT11).snapshotId) /\ UNCHANGED qT11
       ELSE IF qT11.cpRole="ActionCost" /\ AFrame(qT11).point="ProcedureCode88eda145024f" /\ AMutation="early-action-effects" THEN AEffects
       ELSE IF qT11.cpRole="AF" /\ AFrame(qT11).point="ProcedureCodeb74d673a0fc6" /\ AMutation="post-step-child-bypass"
         THEN ABypassReaction
       ELSE IF qT11.cpRole="AF" /\ AFrame(qT11).point="ProcedureCodeb74d673a0fc6" /\ AMutation="advance-with-pending-completion-child" THEN AAdvanceStep("AF")
       ELSE ACheckpointWork
    ELSE IF qT11.stage \in {"AReceive","AChildReady","ASelect","AChildBegin","AChildWork","AChildCPOpen","AChildCPDone","AChildReturn","APass","AReactionReturn","ACostResume"}
       THEN AProtocolWork ELSE AOuterStep

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AMutation, AAdvanceStep, ABypassReaction, ACPNext, ACheckpointWork, AEffects, AFrame, AOpenStep, AOuterStep, AProtocolWork, AStepReturn, CheckpointVictory103, guideCaseT11, qT11