------------------------- MODULE TurnProceduresMC -------------------------
EXTENDS TurnContracts
                                                                             
                                                                                
                                                                                
                                                                                  
VARIABLE q5
IdleActionT5 == [NewAction5(0,"SideA",<<"Sample">>) EXCEPT !.status = "Idle"]
InfoT5(f) == IF f.turn.owner = "SideA" THEN SideAStepInfo5(f.step) ELSE SideBStepInfo5(f.step)
DoneT5 == q5.flow.turn.id = 3
InitTurns5 ==
 \E c \in {0,1,3}, r \in {0,1,4}:
  q5 = [flow |-> OpenSideAProcedure5(OpenTurn5("SideA",1,[p \in SetupPlayers |-> 0])),
         plan |-> [SideA |-> c,SideB |-> r],actionPoints |-> [p \in SetupPlayers |-> 0],
         recurring |-> [p \in SetupPlayers |-> 0],ready |-> FALSE,windowToken |-> FALSE,
         action |-> IdleActionT5,tailDone |-> FALSE,nestedUsed |-> FALSE,actionCount |-> 0,
         allotted |-> {},refilled |-> {},begun |-> {},ended |-> {},phaseEnded |-> {},draws |-> 0,
         windows |-> [p \in SetupPlayers |-> 0]]
WorkStepT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind # "NeutralValue00001"
 /\ LET f == q5.flow
        p == f.turn.owner
        kind == InfoT5(f).kind
    IN CASE kind = "AllotActionPoints" ->
         /\ GainAllottedActionPoints5(q5.actionPoints,[q5.actionPoints EXCEPT ![p] = @+q5.plan[p]],p,q5.plan[p])
         /\ q5' = [q5 EXCEPT !.actionPoints[p] = @+q5.plan[p],!.allotted = @ \cup {p},!.ready = TRUE]
       [] kind = "Refill" ->
         /\ IF p = "SideA" THEN SideARefillAtStep5(f,q5.recurring[p],2,2,TRUE)
            ELSE SideBRefillAtStep5(f,q5.recurring[p],2,2,TRUE)
         /\ q5' = [q5 EXCEPT !.recurring[p] = 2,!.refilled = @ \cup {p},!.ready = TRUE]
       [] kind = "TurnBegins" ->
         LET g == [f EXCEPT !.turn.formalBegun = TRUE,!.turn.begunCounts[p] = @+1]
         IN /\ IF p = "SideA" THEN SideAFormalBeginAtStep5(f,g,{TurnBeginEvent5(f.turn)})
               ELSE SideBFormalBeginAtStep5(f,g,{TurnBeginEvent5(f.turn)})
            /\ q5' = [q5 EXCEPT !.flow = g,!.begun = @ \cup {p},!.ready = TRUE]
       [] kind = "MandatoryDraw" ->
         /\ SideAMandatoryDrawAtStep5(f,[deck |-> <<"top","next">>,hand |-> {},actionPoints |-> q5.actionPoints[p]],
               [deck |-> <<"next">>,hand |-> {"top"},actionPoints |-> q5.actionPoints[p]],TRUE,"NoValue",{MandatoryDrawEvent5})
         /\ q5' = [q5 EXCEPT !.draws = @+1,!.ready = TRUE]
       [] kind = "ActionPhaseEnds" ->
         LET g == [f EXCEPT !.phaseEndMet = TRUE]
         IN /\ IF p = "SideA" THEN SideAActionPhaseEndAtStep5(f,g,{ActionPhaseEndEvent5(f.turn)})
               ELSE SideBActionPhaseEndAtStep5(f,g,{ActionPhaseEndEvent5(f.turn)})
            /\ q5' = [q5 EXCEPT !.flow = g,!.phaseEnded = @ \cup {p},!.ready = TRUE]
       [] kind = "TurnEnds" ->
         LET g == [f EXCEPT !.turn.formalEnded = TRUE]
         IN /\ IF p = "SideA" THEN SideAFormalEndAtStep5(f,g,TurnEndEvents5(f.turn))
               ELSE SideBFormalEndAtStep5(f,g,TurnEndEvents5(f.turn))
            /\ q5' = [q5 EXCEPT !.flow = g,!.ended = @ \cup {p},!.ready = TRUE]
       [] kind = "LoseUnspentActionPoints" ->
         /\ LoseUnspentActionPoints5(q5.actionPoints,[q5.actionPoints EXCEPT ![p] = 0],p)
         /\ q5' = [q5 EXCEPT !.actionPoints[p] = 0,!.ready = TRUE]
       [] kind = "PaidWindow" ->
         q5' = [q5 EXCEPT !.ready = TRUE,!.windows[p] = @+1,
                 !.windowToken = f.step \in {"ProcedureCoded6fbcb09dd4f","ProcedureCode484be3e50aa9"}]
       [] OTHER -> q5' = [q5 EXCEPT !.ready = TRUE]
LatchT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind = "NeutralValue00001"
 /\ q5.flow.decision = "NoValue" /\ q5.windowToken
 /\ LET p == q5.flow.turn.owner
        g == [q5.flow EXCEPT !.decision = IF q5.actionPoints[p] > 0 THEN "NeutralValue00001" ELSE "End"]
    IN /\ IF p = "SideA" THEN SideALatchDecision5(q5.flow,g,q5.actionPoints[p],TRUE)
          ELSE SideBLatchDecision5(q5.flow,g,q5.actionPoints[p],TRUE)
       /\ q5' = [q5 EXCEPT !.flow = g,!.windowToken = FALSE,!.ready = q5.actionPoints[p] <= 0]
StartActionT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind = "NeutralValue00001"
 /\ q5.flow.decision = "NeutralValue00001" /\ q5.action.status \in {"Idle","Complete"}
 /\ LET p == q5.flow.turn.owner
        a == NewAction5(q5.actionCount+1,p,BasicActionKey5(p,"GainResourceUnit"))
    IN /\ q5.actionPoints[p] > 0
       /\ ActionStart5(q5.flow.turn,p,TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,
                        TRUE,TRUE,TRUE,q5.actionCount+1,a.key,a)
       /\ q5' = [q5 EXCEPT !.actionPoints[p] = @-1,!.action = a,!.actionCount = @+1,
                           !.tailDone = FALSE,!.nestedUsed = FALSE]
ActionWorkT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind = "NeutralValue00001" /\ q5.flow.decision = "NeutralValue00001"
 /\ LET a == q5.action
    IN \/ /\ a.status = "CostReactions"
          /\ ActionEffectsBegin5(a,[a EXCEPT !.status = "Effects"],TRUE)
          /\ q5' = [q5 EXCEPT !.action.status = "Effects"]
       \/ /\ a.status = "Effects" /\ ~q5.nestedUsed /\ ~q5.tailDone
          /\ ActionNestedBegin5(a,[a EXCEPT !.status = "Nested",!.nested = "sampleNested"],"sampleNested")
          /\ q5' = [q5 EXCEPT !.action.status = "Nested",!.action.nested = "sampleNested",!.nestedUsed = TRUE]
       \/ /\ a.status = "Nested"
          /\ ActionNestedReturn5(a,[a EXCEPT !.status = "Effects",!.nested = "NoValue"],"sampleNested",TRUE)
          /\ q5' = [q5 EXCEPT !.action.status = "Effects",!.action.nested = "NoValue"]
       \/ /\ a.status = "Effects" /\ ~q5.tailDone
          /\ q5' = [q5 EXCEPT !.tailDone = TRUE]
       \/ /\ a.status = "Effects" /\ q5.tailDone
          /\ ActionComplete5(a,[a EXCEPT !.status = "Complete"],TRUE)
          /\ q5' = [q5 EXCEPT !.action.status = "Complete",!.ready = TRUE]
NextFrameT5(f) ==
 IF f.step \in {"ProcedureCode72a65676fb11","ProcedureCode49c3ccade13b"} THEN
    IF f.turn.owner = "SideA" THEN OpenSideBProcedure5(OpenTurn5("SideB",f.turn.id+1,f.turn.begunCounts))
    ELSE OpenSideAProcedure5(OpenTurn5("SideA",f.turn.id+1,f.turn.begunCounts))
 ELSE LET next == IF f.turn.owner = "SideA" THEN SideANextStep5(f.step,f.decision)
                  ELSE SideBNextStep5(f.step,f.decision)
          phase == IF f.turn.owner = "SideA" THEN SideAStepInfo5(next).phase ELSE SideBStepInfo5(next).phase
      IN [f EXCEPT !.step = next,!.turn.phase = phase,!.decision = "NoValue"]
AdvanceT5 ==
 /\ ~DoneT5 /\ q5.ready
 /\ LET g == NextFrameT5(q5.flow)
    IN /\ IF q5.flow.turn.owner = "SideA" THEN SideAStepAdvance5(q5.flow,g,TRUE)
          ELSE SideBStepAdvance5(q5.flow,g,TRUE)
       /\ q5' = [q5 EXCEPT !.flow = g,!.ready = FALSE,
                   !.action = IF g.turn.id # q5.flow.turn.id THEN IdleActionT5 ELSE @]
NextTurns5 == WorkStepT5 \/ LatchT5 \/ StartActionT5 \/ ActionWorkT5 \/ AdvanceT5 \/ (DoneT5 /\ UNCHANGED q5)
SpecTurns5 == InitTurns5 /\ [][NextTurns5]_q5 /\ WF_q5(NextTurns5)
TurnsInvariant5 ==
 /\ IF q5.flow.turn.owner = "SideA" THEN SideAProcedureValid5(q5.flow) ELSE SideBProcedureValid5(q5.flow)
 /\ q5.flow.turn.id \in 1..3 /\ NoBetweenTurns5(TRUE,q5.flow.turn)
 /\ q5.actionPoints \in [SetupPlayers -> 0..4] /\ q5.recurring \in [SetupPlayers -> {0,2}]
 /\ q5.refilled \subseteq q5.allotted /\ q5.begun \subseteq q5.refilled
 /\ q5.draws \in 0..1 /\ (q5.draws = 1 => "SideA" \in q5.begun)
 /\ (q5.flow.turn.formalBegun => q5.flow.turn.owner \in q5.begun)
 /\ (q5.flow.turn.formalEnded => q5.flow.turn.owner \in q5.ended /\ q5.flow.turn.phase = "Discard")
 /\ (q5.flow.turn.id >= 2 => "SideA" \in q5.ended /\ q5.draws = 1)
 /\ (q5.action.status \in {"CostReactions","Effects","Nested"} =>
       InfoT5(q5.flow).kind = "NeutralValue00001" /\ ~q5.ready /\ q5.flow.decision = "NeutralValue00001")
 /\ (InfoT5(q5.flow).kind = "NeutralValue00001" /\ q5.flow.decision = "NeutralValue00001" /\ q5.ready =>
       q5.action.status = "Complete")
 /\ (q5.flow.decision # "NoValue" => ~q5.windowToken)
 /\ (q5.action.status = "Complete" => q5.tailDone)
 /\ (DoneT5 => q5.ended = SetupPlayers /\ q5.begun = SetupPlayers /\
       q5.flow.turn.begunCounts = [p \in SetupPlayers |-> 1] /\ ~q5.flow.turn.formalBegun /\
       q5.actionCount = q5.plan["SideA"]+q5.plan["SideB"] /\
       q5.actionPoints = [p \in SetupPlayers |-> 0] /\
       q5.windows = [p \in SetupPlayers |-> q5.plan[p]+3])
EventuallyHandoff5 == <>DoneT5
=============================================================================