--------------------------- MODULE SetupContracts --------------------------- EXTENDS Integers, FiniteSets, Sequences SetupPlayers == {"SideA", "SideB"} SetupNoPlayer == "none" SetupObjectiveZones == {"SideAObjectiveCompletion", "SideBObjectiveCompletion"} SetupPrivateZones == {"SideADeck", "SideBDeck", "SideAHand", "SideBHand"} SetupSideAKinds == {"Objective", "Facility", "Barrier", "Profile", "Plan", "Attachment"} SetupSideBKinds == {"Action", "Equipment", "Profile", "Technique", "Support"} SetupRolesLegal(roleOf, players) == /\ Cardinality(players) = 2 /\ DOMAIN roleOf = players /\ {roleOf[p] : p \in players} = SetupPlayers SetupCardKindLegal(card) == IF card.side = "SideA" THEN card.kind \in SetupSideAKinds ELSE card.side = "SideB" /\ card.kind \in SetupSideBKinds SetupRange(seq) == {seq[i] : i \in 1..Len(seq)} 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" 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 ExtraThreeTraitsSelection(provided, selected, cardData) == /\ ExtraThreeTraitsProvision(provided, cardData) /\ selected \subseteq provided /\ Cardinality(selected) = 3 /\ Cardinality({cardData[c].name : c \in selected}) = 3 ExtraThreeTraitsInitialPartition(deckCards, provided, selected, deployed, outside, cardData) == /\ ExtraThreeTraitsSelection(provided, selected, cardData) /\ deckCards \intersect provided = {} /\ selected \subseteq deployed /\ provided \ selected \subseteq outside 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 ExtraLockedProfileChoice(provided, chosen, owner, cardData) == /\ ExtraFamilyProvision(provided, "LockedProfile", owner, cardData) /\ chosen \in provided ExtraSelectableProfileChoice(current, provided, chosen, owner, cardData) == /\ ExtraFamilyProvision(provided, "SelectableProfile", owner, cardData) /\ current \in provided /\ chosen \in provided 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] 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] 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) ExtraMayLookSideBProfile(player, profile, outsideProfiles) == player = "SideB" /\ profile \in outsideProfiles 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] 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] SetupStages == {"PlaceProfiles", "ProfileEffectsSideA", "ProfileEffectsSideB", "CreateBank", "TakeResourceUnits", "Shuffle", "DrawHands", "RedrawSideA", "RedrawSideB", "BeforeSideAFirstTurn", "BeginGame", "Done"} 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} SetupMultiplicity(seq, x) == Cardinality({i \in 1..Len(seq) : seq[i] = x}) SetupPermutation(before, after) == /\ Len(before) = Len(after) /\ \A x \in SetupRange(before) \cup SetupRange(after) : SetupMultiplicity(before, x) = SetupMultiplicity(after, x) SetupAdvance(before, after, next) == after = [before EXCEPT !.stage = next] 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" SetupStageActor(stage) == CASE stage \in {"ProfileEffectsSideA", "RedrawSideA", "BeforeSideAFirstTurn"} -> "SideA" [] stage \in {"ProfileEffectsSideB", "RedrawSideB"} -> "SideB" [] OTHER -> SetupNoPlayer 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 SetupNext(before, after, witness, override(_, _, _)) == /\ after.stage = SetupSuccessor(before.stage) /\ IF witness.overrideRequired THEN override(before, after, witness) ELSE SetupStandardNext(before, after, witness) 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 SetupRetainsPrintedCharacteristics(o, cardData) == ~(o.form = "Card" /\ o.deployed /\ o.face = "Down" /\ cardData[o.card].side = "SideB") SetupOwner(o, cardData) == IF o.card = "none" THEN SetupNoPlayer ELSE cardData[o.card].owner 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) 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 SetupPlayerCounterCostException(o) == o.form = "Counter" /\ o.host = 0 /\ o.kind \in {"ExposureMarker", "LiabilityMarker"} SetupMayUseForCost(payer, o, controller, explicitException) == controller = payer \/ explicitException \/ SetupPlayerCounterCostException(o) DefaultAbilityController(o, sourceController, specifiedPlayer) == IF specifiedPlayer \in SetupPlayers THEN specifiedPlayer ELSE IF o.form = "Card" /\ o.kind = "Objective" THEN "SideA" ELSE sourceController SetupEffectExecutor(abilityController, specifiedPlayer) == IF specifiedPlayer \in SetupPlayers THEN specifiedPlayer ELSE abilityController =============================================================================