BasicContracts

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.

LAMBDA · operator

reference-profile · input revision 2 · CC0 1.0

LAMBDA c :
        ~IgnoreComponent(c, ignoredCategories, ignoreResourceUnits, ignoreAll)

Exact module download · Source bundle and reproduction instructions

low · operator

reference-profile · input revision 2 · CC0 1.0

low == 18 + 2 * ((n - 40) \div 5)

Exact module download · Source bundle and reproduction instructions

x · operator

reference-profile · input revision 2 · CC0 1.0

x == CHOOSE y \in S : TRUE

Exact module download · Source bundle and reproduction instructions

Add · operator

reference-profile · input revision 2 · CC0 1.0

Add(S) == IF S = {} THEN 0
                  ELSE LET x == CHOOSE y \in S : TRUE
                       IN f[x] + Add(S \ {x})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: x, Add

slots · operator

reference-profile · input revision 2 · CC0 1.0

slots == CapacitySourceSlots(capacities)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CapacitySourceSlots

units · operator

reference-profile · input revision 2 · CC0 1.0

units == TechniqueCapacityUnits(demand)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TechniqueCapacityUnits

ActionPointGlyphs · operator

reference-profile · input revision 2 · CC0 1.0

ActionPointGlyphs(glyphCount) == glyphCount

Exact module download · Source bundle and reproduction instructions

ActionPointQuantity · operator

reference-profile · input revision 2 · CC0 1.0

ActionPointQuantity(n) == n

Exact module download · Source bundle and reproduction instructions

AllStandardDeckChecks · operator

reference-profile · input revision 2 · CC0 1.0

AllStandardDeckChecks(checks) ==
    /\ checks.minimumSize
    /\ checks.allowedCards
    /\ checks.importCost
    /\ checks.copies
    /\ checks.objectiveRangeDefined
    /\ checks.objectivePoints

Exact module download · Source bundle and reproduction instructions

AlternatePaymentPreservesValue · operator

reference-profile · input revision 2 · CC0 1.0

AlternatePaymentPreservesValue(originalValue, valueAfterMethodChoice) ==
    valueAfterMethodChoice = originalValue

Exact module download · Source bundle and reproduction instructions

CalculatedCost · operator

reference-profile · input revision 2 · CC0 1.0

CalculatedCost(baseAtPayment, increases, reductions) ==
    ModifiedCost(baseAtPayment, increases, reductions)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ModifiedCost

CapacityFits · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CapacityLimit, CapacitySourceSlots, CapacityUsed, TechniqueCapacityUnits, ValidCapacityAssignment

CapacityLimit · operator

reference-profile · input revision 2 · CC0 1.0

CapacityLimit(capacities) == SumMap(capacities)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

CapacitySourceSlots · operator

reference-profile · input revision 2 · CC0 1.0

CapacitySourceSlots(capacities) ==
    UNION { {<<s, u>> : u \in 1..MaxOf(0, capacities[s])}
            : s \in DOMAIN capacities }

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf

CapacityUsed · operator

reference-profile · input revision 2 · CC0 1.0

CapacityUsed(demand) == SumMap(demand)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

CopiesNamed · operator

reference-profile · input revision 2 · CC0 1.0

CopiesNamed(deck, name) ==
    Cardinality({i \in 1..Len(deck) : deck[i].name = name})

Exact module download · Source bundle and reproduction instructions

CostCategories · operator

reference-profile · input revision 2 · CC0 1.0

CostCategories == {"Deploy", "Play", "Activation", "Trigger", "Additional", "Nested"}

Exact module download · Source bundle and reproduction instructions

DeckLegal · operator

reference-profile · input revision 2 · CC0 1.0

DeckLegal(deck, profile, profilePolicy(_, _, _), tournamentPolicy(_, _)) ==
    /\ profile.side \in {"SideA", "SideB"}
    /\ profile.fullRulesLegal
    /\ profilePolicy(deck, profile, StandardDeckChecks(deck, profile))
    /\ tournamentPolicy(deck, profile)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StandardDeckChecks

EffectiveCosts · operator

reference-profile · input revision 2 · CC0 1.0

EffectiveCosts(costs, ignoredCategories, ignoreResourceUnits, ignoreAll) ==
    SelectSeq(costs, LAMBDA c :
        ~IgnoreComponent(c, ignoredCategories, ignoreResourceUnits, ignoreAll))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LAMBDA

IgnoreComponent · operator

reference-profile · input revision 2 · CC0 1.0

IgnoreComponent(component, ignoredCategories, ignoreResourceUnits, ignoreAll) ==
    ignoreAll \/ component.category \in ignoredCategories \/
    (ignoreResourceUnits /\ component.kind = "ResourceUnit")

Exact module download · Source bundle and reproduction instructions

ImportCostTotal · operator

reference-profile · input revision 2 · CC0 1.0

ImportCostTotal(deck, profile) ==
    SumMap([i \in 1..Len(deck) |->
        IF OutOfAffiliation(deck[i], profile) /\ deck[i].hasImportCost
        THEN deck[i].importCost ELSE 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OutOfAffiliation, SumMap

InherentActivationCost · operator

reference-profile · input revision 2 · CC0 1.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]

Exact module download · Source bundle and reproduction instructions

InherentDeployCost · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

InherentPlayCost · operator

reference-profile · input revision 2 · CC0 1.0

InherentPlayCost(card) ==
    IF card.kind \in {"Action", "Plan"}
    THEN [applicable |-> TRUE, exists |-> TRUE, amount |-> card.playCost]
    ELSE [applicable |-> FALSE, exists |-> FALSE, amount |-> 0]

Exact module download · Source bundle and reproduction instructions

MaxOf · operator

reference-profile · input revision 2 · CC0 1.0

MaxOf(a, b) == IF a >= b THEN a ELSE b

Exact module download · Source bundle and reproduction instructions

MinOf · operator

reference-profile · input revision 2 · CC0 1.0

MinOf(a, b) == IF a <= b THEN a ELSE b

Exact module download · Source bundle and reproduction instructions

ModifiedCost · operator

reference-profile · input revision 2 · CC0 1.0

ModifiedCost(base, increases, reductions) ==
    MaxOf(0, base + SeqSum(increases) - SeqSum(reductions))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, SeqSum

NestedBranch · operator

reference-profile · input revision 2 · CC0 1.0

NestedBranch(paid, resolvesOnPayment) == paid = resolvesOnPayment

Exact module download · Source bundle and reproduction instructions

ObjectivePointTotal · operator

reference-profile · input revision 2 · CC0 1.0

ObjectivePointTotal(deck) ==
    SumMap([i \in 1..Len(deck) |->
        IF deck[i].kind = "Objective" THEN deck[i].objectivePoints ELSE 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

OutOfAffiliation · operator

reference-profile · input revision 2 · CC0 1.0

OutOfAffiliation(card, profile) ==
    card.affiliation = "Unaffiliated" \/ card.affiliation # profile.affiliation

Exact module download · Source bundle and reproduction instructions

RemainingCostIndices · operator

reference-profile · input revision 2 · CC0 1.0

RemainingCostIndices(costs, ignoredCategories, ignoreResourceUnits, ignoreAll) ==
    {i \in 1..Len(costs) :
        ~IgnoreComponent(costs[i], ignoredCategories, ignoreResourceUnits, ignoreAll)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IgnoreComponent

RequiresQuantity · operator

reference-profile · input revision 2 · CC0 1.0

RequiresQuantity(token) == token \in {"{unit}", "{renewable}", "{connection}"}

Exact module download · Source bundle and reproduction instructions

SeqSum · operator

reference-profile · input revision 2 · CC0 1.0

SeqSum(s) == SumMap([i \in 1..Len(s) |-> s[i]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

StandardDeckChecks · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CopiesNamed, ImportCostTotal, ObjectivePointTotal, OutOfAffiliation, StandardObjectiveRange

StandardObjectiveRange · operator

reference-profile · input revision 2 · CC0 1.0

StandardObjectiveRange(n) ==
    IF n < 40 THEN {}
    ELSE LET low == 18 + 2 * ((n - 40) \div 5)
         IN {low, low + 1}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: low

StartingCapacity · operator

reference-profile · input revision 2 · CC0 1.0

StartingCapacity(hasSpecifiedStartingCapacityUnits, profileStartingCapacityUnits) ==
    IF hasSpecifiedStartingCapacityUnits THEN profileStartingCapacityUnits ELSE 4

Exact module download · Source bundle and reproduction instructions

SumMap · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Add

SymbolMeaning · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

TechniqueCapacityUnits · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCapacityUnits(demand) ==
    UNION { {<<p, u>> : u \in 1..demand[p]}
            : p \in DOMAIN demand }

Exact module download · Source bundle and reproduction instructions

TotalDiscountSplit · operator

reference-profile · input revision 2 · CC0 1.0

TotalDiscountSplit(total, deployReduction, activationReduction) ==
    /\ total \in Nat
    /\ deployReduction \in Nat
    /\ activationReduction \in Nat
    /\ deployReduction + activationReduction = total

Exact module download · Source bundle and reproduction instructions

UnusedCapacity · operator

reference-profile · input revision 2 · CC0 1.0

UnusedCapacity(capacities, demand) == CapacityLimit(capacities) - CapacityUsed(demand)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CapacityLimit, CapacityUsed

ValidCapacityAssignment · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: slots, units

ValidX · operator

reference-profile · input revision 2 · CC0 1.0

ValidX(x, restriction(_)) == x \in Nat /\ restriction(x)

Exact module download · Source bundle and reproduction instructions

XValue · operator

reference-profile · input revision 2 · CC0 1.0

XValue(isPayment, announcedX) == IF isPayment THEN announcedX ELSE 0

Exact module download · Source bundle and reproduction instructions