----------------------------- MODULE SchemaContracts ----------------------------- EXTENDS BasicContracts, SetupContracts NameMetadataValid(c) == /\ c.kind \in SetupSideAKinds \cup SetupSideBKinds /\ c.title \in STRING /\ c.title # "" /\ c.canonicalTitle \in STRING /\ c.canonicalTitle # "" /\ c.subtitle \in STRING /\ c.canonicalSubtitle \in STRING /\ c.pronouns \in STRING /\ IF c.kind = "Profile" THEN c.subtitle # "" /\ c.canonicalSubtitle # "" ELSE c.subtitle = "" /\ c.canonicalSubtitle = "" NameParts(c) == IF c.kind = "Profile" THEN <> ELSE <> CanonicalName(c) == IF c.kind = "Profile" THEN <> ELSE <> NamePlacement(kind) == IF kind \in {"Profile","Objective","Barrier","Plan","Action","Support"} THEN "SchemaAtom163" ELSE "SchemaAtom023" CopiesOfName(objects, names, name) == {id \in objects \cap DOMAIN names : names[id] = name} NameReference(isSelf, source, objects, names, name) == IF isSelf THEN {source} \cap objects ELSE CopiesOfName(objects,names,name) DifferentCanonicalNames(chosen, names) == /\ \A i \in 1..Len(chosen) : chosen[i] \in DOMAIN names /\ \A i,j \in 1..Len(chosen) : i # j => names[chosen[i]] # names[chosen[j]] UniquePrefix(unique) == IF unique THEN "SchemaAtom060" ELSE "NoValue" UniqueMetadataValid(c) == /\ c.unique \in BOOLEAN /\ c.uniqueSymbol \in {"SchemaAtom060","NoValue"} /\ c.uniqueSymbol = UniquePrefix(c.unique) UniqueSymbolPlacement == "SchemaAtom022" NumberPart(present, amount) == [present |-> present,isX |-> FALSE,amount |-> amount] NoNumber == NumberPart(FALSE,0) XNumber == [present |-> TRUE,isX |-> TRUE,amount |-> 0] NumberPartValid(p) == /\ p.present \in BOOLEAN /\ p.isX \in BOOLEAN /\ p.amount \in Int /\ (~p.present => ~p.isX) /\ ((~p.present \/ p.isX) => p.amount = 0) NumberValue(p, isPayment, announcedX) == IF ~p.present THEN 0 ELSE IF p.isX THEN XValue(isPayment,announcedX) ELSE p.amount PrintedCostMetadataValid(c) == /\ c.kind \in SetupSideAKinds \cup SetupSideBKinds /\ \A p \in {c.playCost,c.deployCost,c.activationCost} : NumberPartValid(p) /\ c.playCost.present = (c.kind \in {"Action","Plan"}) /\ c.deployCost.present = (c.kind \in {"Equipment","Technique","Support"}) /\ c.activationCost.present = (c.kind \in {"Facility","Barrier","Attachment"}) PrintedCostPart(c, category) == CASE category = "Play" -> c.playCost [] category = "Deploy" -> c.deployCost [] category = "Activation" -> c.activationCost CostPartLayout(category) == [position |-> "SchemaAtom164",currency |-> "ResourceUnit", icon |-> IF category = "Activation" THEN "SchemaAtom148" ELSE "SchemaAtom094"] ResolvedCostCard(c, isPayment, announcedX) == [kind |-> c.kind,playCost |-> NumberValue(c.playCost,isPayment,announcedX), deployCost |-> NumberValue(c.deployCost,isPayment,announcedX), activationCost |-> NumberValue(c.activationCost,isPayment,announcedX)] CardResourceUnitCost(c, category, protectingBarrierCount, isPayment, announcedX) == LET resolved == ResolvedCostCard(c,isPayment,announcedX) IN CASE category = "Play" -> InherentPlayCost(resolved) [] category = "Deploy" -> InherentDeployCost(resolved,protectingBarrierCount) [] category = "Activation" -> InherentActivationCost(resolved) ResolvedNumberPart(p, resolvedX) == [exists |-> p.present, amount |-> IF ~p.present THEN 0 ELSE IF p.isX THEN resolvedX ELSE p.amount] ProgressMetadataValid(c) == /\ NumberPartValid(c.progressRequirement) /\ c.progressRequirement.present = (c.kind = "Objective") ProgressPart(c, resolvedX) == ResolvedNumberPart(c.progressRequirement,resolvedX) ProgressThresholdMet(counterCount, effectiveRequirement) == counterCount >= effectiveRequirement ProgressLayout == [position |-> "SchemaAtom165",icon |-> "SchemaAtom147"] ObjectivePointsMetadataValid(c) == /\ NumberPartValid(c.objectivePoints) /\ c.objectivePoints.present = (c.kind = "Objective") ObjectivePointsPart(c, resolvedX) == ResolvedNumberPart(c.objectivePoints,resolvedX) ObjectivePointLayout == [position |-> "SchemaAtom032",icon |-> "SchemaAtom161"] ObjectivePlacement(objectiveAreaRows) == SumMap([id \in DOMAIN objectiveAreaRows |-> IF objectiveAreaRows[id].form = "Card" /\ objectiveAreaRows[id].kind = "Objective" THEN objectiveAreaRows[id].objectivePoints ELSE 0]) RetireCostMetadataValid(c) == /\ NumberPartValid(c.trashCost) /\ CASE c.kind \in {"Facility","Attachment"} -> c.trashCost.present [] c.kind \in {"Barrier","Plan"} -> TRUE [] OTHER -> ~c.trashCost.present RetireCostPart(c, isPayment, announcedX) == [exists |-> c.trashCost.present,amount |-> NumberValue(c.trashCost,isPayment,announcedX)] RetireCostLayout == [position |-> "SchemaAtom102",icon |-> "SchemaAtom169",currency |-> "ResourceUnit"] StrengthMetadataValid(c) == /\ c.printedBarrierResponseCard \in BOOLEAN /\ NumberPartValid(c.strength) /\ c.strength.present = (c.kind = "Barrier" \/ (c.kind = "Technique" /\ c.printedBarrierResponseCard)) StrengthPart(c, resolvedX) == ResolvedNumberPart(c.strength,resolvedX) StrengthLayout(c) == IF c.kind = "Technique" /\ ~c.printedBarrierResponseCard THEN [position |-> "SchemaAtom027",icon |-> "SchemaAtom052"] ELSE IF c.strength.present THEN [position |-> "SchemaAtom027",icon |-> "SchemaAtom095"] ELSE [position |-> "NoValue",icon |-> "NoValue"] StrengthThresholdMet(effectiveBreakerStrength, effectiveBarrierStrength) == effectiveBreakerStrength >= effectiveBarrierStrength CapacityCostMetadataValid(c) == /\ NumberPartValid(c.capacityCost) /\ c.capacityCost.present = (c.kind = "Technique") CapacityCostPart(c, resolvedX) == ResolvedNumberPart(c.capacityCost,resolvedX) CapacityCostLayout == [position |-> "SchemaAtom135",icon |-> "SchemaAtom103"] BaseLinkMetadataValid(c) == /\ NumberPartValid(c.baseLink) /\ c.baseLink.present = (c.kind = "Profile" /\ c.side = "SideB") BaseLinkPart(c, resolvedX) == ResolvedNumberPart(c.baseLink,resolvedX) BaseLinkLayout == [position |-> "SchemaAtom164",icon |-> "Connection"] LinkValue(effectiveBaseLink, deployedLinkContributions) == effectiveBaseLink + SumMap(deployedLinkContributions) StartingCapacityMetadataValid(c) == /\ NumberPartValid(c.startingCapacityUnits) /\ (c.startingCapacityUnits.present => c.kind = "Profile" /\ c.side = "SideB") ProfileStartingCapacity(c, resolvedX) == LET applicable == c.kind = "Profile" /\ c.side = "SideB" value == ResolvedNumberPart(c.startingCapacityUnits,resolvedX) IN [applicable |-> applicable, amount |-> IF applicable THEN StartingCapacity(value.exists,value.amount) ELSE 0] StartingCapacityLayout == [position |-> "SchemaAtom164",icon |-> "SchemaAtom103"] CapacityLimitWithBase(startingLimit, effectiveAdditiveChanges) == startingLimit + SumMap(effectiveAdditiveChanges) MinimumDeckMetadataValid(c) == /\ c.front \in BOOLEAN /\ NumberPartValid(c.minDeckSize) /\ c.minDeckSize.present = (c.kind = "Profile" /\ c.front) MinimumDeckPart(c, resolvedX) == ResolvedNumberPart(c.minDeckSize,resolvedX) MinimumDeckLayout(side) == [position |-> IF side = "SideA" THEN "SchemaAtom101" ELSE "SchemaAtom102",box |-> "SchemaAtom175"] MinimumDeckSatisfied(deck, effectiveMinimum) == Len(deck) >= effectiveMinimum StandardMinimumBound(effectiveMinimum) == MaxOf(0,effectiveMinimum) ImportCostLimitMetadataValid(c) == /\ c.front \in BOOLEAN /\ NumberPartValid(c.importBudget) /\ c.importBudget.present = (c.kind = "Profile" /\ c.front) ImportCostLimitPart(c, resolvedX) == ResolvedNumberPart(c.importBudget,resolvedX) ImportCostLimitLayout(side) == [position |-> IF side = "SideA" THEN "SchemaAtom101" ELSE "SchemaAtom102",box |-> "SchemaAtom100"] ImportCostWithinLimit(effectiveImportCostTotal, effectiveLimit) == effectiveImportCostTotal <= effectiveLimit SideAAffiliations2 == {"SchemaAtom083","SchemaAtom090","SchemaAtom112","SchemaAtom183"} MajorSideBAffiliations2 == {"SchemaAtom015","GroupB","GroupA"} MiniSideBAffiliations2 == {"SchemaAtom010","SchemaAtom017","SchemaAtom157"} SideBAffiliations2 == MajorSideBAffiliations2 \cup MiniSideBAffiliations2 SchemaSymbol002 == SideAAffiliations2 \cup SideBAffiliations2 Affiliations2 == SchemaSymbol002 \cup {"Unaffiliated"} AffiliationGroup(affiliation) == CASE affiliation \in SideAAffiliations2 -> "SideA" [] affiliation \in MajorSideBAffiliations2 -> "SchemaAtom104" [] affiliation \in MiniSideBAffiliations2 -> "SchemaAtom107" [] affiliation = "Unaffiliated" -> "Unaffiliated" AffiliationMetadataValid(c) == /\ c.side \in {"SideA","SideB"} /\ c.affiliation \in Affiliations2 /\ c.affiliation = "Unaffiliated" \/ IF c.side = "SideA" THEN c.affiliation \in SideAAffiliations2 ELSE c.affiliation \in SideBAffiliations2 StandardProfileAffiliationValid(c) == c.kind # "Profile" \/ c.affiliation \in SchemaSymbol002 AffiliationLogoCorners == {"SchemaAtom164","SchemaAtom165","SchemaAtom027","SchemaAtom028"} AffiliationPresentation(affiliation) == [background |-> IF affiliation = "Unaffiliated" THEN "SchemaAtom184" ELSE "SchemaAtom069", cornerLogo |-> IF affiliation = "Unaffiliated" THEN "NoValue" ELSE affiliation, watermarkLogo |-> IF affiliation = "Unaffiliated" THEN "NoValue" ELSE affiliation] FilledImportCostSlots(slots) == Cardinality({i \in 1..Len(slots) : slots[i]}) ImportCostMetadataValid(c) == /\ NumberPartValid(c.printedImportCost) /\ ~c.printedImportCost.isX /\ c.importCostSlots \in Seq(BOOLEAN) /\ c.printedAlliance \in BOOLEAN /\ IF c.printedImportCost.present THEN /\ Len(c.importCostSlots) = 5 /\ c.printedImportCost.amount \in 0..5 /\ c.printedImportCost.amount = FilledImportCostSlots(c.importCostSlots) ELSE Len(c.importCostSlots) = 0 ImportCostBarLayout == [position |-> "SchemaAtom115",slots |-> 5,filledColor |-> "SchemaAtom026"] ImportCostPartForContext(c, context, allianceSatisfied) == [exists |-> c.printedImportCost.present, amount |-> IF ~c.printedImportCost.present THEN 0 ELSE IF context = "SchemaAtom053" /\ c.side = "SideA" /\ c.printedAlliance /\ allianceSatisfied THEN 0 ELSE c.printedImportCost.amount] ImportCostLegalityInput(part) == [hasImportCost |-> part.exists,importCost |-> part.amount] ImportCostEligibleOutOfAffiliation(card, profile) == ~OutOfAffiliation(card,profile) \/ card.printedImportCost.present CardTypes2 == {"Profile","Objective","Facility","Barrier","Plan","Attachment", "Action","Equipment","Technique","Support"} CardTypeMetadataValid(c) == /\ c.kind \in CardTypes2 /\ c.side \in {"SideA","SideB"} /\ IF c.side = "SideA" THEN c.kind \in SetupSideAKinds ELSE c.kind \in SetupSideBKinds CardTypeLayout(kind) == [position |-> IF kind = "Barrier" THEN "SchemaAtom096" ELSE "SchemaAtom031", rotationDegrees |-> IF kind = "Barrier" THEN 90 ELSE 0, bold |-> TRUE,order |-> "SchemaAtom071"] CardTypesForView(o, cardData, convertedObjective) == IF o.form # "Card" THEN {} ELSE IF ~SetupRetainsPrintedCharacteristics(o,cardData) THEN {} ELSE IF convertedObjective THEN {"Objective"} ELSE {cardData[o.card].kind} SubtypesByPrintedType == [Profile |-> {"SchemaAtom024","SchemaAtom038","SideA","SchemaAtom050","SchemaAtom057","SchemaAtom061","SchemaAtom062","SchemaAtom074","SchemaAtom097","SchemaAtom106","SchemaAtom114","SchemaAtom124","SchemaAtom150","SchemaAtom153","SchemaAtom174"}, Objective |-> {"SchemaAtom014","SchemaAtom019","SchemaAtom066","SchemaAtom067","SchemaAtom089","SchemaAtom097","SchemaAtom113","SchemaAtom127","SchemaAtom128","Research","SchemaAtom142","SchemaAtom145","SchemaAtom149"}, Facility |-> {"SchemaAtom009","SchemaAtom011","SchemaAtom013","SchemaAtom014","SchemaAtom021","SchemaAtom024","SchemaAtom029","SchemaAtom034","SchemaAtom038","SchemaAtom047","SchemaAtom055","SchemaAtom064","SchemaAtom065","SchemaAtom068","SchemaAtom079","SchemaAtom085","SchemaAtom088","SchemaAtom097","SchemaAtom125","SchemaAtom127","SchemaAtom130","Research","SchemaAtom136","SchemaAtom144","SchemaAtom167"}, Barrier |-> {"SchemaAtom007","SchemaAtom011","SchemaAtom014","SchemaSymbol001","SchemaAtom024","SchemaAtom040","SchemaAtom055","SchemaAtom056","SchemaAtom058","SchemaAtom067","SchemaAtom080","SchemaAtom084","SchemaAtom097","SchemaAtom109","SchemaAtom110","SchemaAtom113","SchemaAtom118","SchemaAtom127","Sentry","SchemaAtom166","SchemaAtom168"}, Plan |-> {"SchemaAtom013","SchemaAtom025","SchemaAtom043","SchemaAtom048","SchemaAtom063","SchemaAtom081","SchemaAtom097","SchemaAtom099","SchemaAtom105","SchemaAtom127","SchemaAtom133","SchemaAtom160","SchemaAtom167","SchemaAtom170"}, Attachment |-> {"SchemaAtom009","SchemaAtom011","SchemaAtom013","SchemaAtom014","SchemaAtom021","SchemaAtom024","SchemaAtom034","SchemaAtom038","SchemaAtom064","SchemaAtom065","SchemaAtom067","SchemaAtom068","SchemaAtom085","SchemaAtom119","SchemaAtom121","SchemaAtom127","SchemaAtom130","SchemaAtom136","SchemaAtom144","SchemaAtom143","SchemaAtom159","SchemaAtom173"}, Action |-> {"SchemaAtom043","SchemaAtom048","SchemaAtom063","SchemaAtom091","SchemaAtom108","SchemaAtom121","SchemaAtom126","SchemaAtom138","SchemaAtom139","SchemaAtom150","SchemaAtom160"}, Equipment |-> {"SchemaAtom035","SchemaAtom041","SchemaAtom045","SchemaAtom046","SchemaAtom049","SchemaAtom077","Connection","SchemaAtom108","SchemaAtom150","SchemaAtom178","SchemaAtom182"}, Technique |-> {"SchemaAtom006","SchemaAtom030","SchemaAtom039","SchemaAtom051","SchemaAtom054","SchemaAtom055","SchemaAtom059","SchemaAtom073","SchemaAtom086","SchemaAtom092","SchemaAtom150","SchemaAtom171","SchemaAtom180","SchemaAtom182"}, Support |-> {"SchemaAtom037","SchemaAtom038","SchemaAtom041","SchemaAtom044","Trait","SchemaAtom078","SchemaAtom079","SchemaAtom091","Connection","SchemaAtom098","SchemaAtom132","SchemaAtom136","SchemaAtom139","SchemaAtom144","SchemaAtom149","SchemaAtom150","SchemaAtom179"}] Subtypes2 == UNION {SubtypesByPrintedType[kind] : kind \in CardTypes2} PrintedSubtypeMetadataValid(c) == /\ c.kind \in CardTypes2 /\ c.printedSubtypes \subseteq SubtypesByPrintedType[c.kind] SubtypeFlagsConsistent(c) == /\ c.printedBarrierResponseCard = ("SchemaAtom086" \in c.printedSubtypes) /\ c.printedAlliance = ("SchemaAtom013" \in c.printedSubtypes) SubtypeLayout == [order |-> "SchemaAtom012"] IntrinsicSubtypeRule(subtype) == CASE subtype = "SchemaAtom130" -> "SchemaAtom001" [] subtype = "SchemaAtom045" -> "SchemaAtom002" [] subtype = "SchemaAtom086" -> "SchemaAtom003" [] OTHER -> "NoValue" SubtypeReference(token, isBold) == IF isBold /\ token \in Subtypes2 THEN {token} ELSE {} SubtypeChoiceAllowed(subtype, specificKind) == IF specificKind = "SchemaAtom016" THEN subtype \in Subtypes2 ELSE IF specificKind \in CardTypes2 THEN subtype \in SubtypesByPrintedType[specificKind] ELSE FALSE SingleSubtypeChoiceAllowed(chosen, specificKind) == IF Len(chosen) = 1 THEN SubtypeChoiceAllowed(chosen[1],specificKind) ELSE FALSE SubtypeCount(counts, subtype) == IF subtype \in DOMAIN counts THEN counts[subtype] ELSE 0 SubtypeCountsValid(counts) == /\ DOMAIN counts \subseteq Subtypes2 /\ \A t \in DOMAIN counts : counts[t] \in Nat PrintedSubtypeCounts(printedSubtypes) == [t \in printedSubtypes |-> 1] IncrementSubtypeCount(counts, subtype) == [t \in DOMAIN counts \cup {subtype} |-> IF t = subtype THEN SubtypeCount(counts,t)+1 ELSE counts[t]] SubtypeBalance(base, gains, losses, subtype) == SubtypeCount(base,subtype)+SubtypeCount(gains,subtype)-SubtypeCount(losses,subtype) EffectiveSubtypes(base, gains, losses) == {t \in Subtypes2 : SubtypeBalance(base,gains,losses,t) > 0} CardWithoutSubtype(o, effectiveSubtypes, subtype) == o.form = "Card" /\ subtype \notin effectiveSubtypes CardSubtypesForView(o, cardData, convertedObjective, conversionSubtypes, gains, losses) == IF o.form # "Card" THEN {} ELSE IF ~SetupRetainsPrintedCharacteristics(o,cardData) THEN {} ELSE EffectiveSubtypes( IF convertedObjective THEN conversionSubtypes ELSE PrintedSubtypeCounts(cardData[o.card].printedSubtypes),gains,losses) TextRoles2 == {"SchemaAtom137","SchemaAtom072","SchemaAtom131"} TextSegment(role, text, italic, parenthesized, rulesAst) == [role |-> role,text |-> text,italic |-> italic, parenthesized |-> parenthesized,rulesAst |-> rulesAst] TextSegmentValid(segment) == /\ segment.role \in TextRoles2 /\ segment.text \in STRING /\ segment.italic \in BOOLEAN /\ segment.parenthesized \in BOOLEAN /\ (segment.role \in {"SchemaAtom072","SchemaAtom131"} => segment.italic /\ segment.rulesAst = <<>>) /\ (segment.role = "SchemaAtom131" => segment.parenthesized) TextBoxMetadataValid(segments) == /\ \A i \in 1..Len(segments) : TextSegmentValid(segments[i]) /\ \A i,j \in 1..Len(segments) : (segments[i].role = "SchemaAtom072" /\ segments[j].role = "SchemaAtom137") => j < i RulesTextProjection(segments) == SelectSeq(segments,LAMBDA segment : segment.role = "SchemaAtom137") GameplayTextProjection(segments) == LET rules == RulesTextProjection(segments) IN [i \in 1..Len(rules) |-> rules[i].rulesAst] TextDirectlyReferenceable(segment) == segment.role = "SchemaAtom137" TextAbilityActive(abilityPresent, sourceCardActive, ruleException) == abilityPresent /\ (sourceCardActive \/ ruleException) TextBoxLayout == [position |-> "SchemaAtom033"] TargetSiteIndicatorIcons2 == {"SchemaAtom120","SchemaAtom093","SchemaAtom042"} IndicatorTargetSiteHint(icon) == CASE icon = "SchemaAtom120" -> "SchemaAtom082" [] icon = "SchemaAtom093" -> "SchemaAtom129" [] icon = "SchemaAtom042" -> "SchemaAtom018" TargetSiteIndicatorMetadataValid(c) == /\ c.front \in BOOLEAN /\ c.targetSiteIndicator \in TargetSiteIndicatorIcons2 \cup {"NoValue"} /\ (c.profileFamily = "SelectableProfile" => c.kind = "Profile" /\ c.side = "SideA") /\ IF c.profileFamily = "SelectableProfile" /\ ~c.front THEN c.targetSiteIndicator \in TargetSiteIndicatorIcons2 ELSE c.targetSiteIndicator = "NoValue" TargetSiteIndicatorLayout == [position |-> "SchemaAtom116",purpose |-> "SchemaAtom181"] IndicatorMatchesFirstAbility(c, parsedFirstAbility) == IF c.targetSiteIndicator = "NoValue" THEN TRUE ELSE IndicatorTargetSiteHint(c.targetSiteIndicator) = parsedFirstAbility.triggerTargetSite FirstAbilityCentralTargetSite(parsedFirstAbility) == parsedFirstAbility.triggerTargetSite CardRulesAstProjection(c) == GameplayTextProjection(c.textSegments) =============================================================================