----------------------- MODULE AdditionalProceduresMC -----------------------
EXTENDS AdditionalChecksMC
VARIABLE q10p
vars10p == <<q10p,block10>>
Empty10p == [id \in {} |-> id]
Caller10p == [kind |-> "AbilityInstruction",abilityInstance |-> 55,instruction |-> 77]
Objects10p == [id \in 1..5 |->
 CASE id=1 -> CheckpointObject103("NeutralValue00007","Play",FALSE,0)
   [] id=2 -> CheckpointCounter103("SchemaAtom043","Play",1)
   [] id=3 -> CheckpointCounter103("Power","Play",2)
   [] id=4 -> [CheckpointCounter103("SchemaAtom043","SideADiscard",0) EXCEPT !.card="Specimen0046"]
   [] OTHER -> CheckpointCounter103("SchemaAtom180","SideBDiscard",0)]
InitialSnapshot10p ==
 [id |-> 100,point |-> "BeforeCheckpoint",checkpointId |-> 0,definitions |-> Empty10p,present |-> {},
  objects |-> Objects10p,points |-> [p \in SetupPlayers |-> 0],holds |-> Empty10p,effects |-> Empty10p,
  activity |-> [instances |-> Empty10p],activationEpoch |-> Empty10p,activationSerial |-> 0]
Processing10p == [InitialSnapshot10p EXCEPT !.point="ProcedureCodee605a78f5d5e",!.checkpointId=1]
CP10p == [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> 1,caller |-> Caller10p,
 previousCheckpoint |-> 0,serial |-> 1,previousSnapshot |-> InitialSnapshot10p,
 beginSnapshot |-> [Processing10p EXCEPT !.point="CheckpointBeginning"],processingSnapshot |-> Processing10p,
 stepSerial |-> 0,occurrences |-> Empty10p]
Recognition10p == [route |-> "Ordinary",cp |-> CP10p,definitions |-> Empty10p,lexemes |-> Empty10p,
 conditions |-> Empty10p,allocation |-> Empty10p,bindings |-> Empty10p,departures |-> Empty10p,holds |-> Empty10p,
 usedWindows |-> {},cardFacts |-> CardFacts10]
InitialRegistry10p == [NewLingeringRegistry910 EXCEPT !.effects=[id \in {9} |-> [kind |-> "Ordinary",status |-> "Expired"]],!.usedEffects={9}]
World10p(q) == [id |-> q.frame.snapshotId,objects |-> q.objects,points |-> [p \in SetupPlayers |-> 0],
 present |-> {},activity |-> [instances |-> Empty10p]]
Legal10p(selected) == selected={}
Init10p ==
 /\ block10=3
 /\ q10p=[frame |-> NewCheckpoint103(1,Caller10p,100,{TimingRef9("Turn",1)}),objects |-> Objects10p,
     ledger |-> NewConditionalLedger96(InitialSnapshot10p),registry |-> InitialRegistry10p,used |-> 1..5,
     departures |-> [key \in {<<"Movement",90>>} |-> [source |-> 9,objectiveCompletionLeft |-> FALSE,uninstalled |-> TRUE,hostRemoved |-> TRUE,children |-> {1}]],
     targetSites |-> [s \in CentralTargetSites4 \cup {"r1"} |-> [kind |-> IF s \in CentralTargetSites4 THEN "SchemaAtom033" ELSE "SchemaAtom132"]],
     layout |-> [slots |-> Empty10p,orders |-> [s \in {"r1"} |-> <<>>]],
     capacity |-> [siteInspectionId |-> 8,admittedRoots |-> {},pendingRoots |-> {},deniedRoots |-> {}],
     conversions |-> [id \in {4} |-> [mode |-> "Counter",card |-> "Specimen0046",owner |-> "SideA",createdBy |-> 55,gained |-> [kind |-> "SchemaAtom043"]]]]
Recognize10p ==
 LET ledger==[q10p.ledger EXCEPT !.lastCheckpoint=1,!.checkpointIds={1},!.checkpoints=[id \in {1} |-> [caller |-> Caller10p]],
                !.serial=1,!.lastSnapshot=Processing10p]
     frame==[CheckpointNextFrame103(q10p.frame,100) EXCEPT !.recognition=CP10p,!.recognized=Empty10p]
 IN /\ RecognizeCheckpoint103(q10p.frame,frame,q10p.ledger,ledger,<<>>,<<>>,Recognition10p)
    /\ q10p'=[q10p EXCEPT !.frame=frame,!.ledger=ledger]
Cleanup10p ==
 LET world==World10p(q10p)
     f==LingeringCheckpointFrame910(q10p.ledger,CP10p,world)
     cleanup==[tag |-> "LingeringCheckpointCleanup",frame |-> f,expired |-> {9},complete |-> TRUE]
     registry==[q10p.registry EXCEPT !.effects=Empty10p,!.cleanupIds={1}]
 IN /\ CheckpointCleanupEffects103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.registry,registry,
         q10p.ledger,q10p.ledger,q10p.ledger,<<>>,<<>>,Processing10p,Processing10p,world,f,[f EXCEPT !.returned=TRUE,!.point="ProcedureCodeb681cc249a04"],cleanup)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100),!.registry=registry]
Victory10p ==
 /\ CheckpointVictory103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.objects,[id \in DOMAIN q10p.objects |-> 0],100)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100)]
Unique10p ==
 /\ CheckpointUniqueRetire103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.objects,q10p.objects,
       [id \in DOMAIN q10p.objects |-> q10p.objects[id].card],{},{},{},[id \in DOMAIN q10p.objects |-> "SideB"],Empty10p,
       Empty10p,q10p.used,CheckpointPrinted103,CheckpointOwners103,{},100)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100)]
Illegal10p ==
 /\ CheckpointIllegalRetire103(q10p.frame,CheckpointNextFrame103(q10p.frame,100),q10p.objects,q10p.objects,{},Legal10p,
       Empty10p,"SideB",q10p.targetSites,[applies |-> FALSE],"NoValue",{},Empty10p,q10p.used,CheckpointPrinted103,CheckpointOwners103,{},100)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,100)]
Hosted10p ==
 LET due==CheckpointHostedTargets103(q10p.objects,q10p.departures,q10p.frame.point,Empty10p,Empty10p)
     cards=={id \in due : q10p.objects[id].card#"none"}
     successors==[id \in cards |-> 10+id]
     objects==CheckpointRetireMap103(q10p.objects,due,successors,CheckpointPrinted103,CheckpointOwners103,DOMAIN q10p.objects)
     history==MergeCheckpointDepartures103(q10p.departures,CheckpointNewUninstallDepartures103(q10p.objects,due))
     snapshot==q10p.frame.snapshotId+(IF due={} THEN 0 ELSE 1)
     frame==IF q10p.frame.point="ProcedureCode96bfa1b6a970" /\ due#{} THEN [q10p.frame EXCEPT !.snapshotId=snapshot,!.hostPasses=@+1]
            ELSE CheckpointNextFrame103(q10p.frame,snapshot)
 IN /\ CheckpointHostedCleanup103(q10p.frame,frame,q10p.objects,objects,q10p.departures,history,Empty10p,Empty10p,
         successors,q10p.used,CheckpointPrinted103,CheckpointOwners103,DOMAIN q10p.objects,snapshot)
    /\ q10p'=[q10p EXCEPT !.frame=frame,!.objects=objects,!.departures=history,!.used=@ \cup {successors[id] : id \in cards}]
AuxiliarySite10p ==
 LET targetSites==Without101(q10p.targetSites,{"r1"})
 IN /\ CheckpointAuxiliarySiteCleanup103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.targetSites,targetSites,q10p.objects,Empty10p,q10p.frame.snapshotId)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),!.targetSites=targetSites]
Position10p ==
 /\ CheckpointPositionCleanup103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.layout,q10p.layout,"NoValue",Empty10p,q10p.frame.snapshotId)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId)]
Root10p ==
 /\ CheckpointRootAdmissions103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.capacity,q10p.capacity,
       [id |-> 0,active |-> FALSE,complete |-> FALSE,targetSite |-> "NoValue"],q10p.objects,Empty10p,0,10,{},"NoValue",q10p.frame.snapshotId)
 /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId)]
Restore10p ==
 LET objects==[q10p.objects EXCEPT ![4].form="Card",![4].kind="Plan",![4].properties=CheckpointPrinted103["Specimen0046"]]
 IN /\ CheckpointRestoreDiscard103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.objects,objects,q10p.conversions,Empty10p,CheckpointPrinted103,q10p.frame.snapshotId)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),!.objects=objects,!.conversions=Empty10p]
Counters10p ==
 LET objects==Without101(q10p.objects,{5})
 IN /\ CheckpointReturnDiscardCounters103(q10p.frame,CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),q10p.objects,objects,q10p.frame.snapshotId)
    /\ q10p'=[q10p EXCEPT !.frame=CheckpointNextFrame103(q10p.frame,q10p.frame.snapshotId),!.objects=objects]
Return10p ==
 /\ ReturnCheckpointWithoutReaction103(q10p.frame,[q10p.frame EXCEPT !.phase="Returned",!.returned=TRUE],q10p.ledger,
       World10p(q10p),PersistentCheckpointCompletion912(q10p.ledger,CP10p,World10p(q10p)),Caller10p)
 /\ q10p'=[q10p EXCEPT !.frame.phase="Returned",!.frame.returned=TRUE]
Work10p ==
 /\ q10p.frame.phase#"Returned"
 /\ CASE q10p.frame.point="ProcedureCodee605a78f5d5e" -> Recognize10p [] q10p.frame.point="ProcedureCode88eda145024f" -> Cleanup10p
     [] q10p.frame.point="ProcedureCodeb681cc249a04" -> Victory10p [] q10p.frame.point="ProcedureCodefe50c31480ea" -> Unique10p
     [] q10p.frame.point="ProcedureCodea488e1ba6ca3" -> Illegal10p [] q10p.frame.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} -> Hosted10p
     [] q10p.frame.point="ProcedureCode2d73b20aa788" -> AuxiliarySite10p [] q10p.frame.point="ProcedureCode2d6279f9d639" -> Position10p
     [] q10p.frame.point="ProcedureCode7f181ce21011" -> Root10p [] q10p.frame.point="ProcedureCodeda83a77a1f12" -> Restore10p
     [] q10p.frame.point="ProcedureCode0811ebc5f40e" -> Counters10p [] q10p.frame.point="ProcedureCodeb74d673a0fc6" -> Return10p [] OTHER -> FALSE
ActiveWork10p == Work10p /\ UNCHANGED block10
Next10p == ActiveWork10p \/ (q10p.frame.returned /\ UNCHANGED vars10p)
Spec10p == Init10p /\ [][Next10p]_vars10p /\ WF_vars10p(ActiveWork10p)
EventuallyReturned10p == <>q10p.frame.returned
Safety10p ==
 /\ block10=3 /\ q10p.frame.done \subseteq CheckpointStageSet103
 /\ ("ProcedureCodeb681cc249a04" \in q10p.frame.done => DOMAIN q10p.registry.effects={})
 /\ ("ProcedureCode2d73b20aa788" \in q10p.frame.done => {1,2,3} \cap DOMAIN q10p.objects={})
 /\ ("ProcedureCode0811ebc5f40e" \in q10p.frame.done => q10p.objects[4].form="Card" /\ 5 \notin DOMAIN q10p.objects)
 /\ (q10p.frame.returned => q10p.frame.done=CheckpointStageSet103 /\ q10p.frame.hostPasses=3 /\ DOMAIN q10p.objects={4,11})
=============================================================================