-------------------------- MODULE BasicContracts -------------------------- EXTENDS Integers, FiniteSets, Sequences SumMap(f) == LET RECURSIVE Add(_) Add(S) == IF S = {} THEN 0 ELSE LET x == CHOOSE y \in S : TRUE IN f[x] + Add(S \ {x}) IN Add(DOMAIN f) SeqSum(s) == SumMap([i \in 1..Len(s) |-> s[i]]) MaxOf(a, b) == IF a >= b THEN a ELSE b MinOf(a, b) == IF a <= b THEN a ELSE b SymbolMeaning(token) == CASE token = "{unit}" -> "ResourceUnit" [] token = "{actionPoint}" -> "ActionPoint" [] token = "{renewable}" -> "RenewableResourceUnit" [] token = "{connection}" -> "Connection" [] token = "{capacity}" -> "CapacityUnit" [] token = "{procedure}" -> "BarrierInstructionMarker" [] token = "{retire}" -> "RetireThisCardCost" [] token = "{interrupt}" -> "InterruptTiming" [] OTHER -> "Unrecognized" RequiresQuantity(token) == token \in {"{unit}", "{renewable}", "{connection}"} ActionPointGlyphs(glyphCount) == glyphCount ActionPointQuantity(n) == n OutOfAffiliation(card, profile) == card.affiliation = "Unaffiliated" \/ card.affiliation # profile.affiliation ImportCostTotal(deck, profile) == SumMap([i \in 1..Len(deck) |-> IF OutOfAffiliation(deck[i], profile) /\ deck[i].hasImportCost THEN deck[i].importCost ELSE 0]) StandardObjectiveRange(n) == IF n < 40 THEN {} ELSE LET low == 18 + 2 * ((n - 40) \div 5) IN {low, low + 1} ObjectivePointTotal(deck) == SumMap([i \in 1..Len(deck) |-> IF deck[i].kind = "Objective" THEN deck[i].objectivePoints ELSE 0]) CopiesNamed(deck, name) == Cardinality({i \in 1..Len(deck) : deck[i].name = name}) StandardDeckChecks(deck, profile) == [minimumSize |-> Len(deck) >= profile.minDeckSize, allowedCards |-> \A i \in 1..Len(deck) : /\ deck[i].kind \notin {"Profile", "ReferenceAid"} /\ deck[i].side = profile.side /\ (OutOfAffiliation(deck[i], profile) => deck[i].hasImportCost), importCost |-> ImportCostTotal(deck, profile) <= profile.importBudget, copies |-> \A i \in 1..Len(deck) : CopiesNamed(deck, deck[i].name) <= deck[i].copyLimit, objectiveRangeDefined |-> profile.side # "SideA" \/ Len(deck) >= 40, objectivePoints |-> profile.side # "SideA" \/ ObjectivePointTotal(deck) \in StandardObjectiveRange(Len(deck))] AllStandardDeckChecks(checks) == /\ checks.minimumSize /\ checks.allowedCards /\ checks.importCost /\ checks.copies /\ checks.objectiveRangeDefined /\ checks.objectivePoints DeckLegal(deck, profile, profilePolicy(_, _, _), tournamentPolicy(_, _)) == /\ profile.side \in {"SideA", "SideB"} /\ profile.fullRulesLegal /\ profilePolicy(deck, profile, StandardDeckChecks(deck, profile)) /\ tournamentPolicy(deck, profile) ModifiedCost(base, increases, reductions) == MaxOf(0, base + SeqSum(increases) - SeqSum(reductions)) CalculatedCost(baseAtPayment, increases, reductions) == ModifiedCost(baseAtPayment, increases, reductions) ValidX(x, restriction(_)) == x \in Nat /\ restriction(x) XValue(isPayment, announcedX) == IF isPayment THEN announcedX ELSE 0 AlternatePaymentPreservesValue(originalValue, valueAfterMethodChoice) == valueAfterMethodChoice = originalValue TotalDiscountSplit(total, deployReduction, activationReduction) == /\ total \in Nat /\ deployReduction \in Nat /\ activationReduction \in Nat /\ deployReduction + activationReduction = total CostCategories == {"Deploy", "Play", "Activation", "Trigger", "Additional", "Nested"} IgnoreComponent(component, ignoredCategories, ignoreResourceUnits, ignoreAll) == ignoreAll \/ component.category \in ignoredCategories \/ (ignoreResourceUnits /\ component.kind = "ResourceUnit") RemainingCostIndices(costs, ignoredCategories, ignoreResourceUnits, ignoreAll) == {i \in 1..Len(costs) : ~IgnoreComponent(costs[i], ignoredCategories, ignoreResourceUnits, ignoreAll)} EffectiveCosts(costs, ignoredCategories, ignoreResourceUnits, ignoreAll) == SelectSeq(costs, LAMBDA c : ~IgnoreComponent(c, ignoredCategories, ignoreResourceUnits, ignoreAll)) InherentDeployCost(card, protectingBarrierCount) == CASE card.kind \in {"Technique", "Support", "Equipment"} -> [applicable |-> TRUE, exists |-> TRUE, amount |-> card.deployCost] [] card.kind = "Barrier" -> [applicable |-> TRUE, exists |-> TRUE, amount |-> protectingBarrierCount] [] card.kind \in {"Facility", "Attachment", "Objective"} -> [applicable |-> TRUE, exists |-> FALSE, amount |-> 0] [] OTHER -> [applicable |-> FALSE, exists |-> FALSE, amount |-> 0] InherentPlayCost(card) == IF card.kind \in {"Action", "Plan"} THEN [applicable |-> TRUE, exists |-> TRUE, amount |-> card.playCost] ELSE [applicable |-> FALSE, exists |-> FALSE, amount |-> 0] InherentActivationCost(card) == IF card.kind \in {"Facility", "Attachment", "Barrier"} THEN [applicable |-> TRUE, exists |-> TRUE, amount |-> card.activationCost] ELSE [applicable |-> FALSE, exists |-> FALSE, amount |-> 0] NestedBranch(paid, resolvesOnPayment) == paid = resolvesOnPayment StartingCapacity(hasSpecifiedStartingCapacityUnits, profileStartingCapacityUnits) == IF hasSpecifiedStartingCapacityUnits THEN profileStartingCapacityUnits ELSE 4 CapacityLimit(capacities) == SumMap(capacities) CapacityUsed(demand) == SumMap(demand) UnusedCapacity(capacities, demand) == CapacityLimit(capacities) - CapacityUsed(demand) CapacitySourceSlots(capacities) == UNION { {<> : u \in 1..MaxOf(0, capacities[s])} : s \in DOMAIN capacities } TechniqueCapacityUnits(demand) == UNION { {<> : u \in 1..demand[p]} : p \in DOMAIN demand } ValidCapacityAssignment(capacities, demand, permits, assignment) == LET units == TechniqueCapacityUnits(demand) slots == CapacitySourceSlots(capacities) IN /\ assignment \in [units -> slots] /\ \A unit \in units : unit[1] \in permits[assignment[unit][1]] /\ \A a, b \in units : assignment[a] = assignment[b] => a = b CapacityFits(capacities, demand, permits) == /\ \A s \in DOMAIN capacities : capacities[s] \in Nat /\ CapacityLimit(capacities) >= CapacityUsed(demand) /\ \E assignment \in [TechniqueCapacityUnits(demand) -> CapacitySourceSlots(capacities)] : ValidCapacityAssignment(capacities, demand, permits, assignment) =============================================================================