------------------------ MODULE AbilityProceduresMC ------------------------ EXTENDS AbilityContracts, SpecimenFactsA VARIABLE q9p E9p == [i \in {} |-> i] Turn9p == [OpenTurn5("SideB",1,[p \in SetupPlayers |-> 0]) EXCEPT !.phase="NeutralValue00001"] Site9p == TurnPrioritySite9(Turn9p,"ProcedureCode484be3e50aa9",10,3,[turn |-> Turn9p,step |-> "ProcedureCode484be3e50aa9"]) Syntax9p(id,kind,rule) == [id |-> id,kind |-> kind,side |-> "SideB",controller |-> "SideB",cardKind |-> "NoValue",source |-> RuleAbilitySource9(rule), units |-> <>, arrowAfterFlags |-> TRUE,barrierInstructionPrefix |-> FALSE,paidPrefix |-> [present |-> kind="Paid",bold |-> TRUE,colon |-> TRUE]] 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] 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] Definitions9p(child) == [k \in IF child THEN {ConditionalKey96(ChildDefinition9p)} ELSE {} |-> ChildDefinition9p] Activity9p == [ActivityContext9 EXCEPT !.activeRules={"ProtocolPaidControl","ProtocolReactionControl"}] 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] 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 <<>>] Window9p(id,kind,members,group) == LET o == Opening9p(id,kind,members,group) IN NewPriorityWindow9(id,kind,Site9p,members,group,NoTimingRef9,o.instruction,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] Option9p == PriorityOption9(60,"RegularPaid","SideB",100,0,RootDefinition9p.syntax.source,0,{}) Legality9p(w,option) == [tag |-> "PriorityOptionLegality",windowId |-> w.id,reception |-> w.reception,option |-> option,legal |-> TRUE,active |-> TRUE, transactionId |-> 900+option.id,costsPayable |-> TRUE] PriorityCP9p(w,id) == [tag |-> "NormalPriorityCheckpoint",id |-> id,windowId |-> w.id,reception |-> w.reception,player |-> w.priority,complete |-> TRUE,reactionsDrained |-> TRUE] PaidCP9p(p,id) == [tag |-> "PaidCheckpoint",id |-> id,abilityInstance |-> p.id,transactionId |-> p.transaction,source |-> p.ability.source, phase |-> p.phase,complete |-> TRUE,allNewerChainsComplete |-> TRUE] 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] Targets9p(plan) == [tag |-> "InstructionTargets",instruction |-> plan.id,abilityInstance |-> plan.abilityInstance, source |-> plan.source,sourceZone |-> plan.sourceZone,index |-> plan.index,valid |-> TRUE,targets |-> {}] 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] 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] NoModifiers9p(plan) == [tag |-> "NoInstructionInterruptModifiers",instruction |-> InstructionWindowRef93(plan),conditionalInstances |-> {},paidInterruptAbilities |-> {}] Step9p(plan) == [tag |-> "InstructionStepReturn",instruction |-> plan.id,index |-> plan.cursor,step |-> plan.steps[plan.cursor],complete |-> TRUE] FinishedPlan9p(plan) == [plan EXCEPT !.completedSteps=Append(@,plan.steps[plan.cursor]),!.cursor=@+1, !.phase=IF plan.cursor=Len(plan.steps) THEN "Complete" ELSE "Resolving"] FinishedAbility9p(a,plan) == IF plan.cursor "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] 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)]] 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)}}) Used9p == [tag |-> "AbilityUsed",useId |-> 1,abilityInstance |-> 100,source |-> RootDefinition9p.syntax.source,player |-> "SideB"] UseMap9p == [id \in {1} |-> Used9p] TurnUse9p == [id \in {1} |-> [turnId |-> 1,ability |-> 100,source |-> RootDefinition9p.syntax.source,useId |-> 1]] 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] WorkProcedures9 == CASE q9p.stage="Open" -> /\ OpenPriorityWindow9(<<>>,<>,30,"Paid",Site9p,E9p,Opening9p(30,"Paid",E9p,0),{}) /\ q9p'=[q9p EXCEPT !.stack= <>,!.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,<>,p,100,RootDefinition9p,RootContext9p,Option9p,Legality9p(w,Option9p),{}) /\ q9p'=[q9p EXCEPT !.stack= <>,!.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'=[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 <>,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 -> FALSE NextProcedures9 == WorkProcedures9 SpecProcedures9 == InitProcedures9 /\ [][NextProcedures9]_q9p /\ WF_q9p(WorkProcedures9) EventuallyReturns9 == <> (q9p.stage="Done") 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">>) =============================================================================