---------------------- MODULE ActionAdapters ----------------------
EXTENDS RegistryCompositionMC
                                                                                 
AJoin(base,extra) == RJoin(base,extra)
ANativeObjects == IInitialT11.objects
AObjects == [id \in DOMAIN ANativeObjects |-> AJoin(ANativeObjects[id],
 [virtual |-> FALSE,properties |-> [kind |-> ANativeObjects[id].kind],area |-> "NoValue",targetSite |-> "NoValue"])]
ANativeProjection(objects) == [id \in DOMAIN ANativeObjects |-> [field \in DOMAIN ANativeObjects[id] |-> objects[id][field]]]
APrinted == [card \in {"SyntheticItemInspectionPhysical1"} |-> [kind |-> "Plan"]]
AOwners == [card \in {"SyntheticItemInspectionPhysical1"} |-> "SideA"]
ACostDefinition ==
 LET s==ProtocolP!Syntax9p(300,"Conditional","ActionCostReactionControl")
 IN [RChildDefinition EXCEPT !.syntax=s,!.activity=AbilityDefinition9(300,"Conditional",s.source,"Printed"),
  !.instructions= <<720>>,!.trigger.kinds={"ActionActionPointCostPaid"},!.partsByInstruction=[i \in {720} |-> {1}]]
ACompletionDefinition ==
 LET s==ProtocolP!Syntax9p(301,"Conditional","ActionCompletionReactionControl")
 IN [ACostDefinition EXCEPT !.syntax=s,!.activity=AbilityDefinition9(301,"Conditional",s.source,"Printed"),
  !.instructions= <<721>>,!.trigger.kinds={"OriginalActionCompletes"},!.partsByInstruction=[i \in {721} |-> {1}]]
ACatalog == AJoin(AJoin(RCatalog(0),[id \in {3} |-> [kind |-> "Conditional",nativeId |-> 300,
 source |-> ACostDefinition.syntax.source,definition |-> ACostDefinition]]),
 [id \in {4} |-> [kind |-> "Conditional",nativeId |-> 301,source |-> ACompletionDefinition.syntax.source,definition |-> ACompletionDefinition]])
APermissions == RPermissions \cup {"ActionCostReactionControl"}
A2Permissions(scenario) == CASE scenario="cost-reaction" -> APermissions
 [] scenario="completion-reaction" -> RPermissions \cup {"ActionCompletionReactionControl"} [] OTHER -> RPermissions
ABasis(q) == BasisSA(q.abilityRevision,q.abilityRegistry,q.objects,q.rulePermissions)
ADefinitions(q) == ConditionalDefinitionsSA(q.abilityRegistry)
ATemplate(q,id,point,checkpoint) == [q.ledger.lastSnapshot EXCEPT !.id=id,!.point=point,!.checkpointId=checkpoint]
ASnapshot(q,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,ABasis(q),ledger,ATemplate(q,id,point,checkpoint))
AAdmit(q,ledger,snapshot) == AdmitConditionalSnapshotSA(q.catalog,ABasis(q),ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
 ATemplate(q,snapshot.id,snapshot.point,snapshot.checkpointId),snapshot,MinimalCaptureSA(ABasis(q)))
AInside(q) == {TimingRef9("Turn",q.flow.turn.id),TimingRef9("TurnPhase",q.actionPhaseId)} \cup
 (IF TraversalTimingPresent6(q.control.traversal) THEN {TimingRef9("SchemaAtom138",q.control.traversal.id)} ELSE {}) \cup
 (IF IInsideInspectionT11(q) THEN {TimingRef9("Inspection",IBT11(q).id)} ELSE {}) \cup
 (IF IInsideItemInspectionT11(q) THEN {TimingRef9("ItemInspection",IAT11(q).id)} ELSE {})
AInspection(q) == IF IInsideInspectionT11(q) THEN IBT11(q) ELSE [active |-> FALSE,complete |-> TRUE]
AWorld(q,f) == [id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,
 present |-> ConditionalPresentSA(q.abilityRegistry),activity |-> CommonActivitySA(ABasis(q),q.ledger)]
AWorldBound(q,f,world) ==
 /\ BasisValidSA(q.catalog,ABasis(q)) /\ LedgerDomainSA(q.ledger)
 /\ UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)
 /\ world=AWorld(q,f)
ACapture(q,snapshot) == [basis |-> MinimalCaptureSA(ABasis(q)),snapshot |-> snapshot]
AAddCapture(q,snapshot) == AJoin(q.captures,[key \in {<<snapshot.id,snapshot.point>>} |-> ACapture(q,snapshot)])
ACaptureFrame(before,after) ==
 /\ DOMAIN before.captures \subseteq DOMAIN after.captures
 /\ \A key \in DOMAIN before.captures : after.captures[key]=before.captures[key]
ACostCaller(q) == [kind |-> "ActionTriggerCost",actionId |-> q.action.id,windowId |-> q.payment.window,
 transactionId |-> q.payment.transaction,turnId |-> q.flow.turn.id]
AReservation(q) ==
 /\ Len(q.stack)=1 /\ q.NeutralValue00003.ready=PriorityReadyT11(q.NeutralValue00003.opened)
 /\ q.NeutralValue00003.ready.site=[ITurnSiteT11(q) EXCEPT !.actionPoints=q.NeutralValue00003.opened.site.actionPoints]
 /\ q.NeutralValue00003.ready.kind="NeutralValue00001" /\ q.NeutralValue00003.option=IActionOptionT11
 /\ WindowTop9(q.stack)=StartPriorityOptionFrame9(q.NeutralValue00003.ready,IActionOptionT11,200)
ANativeCommitted(q) ==
 IF q.native=EmptyT11 THEN FALSE ELSE
 /\ q.native.operationId=1 /\ q.native.command=IActionPointCommandT11
 /\ q.native.before=IActionPointWorldT11 /\ q.native.after=IActionPointAfterT11(q.native.before)
 /\ q.native.payment=q.payment /\ q.payment.before=q.native.before /\ q.payment.after=q.native.after
 /\ q.native.actionId=q.action.id /\ q.native.turnId=q.flow.turn.id
 /\ q.payment.transaction=200 /\ q.payment.option=IActionOptionT11
 /\ q.payment.window=q.NeutralValue00003.opened.id /\ q.native.after.event="SpendActionPoints"
AActionCostDrained(q,caller) ==
 IF q.costCP=0 THEN FALSE ELSE
 /\ caller=ACostCaller(q) /\ q.frames[q.costCP].caller=caller
 /\ CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack) /\ ANativeCommitted(q)
AActionPaid(q) ==
 /\ AReservation(q) /\ ANativeCommitted(q) /\ AActionCostDrained(q,ACostCaller(q))
 /\ q.actionPointWorld=[q.payment.after EXCEPT !.checkpointDue=FALSE] /\ q.costDrained
AActionReturn(q) ==
 LET w==WindowTop9(q.stack)
     trigger==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
       allTriggerCostsPaid |-> AActionPaid(q),costCheckpointAndReactionsDrained |-> AActionCostDrained(q,ACostCaller(q))]
 IN [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
  triggerPayment |-> trigger,allCostsPaid |-> AActionPaid(q),optionComplete |-> ActionReadyToContinue5(q.action),
  childrenReturned |-> "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete,
  reactionsDrained |-> AActionCostDrained(q,ACostCaller(q)) /\ "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete]
AChildReturnReceipt(q) ==
 LET w==WindowTop9(q.stack) p==q.child
     drained==CheckpointDrained103(q.frames[p.checkpoint],q.ledger,q.stack)
     noTriggerCost==~(\E u \in {p.definition.syntax.units[i] : i \in 1..Len(p.definition.syntax.units)} : u.category="SchemaAtom043" /\ u.subtype="Cost")
     bodyComplete==p.ability.complete /\ q.childPlan.phase="Complete" /\ q.childPlan.completedSteps=q.childPlan.steps /\ p.id \in q.noUseChildren
     payment==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> p.transaction,
        allTriggerCostsPaid |-> noTriggerCost,costCheckpointAndReactionsDrained |-> drained]
 IN [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> p.transaction,
   triggerPayment |-> payment,allCostsPaid |-> noTriggerCost /\ bodyComplete,optionComplete |-> bodyComplete,
   childrenReturned |-> drained,reactionsDrained |-> drained,finalCheckpointId |-> p.checkpoint]
AStepRoles == {"AF","AG","AE"}
AStepName(role) == CASE role="AF" -> "ProcedureCode989abc27e0c6" [] role="AG" -> "ProcedureCodea439ce381bba" [] OTHER -> "ProcedureCode484be3e50aa9"
AStepLower(role) == CASE role="AF" -> "af" [] role="AG" -> "ag" [] OTHER -> "ae"
AStepStage(role) == CASE role="AF" -> "TurnAdvance" [] role="AG" -> "TurnLoop" [] OTHER -> "TurnContinue"
AStepWindow(q,role) == IF role="AE" THEN q.poppedWindows["AE"].id ELSE q.NeutralValue00003.opened.id
AStepCaller(q,role,windowId) == [kind |-> "ActionTimingStep",role |-> role,step |-> AStepName(role),
 turnId |-> q.flow.turn.id,phaseId |-> q.actionPhaseId,actionId |-> q.action.id,windowId |-> windowId,transactionId |-> q.payment.transaction]
AStepEvent(q,role,id,windowId,source,complete) == [id |-> id,tag |-> "InstructionFinished",origin |-> "TimingStep",
 instruction |-> AStepName(role),caller |-> AStepCaller(q,role,windowId),source |-> source,complete |-> complete]
AReactionSite(q) == IF Len(q.stack)=0 THEN ITurnSiteT11(q) ELSE WindowTop9(q.stack).site
AInstanceDefinition(id) == IF id=301 THEN ACostDefinition ELSE ACompletionDefinition
AInstanceWindow(id) == IF id=301 THEN 20 ELSE 21
AReactionContext(q,f) ==
 LET chosen==CHOOSE candidate \in DOMAIN f.recognized : TRUE d==q.ledger.instances[chosen].definitionCopy
 IN [instanceId |-> chosen,definition |-> d,windowId |-> f.recognized[chosen].windowId,transaction |-> 2600+chosen-301,
  instructionId |-> d.instructions[1],work |-> IF chosen=301 THEN "ActionCostReaction" ELSE "ActionCompletionReaction"]
ACompletionCommitted(q) ==
 IF q.nativeCompletion=EmptyT11 THEN FALSE ELSE
 /\ q.completionCommitCount=1 /\ q.nativeCompletion.operationId=2
 /\ q.nativeCompletion.before.status="Effects" /\ q.nativeCompletion.after=[q.nativeCompletion.before EXCEPT !.status="Complete"]
 /\ q.nativeCompletion.after=q.action /\ q.nativeCompletion.windowId=q.NeutralValue00003.opened.id
 /\ q.nativeCompletion.turnId=q.flow.turn.id /\ q.nativeCompletion.phaseId=q.actionPhaseId
 /\ q.completionEvent.nativeCompletion=q.nativeCompletion /\ q.completionEvent.rawEvent=[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]
 /\ q.rawEvents[q.nativeCompletion.rawIndex]={q.completionEvent.rawEvent}
 /\ q.completionOccurrence.actualEvent=q.completionEvent /\ q.completionOccurrence.nativeCompletion=q.nativeCompletion
APlacement(q,role) ==
 /\ q.stack= <<>> /\ q.flow.step=AStepName(role) /\ q.action.status="Complete"
 /\ IF role="AF" THEN "AF" \in DOMAIN q.poppedWindows /\ q.poppedWindows["AF"]=q.closedWindows["AF"] /\ ACompletionCommitted(q)
    ELSE IF role="AE" THEN "AE" \in DOMAIN q.poppedWindows /\ q.poppedWindows["AE"]=q.closedWindows["AE"]
    ELSE "AF" \in q.stepConsumed
AStepDrained(q,role,f) ==
 /\ role \in DOMAIN q.stepEvents /\ q.stepCP[role]>0 /\ f=q.frames[q.stepCP[role]]
 /\ f.caller=AStepCaller(q,role,AStepWindow(q,role)) /\ f.caller=q.stepEvents[role].caller
 /\ f.inside=AInside(q) /\ CheckpointDrained103(f,q.ledger,q.stack)
 /\ q.flow.step=AStepName(role) /\ APlacement(q,role)
AStepReceipt(q,role,f,revision) == [checkpointId |-> f.id,caller |-> f.caller,eventId |-> q.stepEvents[role].id,
 flow |-> q.flow,revision |-> revision,worldId |-> f.snapshotId,basis |-> MinimalCaptureSA(ABasis(q))]
ARequireStep(q,role,f,flow) ==
 /\ role \notin q.stepConsumed /\ role \in DOMAIN q.stepReturnReceipts
 /\ flow=q.flow /\ AStepDrained(q,role,f)
 /\ q.stepReturnReceipts[role]=AStepReceipt(q,role,f,q.revision)
ALatchAfterSteps(q) ==
 /\ "AE" \in q.stepConsumed /\ q.stepContinuations["AE"].after=q.flow
 /\ q.stepReturnReceipts["AE"].checkpointId=q.stepCP["AE"]
 /\ CheckpointDrained103(q.frames[q.stepCP["AE"]],q.ledger,q.stack)
=============================================================================