------------------------ MODULE OperationProceduresMC ------------------------
EXTENDS OperationContracts
                                                                            
                                                                               
                                                                           
                                                                              
                                                                                  
VARIABLE q8
EmptyT8 == [i \in {} |-> i]
CardT8(side,cost,x) ==
 [card |-> "SchemaAtom149",form |-> "Card",side |-> side,kind |-> IF side="SideA" THEN "Plan" ELSE "Action",
  zone |-> side \o "Hand",loc |-> side \o "Hand",area |-> "NoValue",targetSite |-> "NoValue",targetSiteKind |-> "NoValue",
  position |-> "NoValue",host |-> 0,deployed |-> FALSE,face |-> "Down",activated |-> FALSE,
  marks |-> {"old"},subtypes |-> {},playCost |-> cost,playX |-> x]
HostT8(side) ==
 [CardT8(side,0,FALSE) EXCEPT !.card = "Host",!.kind = IF side="SideA" THEN "Facility" ELSE "Equipment",
    !.zone = "Play",!.loc = "HostLocation",!.area = "Host",!.deployed = TRUE,!.face = "Up",
    !.activated = side="SideA",!.marks = {}]
PutEffectT8(effects,receipt) ==
 [id \in DOMAIN effects \cup {receipt.id} |-> IF id=receipt.id THEN receipt ELSE effects[id]]
IndependentEffectT8 == [id |-> 50,source |-> 2,kind |-> "IndependentDelayed"]
RetentionT8 == [id |-> 51,playId |-> 1,source |-> 2,created |-> TRUE,expiryEffect |-> "NextTurn"]
RelocatedSourceT8(objects,zone) ==
 [id \in {3,9} |-> IF id=3 THEN
    [WithCardLocation8(objects[2],[NoDeployDestination8 EXCEPT !.zone = zone,!.loc = zone,!.area = "NoValue"]) EXCEPT
       !.deployed = FALSE,!.face = "Up",!.activated = FALSE,!.marks = {}]
    ELSE objects[id]]
ActualPaymentT8 ==
 [id |-> 10,procedureId |-> 1,object |-> 2,allPaid |-> TRUE,
  basePart |-> PlayInherentPart8(q8.objects[2],IF q8.plan.x THEN 2 ELSE 0),
  playCostIgnored |-> q8.plan.ignored,paidSomething |-> ~q8.plan.ignored,checkpointRequired |-> ~q8.plan.ignored]
DoneT8 == q8.f.returned
InitProcedures8 ==
 \E side \in SetupPlayers,cost \in {0,3},ignored \in BOOLEAN,x \in BOOLEAN,timing \in BOOLEAN:
 \E cleanup \in {"Retire","LeftPlay","Converted","Hosted","Retention","Nested"}:
  q8 = [plan |-> [side |-> side,cost |-> cost,ignored |-> ignored,x |-> x,timing |-> timing,cleanup |-> cleanup],
     f |-> OpenPlay8(1,1,side,"Parent"),objects |-> [id \in {1,9} |-> IF id=1 THEN CardT8(side,cost,x) ELSE HostT8(side)],
     effects |-> EmptyT8,scheduler |-> "Work",paid |-> FALSE,costDrained |-> FALSE,playedDrained |-> FALSE,
     childReturned |-> ~timing,ownEndTriggers |-> ~timing,endDrained |-> FALSE,
     played |-> 0,resolved |-> 0,cleanupDone |-> FALSE,trash |-> 0,nestedPending |-> FALSE,nestedRemoved |-> FALSE]
WorkPlayT8 ==
 /\ q8.scheduler = "Work"
 /\ LET f == q8.f
    IN CASE f.stage = "ProcedureCodebfd1895de2c0" ->
        LET objects == [id \in {2,9} |-> IF id=2 THEN PlayedPlacementRow8(q8.objects[1],TRUE) ELSE q8.objects[id]]
            after == [f EXCEPT !.object = 2,!.stage = "ProcedureCode0f076861472c",!.kind = q8.objects[1].kind,!.subtypes = {}]
        IN /\ BeginPlay8(f,after,q8.objects,objects,2,{1,9},TRUE)
           /\ q8' = [q8 EXCEPT !.f = after,!.objects = objects]
      [] f.stage = "ProcedureCode0f076861472c" ->
        LET after == [f EXCEPT !.stage = "CostBarrier",!.transaction = 10,!.checkpointRequired = ~q8.plan.ignored,
              !.x = [exists |-> q8.plan.x,amount |-> IF q8.plan.x THEN 2 ELSE 0]]
        IN /\ PayPlayStep8(f,after,q8.objects,ActualPaymentT8,q8.plan.ignored,IF q8.plan.x THEN 2 ELSE 0,TRUE)
           /\ q8' = [q8 EXCEPT !.f = after,!.paid = TRUE,!.scheduler = "CostCheckpoint"]
      [] f.stage = "ProcedureCodecbf6b11f0ae0" ->
        LET after == [f EXCEPT !.stage = "ProcedureCode7647b901fcb1",!.activationReached = TRUE]
        IN /\ ActivatePlayedCard8(f,after)
           /\ q8' = [q8 EXCEPT !.f = after]
      [] f.stage = "ProcedureCode7647b901fcb1" ->
        LET after == [f EXCEPT !.stage = "ProcedureCodebddd9a1a600b"]
        IN /\ MeetPlayedConditions8(f,after,{PlayedCondition8(f)})
           /\ q8' = [q8 EXCEPT !.f = after,!.played = @+1,!.scheduler = "PlayedCheckpoint"]
      [] f.stage = "ProcedureCode3d7f756d78f7" ->
        IF ~q8.childReturned THEN q8' = [q8 EXCEPT !.scheduler = "ChildReturn"]
        ELSE LET receipt == [playId |-> 1,object |-> 2,allPlayAbilitiesResolved |-> TRUE,
                     ownedTimingIds |-> IF q8.plan.timing THEN {77} ELSE {},
                     returnedTimingIds |-> IF q8.childReturned /\ q8.plan.timing THEN {77} ELSE {},
                     ownEndTriggersResolved |-> q8.ownEndTriggers]
                 after == [f EXCEPT !.stage = "ProcedureCodee977e478b45b"]
                 objects == CASE q8.plan.cleanup = "LeftPlay" -> RelocatedSourceT8(q8.objects,"Removed")
                   [] q8.plan.cleanup = "Converted" ->
                       [q8.objects EXCEPT ![2].form = "Counter",![2].kind = "SchemaAtom043",![2].host = 9,
                            ![2].loc = <<"Host",9>>,![2].area = "Hosted",![2].deployed = TRUE]
                   [] q8.plan.cleanup = "Hosted" ->
                       [q8.objects EXCEPT ![2].host = 9,![2].loc = <<"Host",9>>,![2].area = "Hosted"]
                   [] OTHER -> q8.objects
             IN /\ FinishPlayAbilities8(f,after,receipt)
                /\ IF q8.plan.cleanup = "LeftPlay" THEN
                     CardBatchTransfer8(q8.objects,objects,{2},[id \in {2} |-> 3],{1,2,9},"Removed","Up",[id \in {2} |-> "Removed"])
                   ELSE TRUE
                /\ q8' = [q8 EXCEPT !.f = after,!.objects = objects,!.effects = PutEffectT8(@,IndependentEffectT8)]
      [] f.stage = "ProcedureCodee977e478b45b" ->
        LET disposition == PlayCleanupDisposition8(f,q8.objects,q8.plan.cleanup="Retention",q8.plan.cleanup="Nested")
            cleanupReceipt == [playId |-> 1,object |-> 2,disposition |-> disposition,trashInstructionComplete |-> TRUE]
            effects == IF disposition="RetainSelf" THEN PutEffectT8(q8.effects,RetentionT8) ELSE q8.effects
            objects == IF disposition="Retire" THEN RelocatedSourceT8(q8.objects,q8.plan.side \o "Discard") ELSE q8.objects
            after == [f EXCEPT !.stage = "ProcedureCodec610fc738935"]
        IN /\ FinishPlayCleanup8(f,after,q8.objects,q8.plan.cleanup="Retention",q8.plan.cleanup="Nested",
                    cleanupReceipt,q8.effects,effects,RetentionT8)
           /\ IF disposition="Retire" THEN CardBatchTransfer8(q8.objects,objects,{2},[id \in {2} |-> 3],
                  {1,2,9},q8.plan.side \o "Discard","Up",[id \in {2} |-> q8.plan.side \o "Discard"]) ELSE TRUE
           /\ q8' = [q8 EXCEPT !.f = after,!.objects = objects,!.effects = effects,!.cleanupDone = TRUE,
                          !.trash = IF disposition="Retire" THEN 1 ELSE 0]
      [] f.stage = "ProcedureCodec610fc738935" ->
        LET after == [f EXCEPT !.stage = "ProcedureCode03de9212dc90"]
        IN /\ MeetPlayResolvedConditions8(f,after,{[tag |-> "PlayResolved",object |-> 2,kind |-> f.kind,actor |-> f.actor,playId |-> 1]})
           /\ q8' = [q8 EXCEPT !.f = after,!.resolved = @+1,!.nestedPending = q8.plan.cleanup="Nested"]
      [] f.stage = "ProcedureCode03de9212dc90" ->
        LET after == [f EXCEPT !.stage = "Complete",!.complete = TRUE]
        IN /\ CompletePlay8(f,after)
           /\ q8' = [q8 EXCEPT !.f = after,!.scheduler = "EndCheckpoint"]
      [] OTHER -> FALSE
DrainPlayCostT8 ==
 /\ q8.scheduler = "CostCheckpoint"
 /\ LET after == [q8.f EXCEPT !.stage = "ProcedureCodecbf6b11f0ae0"]
    IN /\ DrainPlayCostBarrier8(q8.f,after,10,IF q8.plan.ignored THEN 0 ELSE 11,TRUE)
       /\ q8' = [q8 EXCEPT !.f = after,!.scheduler = "Work",!.costDrained = TRUE]
DrainPlayedT8 ==
 /\ q8.scheduler = "PlayedCheckpoint"
 /\ LET after == [q8.f EXCEPT !.stage = "ProcedureCode3d7f756d78f7"]
    IN /\ OpenPlayAbilities8(q8.f,after,12,TRUE)
       /\ q8' = [q8 EXCEPT !.f = after,!.scheduler = "Work",!.playedDrained = TRUE]
ReturnChildT8 ==
 /\ q8.scheduler = "ChildReturn"
 /\ q8' = [q8 EXCEPT !.childReturned = TRUE,!.scheduler = "SourceEndTriggers"]
DrainSourceEndT8 ==
 /\ q8.scheduler = "SourceEndTriggers" /\ q8.childReturned
 /\ q8' = [q8 EXCEPT !.ownEndTriggers = TRUE,!.scheduler = "Work"]
NestedRemovalT8 ==
 /\ q8.scheduler = "EndCheckpoint" /\ q8.nestedPending /\ ~q8.nestedRemoved
 /\ LET objects == RelocatedSourceT8(q8.objects,"Removed")
    IN /\ CardBatchTransfer8(q8.objects,objects,{2},[id \in {2} |-> 3],{1,2,9},"Removed","Up",[id \in {2} |-> "Removed"])
       /\ q8' = [q8 EXCEPT !.objects = objects,!.nestedRemoved = TRUE]
DrainPlayEndT8 ==
 /\ q8.scheduler = "EndCheckpoint" /\ (q8.nestedPending => q8.nestedRemoved)
 /\ q8' = [q8 EXCEPT !.endDrained = TRUE,!.scheduler = "Return"]
ReturnPlayT8 ==
 /\ q8.scheduler = "Return" /\ q8.endDrained
 /\ ReturnPlayToCaller8(q8.f,[q8.f EXCEPT !.returned = TRUE],TRUE,"Parent")
 /\ q8' = [q8 EXCEPT !.f.returned = TRUE,!.scheduler = "Done"]
NextProcedures8 ==
 WorkPlayT8 \/ DrainPlayCostT8 \/ DrainPlayedT8 \/ ReturnChildT8 \/ DrainSourceEndT8 \/
 NestedRemovalT8 \/ DrainPlayEndT8 \/ ReturnPlayT8 \/ (DoneT8 /\ UNCHANGED q8)
SpecProcedures8 == InitProcedures8 /\ [][NextProcedures8]_q8 /\ WF_q8(NextProcedures8)
ProceduresInvariant8 ==
 /\ DOMAIN q8.objects \subseteq {1,2,3,9}
 /\ Cardinality({id \in DOMAIN q8.objects : q8.objects[id].card="SchemaAtom149"}) = 1
 /\ \A id \in DOMAIN q8.objects : ActivationCacheValid8(q8.objects[id])
 /\ q8.f.activationReached => q8.costDrained /\ q8.paid
 /\ q8.played = IF q8.f.stage \in {"ProcedureCodebddd9a1a600b","ProcedureCode3d7f756d78f7","ProcedureCodee977e478b45b","ProcedureCodec610fc738935","ProcedureCode03de9212dc90","Complete"} THEN 1 ELSE 0
 /\ q8.f.stage \in {"ProcedureCodee977e478b45b","ProcedureCodec610fc738935","ProcedureCode03de9212dc90","Complete"} => q8.playedDrained /\ q8.childReturned /\ q8.ownEndTriggers
 /\ q8.paid => q8.f.x = [exists |-> q8.plan.x,amount |-> IF q8.plan.x THEN 2 ELSE 0]
 /\ (2 \in DOMAIN q8.objects /\ ~q8.f.activationReached) => ~PlayEffectiveCardActivity8(q8.f,2,q8.objects[2],TRUE)
 /\ q8.cleanupDone => 50 \in DOMAIN q8.effects /\ q8.effects[50] = IndependentEffectT8
 /\ q8.trash = IF q8.cleanupDone /\ q8.plan.cleanup="Retire" THEN 1 ELSE 0
 /\ q8.f.complete => q8.cleanupDone /\ q8.resolved = 1
 /\ q8.nestedRemoved => q8.nestedPending /\ q8.resolved = 1 /\ q8.f.complete
 /\ q8.f.returned => q8.endDrained /\ q8.played = 1 /\ q8.resolved = 1
 /\ IF q8.f.returned THEN
       CASE q8.plan.cleanup="Retire" -> 3 \in DOMAIN q8.objects /\ q8.objects[3].zone=q8.plan.side \o "Discard"
         [] q8.plan.cleanup="LeftPlay" \/ q8.plan.cleanup="Nested" -> 3 \in DOMAIN q8.objects /\ q8.objects[3].zone="Removed"
         [] q8.plan.cleanup="Converted" -> q8.objects[2].form="Counter" /\ q8.objects[2].host=9
         [] q8.plan.cleanup="Hosted" -> q8.objects[2].host=9 /\ ~q8.objects[2].deployed
         [] OTHER -> 51 \in DOMAIN q8.effects /\ q8.objects[2].zone="Play"
    ELSE TRUE
EventuallyReturns8 == <>DoneT8
=============================================================================