SetupContracts

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.

next · operator

reference-profile · input revision 2 · CC0 1.0

next == IF p = "SideA" THEN "RedrawSideB"
                        ELSE "BeforeSideAFirstTurn"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: p

p · operator

reference-profile · input revision 2 · CC0 1.0

p == IF before.stage = "RedrawSideA" THEN "SideA" ELSE "SideB"

Exact module download · Source bundle and reproduction instructions

DefaultAbilityController · operator

reference-profile · input revision 2 · CC0 1.0

DefaultAbilityController(o, sourceController, specifiedPlayer) ==
    IF specifiedPlayer \in SetupPlayers THEN specifiedPlayer
    ELSE IF o.form = "Card" /\ o.kind = "Objective" THEN "SideA"
    ELSE sourceController

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

DefaultActive · operator

reference-profile · input revision 2 · CC0 1.0

DefaultActive(o, gameStarted, cardData) ==
    /\ gameStarted
    /\ o.form = "Card"
    /\ CASE o.zone = "SideAObjectiveCompletion" -> o.kind = "Objective"
         [] o.zone = "Play" ->
            /\ o.face = "Up"
            /\ (o.kind = "Profile" \/ o.kind \in {"Action", "Plan"} \/
                (o.deployed /\
                  (cardData[o.card].side = "SideB" \/ o.activated)))
         [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

ExtraFamilyProvision · operator

reference-profile · input revision 2 · CC0 1.0

ExtraFamilyProvision(provided, family, owner, cardData) ==
    /\ provided \subseteq DOMAIN cardData
    /\ \A c \in provided :
        /\ cardData[c].owner = owner
        /\ cardData[c].kind = "Profile"
        /\ cardData[c].profileFamily = family

Exact module download · Source bundle and reproduction instructions

ExtraLockedProfileChoice · operator

reference-profile · input revision 2 · CC0 1.0

ExtraLockedProfileChoice(provided, chosen, owner, cardData) ==
    /\ ExtraFamilyProvision(provided, "LockedProfile", owner, cardData)
    /\ chosen \in provided

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExtraFamilyProvision

ExtraLockedProfileSet · operator

reference-profile · input revision 2 · CC0 1.0

ExtraLockedProfileSet(before, after, provided, chosen, owner, cardData) ==
    /\ before.stage = "AfterSetup"
    /\ ~before.locked
    /\ before.active \in provided
    /\ ExtraLockedProfileChoice(provided, chosen, owner, cardData)
    /\ after = [before EXCEPT
          !.active = chosen,
          !.outside = (@ \cup provided) \ {chosen},
          !.face = [c \in DOMAIN @ |->
              IF c = chosen THEN "Up"
              ELSE IF c \in provided THEN "NA" ELSE @[c]],
          !.front[chosen] = TRUE,
          !.locked = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExtraLockedProfileChoice

ExtraMayLookSideBProfile · operator

reference-profile · input revision 2 · CC0 1.0

ExtraMayLookSideBProfile(player, profile, outsideProfiles) ==
    player = "SideB" /\ profile \in outsideProfiles

Exact module download · Source bundle and reproduction instructions

ExtraProfileReplacement · operator

reference-profile · input revision 2 · CC0 1.0

ExtraProfileReplacement(before, after, chosen, cardData) ==
    /\ chosen \in before.outside
    /\ cardData[before.active].side = "SideB"
    /\ cardData[chosen].side = "SideB"
    /\ cardData[chosen].kind = "Profile"
    /\ after = [before EXCEPT
          !.active = chosen,
          !.outside = (@ \ {chosen}) \cup {before.active},
          !.face[chosen] = "Up",
          !.face[before.active] = "NA",
          !.front[chosen] = TRUE]

Exact module download · Source bundle and reproduction instructions

ExtraSelectableProfileChoice · operator

reference-profile · input revision 2 · CC0 1.0

ExtraSelectableProfileChoice(current, provided, chosen, owner, cardData) ==
    /\ ExtraFamilyProvision(provided, "SelectableProfile", owner, cardData)
    /\ current \in provided
    /\ chosen \in provided

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExtraFamilyProvision

ExtraSelectableProfileSet · operator

reference-profile · input revision 2 · CC0 1.0

ExtraSelectableProfileSet(before, after, provided, chosen, owner, cardData) ==
    /\ ExtraSelectableProfileChoice(before.active, provided, chosen, owner, cardData)
    /\ provided \subseteq before.outside \cup {before.active}
    /\ after = [before EXCEPT
          !.active = chosen,
          !.outside = (@ \cup provided) \ {chosen},
          !.face = [c \in DOMAIN @ |->
              IF c = chosen THEN "Up"
              ELSE IF c \in provided THEN "NA" ELSE @[c]],
          !.front[chosen] = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExtraSelectableProfileChoice

ExtraSideBProfilesLegal · operator

reference-profile · input revision 2 · CC0 1.0

ExtraSideBProfilesLegal(provided, cardData, tournamentLegal(_)) ==
    /\ provided \subseteq DOMAIN cardData
    /\ \A c \in provided :
        /\ cardData[c].owner = "SideB"
        /\ cardData[c].side = "SideB"
        /\ cardData[c].kind = "Profile"
        /\ tournamentLegal(c)

Exact module download · Source bundle and reproduction instructions

ExtraThreeTraitsInitialPartition · operator

reference-profile · input revision 2 · CC0 1.0

ExtraThreeTraitsInitialPartition(deckCards, provided, selected, deployed, outside,
                          cardData) ==
    /\ ExtraThreeTraitsSelection(provided, selected, cardData)
    /\ deckCards \intersect provided = {}
    /\ selected \subseteq deployed
    /\ provided \ selected \subseteq outside

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExtraThreeTraitsSelection

ExtraThreeTraitsProvision · operator

reference-profile · input revision 2 · CC0 1.0

ExtraThreeTraitsProvision(provided, cardData) ==
    /\ provided \subseteq DOMAIN cardData
    /\ \A c \in provided :
        /\ cardData[c].owner = "SideB"
        /\ "Trait" \in cardData[c].subtypes
    /\ Cardinality({cardData[c].name : c \in provided}) >= 3

Exact module download · Source bundle and reproduction instructions

ExtraThreeTraitsSelection · operator

reference-profile · input revision 2 · CC0 1.0

ExtraThreeTraitsSelection(provided, selected, cardData) ==
    /\ ExtraThreeTraitsProvision(provided, cardData)
    /\ selected \subseteq provided
    /\ Cardinality(selected) = 3
    /\ Cardinality({cardData[c].name : c \in selected}) = 3

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExtraThreeTraitsProvision

SetupAdvance · operator

reference-profile · input revision 2 · CC0 1.0

SetupAdvance(before, after, next) == after = [before EXCEPT !.stage = next]

Exact module download · Source bundle and reproduction instructions

SetupCardController · operator

reference-profile · input revision 2 · CC0 1.0

SetupCardController(o, cardData) ==
    CASE o.zone = "Play" -> o.placedBy
      [] o.kind = "Objective" /\ o.zone = "SideAObjectiveCompletion" -> "SideA"
      [] o.kind = "Objective" /\ o.zone = "SideBObjectiveCompletion" -> "SideB"
      [] OTHER -> SetupOwner(o, cardData)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupOwner

SetupCardKindLegal · operator

reference-profile · input revision 2 · CC0 1.0

SetupCardKindLegal(card) ==
    IF card.side = "SideA" THEN card.kind \in SetupSideAKinds
    ELSE card.side = "SideB" /\ card.kind \in SetupSideBKinds

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupSideAKinds, SetupSideBKinds

SetupCounterController · operator

reference-profile · input revision 2 · CC0 1.0

SetupCounterController(o, hostController, poolOwner) ==
    CASE o.kind \in {"ActionPoint", "PersistentCapacityLoss"} -> SetupNoPlayer
      [] o.host # 0 -> hostController
      [] o.kind = "ResourceUnit" /\ poolOwner \in SetupPlayers -> poolOwner
      [] o.kind = "LiabilityMarker" -> "SideA"
      [] o.kind = "ExposureMarker" -> "SideB"
      [] OTHER -> SetupNoPlayer

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupNoPlayer, SetupPlayers

SetupEffectExecutor · operator

reference-profile · input revision 2 · CC0 1.0

SetupEffectExecutor(abilityController, specifiedPlayer) ==
    IF specifiedPlayer \in SetupPlayers THEN specifiedPlayer
    ELSE abilityController

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

SetupInitialProfilesLegal · operator

reference-profile · input revision 2 · CC0 1.0

SetupInitialProfilesLegal(profiles, cardData) ==
    /\ DOMAIN profiles = SetupPlayers
    /\ \A p \in SetupPlayers :
        /\ profiles[p] \in DOMAIN cardData
        /\ cardData[profiles[p]].owner = p
        /\ cardData[profiles[p]].side = p
        /\ cardData[profiles[p]].kind = "Profile"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

SetupMayUseForCost · operator

reference-profile · input revision 2 · CC0 1.0

SetupMayUseForCost(payer, o, controller, explicitException) ==
    controller = payer \/ explicitException \/ SetupPlayerCounterCostException(o)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayerCounterCostException

SetupMultiplicity · operator

reference-profile · input revision 2 · CC0 1.0

SetupMultiplicity(seq, x) == Cardinality({i \in 1..Len(seq) : seq[i] = x})

Exact module download · Source bundle and reproduction instructions

SetupNext · operator

reference-profile · input revision 2 · CC0 1.0

SetupNext(before, after, witness, override(_, _, _)) ==
    /\ after.stage = SetupSuccessor(before.stage)
    /\ IF witness.overrideRequired
       THEN override(before, after, witness)
       ELSE SetupStandardNext(before, after, witness)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupStandardNext, SetupSuccessor

SetupNoPlayer · operator

reference-profile · input revision 2 · CC0 1.0

SetupNoPlayer == "none"

Exact module download · Source bundle and reproduction instructions

SetupObjectiveZones · operator

reference-profile · input revision 2 · CC0 1.0

SetupObjectiveZones == {"SideAObjectiveCompletion", "SideBObjectiveCompletion"}

Exact module download · Source bundle and reproduction instructions

SetupOwner · operator

reference-profile · input revision 2 · CC0 1.0

SetupOwner(o, cardData) ==
    IF o.card = "none" THEN SetupNoPlayer ELSE cardData[o.card].owner

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupNoPlayer

SetupPermutation · operator

reference-profile · input revision 2 · CC0 1.0

SetupPermutation(before, after) ==
    /\ Len(before) = Len(after)
    /\ \A x \in SetupRange(before) \cup SetupRange(after) :
        SetupMultiplicity(before, x) = SetupMultiplicity(after, x)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupMultiplicity, SetupRange

SetupPlayerCounterCostException · operator

reference-profile · input revision 2 · CC0 1.0

SetupPlayerCounterCostException(o) ==
    o.form = "Counter" /\ o.host = 0 /\ o.kind \in {"ExposureMarker", "LiabilityMarker"}

Exact module download · Source bundle and reproduction instructions

SetupPlayers · operator

reference-profile · input revision 2 · CC0 1.0

SetupPlayers == {"SideA", "SideB"}

Exact module download · Source bundle and reproduction instructions

SetupPrivateZones · operator

reference-profile · input revision 2 · CC0 1.0

SetupPrivateZones == {"SideADeck", "SideBDeck", "SideAHand", "SideBHand"}

Exact module download · Source bundle and reproduction instructions

SetupRange · operator

reference-profile · input revision 2 · CC0 1.0

SetupRange(seq) == {seq[i] : i \in 1..Len(seq)}

Exact module download · Source bundle and reproduction instructions

SetupRetainsPrintedCharacteristics · operator

reference-profile · input revision 2 · CC0 1.0

SetupRetainsPrintedCharacteristics(o, cardData) ==
    ~(o.form = "Card" /\ o.deployed /\ o.face = "Down" /\
      cardData[o.card].side = "SideB")

Exact module download · Source bundle and reproduction instructions

SetupRolesLegal · operator

reference-profile · input revision 2 · CC0 1.0

SetupRolesLegal(roleOf, players) ==
    /\ Cardinality(players) = 2
    /\ DOMAIN roleOf = players
    /\ {roleOf[p] : p \in players} = SetupPlayers

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

SetupSideAKinds · operator

reference-profile · input revision 2 · CC0 1.0

SetupSideAKinds == {"Objective", "Facility", "Barrier", "Profile", "Plan", "Attachment"}

Exact module download · Source bundle and reproduction instructions

SetupSideBKinds · operator

reference-profile · input revision 2 · CC0 1.0

SetupSideBKinds == {"Action", "Equipment", "Profile", "Technique", "Support"}

Exact module download · Source bundle and reproduction instructions

SetupStageActor · operator

reference-profile · input revision 2 · CC0 1.0

SetupStageActor(stage) ==
    CASE stage \in {"ProfileEffectsSideA", "RedrawSideA", "BeforeSideAFirstTurn"}
            -> "SideA"
      [] stage \in {"ProfileEffectsSideB", "RedrawSideB"} -> "SideB"
      [] OTHER -> SetupNoPlayer

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupNoPlayer

SetupStages · operator

reference-profile · input revision 2 · CC0 1.0

SetupStages == {"PlaceProfiles", "ProfileEffectsSideA",
    "ProfileEffectsSideB", "CreateBank", "TakeResourceUnits", "Shuffle",
    "DrawHands", "RedrawSideA", "RedrawSideB", "BeforeSideAFirstTurn",
    "BeginGame", "Done"}

Exact module download · Source bundle and reproduction instructions

SetupStandardNext · operator

reference-profile · input revision 2 · CC0 1.0

SetupStandardNext(before, after, witness) ==
    CASE before.stage = "PlaceProfiles" ->
            SetupAdvance(before, after, "ProfileEffectsSideA")
      [] before.stage = "ProfileEffectsSideA" ->
            SetupAdvance(before, after, "ProfileEffectsSideB")
      [] before.stage = "ProfileEffectsSideB" ->
            SetupAdvance(before, after, "CreateBank")
      [] before.stage = "CreateBank" ->
            after = [before EXCEPT !.bankReady = TRUE, !.stage = "TakeResourceUnits"]
      [] before.stage = "TakeResourceUnits" ->
            after = [before EXCEPT
                !.pool = [p \in SetupPlayers |-> @[p] + 5],
                !.stage = "Shuffle"]
      [] before.stage = "Shuffle" ->
            /\ \A p \in SetupPlayers :
                SetupPermutation(before.deck[p], witness.deck[p])
            /\ after = [before EXCEPT !.deck = witness.deck, !.stage = "DrawHands"]
      [] before.stage = "DrawHands" ->
            /\ \A p \in SetupPlayers : Len(before.deck[p]) >= 5
            /\ after = [before EXCEPT
                !.hand = [p \in SetupPlayers |->
                    @ [p] \o SubSeq(before.deck[p], 1, 5)],
                !.deck = [p \in SetupPlayers |->
                    SubSeq(before.deck[p], 6, Len(before.deck[p]))],
                !.stage = "RedrawSideA"]
      [] before.stage \in {"RedrawSideA", "RedrawSideB"} ->
            LET p == IF before.stage = "RedrawSideA" THEN "SideA" ELSE "SideB"
                next == IF p = "SideA" THEN "RedrawSideB"
                        ELSE "BeforeSideAFirstTurn"
            IN IF ~witness.redraw
               THEN SetupAdvance(before, after, next)
               ELSE /\ p \notin before.redrawn
                    /\ SetupPermutation(before.deck[p] \o before.hand[p],
                                        witness.deck)
                    /\ Len(witness.deck) >= 5
                    /\ after = [before EXCEPT
                        !.deck[p] = SubSeq(witness.deck, 6, Len(witness.deck)),
                        !.hand[p] = SubSeq(witness.deck, 1, 5),
                        !.redrawn = @ \cup {p}, !.stage = next]
      [] before.stage = "BeforeSideAFirstTurn" ->
            SetupAdvance(before, after, "BeginGame")
      [] before.stage = "BeginGame" ->
            after = [before EXCEPT !.gameStarted = TRUE,
                     !.activePlayer = "SideA", !.stage = "Done"]
      [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: next, p, SetupAdvance, SetupPermutation, SetupPlayers

SetupStart · operator

reference-profile · input revision 2 · CC0 1.0

SetupStart(profiles, decks, extras) ==
    [stage |-> "PlaceProfiles",
     profile |-> profiles,
     profileFace |-> [p \in SetupPlayers |-> "Up"],
     profileFront |-> [p \in SetupPlayers |-> TRUE],
     deck |-> decks,
     hand |-> [p \in SetupPlayers |-> <<>>],
     extras |-> extras,
     pool |-> [p \in SetupPlayers |-> 0],
     redrawn |-> {},
     bankReady |-> FALSE,
     gameStarted |-> FALSE,
     activePlayer |-> SetupNoPlayer]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupNoPlayer, SetupPlayers

SetupSuccessor · operator

reference-profile · input revision 2 · CC0 1.0

SetupSuccessor(stage) ==
    CASE stage = "PlaceProfiles" -> "ProfileEffectsSideA"
      [] stage = "ProfileEffectsSideA" -> "ProfileEffectsSideB"
      [] stage = "ProfileEffectsSideB" -> "CreateBank"
      [] stage = "CreateBank" -> "TakeResourceUnits"
      [] stage = "TakeResourceUnits" -> "Shuffle"
      [] stage = "Shuffle" -> "DrawHands"
      [] stage = "DrawHands" -> "RedrawSideA"
      [] stage = "RedrawSideA" -> "RedrawSideB"
      [] stage = "RedrawSideB" -> "BeforeSideAFirstTurn"
      [] stage = "BeforeSideAFirstTurn" -> "BeginGame"
      [] stage = "BeginGame" -> "Done"
      [] OTHER -> "NoSuccessor"

Exact module download · Source bundle and reproduction instructions

SetupViewType · operator

reference-profile · input revision 2 · CC0 1.0

SetupViewType(s) ==
    /\ s.stage \in SetupStages
    /\ DOMAIN s.profile = SetupPlayers
    /\ s.profileFace \in [SetupPlayers -> {"Up", "Down"}]
    /\ s.profileFront \in [SetupPlayers -> BOOLEAN]
    /\ DOMAIN s.deck = SetupPlayers
    /\ DOMAIN s.hand = SetupPlayers
    /\ \A p \in SetupPlayers :
        /\ s.deck[p] \in Seq(UNION {SetupRange(s.deck[q]) : q \in SetupPlayers})
        /\ s.hand[p] \in Seq(UNION {SetupRange(s.hand[q]) : q \in SetupPlayers})
    /\ s.pool \in [SetupPlayers -> Nat]
    /\ s.redrawn \subseteq SetupPlayers
    /\ s.bankReady \in BOOLEAN
    /\ s.gameStarted \in BOOLEAN
    /\ s.activePlayer \in SetupPlayers \cup {SetupNoPlayer}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupNoPlayer, SetupPlayers, SetupRange, SetupStages