------------------------ MODULE InspectionProceduresMC ------------------------
EXTENDS InspectionContracts
                                                                      
                                                                      
                                                                        
                                                                         
                                                                      
                                                                              
VARIABLE q7
EmptyMapT7 == [i \in {} |-> i]
CardT7(zone,targetSite,area) ==
 [form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> <<zone,targetSite,area>>,
  kind |-> IF area = "Root" THEN "Attachment" ELSE "Facility",deployed |-> zone = "Play",
  face |-> "Down",targetSite |-> targetSite,area |-> area,host |-> 0]
ObjectsT7(targetSite,n,root) ==
 [id \in (1..n) \cup (IF root THEN {3} ELSE {}) |->
   IF id = 3 THEN CardT7("Play",targetSite,"Root")
   ELSE CardT7(CentralTargetSiteZone4(targetSite),"NoValue","NoValue")]
PolicyT7(mode) ==
 IF mode = "Normal" THEN InspectionPolicy7("Normal",0)
 ELSE InspectionPolicy7("CounterExampleFamily064",IF mode = "Cap1" THEN 1 ELSE 2)
ViewT7 == InspectionCandidates7(q7.b,q7.capacity,q7.objects,q7.deck,{})
DoneT7 == q7.b.returned
InitInspectiones7 ==
 \E targetSite \in {"SchemaAtom082","SchemaAtom129","SchemaAtom018","auxiliarySite1"}:
 \E n \in (IF targetSite = "auxiliarySite1" THEN {0} ELSE 0..2),root \in BOOLEAN:
 \E mode \in {"Normal","Cap1","Cap2"}:
 \E perform \in SUBSET ((1..n) \cup (IF root THEN {3} ELSE {})):
  LET b == OpenInspection7(2,targetSite,InspectionTargetSiteCategory7(targetSite),1,"RulesTraversalInspection","traversal1",{},PolicyT7(mode))
      objects == ObjectsT7(targetSite,n,root)
  IN q7 = [b |-> b,capacity |-> OpenCandidateCapacity7(b,objects),objects |-> objects,
     deck |-> IF targetSite = "SchemaAtom129" THEN [i \in 1..n |-> i] ELSE <<>>,
     plan |-> [targetSite |-> targetSite,n |-> n,root |-> root,mode |-> mode,perform |-> perform],
     history |-> EmptyMapT7,a |-> OpenItemInspection7(1,1,CardT7("SideAHand","NoValue","NoValue"),1,2,InspectionItemInspectionCaller7(b),{}),
     stage |-> "InspectionWork",beginEvents |-> 0,endEvents |-> 0,itemInspectionEndEvents |-> 0,
     finishedChoices |-> 0,checkpointDrains |-> 0,endDrained |-> FALSE]
WorkInspectionT7 ==
 /\ q7.stage = "InspectionWork" /\ ~q7.b.complete
 /\ LET b == q7.b
    IN CASE b.step = "ProcedureCode839b301bad95" ->
        LET after == [b EXCEPT !.active = TRUE,!.beginMet = TRUE]
        IN /\ BeginInspectionWithCandidates7(b,after,q7.capacity,q7.objects,0,{b.targetSite},TRUE,TRUE,{InspectionBeginEvent7(b)})
           /\ q7' = [q7 EXCEPT !.b = after,!.stage = "InspectionCheckpoint",!.beginEvents = @+1]
      [] b.step = "ProcedureCodeb6067693902e" ->
        LET after == IF b.kind = "SchemaAtom018" THEN [b EXCEPT !.archivesPrepared = TRUE] ELSE b
            objects == IF b.kind = "SchemaAtom018" THEN
              [id \in DOMAIN q7.objects |-> IF q7.objects[id].zone = "SideADiscard"
               THEN [q7.objects[id] EXCEPT !.face = "Up"] ELSE q7.objects[id]] ELSE q7.objects
        IN /\ IF b.kind = "SchemaAtom018" THEN PrepareDiscardSite7(b,after,q7.objects,objects) ELSE TRUE
           /\ q7' = [q7 EXCEPT !.b = after,!.objects = objects,!.stage = "InspectionCheckpoint"]
      [] b.step = "ProcedureCode91f3ee0da236" ->
        LET after == IF RandomLimitApplies7(b) THEN [b EXCEPT !.limitSet = TRUE] ELSE b
        IN /\ IF RandomLimitApplies7(b) THEN FreezeInspectionLimit7(b,after,TRUE) ELSE TRUE
           /\ q7' = [q7 EXCEPT !.b = after,!.stage = "InspectionCheckpoint"]
      [] b.step = "ProcedureCode1404a82ab3ee" ->
        IF InspectionPolicyComplete7(b.policy,Len(b.choices),ViewT7.roots \cup ViewT7.central = {}) THEN
          LET after == [b EXCEPT !.step = "ProcedureCode8c612115d469"]
          IN /\ SkipInspectionSelection7(b,after,q7.capacity,q7.objects,q7.deck,{},FALSE,TRUE)
             /\ q7' = [q7 EXCEPT !.b = after]
        ELSE \E object \in ViewT7.roots \cup ViewT7.central:
          LET source == IF object \in ViewT7.roots THEN "Root" ELSE "SchemaAtom033"
              after == [b EXCEPT !.choices = Append(@,[object |-> object,source |-> source,chooser |-> "SideB"]),
                   !.selectionPending = TRUE,!.selectedObject = object,!.selectedSource = source]
          IN /\ DeriveCandidateView7(b,q7.capacity,q7.objects,q7.deck,{},FALSE,ViewT7)
             /\ IF b.kind = "SchemaAtom082" /\ source = "SchemaAtom033" THEN ChooseCentralAInspectionCard7(b,after,ViewT7,object,0,FALSE,TRUE)
                ELSE ChooseSpecificInspectionCard7(b,after,object,ViewT7)
             /\ q7' = [q7 EXCEPT !.b = after,!.stage = "InspectionCheckpoint"]
      [] b.step = "ProcedureCodee35e7c8fc57b" ->
        LET planned == OpenItemInspection7(Len(b.choices),b.selectedObject,q7.objects[b.selectedObject],1,2,InspectionItemInspectionCaller7(b),{})
        IN IF b.selectedObject \in q7.plan.perform THEN
          LET a == [planned EXCEPT !.active = TRUE,!.beginMet = TRUE]
              attached == [b EXCEPT !.currentItemInspectionId = a.id,!.usedItemInspectionIds = @ \cup {a.id}]
              history == [id \in DOMAIN q7.history \cup {a.id} |-> IF id = a.id
                 THEN [object |-> a.object,traversalId |-> 1,siteInspectionId |-> 2,turnId |-> 1,hadRetireCost |-> TRUE] ELSE q7.history[id]]
          IN /\ BeginItemInspection7(planned,a,q7.objects,TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(a)})
             /\ RecordActualItemInspection7(q7.history,history,a,1,TRUE,ItemInspectionBeginEvent7(a))
             /\ AttachChosenItemInspection7(b,attached,a,ItemInspectionBeginEvent7(a))
             /\ q7' = [q7 EXCEPT !.a = a,!.b = attached,!.history = history,!.stage = "ItemInspectionCheckpoint"]
        ELSE LET cancelled == [planned EXCEPT !.complete = TRUE,!.step = "Complete",!.completionReason = "Replaced"]
             IN /\ CancelUnstartedItemInspection7(planned,cancelled,"Replaced",TRUE,{})
                /\ q7' = [q7 EXCEPT !.a = cancelled,!.stage = "ItemInspectionEndCheckpoint"]
      [] b.step = "ProcedureCodeb1fbc90c4ab0" -> q7' = [q7 EXCEPT !.stage = "InspectionCheckpoint"]
      [] b.step = "ProcedureCode8c612115d469" ->
        LET after == [b EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Normal"]
        IN /\ CompleteNormalInspection7(b,after,TRUE,{InspectionEndEvent7(b)})
           /\ q7' = [q7 EXCEPT !.b = after,!.endEvents = @+1,!.stage = "InspectionEndCheckpoint"]
DrainInspectionT7 ==
 /\ q7.stage = "InspectionCheckpoint"
 /\ q7' = [q7 EXCEPT !.stage = "InspectionAdvance",!.checkpointDrains = @+1]
AdvanceInspectionT7 ==
 /\ q7.stage = "InspectionAdvance"
 /\ LET after == [q7.b EXCEPT !.step = NextInspectionStep7(@)]
    IN /\ IF q7.b.step = "ProcedureCode1404a82ab3ee" THEN AdvanceInspectionSelection7(q7.b,after,TRUE)
          ELSE AdvanceInspectionStep7(q7.b,after,TRUE,TRUE)
       /\ q7' = [q7 EXCEPT !.b = after,!.stage = "InspectionWork"]
WorkItemInspectionT7 ==
 /\ q7.stage = "ItemInspectionWork"
 /\ LET a == q7.a
    IN CASE a.step = "ProcedureCode1dd0e8f05be2" ->
        LET after == [a EXCEPT !.midDone = TRUE]
        IN /\ DeclineMidItemInspection7(a,after,q7.objects,{},FALSE,FALSE,TRUE)
           /\ q7' = [q7 EXCEPT !.a = after,!.stage = "ItemInspectionCheckpoint"]
      [] a.step = "ProcedureCode546db7cc4546" ->
        LET after == [a EXCEPT !.claimObjectiveDone = TRUE]
        IN /\ ResolveItemInspectionClaimObjective7(a,after,q7.objects,FALSE,FALSE,FALSE,TRUE,TRUE,TRUE)
           /\ q7' = [q7 EXCEPT !.a = after,!.stage = "ItemInspectionCheckpoint"]
      [] a.step = "ProcedureCode662478499367" ->
        LET after == [a EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Normal"]
        IN /\ CompleteNormalItemInspection7(a,after,q7.objects,TRUE,{ItemInspectionEndEvent7(a)})
           /\ q7' = [q7 EXCEPT !.a = after,!.stage = "ItemInspectionEndCheckpoint",!.itemInspectionEndEvents = @+1]
DrainItemInspectionT7 ==
 /\ q7.stage = "ItemInspectionCheckpoint"
 /\ q7' = [q7 EXCEPT !.stage = "ItemInspectionAdvance",!.checkpointDrains = @+1]
AdvanceItemInspectionT7 ==
 /\ q7.stage = "ItemInspectionAdvance"
 /\ LET after == [q7.a EXCEPT !.step = NextItemInspectionStep7(@)]
    IN /\ AdvanceItemInspectionStep7(q7.a,after,q7.objects,TRUE,TRUE)
       /\ q7' = [q7 EXCEPT !.a = after,!.stage = "ItemInspectionWork"]
DrainItemInspectionEndT7 ==
 /\ q7.stage = "ItemInspectionEndCheckpoint"
 /\ q7' = [q7 EXCEPT !.stage = "ItemInspectionReturn",!.checkpointDrains = @+1]
ReturnItemInspectionT7 ==
 /\ q7.stage = "ItemInspectionReturn"
 /\ ReturnItemInspectionToCaller7(q7.a,[q7.a EXCEPT !.returned = TRUE],TRUE,InspectionItemInspectionCaller7(q7.b))
 /\ q7' = [q7 EXCEPT !.a.returned = TRUE,!.stage = "FinishInstruction"]
FinishInstructionT7 ==
 /\ q7.stage = "FinishInstruction" /\ q7.a.returned
 /\ LET after == [q7.b EXCEPT !.selectionPending = FALSE,!.selectedObject = 0,!.selectedSource = "NoValue",!.currentItemInspectionId = 0]
    IN /\ FinishInspectionItemInspectionInstruction7(q7.b,after,TRUE)
       /\ q7' = [q7 EXCEPT !.b = after,!.stage = "InspectionCheckpoint",!.finishedChoices = @+1]
DrainInspectionEndT7 ==
 /\ q7.stage = "InspectionEndCheckpoint"
 /\ q7' = [q7 EXCEPT !.stage = "InspectionReturn",!.checkpointDrains = @+1,!.endDrained = TRUE]
ReturnInspectionT7 ==
 /\ q7.stage = "InspectionReturn" /\ q7.endDrained
 /\ ReturnInspectionToCaller7(q7.b,[q7.b EXCEPT !.returned = TRUE],TRUE,"traversal1")
 /\ q7' = [q7 EXCEPT !.b.returned = TRUE,!.stage = "Done"]
NextInspectiones7 == WorkInspectionT7 \/ DrainInspectionT7 \/ AdvanceInspectionT7 \/ WorkItemInspectionT7 \/ DrainItemInspectionT7 \/
 AdvanceItemInspectionT7 \/ DrainItemInspectionEndT7 \/ ReturnItemInspectionT7 \/ FinishInstructionT7 \/ DrainInspectionEndT7 \/ ReturnInspectionT7 \/
 (DoneT7 /\ UNCHANGED q7)
SpecInspectiones7 == InitInspectiones7 /\ [][NextInspectiones7]_q7 /\ WF_q7(NextInspectiones7)
ExpectedChoicesT7(plan) ==
 LET total == plan.n + (IF plan.root THEN 1 ELSE 0)
     central == IF plan.targetSite = "SchemaAtom018" THEN plan.n ELSE IF plan.n = 0 THEN 0 ELSE 1
     cap == IF plan.mode = "Cap1" THEN 1 ELSE 2
 IN IF plan.mode = "Normal" THEN central + (IF plan.root THEN 1 ELSE 0)
    ELSE IF total < cap THEN total ELSE cap
InspectionesInvariant7 ==
 /\ InspectionProcedureValid7(q7.b) /\ CandidateInputsValid7(q7.b,q7.capacity,q7.objects,q7.deck)
 /\ ItemInspectionProcedureValid7(q7.a,q7.objects)
 /\ q7.beginEvents = IF q7.b.beginMet THEN 1 ELSE 0
 /\ q7.endEvents = IF q7.b.complete THEN 1 ELSE 0
 /\ q7.b.usedItemInspectionIds = DOMAIN q7.history
 /\ \A id \in DOMAIN q7.history :
      id \in 1..Len(q7.b.choices) /\ q7.history[id].object = q7.b.choices[id].object /\ q7.history[id].object \in q7.plan.perform
 /\ RandomLimitApplies7(q7.b) => InspectionCentralChoices7(q7.b) <= q7.b.randomLimit
 /\ q7.b.policy.chosenCapEnabled => Len(q7.b.choices) <= q7.b.policy.chosenCap
 /\ q7.finishedChoices <= Len(q7.b.choices)
 /\ q7.b.returned => q7.endDrained /\ q7.finishedChoices = Len(q7.b.choices)
 /\ q7.b.returned => Len(q7.b.choices) = ExpectedChoicesT7(q7.plan)
 /\ q7.b.returned => q7.itemInspectionEndEvents = Cardinality(DOMAIN q7.history)
 /\ q7.b.returned => DOMAIN q7.history = {i \in 1..Len(q7.b.choices) : q7.b.choices[i].object \in q7.plan.perform}
 /\ q7.b.archivesPrepared => \A id \in SideAZoneCards7(q7.objects,"SideADiscard") : q7.objects[id].face = "Up"
 /\ \A id \in DOMAIN q7.objects :
       InspectionObjectVisible7(q7.b,q7.history,q7.objects,id) = (q7.b.active /\ id \in InspectionSeenObjects7(q7.b,q7.history))
EventuallyReturns7 == <>DoneT7
=============================================================================