----------------------- MODULE DetachedChecksMC -----------------------
EXTENDS PendingChecksMC
                                                                           
                                                                              
CONSTANT DetachedProfiles
DProfiles == {"none","imminent-permission","imminent-entry","resolving-permission","resolving-entry"}
DInitial(NeutralValue00013) == PJoin(U4Initial("no-loss"),[detachedProfile |-> NeutralValue00013])
DInit == registryCaseSA=0 /\ guideCaseT11=0 /\ \E NeutralValue00013 \in DetachedProfiles : qT11=DInitial(NeutralValue00013)
DImminent(q) == q.detachedProfile \in {"imminent-permission","imminent-entry"}
DPermission(q) == q.detachedProfile \in {"imminent-permission","resolving-permission"}
DWork ==
 LET q==qT11 IN
 IF q.stage="PaidReturn" THEN
   LET p==[q.paid EXCEPT !.phase="Returned",!.ability.returned=TRUE]
       stack==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
   /\ FinishPaidProcedure95(q.stack,stack,q.paid,p,U4ReturnReceipt(q,q.paid,FALSE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stack=stack,!.returnedPaid=PJoin(@,[id \in {p.id} |-> p]),!.stage="Receive",!.resume="Pass"]
 ELSE IF q.detachedProfile # "none" /\ Len(q.publications)=0 /\
     ((DImminent(q) /\ q.stage="ChildBegin") \/ (~DImminent(q) /\ q.stage="ChildWork"))
 THEN /\ q.child.ability.detached /\ q.child.definition=q.catalog[2].definition
      /\ U4Kernel(IF DPermission(q) THEN "PermissionWithdraw" ELSE "EntryWithdraw",q.stage)
 ELSE U4Work
DNext == DWork /\ U4CaptureFrame(qT11,qT11') /\ UNCHANGED <<registryCaseSA,guideCaseT11>>
DSpec == DInit /\ [][DNext]_<<qT11,registryCaseSA,guideCaseT11>> /\ WF_<<qT11,registryCaseSA,guideCaseT11>>(DNext)
DEventuallyDone == <> (qT11.stage="Done")
                                                                               
                                                                                   
DInstanceCapture(i) == [member |-> i.member,definition |-> i.definition,definitionCopy |-> i.definitionCopy,
 activationEpoch |-> i.activationEpoch,checkpointId |-> i.checkpointId,occurrence |-> i.occurrence,hadSnapshot |-> i.hadSnapshot]
DRecognitionCapture(q) ==
 /\ DOMAIN q.ledger.instances \subseteq {201}
 /\ \A id \in DOMAIN q.ledger.instances :
      LET i==q.ledger.instances[id] cp==q.checkpointHistory[i.checkpointId]
          original==NewConditionalInstance96(201,q.catalog[2].definition,cp,U4OccurrenceId(1),U4ReactionWindow(1),5)
      IN /\ i.checkpointId=q.costCheckpoint /\ DInstanceCapture(i)=DInstanceCapture(original)
DSafety ==
 LET q==qT11 IN
 /\ U4Safety /\ U4CaptureSafety /\ DRecognitionCapture(q) /\ q.detachedProfile \in DProfiles /\ q.round=1
 /\ (201 \in DOMAIN q.ledger.instances => q.ledger.instances[201].status # "Lost" /\ q.ledger.instances[201].definitionCopy=q.catalog[2].definition)
 /\ (q.child # EmptyT11 => q.child.definition=q.catalog[2].definition /\ q.child.ability.detached /\ ConditionalProcedureBound96(q.ledger,q.child))
 /\ (Len(q.publications)>0 =>
       LET p==q.publications[1] expected==IF DImminent(q) THEN "Imminent" ELSE "Resolving" IN
       /\ Len(q.publications)=1 /\ p.beforeLedger.instances[201].status=expected /\ p.afterLedger.instances[201].status=expected
       /\ q.ledger.activationEpoch[ConditionalKey96(q.catalog[2].definition)]=1 /\ q.ledger.instances[201].activationEpoch=0
       /\ ~ConditionalActive96(q.catalog[2].definition,q.current)
       /\ (2 \in DOMAIN q.basis.registry)=DPermission(q)
       /\ q.child.definition=p.beforeLedger.instances[201].definitionCopy)
 /\ (q.stage="Done" =>
       /\ q.stack= <<>> /\ DOMAIN q.uses={1} /\ DOMAIN q.returnedPaid={101} /\ DOMAIN q.returnedChildren={201}
       /\ q.ledger.instances[201].status="Complete" /\ ~q.ledger.instances[201].used /\ Cardinality(DOMAIN q.wallet.obj)=2
       /\ q.work= <<[round |-> 1,kind |-> "Conditional"],[round |-> 1,kind |-> "Paid"]>>
       /\ Len(q.publications)=(IF q.detachedProfile="none" THEN 0 ELSE 1))
DObservation(q) == [tag |-> "Unit5Stage",family |-> "detached",NeutralValue00013 |-> q.detachedProfile,stage |-> q.stage,
 conditionalStatus |-> IF 201 \in DOMAIN q.ledger.instances THEN q.ledger.instances[201].status ELSE "Absent",
 childPhase |-> IF q.child=EmptyT11 THEN "NoValue" ELSE q.child.phase,paidPhase |-> IF q.paid=EmptyT11 THEN "NoValue" ELSE q.paid.phase,
 active |-> ConditionalActive96(q.catalog[2].definition,q.current),present |-> 2 \in DOMAIN q.basis.registry,
 revision |-> q.basis.revision,epoch |-> q.ledger.activationEpoch[ConditionalKey96(q.catalog[2].definition)],
 publicationCount |-> Len(q.publications),useCount |-> Cardinality(DOMAIN q.uses),walletCount |-> Cardinality(DOMAIN q.wallet.obj),
 captureCount |-> Cardinality(DOMAIN q.captures),windowId |-> IF Len(q.stack)=0 THEN 0 ELSE WindowTop9(q.stack).id,
 windowStage |-> IF Len(q.stack)=0 THEN "Absent" ELSE WindowTop9(q.stack).stage,done |-> q.stage="Done"]
DCompletion(q) == [tag |-> "Unit5Completion",family |-> "detached",NeutralValue00013 |-> q.detachedProfile,
 native |-> q.native,uses |-> q.uses,turnUses |-> q.turnUses,useIndex |-> q.useIndex,procedures |-> q.procedures,
 instances |-> q.ledger.instances,returnedPaid |-> q.returnedPaid,returnedChildren |-> q.returnedChildren,
 work |-> q.work,closedWindows |-> q.closedWindows,checkpointIds |-> DOMAIN q.checkpointHistory,
 captures |-> [id \in DOMAIN q.captures |-> [revision |-> q.captures[id].basis.revision,entries |-> DOMAIN q.captures[id].basis.registry,
      permissions |-> q.captures[id].basis.rulePermissions,snapshotId |-> q.captures[id].snapshot.id]],
 publications |-> [i \in 1..Len(q.publications) |-> LET p==q.publications[i] IN
      [cause |-> p.cause,target |-> p.target,beforeStatus |-> p.beforeLedger.instances[201].status,
       afterStatus |-> p.afterLedger.instances[201].status,beforeEpoch |-> p.beforeLedger.activationEpoch[ConditionalKey96(q.catalog[2].definition)],
       afterEpoch |-> p.afterLedger.activationEpoch[ConditionalKey96(q.catalog[2].definition)],capturedDefinition |-> p.beforeLedger.instances[201].definitionCopy,
       capturedSource |-> p.beforeLedger.instances[201].member.source,afterCurrentRows |-> p.currentSnapshot.activity.instances]]]
=============================================================================