AbilityProceduresMC¶
Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.
Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.
This is a definition inventory. Start with the learning chapters for the contract and its assumptions.
This model/fact module also contains 71 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.
Activity9p · operator
reference-profile · input revision 2 · CC0 1.0
Activity9p == [ActivityContext9 EXCEPT !.activeRules={"ProtocolPaidControl","ProtocolReactionControl"}]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ActivityContext9
CPAfter9p · operator
reference-profile · input revision 2 · CC0 1.0
CPAfter9p(l,cp,allocation,bindings) ==
[l EXCEPT !.lastCheckpoint=cp.id,!.checkpointIds=@ \cup {cp.id},!.checkpoints=[id \in DOMAIN @ \cup {cp.id} |->
IF id=cp.id THEN [caller |-> cp.caller] ELSE @[id]],!.serial=cp.serial,!.lastSnapshot=cp.processingSnapshot,!.processed=@ \cup DOMAIN cp.occurrences,
!.instances=[id \in DOMAIN @ \cup {allocation[k] : k \in DOMAIN allocation} |-> IF id \in DOMAIN @ THEN @[id] ELSE
LET k == CHOOSE key \in DOMAIN allocation : allocation[key]=id
IN NewConditionalInstance96(id,cp.processingSnapshot.definitions[k.definition],cp,k.occurrence,bindings[k].windowId,bindings[k].group)]]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: NewConditionalInstance96
CPData9p · operator
reference-profile · input revision 2 · CC0 1.0
CPData9p(l,caller,events) ==
LET n == l.lastCheckpoint+1
s == SnapshotWithConditionalRegistry96(l.lastSnapshot,l)
b == [s EXCEPT !.id=100+2*n,!.checkpointId=n,!.point="CheckpointBeginning"]
a == [b EXCEPT !.id=101+2*n,!.point="ProcedureCodee605a78f5d5e"]
IN [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> n,previousCheckpoint |-> l.lastCheckpoint,serial |-> l.serial+1,
previousSnapshot |-> l.lastSnapshot,beginSnapshot |-> b,processingSnapshot |-> a,stepSerial |-> l.stepSerial,occurrences |-> events,caller |-> caller]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SnapshotWithConditionalRegistry96
ChildDefinition9p · operator
reference-profile · input revision 2 · CC0 1.0
ChildDefinition9p ==
LET s == Syntax9p(200,"Conditional","ProtocolReactionControl")
IN [syntax |-> s,activity |-> AbilityDefinition9(200,"Conditional",s.source,"Printed"),primaryKind |-> "Trigger",primaryCondition |-> 1,
instructions |-> <<710>>,instructionHasWould |-> FALSE,
trigger |-> [kinds |-> {"AbilityUsed"},subject |-> "SchemaAtom016",actor |-> "SideB",side |-> "SchemaAtom016"],triggerRequirements |-> {},
effectChoices |-> {{1}},optionalParts |-> {},partsByInstruction |-> [i \in {710} |-> {1}],delayedEffect |-> 0,thisTraversal |-> FALSE]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AbilityDefinition9, Syntax9p
Clearance9p · operator
reference-profile · input revision 2 · CC0 1.0
Clearance9p(plan) == [tag |-> "InstructionInterruptReturn",instruction |-> plan.id,revision |-> plan.revision,origin |-> plan.origin,
abilityInstance |-> plan.abilityInstance,index |-> plan.index,source |-> plan.source,sourceZone |-> plan.sourceZone,
windowId |-> 0,openingRevision |-> plan.revision,complete |-> TRUE]Exact module download · Source bundle and reproduction instructions
Definitions9p · operator
reference-profile · input revision 2 · CC0 1.0
Definitions9p(child) == [k \in IF child THEN {ConditionalKey96(ChildDefinition9p)} ELSE {} |-> ChildDefinition9p]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ConditionalKey96, ChildDefinition9p
E9p · operator
reference-profile · input revision 2 · CC0 1.0
E9p == [i \in {} |-> i]Exact module download · Source bundle and reproduction instructions
Entry9p · operator
reference-profile · input revision 2 · CC0 1.0
Entry9p(plan,id) == [tag |-> "AbilityInstructionEntry",abilityInstance |-> plan.abilityInstance,instruction |-> plan.id,
source |-> plan.source,sourceZone |-> plan.sourceZone,index |-> plan.index,schedulerAllows |-> TRUE,sourceEligible |-> TRUE,
checkpointAndAllNewerChainsComplete |-> TRUE,checkpointId |-> id]Exact module download · Source bundle and reproduction instructions
EventuallyReturns9 · operator
reference-profile · input revision 2 · CC0 1.0
EventuallyReturns9 == <> (q9p.stage="Done")Exact module download · Source bundle and reproduction instructions
Resolved project definitions: q9p
FinishedAbility9p · operator
reference-profile · input revision 2 · CC0 1.0
FinishedAbility9p(a,plan) == IF plan.cursor<Len(plan.steps) THEN a ELSE
[a EXCEPT !.phase=IF a.cursor=Len(a.instructions) THEN "Complete" ELSE "Between",
!.lastFinished=a.cursor=Len(a.instructions),!.complete=a.cursor=Len(a.instructions)]Exact module download · Source bundle and reproduction instructions
FinishedPlan9p · operator
reference-profile · input revision 2 · CC0 1.0
FinishedPlan9p(plan) == [plan EXCEPT !.completedSteps=Append(@,plan.steps[plan.cursor]),!.cursor=@+1,
!.phase=IF plan.cursor=Len(plan.steps) THEN "Complete" ELSE "Resolving"]Exact module download · Source bundle and reproduction instructions
InitProcedures9 · operator
reference-profile · input revision 2 · CC0 1.0
InitProcedures9 ==
\E child \in BOOLEAN,steps \in {1,2} : q9p=[stage |-> "Open",child |-> child,steps |-> steps,stack |-> <<>>,
p |-> E9p,plan |-> E9p,childP |-> E9p,childPlan |-> E9p,ledger |-> NewConditionalLedger96(Snapshot9p(child)),
resourceUnits |-> 3,uses |-> E9p,turnUses |-> E9p,costCheckpoint |-> 0,childReturned |-> ~child,work |-> <<>>,tick |-> 0]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: NewConditionalLedger96, E9p, Snapshot9p, q9p
Legality9p · operator
reference-profile · input revision 2 · CC0 1.0
Legality9p(w,option) ==
[tag |-> "PriorityOptionLegality",windowId |-> w.id,reception |-> w.reception,option |-> option,legal |-> TRUE,active |-> TRUE,
transactionId |-> 900+option.id,costsPayable |-> TRUE]Exact module download · Source bundle and reproduction instructions
NextProcedures9 · operator
reference-profile · input revision 2 · CC0 1.0
NextProcedures9 == WorkProcedures9Exact module download · Source bundle and reproduction instructions
Resolved project definitions: WorkProcedures9
NoModifiers9p · operator
reference-profile · input revision 2 · CC0 1.0
NoModifiers9p(plan) == [tag |-> "NoInstructionInterruptModifiers",instruction |-> InstructionWindowRef93(plan),conditionalInstances |-> {},paidInterruptAbilities |-> {}]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: InstructionWindowRef93
Opening9p · operator
reference-profile · input revision 2 · CC0 1.0
Opening9p(id,kind,members,group) ==
[tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> kind,site |-> Site9p,members |-> DOMAIN members,instances |-> members,
group |-> group,beginning |-> NoTimingRef9,instruction |-> [id |-> 0,abilityInstance |-> 0,index |-> 0],effectRevision |-> 0,
modifiersExist |-> FALSE,preparation |-> IF kind="Reaction" THEN <<"ConditionsMet","PendingGroup">> ELSE <<>>]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: NoTimingRef9, Site9p
Option9p · operator
reference-profile · input revision 2 · CC0 1.0
Option9p == PriorityOption9(60,"RegularPaid","SideB",100,0,RootDefinition9p.syntax.source,0,{})Exact module download · Source bundle and reproduction instructions
Resolved project definitions: PriorityOption9, RootDefinition9p
PaidCP9p · operator
reference-profile · input revision 2 · CC0 1.0
PaidCP9p(p,id) ==
[tag |-> "PaidCheckpoint",id |-> id,abilityInstance |-> p.id,transactionId |-> p.transaction,source |-> p.ability.source,
phase |-> p.phase,complete |-> TRUE,allNewerChainsComplete |-> TRUE]Exact module download · Source bundle and reproduction instructions
PriorityCP9p · operator
reference-profile · input revision 2 · CC0 1.0
PriorityCP9p(w,id) ==
[tag |-> "NormalPriorityCheckpoint",id |-> id,windowId |-> w.id,reception |-> w.reception,player |-> w.priority,complete |-> TRUE,reactionsDrained |-> TRUE]Exact module download · Source bundle and reproduction instructions
ProceduresInvariant9 · operator
reference-profile · input revision 2 · CC0 1.0
ProceduresInvariant9 ==
/\ q9p.tick \in 0..50 /\ Len(q9p.stack)<=2 /\ PriorityStackValid9(q9p.stack)
/\ Len(q9p.stack)=2 =>
/\ q9p.p.phase="CostCheckpoint" /\ q9p.stack[1].stage="Resolving" /\ q9p.stack[1].busy=Option9p
/\ q9p.stage="OpenChild" =>
LET proposed == [q9p.p EXCEPT !.phase="Targets",!.checkpoint=q9p.costCheckpoint]
IN /\ ~ConditionalCheckpointDrained96(q9p.ledger,q9p.stack,q9p.costCheckpoint)
/\ ~PaidCheckpointWithConditionals96(q9p.ledger,q9p.stack,q9p.p,proposed,E9p,E9p,PaidCP9p(q9p.p,q9p.costCheckpoint))
/\ q9p.resourceUnits \in {2,3}
/\ q9p.uses=E9p => q9p.resourceUnits=3
/\ q9p.uses # E9p => q9p.uses=UseMap9p /\ q9p.turnUses=TurnUse9p /\ q9p.resourceUnits=2
/\ q9p.stage \in {"SelectChild","ChildBegin","ChildWork","ChildFinalCP","ChildReturn","PopChild"} =>
/\ q9p.p.phase="CostCheckpoint" /\ ~AbilityIsResolving9(q9p.p.ability)
/\ q9p.stack[1].stage="Resolving" /\ q9p.stack[1].busy=Option9p
/\ q9p.stage \in {"EnterRoot","BeginRoot","RootWork","RootCP","RootReturn","Done"} =>
/\ q9p.childReturned /\ q9p.p.costPaid /\ q9p.resourceUnits=2
/\ ConditionalCheckpointDrained96(q9p.ledger,q9p.stack,q9p.costCheckpoint)
/\ q9p.stage="Done" =>
/\ q9p.p.phase="Returned" /\ q9p.p.ability.returned /\ q9p.p.ability.caller=30
/\ Len(q9p.stack)=1 /\ ~q9p.stack[1].open /\ q9p.stack[1].busy.id=0
/\ q9p.work=(IF q9p.child THEN <<"Child">> ELSE <<>>) \o
(IF q9p.steps=2 THEN <<"RootA","RootB","RootFinal">> ELSE <<"RootA","RootFinal">>)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AbilityIsResolving9, ConditionalCheckpointDrained96, PaidCheckpointWithConditionals96, PriorityStackValid9, E9p, Option9p, PaidCP9p, TurnUse9p, UseMap9p, q9p
ProcessCP9p · operator
reference-profile · input revision 2 · CC0 1.0
ProcessCP9p(l,a,stack,cp,conditions,allocation,bindings) ==
ProcessConditionalCheckpoint96(l,a,stack,stack,cp.processingSnapshot.definitions,cp,conditions,allocation,bindings,E9p,E9p,{w.id : w \in {stack[i] : i \in 1..Len(stack)}})Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ProcessConditionalCheckpoint96, E9p
Return9p · operator
reference-profile · input revision 2 · CC0 1.0
Return9p(w,id) ==
[tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> w.busyTransaction,
triggerPayment |-> [tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> w.busyTransaction,
allTriggerCostsPaid |-> TRUE,costCheckpointAndReactionsDrained |-> TRUE],allCostsPaid |-> TRUE,optionComplete |-> TRUE,
childrenReturned |-> TRUE,reactionsDrained |-> TRUE,finalCheckpointId |-> id]Exact module download · Source bundle and reproduction instructions
RootContext9p · operator
reference-profile · input revision 2 · CC0 1.0
RootContext9p ==
[objects |-> E9p,turn |-> Turn9p,traversal |-> NoTraversal6,traversalControl |-> [traversal |-> NoTraversal6,phaseEndedIds |-> {}],
encounter |-> [OpenEncounter6(20,2,0,TRUE,"forced",<<301>>) EXCEPT !.stage="Paid"],
approach |-> [id |-> 10,traversalId |-> 0,begun |-> FALSE],layout |-> E9p,subtypes |-> E9p,strengths |-> E9p,references |-> E9p,
paidRelevance |-> [tag |-> "PaidInterruptRelevance",windowId |-> 0,instruction |-> [id |-> 0],revision |-> 0,eligible |-> {}],
present |-> {100},defaultActive |-> FALSE,activity |-> Activity9p,points |-> [p \in SetupPlayers |-> 0],uses |-> E9p,useProhibitions |-> {},
ownRestrictions |-> [tag |-> "AbilityRestrictions",ability |-> 100,source |-> RootDefinition9p.syntax.source,results |-> E9p],
otherRestrictions |-> [tag |-> "OtherPaidRestrictions",ability |-> 100,source |-> RootDefinition9p.syntax.source,results |-> E9p],currentEffect |-> E9p]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Activity9p, E9p, RootDefinition9p, Turn9p, SetupPlayers, NoTraversal6, OpenEncounter6
RootDefinition9p · operator
reference-profile · input revision 2 · CC0 1.0
RootDefinition9p ==
LET s == Syntax9p(100,"Paid","ProtocolPaidControl")
IN [syntax |-> s,activity |-> AbilityDefinition9(100,"Paid",s.source,"Printed"),triggerCost |-> <<[kind |-> "ResourceUnits",amount |-> 1]>>,
instructions |-> <<700,701>>,instructionHasWould |-> FALSE,ruleTiming |-> "NoValue",canSuppressBarrierInstructions |-> FALSE,
refersApproachedBarrier |-> FALSE,refersEncounteredBarrier |-> FALSE,approachRequirements |-> [subtypes |-> {},activated |-> FALSE,otherIds |-> {}],
encounterRequirements |-> [subtypes |-> {},activated |-> FALSE,otherIds |-> {}],interfaceSubtype |-> [present |-> FALSE,name |-> "NoValue"],
otherRestrictionIds |-> {},refersHosted |-> FALSE]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AbilityDefinition9, Syntax9p
Site9p · operator
reference-profile · input revision 2 · CC0 1.0
Site9p == TurnPrioritySite9(Turn9p,"ProcedureCode484be3e50aa9",10,3,[turn |-> Turn9p,step |-> "ProcedureCode484be3e50aa9"])Exact module download · Source bundle and reproduction instructions
Resolved project definitions: TurnPrioritySite9, Turn9p
Snapshot9p · operator
reference-profile · input revision 2 · CC0 1.0
Snapshot9p(child) ==
[id |-> 1,checkpointId |-> 0,point |-> "ProcedureCodee605a78f5d5e",definitions |-> Definitions9p(child),objects |-> E9p,
present |-> {100,200},ordinaryActivity |-> [k \in DOMAIN Definitions9p(child) |-> FALSE],cardActivity |-> E9p,
activationEpoch |-> [k \in DOMAIN Definitions9p(child) |-> 0],activationSerial |-> 0,activity |-> Activity9p,
points |-> [p \in SetupPlayers |-> 0],progress |-> E9p,link |-> [p \in SetupPlayers |-> 0],exposureMarkers |-> [p \in SetupPlayers |-> 0],
objectiveCompletionEvents |-> {},usedObjects |-> {},holds |-> E9p,effects |-> E9p]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Activity9p, Definitions9p, E9p, SetupPlayers
SpecProcedures9 · operator
reference-profile · input revision 2 · CC0 1.0
SpecProcedures9 == InitProcedures9 /\ [][NextProcedures9]_q9p /\ WF_q9p(WorkProcedures9)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: InitProcedures9, NextProcedures9, WorkProcedures9, q9p
Step9p · operator
reference-profile · input revision 2 · CC0 1.0
Step9p(plan) == [tag |-> "InstructionStepReturn",instruction |-> plan.id,index |-> plan.cursor,step |-> plan.steps[plan.cursor],complete |-> TRUE]Exact module download · Source bundle and reproduction instructions
Syntax9p · operator
reference-profile · input revision 2 · CC0 1.0
Syntax9p(id,kind,rule) ==
[id |-> id,kind |-> kind,side |-> "SideB",controller |-> "SideB",cardKind |-> "NoValue",source |-> RuleAbilitySource9(rule),
units |-> <<TextUnit93(1,"SchemaAtom043",IF kind="Paid" THEN "Cost" ELSE "Trigger",TRUE,0),TextUnit93(10,"Instruction","NoValue",FALSE,0)>>,
arrowAfterFlags |-> TRUE,barrierInstructionPrefix |-> FALSE,paidPrefix |-> [present |-> kind="Paid",bold |-> TRUE,colon |-> TRUE]]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: RuleAbilitySource9, TextUnit93
Targets9p · operator
reference-profile · input revision 2 · CC0 1.0
Targets9p(plan) == [tag |-> "InstructionTargets",instruction |-> plan.id,abilityInstance |-> plan.abilityInstance,
source |-> plan.source,sourceZone |-> plan.sourceZone,index |-> plan.index,valid |-> TRUE,targets |-> {}]Exact module download · Source bundle and reproduction instructions
Turn9p · operator
reference-profile · input revision 2 · CC0 1.0
Turn9p == [OpenTurn5("SideB",1,[p \in SetupPlayers |-> 0]) EXCEPT !.phase="NeutralValue00001"]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetupPlayers, OpenTurn5
TurnUse9p · operator
reference-profile · input revision 2 · CC0 1.0
TurnUse9p == [id \in {1} |-> [turnId |-> 1,ability |-> 100,source |-> RootDefinition9p.syntax.source,useId |-> 1]]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: RootDefinition9p
UseMap9p · operator
reference-profile · input revision 2 · CC0 1.0
UseMap9p == [id \in {1} |-> Used9p]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Used9p
Used9p · operator
reference-profile · input revision 2 · CC0 1.0
Used9p == [tag |-> "AbilityUsed",useId |-> 1,abilityInstance |-> 100,source |-> RootDefinition9p.syntax.source,player |-> "SideB"]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: RootDefinition9p
Window9p · operator
reference-profile · input revision 2 · CC0 1.0
Window9p(id,kind,members,group) ==
LET o == Opening9p(id,kind,members,group)
IN NewPriorityWindow9(id,kind,Site9p,members,group,NoTimingRef9,o.instruction,0)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: NewPriorityWindow9, NoTimingRef9, Opening9p, Site9p
WorkProcedures9 · operator
reference-profile · input revision 2 · CC0 1.0
WorkProcedures9 ==
CASE q9p.stage="Open" ->
/\ OpenPriorityWindow9(<<>>,<<Window9p(30,"Paid",E9p,0)>>,30,"Paid",Site9p,E9p,Opening9p(30,"Paid",E9p,0),{})
/\ q9p'=[q9p EXCEPT !.stack= <<Window9p(30,"Paid",E9p,0)>>,!.stage="RootReceive",!.tick=@+1]
[] q9p.stage \in {"RootReceive","ChildReceive","PassReceive"} ->
LET w == WindowTop9(q9p.stack)
cp == CPData9p(q9p.ledger,ConditionalPriorityCaller96(w),E9p)
l == CPAfter9p(q9p.ledger,cp,E9p,E9p)
ready == [w EXCEPT !.stage="Ready",!.checkpoint=cp.id]
IN /\ ProcessCP9p(q9p.ledger,l,q9p.stack,cp,E9p,E9p,E9p)
/\ CheckpointPriorityWithConditionals96(l,q9p.stack,ReplaceWindowTop9(q9p.stack,ready),PriorityCP9p(w,cp.id))
/\ q9p'=[q9p EXCEPT !.ledger=l,!.stack=ReplaceWindowTop9(@,ready),!.tick=@+1,
!.stage=CASE q9p.stage="RootReceive" -> "Reserve" [] q9p.stage="ChildReceive" -> "SelectChild" [] OTHER -> "Pass"]
[] q9p.stage="Reserve" ->
LET w == WindowTop9(q9p.stack)
busy == StartPriorityOptionFrame9(w,Option9p,960)
p == OpenPaidProcedure95(100,RootDefinition9p,Option9p,w,960,"Rule")
IN /\ ReservePaidAbility95(q9p.stack,<<busy>>,p,100,RootDefinition9p,RootContext9p,Option9p,Legality9p(w,Option9p),{})
/\ q9p'=[q9p EXCEPT !.stack= <<busy>>,!.p=p,!.stage="Pay",!.tick=@+1]
[] q9p.stage="Pay" ->
LET p == [q9p.p EXCEPT !.ability.detached=TRUE,!.phase="CostCheckpoint",!.costPaid=TRUE]
payment == [tag |-> "PaidTriggerPayment",abilityInstance |-> 100,transactionId |-> 960,ability |-> 100,source |-> q9p.p.ability.source,
triggerCost |-> RootDefinition9p.triggerCost,beforeObjects |-> E9p,afterObjects |-> E9p,announced |-> TRUE,allPaid |-> TRUE,
additionalCostsPaid |-> TRUE,restrictionsBefore |-> TRUE,restrictionsAfter |-> TRUE,simultaneousProcedureComplete |-> TRUE,
sourceAfter |-> 0,sourceUninstalled |-> FALSE,sourceForfeited |-> FALSE,paidOperations |-> {},publicEvents |-> {}]
IN /\ q9p.resourceUnits=3
/\ PayPaidTrigger95(q9p.stack,q9p.p,p,E9p,E9p,E9p,E9p,E9p,{},payment,q9p.uses,UseMap9p,q9p.turnUses,TurnUse9p,1,{Used9p})
/\ q9p'=[q9p EXCEPT !.p=p,!.uses=UseMap9p,!.turnUses=TurnUse9p,!.resourceUnits=@-1,!.stage="CostCP",!.tick=@+1]
[] q9p.stage="CostCP" ->
LET d == ChildDefinition9p
key == [definition |-> ConditionalKey96(d),occurrence |-> 1]
e == [id |-> 1,kind |-> "AbilityUsed",object |-> 0,actor |-> "SideB",side |-> "SideB",snapshot |-> q9p.ledger.lastSnapshot,
scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(d),traversal |-> NoTraversal6,structure |-> NoTimingRef9]
events == [id \in {1} |-> e]
cp == CPData9p(q9p.ledger,PaidCheckpointCaller96(q9p.p),events)
allocation == [k \in IF q9p.child THEN {key} ELSE {} |-> 201]
bindings == [k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> 40,group |-> 4]]
conditions == [k \in DOMAIN Definitions9p(q9p.child) |-> [id \in {1} |-> [tag |-> "ConditionalTriggerStipulations",ability |-> 200,
source |-> d.syntax.source,occurrence |-> 1,snapshotId |-> e.snapshot.id,results |-> E9p]]]
l == CPAfter9p(q9p.ledger,cp,allocation,bindings)
IN /\ ProcessCP9p(q9p.ledger,l,q9p.stack,cp,conditions,allocation,bindings)
/\ q9p'=[q9p EXCEPT !.ledger=l,!.costCheckpoint=cp.id,!.stage=IF q9p.child THEN "OpenChild" ELSE "CostResume",!.tick=@+1]
[] q9p.stage="OpenChild" ->
LET members == ConditionalWindowMembers96(q9p.ledger.instances,40)
child == Window9p(40,"Reaction",members,4)
IN /\ OpenConditionalReaction96(q9p.stack,Append(q9p.stack,child),q9p.ledger,40,Site9p,Opening9p(40,"Reaction",members,4),{30})
/\ q9p'=[q9p EXCEPT !.stack=Append(@,child),!.stage="ChildReceive",!.tick=@+1]
[] q9p.stage="SelectChild" ->
LET w == WindowTop9(q9p.stack)
d == ChildDefinition9p
option == PriorityOption9(70,"Conditional","SideB",200,201,d.syntax.source,0,{})
busy == StartPriorityOptionFrame9(w,option,970)
p == OpenConditionalProcedure96(201,d,w,option,970,"Rule")
plan == OpenInstruction93(710,"Ability",201,d.syntax.source,"Rule",1,"NoValue",<<"ChildWork">>,FALSE)
ip == [p EXCEPT !.phase="Imminent",!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.detached=TRUE]
announced == [plan EXCEPT !.phase="Imminent",!.announced=TRUE]
l == [q9p.ledger EXCEPT !.instances[201].status="Imminent"]
IN /\ BeginConditionalResolution96(q9p.ledger,l,q9p.stack,ReplaceWindowTop9(q9p.stack,busy),p,ip,d,
SnapshotWithConditionalRegistry96(q9p.ledger.lastSnapshot,q9p.ledger),201,option,Legality9p(w,option),E9p,plan,announced,
Targets9p(plan),Entry9p(plan,0),q9p.turnUses,[tag |-> "AbilityRestrictions",ability |-> 200,source |-> d.syntax.source,results |-> E9p])
/\ q9p'=[q9p EXCEPT !.ledger=l,!.stack=ReplaceWindowTop9(@,busy),!.childP=ip,!.childPlan=announced,!.stage="ChildBegin",!.tick=@+1]
[] q9p.stage="ChildBegin" ->
LET p == [q9p.childP EXCEPT !.phase="Resolve",!.ability.phase="Resolving"]
plan == [q9p.childPlan EXCEPT !.phase="Resolving"]
expected == [tag |-> "ConditionalExpectedEffects",point |-> "ExpectedEffectsBeforeInterrupt",instruction |-> InstructionWindowRef93(q9p.childPlan),effects |-> {1}]
l == [q9p.ledger EXCEPT !.instances[201].status="Resolving",!.instances[201].expected=[i \in {1} |->
[instruction |-> InstructionWindowRef93(q9p.childPlan),effects |-> {1}]]]
IN /\ ResolveConditionalWithoutInterrupt96(q9p.ledger,l,q9p.stack,q9p.childP,p,q9p.childPlan,plan,NoModifiers9p(q9p.childPlan),Clearance9p(q9p.childPlan),expected)
/\ q9p'=[q9p EXCEPT !.ledger=l,!.childP=p,!.childPlan=plan,!.stage="ChildWork",!.tick=@+1]
[] q9p.stage="ChildWork" ->
LET a == FinishedAbility9p(q9p.childP.ability,q9p.childPlan)
p == [q9p.childP EXCEPT !.ability=a,!.phase="InstructionCheckpoint",!.checkpoint=0]
plan == FinishedPlan9p(q9p.childPlan)
l == [q9p.ledger EXCEPT !.instances[201].status="Complete"]
IN /\ CarryConditionalInstructionCore96(q9p.ledger,l,q9p.stack,q9p.stack,q9p.childP,p,q9p.childPlan,plan,Step9p(q9p.childPlan))
/\ q9p'=[q9p EXCEPT !.ledger=l,!.childP=p,!.childPlan=plan,!.work=Append(@,"Child"),!.stage="ChildFinalCP",!.tick=@+1]
[] q9p.stage="ChildFinalCP" ->
LET cp == CPData9p(q9p.ledger,ConditionalInstructionCaller96(q9p.childP),E9p)
l == CPAfter9p(q9p.ledger,cp,E9p,E9p)
p == [q9p.childP EXCEPT !.phase="Complete",!.checkpoint=cp.id]
receipt == [tag |-> "ConditionalInstructionCheckpoint",id |-> cp.id,abilityInstance |-> 201,transactionId |-> 970,
source |-> p.ability.source,instruction |-> 710,index |-> 1,complete |-> TRUE,allNewerChainsComplete |-> TRUE]
IN /\ ProcessCP9p(q9p.ledger,l,q9p.stack,cp,E9p,E9p,E9p)
/\ ConditionalInstructionCheckpoint96(l,q9p.stack,q9p.childP,p,receipt)
/\ q9p'=[q9p EXCEPT !.ledger=l,!.childP=p,!.stage="ChildReturn",!.tick=@+1]
[] q9p.stage="ChildReturn" ->
LET p == [q9p.childP EXCEPT !.phase="Returned",!.ability.returned=TRUE]
w == WindowTop9(q9p.stack)
stack == ReplaceWindowTop9(q9p.stack,CompletePriorityOptionFrame9(w))
IN /\ FinishConditionalProcedure96(q9p.stack,stack,q9p.childP,p,Return9p(w,p.checkpoint))
/\ q9p'=[q9p EXCEPT !.childP=p,!.stack=stack,!.childReturned=TRUE,!.stage="PassReceive",!.tick=@+1]
[] q9p.stage="Pass" ->
LET w == WindowTop9(q9p.stack)
a == PassPriorityFrame9(w)
IN /\ PassPriority9(q9p.stack,ReplaceWindowTop9(q9p.stack,a),w.priority,E9p)
/\ q9p'=[q9p EXCEPT !.stack=ReplaceWindowTop9(@,a),!.stage=IF a.open THEN "PassReceive" ELSE IF Len(q9p.stack)=2 THEN "PopChild" ELSE "Done",!.tick=@+1]
[] q9p.stage="PopChild" ->
/\ PopClosedPriorityWindow9(q9p.stack,<<q9p.stack[1]>>)
/\ q9p'=[q9p EXCEPT !.stack= <<@[1]>>,!.stage="CostResume",!.tick=@+1]
[] q9p.stage="CostResume" ->
LET p == [q9p.p EXCEPT !.phase="Targets",!.checkpoint=q9p.costCheckpoint]
IN /\ PaidCheckpointWithConditionals96(q9p.ledger,q9p.stack,q9p.p,p,E9p,E9p,PaidCP9p(q9p.p,q9p.costCheckpoint))
/\ q9p'=[q9p EXCEPT !.p=p,!.stage="EnterRoot",!.tick=@+1]
[] q9p.stage="EnterRoot" ->
LET i == IF q9p.p.ability.phase="Ready" THEN 1 ELSE 2
plan == OpenInstruction93(RootDefinition9p.instructions[i],"Ability",100,RootDefinition9p.syntax.source,"Rule",i,"NoValue",
IF i=1 /\ q9p.steps=2 THEN <<"RootA","RootB">> ELSE <<IF i=1 THEN "RootA" ELSE "RootFinal">>,FALSE)
ip == [q9p.p EXCEPT !.phase="Imminent",!.checkpoint=0,!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.cursor=i]
announced == [plan EXCEPT !.phase="Imminent",!.announced=TRUE]
IN /\ EnterPaidInstruction95(q9p.stack,q9p.p,ip,plan,announced,Targets9p(plan),Entry9p(plan,q9p.p.checkpoint))
/\ q9p'=[q9p EXCEPT !.p=ip,!.plan=announced,!.stage="BeginRoot",!.tick=@+1]
[] q9p.stage="BeginRoot" ->
LET p == [q9p.p EXCEPT !.phase="Resolve",!.ability.phase="Resolving"]
plan == [q9p.plan EXCEPT !.phase="Resolving"]
IN /\ ResolvePaidWithoutInterrupt95(q9p.stack,q9p.p,p,q9p.plan,plan,NoModifiers9p(q9p.plan),Clearance9p(q9p.plan))
/\ q9p'=[q9p EXCEPT !.p=p,!.plan=plan,!.stage="RootWork",!.tick=@+1]
[] q9p.stage="RootWork" ->
LET plan == FinishedPlan9p(q9p.plan)
a == FinishedAbility9p(q9p.p.ability,q9p.plan)
p == [q9p.p EXCEPT !.ability=a,!.checkpoint=0,!.phase=IF plan.phase="Complete" THEN "InstructionCheckpoint" ELSE "Resolve"]
IN /\ CarryPaidInstruction95(q9p.stack,q9p.p,p,q9p.plan,plan,Step9p(q9p.plan))
/\ q9p'=[q9p EXCEPT !.p=p,!.plan=plan,!.work=Append(@,q9p.plan.steps[q9p.plan.cursor]),
!.stage=IF plan.phase="Complete" THEN "RootCP" ELSE "RootWork",!.tick=@+1]
[] q9p.stage="RootCP" ->
LET cp == CPData9p(q9p.ledger,PaidCheckpointCaller96(q9p.p),E9p)
l == CPAfter9p(q9p.ledger,cp,E9p,E9p)
p == [q9p.p EXCEPT !.checkpoint=cp.id,!.phase=IF q9p.p.ability.lastFinished THEN "Complete" ELSE "Targets"]
IN /\ ProcessCP9p(q9p.ledger,l,q9p.stack,cp,E9p,E9p,E9p)
/\ PaidCheckpointWithConditionals96(l,q9p.stack,q9p.p,p,E9p,E9p,PaidCP9p(q9p.p,cp.id))
/\ q9p'=[q9p EXCEPT !.p=p,!.ledger=l,!.stage=IF p.phase="Complete" THEN "RootReturn" ELSE "EnterRoot",!.tick=@+1]
[] q9p.stage="RootReturn" ->
LET p == [q9p.p EXCEPT !.phase="Returned",!.ability.returned=TRUE]
w == WindowTop9(q9p.stack)
stack == ReplaceWindowTop9(q9p.stack,CompletePriorityOptionFrame9(w))
IN /\ FinishPaidProcedure95(q9p.stack,stack,q9p.p,p,Return9p(w,p.checkpoint))
/\ q9p'=[q9p EXCEPT !.p=p,!.stack=stack,!.stage="PassReceive",!.tick=@+1]
[] OTHER -> FALSEExact module download · Source bundle and reproduction instructions
Resolved project definitions: BeginConditionalResolution96, CarryConditionalInstructionCore96, CarryPaidInstruction95, CheckpointPriorityWithConditionals96, CompletePriorityOptionFrame9, ConditionalInstructionCaller96, ConditionalInstructionCheckpoint96, ConditionalKey96, ConditionalPriorityCaller96, ConditionalWindowMembers96, EnterPaidInstruction95, FinishConditionalProcedure96, FinishPaidProcedure95, InstructionWindowRef93, NoTimingRef9, OpenConditionalProcedure96, OpenConditionalReaction96, OpenInstruction93, OpenPaidProcedure95, OpenPriorityWindow9, PaidCheckpointCaller96, PaidCheckpointWithConditionals96, PassPriority9, PassPriorityFrame9, PayPaidTrigger95, PopClosedPriorityWindow9, PriorityOption9, ReplaceWindowTop9, ReservePaidAbility95, ResolveConditionalWithoutInterrupt96, ResolvePaidWithoutInterrupt95, SnapshotWithConditionalRegistry96, StartPriorityOptionFrame9, WindowTop9, CPAfter9p, CPData9p, ChildDefinition9p, Clearance9p, Definitions9p, E9p, Entry9p, FinishedAbility9p, FinishedPlan9p, Legality9p, NoModifiers9p, Opening9p, Option9p, PaidCP9p, PriorityCP9p, ProcessCP9p, Return9p, RootContext9p, RootDefinition9p, Site9p, Step9p, Targets9p, TurnUse9p, UseMap9p, Used9p, Window9p, q9p, NoTraversal6
q9p · variable
reference-profile · input revision 2 · CC0 1.0
q9pExact module download · Source bundle and reproduction instructions