-------------------------- MODULE SetupChecksMC --------------------------
EXTENDS SetupContracts

                                                                            
                                                          
                                                                          
                                                                         
                                                                          
                                                           
                                                                            

VARIABLES setupState, setupDecisions
setupVars == <<setupState, setupDecisions>>

SetupMCDecks ==
    [p \in SetupPlayers |-> IF p = "SideA"
        THEN <<"c1", "c2", "c3", "c4", "c5", "c6">>
        ELSE <<"r1", "r2", "r3", "r4", "r5", "r6">>]
SetupMCProfiles ==
    [p \in SetupPlayers |-> IF p = "SideA" THEN "ci" ELSE "ri"]
SetupMCReverse(seq) == [i \in 1..Len(seq) |-> seq[Len(seq) - i + 1]]
SetupMCOrders(seq) == {seq, SetupMCReverse(seq)}

SetupMCInit ==
    /\ setupState = SetupStart(SetupMCProfiles, SetupMCDecks,
                              [p \in SetupPlayers |-> {}])
    /\ setupDecisions = <<>>

SetupMCShuffle ==
    /\ setupState.stage = "Shuffle"
    /\ \E sideADeck \in SetupMCOrders(setupState.deck["SideA"]),
          sideBDeck \in SetupMCOrders(setupState.deck["SideB"]) :
        SetupStandardNext(setupState, setupState',
            [deck |-> [p \in SetupPlayers |->
                IF p = "SideA" THEN sideADeck ELSE sideBDeck]])
    /\ UNCHANGED setupDecisions

SetupMCKeep(p) ==
    /\ setupState.stage = IF p = "SideA" THEN "RedrawSideA"
                         ELSE "RedrawSideB"
    /\ SetupStandardNext(setupState, setupState', [redraw |-> FALSE])
    /\ setupDecisions' = Append(setupDecisions,
        [player |-> p, redraw |-> FALSE])

SetupMCRedraw(p) ==
    /\ setupState.stage = IF p = "SideA" THEN "RedrawSideA"
                         ELSE "RedrawSideB"
    /\ \E cards \in SetupMCOrders(setupState.deck[p] \o setupState.hand[p]) :
        SetupStandardNext(setupState, setupState',
                          [redraw |-> TRUE, deck |-> cards])
    /\ setupDecisions' = Append(setupDecisions,
        [player |-> p, redraw |-> TRUE])

SetupMCOrdinaryStep ==
    /\ setupState.stage \notin
        {"Shuffle", "RedrawSideA", "RedrawSideB", "Done"}
    /\ SetupStandardNext(setupState, setupState', [dummy |-> TRUE])
    /\ UNCHANGED setupDecisions

SetupMCProgress ==
    \/ SetupMCShuffle
    \/ \E p \in SetupPlayers : SetupMCKeep(p) \/ SetupMCRedraw(p)
    \/ SetupMCOrdinaryStep

SetupMCNext ==
    \/ SetupMCProgress
    \/ setupState.stage = "Done" /\ UNCHANGED setupVars

                                                                       
SetupMCSpec ==
    /\ SetupMCInit
    /\ [][SetupMCNext]_setupVars
    /\ WF_setupVars(SetupMCProgress)

SetupMCType ==
    /\ SetupViewType(setupState)
    /\ setupDecisions \in Seq([player : SetupPlayers, redraw : BOOLEAN])

SetupMCConservation ==
    \A p \in SetupPlayers :
        SetupPermutation(SetupMCDecks[p],
                         setupState.deck[p] \o setupState.hand[p])

                                                                          
                                                                            
SetupMCDecisionOrder ==
    /\ Len(setupDecisions) <= 2
    /\ Len(setupDecisions) >= 1 => setupDecisions[1].player = "SideA"
    /\ Len(setupDecisions) = 2 => setupDecisions[2].player = "SideB"
    /\ setupState.redrawn =
        {setupDecisions[i].player :
            i \in {j \in 1..Len(setupDecisions) : setupDecisions[j].redraw}}

SetupMCBothHandsBeforeRedraw ==
    setupState.stage \in {"RedrawSideA", "RedrawSideB",
        "BeforeSideAFirstTurn", "BeginGame", "Done"} =>
        \A p \in SetupPlayers : Len(setupState.hand[p]) = 5

SetupMCGameStartsLast ==
    /\ setupState.gameStarted = (setupState.stage = "Done")
    /\ setupState.activePlayer =
        IF setupState.stage = "Done" THEN "SideA" ELSE SetupNoPlayer

SetupMCFinished ==
    setupState.stage = "Done" =>
        /\ setupState.pool = [p \in SetupPlayers |-> 5]
        /\ Len(setupDecisions) = 2
        /\ setupState.bankReady
        /\ setupState.gameStarted
        /\ setupState.activePlayer = "SideA"
        /\ \A p \in SetupPlayers :
            /\ Len(setupState.hand[p]) = 5
            /\ Len(setupState.deck[p]) = 1

SetupMCEventuallyDone == <>(setupState.stage = "Done")

=============================================================================