------------------------------ MODULE DefinitionChecksMC ------------------------------ EXTENDS BasicContracts, SetupContracts VARIABLE done Init == done = TRUE Next == UNCHANGED done Spec == Init /\ [][Next]_done Id == [side |-> "SideB", affiliation |-> "GroupA", minDeckSize |-> 2, importBudget |-> 4, fullRulesLegal |-> TRUE] SampleAction == [name |-> "SampleAction", side |-> "SideB", kind |-> "Action", affiliation |-> "GroupA", hasImportCost |-> TRUE, importCost |-> 2, objectivePoints |-> 0, copyLimit |-> 3] Unaffiliated == [SampleAction EXCEPT !.affiliation = "Unaffiliated", !.name = "Unaffiliated"] Deck == <> DefaultProfile(d, id, c) == AllStandardDeckChecks(c) NoTournament(d, id) == TRUE Cap == [s \in {"base", "restrictedDemand"} |-> IF s = "base" THEN 1 ELSE 2] Dem == [p \in {"restrictedDemand", "generalDemand"} |-> IF p = "restrictedDemand" THEN 2 ELSE 1] Perm == [s \in {"base", "restrictedDemand"} |-> IF s = "base" THEN {"restrictedDemand", "generalDemand"} ELSE {"restrictedDemand"}] BadDem == [p \in {"restrictedDemand", "generalDemand"} |-> IF p = "restrictedDemand" THEN 0 ELSE 3] EmptyMap == [x \in {} |-> 0] Costs == <<[category |-> "Play", kind |-> "ResourceUnit", amount |-> 2], [category |-> "Additional", kind |-> "Retire", amount |-> 1]>> StaticChecks == /\ SymbolMeaning("{retire}") = "RetireThisCardCost" /\ StandardObjectiveRange(39) = {} /\ StandardObjectiveRange(40) = {18,19} /\ StandardObjectiveRange(44) = {18,19} /\ StandardObjectiveRange(45) = {20,21} /\ StandardObjectiveRange(54) = {22,23} /\ StandardObjectiveRange(55) = {24,25} /\ StandardObjectiveRange(66) = {28,29} /\ OutOfAffiliation(Unaffiliated, [Id EXCEPT !.affiliation = "Unaffiliated"]) /\ ImportCostTotal(Deck, [Id EXCEPT !.affiliation = "GroupB"]) = 4 /\ DeckLegal(Deck, Id, DefaultProfile, NoTournament) /\ ~DeckLegal(<>, Id, DefaultProfile, NoTournament) /\ ~DeckLegal(Deck, [Id EXCEPT !.fullRulesLegal = FALSE], DefaultProfile, NoTournament) /\ ModifiedCost(2, <<1,1>>, <<7>>) = 0 /\ XValue(FALSE, 7) = 0 /\ TotalDiscountSplit(3,1,2) /\ ~TotalDiscountSplit(3,2,2) /\ EffectiveCosts(Costs, {"Play"}, FALSE, FALSE) = <> /\ EffectiveCosts(Costs, {}, TRUE, FALSE) = <> /\ EffectiveCosts(Costs, {}, FALSE, TRUE) = <<>> /\ CapacityFits(Cap, Dem, Perm) /\ UnusedCapacity(Cap, BadDem) = 0 /\ ~CapacityFits(Cap, BadDem, Perm) /\ CapacityFits(EmptyMap, EmptyMap, EmptyMap) /\ StartingCapacity(FALSE, 0) = 4 /\ ~NestedBranch(FALSE, TRUE) /\ NestedBranch(FALSE, FALSE) Meta(owner, kind, name, family, subtypes) == [owner |-> owner, side |-> owner, kind |-> kind, name |-> name, profileFamily |-> family, subtypes |-> subtypes] CardIds == {"ci", "ri", "dA", "dA2", "dB", "dC", "mA", "mB", "bA", "bB", "rExtra", "technique", "objective"} Data == [c \in CardIds |-> CASE c = "ci" -> Meta("SideA", "Profile", "SideAId", "Other", {}) [] c = "ri" -> Meta("SideB", "Profile", "SideBId", "Other", {}) [] c \in {"dA", "dA2"} -> Meta("SideB", "Support", "TraitA", "Other", {"Trait"}) [] c = "dB" -> Meta("SideB", "Support", "TraitB", "Other", {"Trait"}) [] c = "dC" -> Meta("SideB", "Support", "TraitC", "Other", {"Trait"}) [] c \in {"mA", "mB"} -> Meta("SideA", "Profile", "SelectableProfile", "SelectableProfile", {}) [] c \in {"bA", "bB"} -> Meta("SideA", "Profile", "LockedProfile", "LockedProfile", {}) [] c = "rExtra" -> Meta("SideB", "Profile", "ExtraSideB", "Other", {}) [] c = "technique" -> Meta("SideB", "Technique", "Technique", "Other", {}) [] OTHER -> Meta("SideA", "Objective", "Objective", "Other", {})] Obj(card, form, kind, zone, deployed, face, activated, host, placedBy) == [card |-> card, form |-> form, kind |-> kind, zone |-> zone, deployed |-> deployed, face |-> face, front |-> TRUE, activated |-> activated, host |-> host, placedBy |-> placedBy] TechniqueUp == Obj("technique", "Card", "Technique", "Play", TRUE, "Up", FALSE, 0, "SideB") TechniqueDown == [TechniqueUp EXCEPT !.face = "Down"] SideAObjective == Obj("objective", "Card", "Objective", "SideAObjectiveCompletion", FALSE, "Up", FALSE, 0, "SideA") SideBObjective == [SideAObjective EXCEPT !.zone = "SideBObjectiveCompletion"] HostedResourceUnit == Obj("none", "Counter", "ResourceUnit", "Play", FALSE, "NA", FALSE, 3, "none") ActionPointAid == [HostedResourceUnit EXCEPT !.kind = "ActionPoint"] ExposureMarker == [HostedResourceUnit EXCEPT !.host = 0, !.kind = "ExposureMarker"] Ids == [p \in SetupPlayers |-> IF p = "SideA" THEN "ci" ELSE "ri"] Decks == [p \in SetupPlayers |-> IF p = "SideA" THEN <<"c1", "c2", "c3", "c4", "c5">> ELSE <<"r1", "r2", "r3", "r4", "r5">>] Start == SetupStart(Ids, Decks, [p \in SetupPlayers |-> {}]) ResourceUnitsBefore == [Start EXCEPT !.stage = "TakeResourceUnits", !.bankReady = TRUE] ResourceUnitsAfter == [ResourceUnitsBefore EXCEPT !.stage = "Shuffle", !.pool = [p \in SetupPlayers |-> 5]] RedrawBefore == [Start EXCEPT !.stage = "RedrawSideA", !.bankReady = TRUE, !.pool = [p \in SetupPlayers |-> 5], !.hand = Decks, !.deck = [p \in SetupPlayers |-> <<>>]] RedrawAfter == [RedrawBefore EXCEPT !.stage = "RedrawSideB", !.redrawn = {"SideA"}] RedrawWitness == [redraw |-> TRUE, deck |-> Decks["SideA"]] NoOverride(before, after, witness) == FALSE Traits == {"dA", "dA2", "dB", "dC"} ChosenTraits == {"dA", "dB", "dC"} SelectableProfileBefore == [active |-> "mA", outside |-> {"mB"}, face |-> [c \in {"mA", "mB"} |-> IF c = "mA" THEN "Down" ELSE "NA"], front |-> [c \in {"mA", "mB"} |-> FALSE], locked |-> FALSE, stage |-> "InGame"] SelectableProfileSameAfter == [SelectableProfileBefore EXCEPT !.face["mA"] = "Up", !.front["mA"] = TRUE] ReplacementBefore == [active |-> "ri", outside |-> {"rExtra"}, face |-> [c \in {"ri", "rExtra"} |-> IF c = "ri" THEN "Down" ELSE "NA"], front |-> [c \in {"ri", "rExtra"} |-> FALSE], locked |-> FALSE, stage |-> "InGame"] ReplacementAfter == [ReplacementBefore EXCEPT !.active = "rExtra", !.outside = {"ri"}, !.face["ri"] = "NA", !.face["rExtra"] = "Up", !.front["rExtra"] = TRUE] SetupChecks == /\ SetupRolesLegal([p \in {"Alice", "Bob"} |-> IF p = "Alice" THEN "SideA" ELSE "SideB"], {"Alice", "Bob"}) /\ ~SetupRolesLegal([p \in {"Alice", "Bob"} |-> "SideA"], {"Alice", "Bob"}) /\ SetupInitialProfilesLegal(Ids, Data) /\ SetupCardKindLegal(Data["objective"]) /\ ~SetupCardKindLegal([Data["objective"] EXCEPT !.side = "SideB"]) /\ (\A p \in SetupPlayers : Start.profileFront[p] /\ Start.profileFace[p] = "Up") /\ Start.pool = [p \in SetupPlayers |-> 0] /\ SetupStandardNext(ResourceUnitsBefore, ResourceUnitsAfter, [unused |-> TRUE]) /\ SetupSuccessor("PlaceProfiles") = "ProfileEffectsSideA" /\ SetupSuccessor("ProfileEffectsSideA") = "ProfileEffectsSideB" /\ SetupSuccessor("DrawHands") = "RedrawSideA" /\ SetupSuccessor("RedrawSideA") = "RedrawSideB" /\ SetupSuccessor("BeforeSideAFirstTurn") = "BeginGame" /\ (~Start.gameStarted /\ Start.activePlayer = SetupNoPlayer) /\ SetupStandardNext(RedrawBefore, RedrawAfter, RedrawWitness) /\ ~SetupStandardNext([RedrawBefore EXCEPT !.redrawn = {"SideA"}], RedrawAfter, RedrawWitness) /\ SetupStandardNext(RedrawBefore, [RedrawBefore EXCEPT !.stage = "RedrawSideB"], [redraw |-> FALSE]) /\ ~SetupPermutation(<<"a", "a", "b">>, <<"a", "b", "b">>) /\ ~SetupNext(Start, [Start EXCEPT !.stage = "ProfileEffectsSideA"], [overrideRequired |-> TRUE], NoOverride) /\ ExtraThreeTraitsProvision(Traits, Data) /\ ExtraThreeTraitsSelection(Traits, ChosenTraits, Data) /\ ~ExtraThreeTraitsSelection(Traits, {"dA", "dA2", "dB"}, Data) /\ ExtraThreeTraitsInitialPartition({"technique"}, Traits, ChosenTraits, ChosenTraits, {"dA2"}, Data) /\ ExtraSelectableProfileChoice("mA", {"mA", "mB"}, "mA", "SideA", Data) /\ ExtraSelectableProfileSet(SelectableProfileBefore, SelectableProfileSameAfter, {"mA", "mB"}, "mA", "SideA", Data) /\ ExtraProfileReplacement(ReplacementBefore, ReplacementAfter, "rExtra", Data) /\ ExtraMayLookSideBProfile("SideB", "rExtra", {"rExtra"}) /\ ~ExtraMayLookSideBProfile("SideA", "rExtra", {"rExtra"}) /\ DefaultActive(TechniqueUp, TRUE, Data) /\ ~DefaultActive(TechniqueUp, FALSE, Data) /\ ~DefaultActive(TechniqueDown, TRUE, Data) /\ DefaultActive(SideAObjective, TRUE, Data) /\ ~DefaultActive(SideBObjective, TRUE, Data) /\ ~SetupRetainsPrintedCharacteristics(TechniqueDown, Data) /\ SetupOwner([TechniqueUp EXCEPT !.form = "Counter"], Data) = "SideB" /\ SetupOwner(HostedResourceUnit, Data) = SetupNoPlayer /\ SetupCardController(SideBObjective, Data) = "SideB" /\ SetupCounterController(HostedResourceUnit, "SideA", SetupNoPlayer) = "SideA" /\ SetupCounterController(ActionPointAid, "SideA", SetupNoPlayer) = SetupNoPlayer /\ SetupCounterController(ExposureMarker, "SideA", SetupNoPlayer) = "SideB" /\ DefaultAbilityController(SideBObjective, "SideB", SetupNoPlayer) = "SideA" /\ DefaultAbilityController(SideBObjective, "SideB", "SideB") = "SideB" /\ SetupEffectExecutor("SideA", "SideB") = "SideB" /\ SetupMayUseForCost("SideA", ExposureMarker, "SideB", FALSE) LockedProfileCopies == {"bA", "bB"} LockedProfileBefore == [active |-> "bA", outside |-> {"bB"}, face |-> [c \in LockedProfileCopies |-> IF c = "bA" THEN "Up" ELSE "NA"], front |-> [c \in LockedProfileCopies |-> TRUE], locked |-> FALSE, stage |-> "AfterSetup"] LockedProfileSwitchAfter == [LockedProfileBefore EXCEPT !.active = "bB", !.outside = {"bA"}, !.face["bA"] = "NA", !.face["bB"] = "Up", !.locked = TRUE] LockedProfileLostOutgoing == [LockedProfileSwitchAfter EXCEPT !.outside = {}, !.face["bA"] = "Up"] LockedProfileKeepAfter == [LockedProfileBefore EXCEPT !.locked = TRUE] LockedProfileSoloBefore == [active |-> "bA", outside |-> {}, face |-> [c \in {"bA"} |-> "Up"], front |-> [c \in {"bA"} |-> TRUE], locked |-> FALSE, stage |-> "AfterSetup"] LockedProfileCandidateViews == [active : LockedProfileCopies, outside : SUBSET LockedProfileCopies, face : [LockedProfileCopies -> {"Up", "NA"}], front : [LockedProfileCopies -> BOOLEAN], locked : BOOLEAN, stage : {"AfterSetup"}] LockedProfileChecks == /\ ~ExtraLockedProfileSet(LockedProfileBefore, LockedProfileLostOutgoing, {"bB"}, "bB", "SideA", Data) /\ ExtraLockedProfileSet(LockedProfileBefore, LockedProfileSwitchAfter, LockedProfileCopies, "bB", "SideA", Data) /\ ~ExtraLockedProfileSet(LockedProfileBefore, LockedProfileLostOutgoing, LockedProfileCopies, "bB", "SideA", Data) /\ ~ExtraLockedProfileSet(LockedProfileBefore, [LockedProfileSwitchAfter EXCEPT !.face["bA"] = "Up"], LockedProfileCopies, "bB", "SideA", Data) /\ ExtraLockedProfileSet(LockedProfileBefore, LockedProfileKeepAfter, LockedProfileCopies, "bA", "SideA", Data) /\ ExtraLockedProfileSet(LockedProfileSoloBefore, [LockedProfileSoloBefore EXCEPT !.locked = TRUE], {"bA"}, "bA", "SideA", Data) /\ ~ExtraLockedProfileSet([LockedProfileBefore EXCEPT !.locked = TRUE], LockedProfileSwitchAfter, LockedProfileCopies, "bB", "SideA", Data) /\ ~ExtraLockedProfileSet([LockedProfileBefore EXCEPT !.stage = "InGame"], [LockedProfileSwitchAfter EXCEPT !.stage = "InGame"], LockedProfileCopies, "bB", "SideA", Data) /\ \A provided \in SUBSET LockedProfileCopies, chosen \in LockedProfileCopies, after \in LockedProfileCandidateViews : ExtraLockedProfileSet(LockedProfileBefore, after, provided, chosen, "SideA", Data) => /\ after.active = chosen /\ after.outside = LockedProfileCopies \ {chosen} /\ after.face[chosen] = "Up" /\ \A outgoing \in LockedProfileCopies \ {chosen} : after.face[outgoing] = "NA" /\ after.locked AllAssertions == done /\ StaticChecks /\ SetupChecks /\ LockedProfileChecks =============================================================================