SetupChecksMC

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

SetupMCBothHandsBeforeRedraw · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupState, SetupPlayers

SetupMCConservation · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCDecks, setupState, SetupPermutation, SetupPlayers

SetupMCDecisionOrder · operator

reference-profile · input revision 2 · CC0 1.0

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}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupDecisions, setupState

SetupMCDecks · operator

reference-profile · input revision 2 · CC0 1.0

SetupMCDecks ==
    [p \in SetupPlayers |-> IF p = "SideA"
        THEN <<"c1", "c2", "c3", "c4", "c5", "c6">>
        ELSE <<"r1", "r2", "r3", "r4", "r5", "r6">>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

SetupMCEventuallyDone · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupState

SetupMCFinished · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupDecisions, setupState, SetupPlayers

SetupMCGameStartsLast · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupState, SetupNoPlayer

SetupMCInit · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCDecks, SetupMCProfiles, setupDecisions, setupState, SetupPlayers, SetupStart

SetupMCKeep · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupDecisions, setupState, SetupStandardNext

SetupMCNext · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCProgress, setupVars, setupState

SetupMCOrders · operator

reference-profile · input revision 2 · CC0 1.0

SetupMCOrders(seq) == {seq, SetupMCReverse(seq)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCReverse

SetupMCOrdinaryStep · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupDecisions, setupState, SetupStandardNext

SetupMCProfiles · operator

reference-profile · input revision 2 · CC0 1.0

SetupMCProfiles ==
    [p \in SetupPlayers |-> IF p = "SideA" THEN "ci" ELSE "ri"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

SetupMCProgress · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCKeep, SetupMCOrdinaryStep, SetupMCRedraw, SetupMCShuffle, SetupPlayers

SetupMCRedraw · operator

reference-profile · input revision 2 · CC0 1.0

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])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCOrders, setupDecisions, setupState, SetupStandardNext

SetupMCReverse · operator

reference-profile · input revision 2 · CC0 1.0

SetupMCReverse(seq) == [i \in 1..Len(seq) |-> seq[Len(seq) - i + 1]]

Exact module download · Source bundle and reproduction instructions

SetupMCShuffle · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCOrders, setupDecisions, setupState, SetupPlayers, SetupStandardNext

SetupMCSpec · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMCInit, SetupMCNext, SetupMCProgress, setupVars

SetupMCType · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupDecisions, setupState, SetupPlayers, SetupViewType

setupVars · operator

reference-profile · input revision 2 · CC0 1.0

setupVars == <<setupState, setupDecisions>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: setupDecisions, setupState

setupDecisions · variable

reference-profile · input revision 2 · CC0 1.0

setupDecisions

Exact module download · Source bundle and reproduction instructions

setupState · variable

reference-profile · input revision 2 · CC0 1.0

setupState

Exact module download · Source bundle and reproduction instructions