---------------------------- MODULE SchemaChecksMC ---------------------------- EXTENDS SchemaContracts VARIABLE block2 Init2 == block2 \in 1..18 Next2 == UNCHANGED block2 Spec2 == Init2 /\ [][Next2]_block2 NameCard == [kind |-> "Profile",title |-> "SchemaAtom123",subtitle |-> "SchemaAtom070", canonicalTitle |-> "SchemaAtom123",canonicalSubtitle |-> "SchemaAtom070",pronouns |-> "SchemaAtom189"] NameTechnique == [kind |-> "Technique",title |-> "SchemaAtom122",subtitle |-> "", canonicalTitle |-> "SchemaAtom162",canonicalSubtitle |-> "",pronouns |-> ""] ExampleNames == [id \in 1..4 |-> IF id \in {1,2} THEN CanonicalName(NameCard) ELSE IF id = 3 THEN CanonicalName(NameTechnique) ELSE <<"Other">>] NameChecks == /\ NameMetadataValid(NameCard) /\ NameMetadataValid(NameTechnique) /\ ~NameMetadataValid([NameCard EXCEPT !.subtitle = ""]) /\ NameParts(NameCard) = <<"SchemaAtom123","SchemaAtom070">> /\ NameParts(NameTechnique) = <<"SchemaAtom122">> /\ CanonicalName(NameTechnique) = <<"SchemaAtom162">> /\ CanonicalName([NameCard EXCEPT !.pronouns = "SchemaAtom188"]) = <<"SchemaAtom123","SchemaAtom070">> /\ CanonicalName([NameCard EXCEPT !.canonicalSubtitle = "SchemaAtom140"]) = <<"SchemaAtom123","SchemaAtom140">> /\ \A k \in {"Profile","Objective","Barrier","Plan","Action","Support"} : NamePlacement(k) = "SchemaAtom163" /\ \A k \in {"Facility","Attachment","Equipment","Technique"} : NamePlacement(k) = "SchemaAtom023" /\ CopiesOfName({1,2,3,5},ExampleNames,<<"SchemaAtom123","SchemaAtom070">>) = {1,2} /\ NameReference(TRUE,1,{1,2,3},ExampleNames,<<"SchemaAtom123","SchemaAtom070">>) = {1} /\ NameReference(FALSE,1,{1,2,3},ExampleNames,<<"SchemaAtom123","SchemaAtom070">>) = {1,2} /\ NameReference(TRUE,9,{1,2,3},ExampleNames,<<"SchemaAtom123","SchemaAtom070">>) = {} /\ DifferentCanonicalNames(<<1,3>>,ExampleNames) /\ DifferentCanonicalNames(<<>>,ExampleNames) /\ ~DifferentCanonicalNames(<<1,2>>,ExampleNames) /\ ~DifferentCanonicalNames(<<1,1>>,ExampleNames) /\ ~DifferentCanonicalNames(<<5>>,ExampleNames) UniqueChecks == /\ UniqueMetadataValid([unique |-> TRUE,uniqueSymbol |-> "SchemaAtom060"]) /\ UniqueMetadataValid([unique |-> FALSE,uniqueSymbol |-> "NoValue"]) /\ ~UniqueMetadataValid([unique |-> TRUE,uniqueSymbol |-> "NoValue"]) /\ ~UniqueMetadataValid([unique |-> FALSE,uniqueSymbol |-> "SchemaAtom060"]) /\ ~UniqueMetadataValid([unique |-> TRUE,uniqueSymbol |-> "SchemaAtom036"]) /\ UniquePrefix(TRUE) = "SchemaAtom060" /\ UniquePrefix(FALSE) = "NoValue" /\ UniqueSymbolPlacement = "SchemaAtom022" CostExample(kind, play, deploy, activation) == [kind |-> kind,playCost |-> play,deployCost |-> deploy,activationCost |-> activation] EventCost == CostExample("Action",NumberPart(TRUE,5),NoNumber,NoNumber) TechniqueCost == CostExample("Technique",NoNumber,NumberPart(TRUE,0),NoNumber) BarrierCost == CostExample("Barrier",NoNumber,NoNumber,NumberPart(TRUE,3)) FacilityCost == CostExample("Facility",NoNumber,NoNumber,NumberPart(TRUE,0)) CostChecks == /\ NumberPartValid(NoNumber) /\ NumberPartValid(XNumber) /\ ~NumberPartValid(NumberPart(FALSE,2)) /\ \A c \in {EventCost,TechniqueCost,BarrierCost,FacilityCost, CostExample("Plan",XNumber,NoNumber,NoNumber), CostExample("Equipment",NoNumber,NumberPart(TRUE,2),NoNumber), CostExample("Support",NoNumber,NumberPart(TRUE,1),NoNumber), CostExample("Attachment",NoNumber,NoNumber,NumberPart(TRUE,2)), CostExample("Objective",NoNumber,NoNumber,NoNumber), CostExample("Profile",NoNumber,NoNumber,NoNumber)} : PrintedCostMetadataValid(c) /\ ~PrintedCostMetadataValid([EventCost EXCEPT !.playCost = NoNumber]) /\ ~PrintedCostMetadataValid([BarrierCost EXCEPT !.deployCost = NumberPart(TRUE,1)]) /\ PrintedCostMetadataValid([EventCost EXCEPT !.playCost = NumberPart(TRUE,-1)]) /\ CardResourceUnitCost([EventCost EXCEPT !.playCost = NumberPart(TRUE,-1)],"Play",0,TRUE,0).amount = -1 /\ ModifiedCost(-1,<<2>>,<<>>) = 1 /\ ModifiedCost(-1,<<>>,<<>>) = 0 /\ PrintedCostPart(BarrierCost,"Deploy") = NoNumber /\ CardResourceUnitCost(BarrierCost,"Deploy",4,TRUE,0) = [applicable |-> TRUE,exists |-> TRUE,amount |-> 4] /\ CardResourceUnitCost(TechniqueCost,"Deploy",4,TRUE,0) = [applicable |-> TRUE,exists |-> TRUE,amount |-> 0] /\ CardResourceUnitCost(FacilityCost,"Deploy",4,TRUE,0) = [applicable |-> TRUE,exists |-> FALSE,amount |-> 0] /\ CardResourceUnitCost(EventCost,"Play",0,TRUE,0).amount = 5 /\ CardResourceUnitCost(BarrierCost,"Activation",0,TRUE,0).amount = 3 /\ CardResourceUnitCost([EventCost EXCEPT !.playCost = XNumber],"Play",0,TRUE,4).amount = 4 /\ CardResourceUnitCost([EventCost EXCEPT !.playCost = XNumber],"Play",0,FALSE,4).amount = 0 /\ CostPartLayout("Play").icon = "SchemaAtom094" /\ CostPartLayout("Deploy").currency = "ResourceUnit" /\ CostPartLayout("Activation").icon = "SchemaAtom148" ProgressExample == [kind |-> "Objective",progressRequirement |-> NumberPart(TRUE,3)] ProgressChecks == /\ ProgressMetadataValid(ProgressExample) /\ ProgressMetadataValid([ProgressExample EXCEPT !.progressRequirement = NumberPart(TRUE,-1)]) /\ ProgressMetadataValid([kind |-> "Technique",progressRequirement |-> NoNumber]) /\ ~ProgressMetadataValid([ProgressExample EXCEPT !.kind = "Barrier"]) /\ ~ProgressMetadataValid([ProgressExample EXCEPT !.progressRequirement = NoNumber]) /\ ProgressPart(ProgressExample,9) = [exists |-> TRUE,amount |-> 3] /\ ProgressPart([ProgressExample EXCEPT !.progressRequirement = NumberPart(TRUE,0)],9) = [exists |-> TRUE,amount |-> 0] /\ ProgressPart([kind |-> "Technique",progressRequirement |-> NoNumber],9) = [exists |-> FALSE,amount |-> 0] /\ ResolvedNumberPart(XNumber,4) = [exists |-> TRUE,amount |-> 4] /\ ~ProgressThresholdMet(2,3) /\ ProgressThresholdMet(3,3) /\ ProgressThresholdMet(4,3) /\ ProgressThresholdMet(0,0) /\ ProgressThresholdMet(0,-1) /\ ProgressLayout.position = "SchemaAtom165" /\ ProgressLayout.icon = "SchemaAtom147" PointChecks == /\ ObjectivePointsMetadataValid([kind |-> "Objective",objectivePoints |-> NumberPart(TRUE,0)]) /\ ObjectivePointsMetadataValid([kind |-> "Objective",objectivePoints |-> NumberPart(TRUE,-1)]) /\ ObjectivePointsMetadataValid([kind |-> "Facility",objectivePoints |-> NoNumber]) /\ ~ObjectivePointsMetadataValid([kind |-> "Barrier",objectivePoints |-> NumberPart(TRUE,2)]) /\ ~ObjectivePointsMetadataValid([kind |-> "Objective",objectivePoints |-> NoNumber]) /\ ObjectivePointsPart([kind |-> "Objective",objectivePoints |-> NumberPart(TRUE,-1)],0) = [exists |-> TRUE,amount |-> -1] /\ ObjectivePlacement([id \in {} |-> id]) = 0 /\ \A p,q \in -2..2 : ObjectivePlacement([id \in 1..4 |-> [form |-> IF id = 4 THEN "Counter" ELSE "Card", kind |-> IF id = 3 THEN "Support" ELSE "Objective", objectivePoints |-> CASE id = 1 -> p [] id = 2 -> q [] OTHER -> 99]]) = p + q /\ ObjectivePointLayout.position = "SchemaAtom032" /\ ObjectivePointLayout.icon = "SchemaAtom161" RetireCostChecks == /\ RetireCostMetadataValid([kind |-> "Facility",trashCost |-> NumberPart(TRUE,0)]) /\ RetireCostMetadataValid([kind |-> "Attachment",trashCost |-> NumberPart(TRUE,3)]) /\ RetireCostMetadataValid([kind |-> "Barrier",trashCost |-> NoNumber]) /\ RetireCostMetadataValid([kind |-> "Barrier",trashCost |-> NumberPart(TRUE,2)]) /\ RetireCostMetadataValid([kind |-> "Plan",trashCost |-> NoNumber]) /\ RetireCostMetadataValid([kind |-> "Plan",trashCost |-> NumberPart(TRUE,-1)]) /\ ~RetireCostMetadataValid([kind |-> "Facility",trashCost |-> NoNumber]) /\ ~RetireCostMetadataValid([kind |-> "Action",trashCost |-> NumberPart(TRUE,2)]) /\ RetireCostPart([trashCost |-> NumberPart(TRUE,0)],TRUE,0) = [exists |-> TRUE,amount |-> 0] /\ RetireCostPart([trashCost |-> NoNumber],TRUE,0) = [exists |-> FALSE,amount |-> 0] /\ RetireCostPart([trashCost |-> XNumber],TRUE,3).amount = 3 /\ RetireCostPart([trashCost |-> XNumber],FALSE,3).amount = 0 /\ RetireCostLayout.position = "SchemaAtom102" /\ RetireCostLayout.icon = "SchemaAtom169" StrengthExample(kind, generalDemand, part) == [kind |-> kind,printedBarrierResponseCard |-> generalDemand,strength |-> part] StrengthChecks == /\ StrengthMetadataValid(StrengthExample("Barrier",FALSE,NumberPart(TRUE,-1))) /\ StrengthMetadataValid(StrengthExample("Technique",TRUE,NumberPart(TRUE,0))) /\ StrengthMetadataValid(StrengthExample("Technique",FALSE,NoNumber)) /\ ~StrengthMetadataValid(StrengthExample("Technique",FALSE,NumberPart(TRUE,0))) /\ ~StrengthMetadataValid(StrengthExample("Technique",TRUE,NoNumber)) /\ StrengthPart(StrengthExample("Technique",FALSE,NoNumber),7) = [exists |-> FALSE,amount |-> 0] /\ StrengthPart(StrengthExample("Barrier",FALSE,XNumber),7) = [exists |-> TRUE,amount |-> 7] /\ StrengthLayout(StrengthExample("Technique",FALSE,NoNumber)).icon = "SchemaAtom052" /\ StrengthLayout(StrengthExample("Technique",TRUE,NumberPart(TRUE,0))).icon = "SchemaAtom095" /\ StrengthLayout(StrengthExample("Barrier",FALSE,NumberPart(TRUE,1))).position = "SchemaAtom027" /\ ~StrengthThresholdMet(2,3) /\ StrengthThresholdMet(3,3) /\ StrengthThresholdMet(-1,-2) CapacityPartChecks == /\ CapacityCostMetadataValid([kind |-> "Technique",capacityCost |-> NumberPart(TRUE,2)]) /\ CapacityCostMetadataValid([kind |-> "Technique",capacityCost |-> NumberPart(TRUE,0)]) /\ CapacityCostMetadataValid([kind |-> "Technique",capacityCost |-> NumberPart(TRUE,-1)]) /\ CapacityCostMetadataValid([kind |-> "Support",capacityCost |-> NoNumber]) /\ ~CapacityCostMetadataValid([kind |-> "Technique",capacityCost |-> NoNumber]) /\ ~CapacityCostMetadataValid([kind |-> "Equipment",capacityCost |-> NumberPart(TRUE,1)]) /\ CapacityCostPart([capacityCost |-> NumberPart(TRUE,2)],0) = [exists |-> TRUE,amount |-> 2] /\ CapacityCostPart([capacityCost |-> XNumber],3).amount = 3 /\ LET p == [kind |-> "Technique",playCost |-> NoNumber,deployCost |-> NumberPart(TRUE,3), activationCost |-> NoNumber,capacityCost |-> NumberPart(TRUE,2)] IN /\ ModifiedCost(CardResourceUnitCost(p,"Deploy",0,TRUE,0).amount,<<>>,<<3>>) = 0 /\ CapacityCostPart(p,0).amount = 2 /\ CapacityCostLayout.position = "SchemaAtom135" /\ CapacityCostLayout.icon = "SchemaAtom103" LinkChecks == /\ BaseLinkMetadataValid([kind |-> "Profile",side |-> "SideB",baseLink |-> NumberPart(TRUE,0)]) /\ BaseLinkMetadataValid([kind |-> "Profile",side |-> "SideB",baseLink |-> NumberPart(TRUE,-1)]) /\ BaseLinkMetadataValid([kind |-> "Profile",side |-> "SideA",baseLink |-> NoNumber]) /\ BaseLinkMetadataValid([kind |-> "Technique",side |-> "SideB",baseLink |-> NoNumber]) /\ ~BaseLinkMetadataValid([kind |-> "Profile",side |-> "SideB",baseLink |-> NoNumber]) /\ ~BaseLinkMetadataValid([kind |-> "Profile",side |-> "SideA",baseLink |-> NumberPart(TRUE,0)]) /\ BaseLinkPart([baseLink |-> XNumber],2).amount = 2 /\ LinkValue(1,[id \in {1,2} |-> IF id = 1 THEN 2 ELSE 1]) = 4 /\ LinkValue(0,[id \in {} |-> id]) = 0 /\ LinkValue(-1,[id \in {} |-> id]) = -1 /\ BaseLinkLayout.position = "SchemaAtom164" /\ BaseLinkLayout.icon = "Connection" StartingCapacityUnits(kind,side,part) == [kind |-> kind,side |-> side,startingCapacityUnits |-> part] StartingCapacityUnitsChecks == /\ StartingCapacityMetadataValid(StartingCapacityUnits("Profile","SideB",NoNumber)) /\ StartingCapacityMetadataValid(StartingCapacityUnits("Profile","SideB",NumberPart(TRUE,-1))) /\ StartingCapacityMetadataValid(StartingCapacityUnits("Profile","SideA",NoNumber)) /\ ~StartingCapacityMetadataValid(StartingCapacityUnits("Support","SideB",NumberPart(TRUE,1))) /\ ~StartingCapacityMetadataValid(StartingCapacityUnits("Profile","SideA",NumberPart(TRUE,4))) /\ ProfileStartingCapacity(StartingCapacityUnits("Profile","SideB",NoNumber),0) = [applicable |-> TRUE,amount |-> 4] /\ ProfileStartingCapacity(StartingCapacityUnits("Profile","SideB",NumberPart(TRUE,0)),0).amount = 0 /\ ProfileStartingCapacity(StartingCapacityUnits("Profile","SideB",NumberPart(TRUE,6)),0).amount = 6 /\ ProfileStartingCapacity(StartingCapacityUnits("Profile","SideB",NumberPart(TRUE,-1)),0).amount = -1 /\ ProfileStartingCapacity(StartingCapacityUnits("Profile","SideA",NoNumber),0) = [applicable |-> FALSE,amount |-> 0] /\ CapacityLimitWithBase(4,[id \in {1,2} |-> IF id = 1 THEN 2 ELSE -1]) = 5 /\ StartingCapacityLayout.position = "SchemaAtom164" /\ StartingCapacityLayout.icon = "SchemaAtom103" MinimumExample(kind, front, part) == [kind |-> kind,front |-> front,minDeckSize |-> part] MinimumChecks == /\ MinimumDeckMetadataValid(MinimumExample("Profile",TRUE,NumberPart(TRUE,45))) /\ MinimumDeckMetadataValid(MinimumExample("Profile",TRUE,NumberPart(TRUE,-1))) /\ MinimumDeckMetadataValid(MinimumExample("Profile",FALSE,NoNumber)) /\ MinimumDeckMetadataValid(MinimumExample("Technique",TRUE,NoNumber)) /\ ~MinimumDeckMetadataValid(MinimumExample("Profile",FALSE,NumberPart(TRUE,45))) /\ ~MinimumDeckMetadataValid(MinimumExample("Profile",TRUE,NoNumber)) /\ MinimumDeckLayout("SideA") = [position |-> "SchemaAtom101",box |-> "SchemaAtom175"] /\ MinimumDeckLayout("SideB") = [position |-> "SchemaAtom102",box |-> "SchemaAtom175"] /\ ~MinimumDeckSatisfied(<<1,2>>,3) /\ MinimumDeckSatisfied(<<1,2,3>>,3) /\ MinimumDeckSatisfied(<<>>, -1) /\ \A n \in 0..5, m \in -2..5 : MinimumDeckSatisfied([i \in 1..n |-> i],m) = (n >= StandardMinimumBound(m)) ImportCostLimitExample(front, part) == [kind |-> "Profile",front |-> front,importBudget |-> part] ImportCostLimitChecks == /\ ImportCostLimitMetadataValid(ImportCostLimitExample(TRUE,NumberPart(TRUE,15))) /\ ImportCostLimitMetadataValid(ImportCostLimitExample(TRUE,NumberPart(TRUE,0))) /\ ImportCostLimitMetadataValid(ImportCostLimitExample(TRUE,NumberPart(TRUE,-1))) /\ ImportCostLimitMetadataValid(ImportCostLimitExample(FALSE,NoNumber)) /\ ~ImportCostLimitMetadataValid(ImportCostLimitExample(FALSE,NumberPart(TRUE,15))) /\ ~ImportCostLimitMetadataValid(ImportCostLimitExample(TRUE,NoNumber)) /\ ~ImportCostLimitMetadataValid([kind |-> "Technique",front |-> TRUE,importBudget |-> NumberPart(TRUE,1)]) /\ ImportCostLimitPart(ImportCostLimitExample(TRUE,NumberPart(TRUE,-1)),0).amount = -1 /\ ImportCostWithinLimit(2,2) /\ ~ImportCostWithinLimit(2,1) /\ ImportCostWithinLimit(0,0) /\ ~ImportCostWithinLimit(0,-1) /\ ImportCostLimitLayout("SideA") = [position |-> "SchemaAtom101",box |-> "SchemaAtom100"] /\ ImportCostLimitLayout("SideB") = [position |-> "SchemaAtom102",box |-> "SchemaAtom100"] AffiliationChecks == LET sideA == [kind |-> "Profile",side |-> "SideA",affiliation |-> "SchemaAtom112"] sideB == [kind |-> "Profile",side |-> "SideB",affiliation |-> "SchemaAtom017"] neutral == [kind |-> "Facility",side |-> "SideA",affiliation |-> "Unaffiliated"] IN /\ SideAAffiliations2 = {"SchemaAtom083","SchemaAtom090","SchemaAtom112","SchemaAtom183"} /\ MajorSideBAffiliations2 = {"SchemaAtom015","GroupB","GroupA"} /\ MiniSideBAffiliations2 = {"SchemaAtom010","SchemaAtom017","SchemaAtom157"} /\ Cardinality(SchemaSymbol002) = 10 /\ "Unaffiliated" \notin SchemaSymbol002 /\ AffiliationMetadataValid(sideA) /\ AffiliationMetadataValid(sideB) /\ AffiliationMetadataValid(neutral) /\ StandardProfileAffiliationValid(sideA) /\ StandardProfileAffiliationValid(sideB) /\ ~AffiliationMetadataValid([sideA EXCEPT !.affiliation = "SchemaAtom015"]) /\ ~AffiliationMetadataValid([sideB EXCEPT !.affiliation = "SchemaAtom112"]) /\ ~AffiliationMetadataValid([sideA EXCEPT !.affiliation = "SchemaAtom172"]) /\ ~StandardProfileAffiliationValid([sideA EXCEPT !.affiliation = "Unaffiliated"]) /\ AffiliationMetadataValid([sideA EXCEPT !.affiliation = "Unaffiliated"]) /\ AffiliationGroup("SchemaAtom017") = "SchemaAtom107" /\ AffiliationGroup("GroupA") = "SchemaAtom104" /\ AffiliationGroup("SchemaAtom090") = "SideA" /\ AffiliationGroup("Unaffiliated") = "Unaffiliated" /\ AffiliationPresentation("Unaffiliated") = [background |-> "SchemaAtom184",cornerLogo |-> "NoValue",watermarkLogo |-> "NoValue"] /\ AffiliationPresentation("SchemaAtom112").cornerLogo = "SchemaAtom112" /\ AffiliationPresentation("SchemaAtom112").watermarkLogo = "SchemaAtom112" /\ Cardinality(AffiliationLogoCorners) = 4 ImportCostChecks == LET zero == [side |-> "SideA",affiliation |-> "SchemaAtom112",printedAlliance |-> FALSE, printedImportCost |-> NumberPart(TRUE,0), importCostSlots |-> <>] alliance == [zero EXCEPT !.printedAlliance = TRUE, !.printedImportCost = NumberPart(TRUE,2), !.importCostSlots = <>] none == [zero EXCEPT !.printedImportCost = NoNumber,!.importCostSlots = <<>>] full == [zero EXCEPT !.printedImportCost = NumberPart(TRUE,5), !.importCostSlots = <>] IN /\ ImportCostMetadataValid(zero) /\ ImportCostMetadataValid(none) /\ ImportCostMetadataValid(alliance) /\ ImportCostMetadataValid(full) /\ ~ImportCostMetadataValid([zero EXCEPT !.printedImportCost = NumberPart(TRUE,-1)]) /\ ~ImportCostMetadataValid([full EXCEPT !.printedImportCost = NumberPart(TRUE,6)]) /\ ~ImportCostMetadataValid([zero EXCEPT !.printedImportCost = XNumber]) /\ ~ImportCostMetadataValid([zero EXCEPT !.importCostSlots = <<>>]) /\ ~ImportCostMetadataValid([none EXCEPT !.importCostSlots = <>]) /\ ImportCostPartForContext(zero,"SchemaAtom053",FALSE) = [exists |-> TRUE,amount |-> 0] /\ ImportCostPartForContext(none,"SchemaAtom053",TRUE) = [exists |-> FALSE,amount |-> 0] /\ ImportCostPartForContext(alliance,"SchemaAtom053",TRUE).amount = 0 /\ ImportCostPartForContext(alliance,"SchemaAtom053",FALSE).amount = 2 /\ ImportCostPartForContext(alliance,"SchemaAtom076",TRUE).amount = 2 /\ ImportCostPartForContext(alliance,"SchemaAtom076",FALSE).amount = 2 /\ ImportCostPartForContext([alliance EXCEPT !.side = "SideB"],"SchemaAtom053",TRUE).amount = 2 /\ ImportCostPartForContext([alliance EXCEPT !.printedAlliance = FALSE],"SchemaAtom053",TRUE).amount = 2 /\ ImportCostPartForContext([none EXCEPT !.printedAlliance = TRUE],"SchemaAtom053",TRUE).exists = FALSE /\ ImportCostEligibleOutOfAffiliation(zero,[affiliation |-> "SchemaAtom090"]) /\ ~ImportCostEligibleOutOfAffiliation(none,[affiliation |-> "SchemaAtom090"]) /\ ImportCostEligibleOutOfAffiliation(none,[affiliation |-> "SchemaAtom112"]) /\ ~ImportCostEligibleOutOfAffiliation([none EXCEPT !.affiliation = "Unaffiliated"],[affiliation |-> "Unaffiliated"]) /\ ImportCostLegalityInput(ImportCostPartForContext(none,"SchemaAtom053",TRUE)) = [hasImportCost |-> FALSE,importCost |-> 0] /\ ImportCostBarLayout = [position |-> "SchemaAtom115",slots |-> 5,filledColor |-> "SchemaAtom026"] CardTypeChecks == LET data == [p |-> [kind |-> "Technique",side |-> "SideB"], a |-> [kind |-> "Facility",side |-> "SideA"]] technique == [card |-> "p",form |-> "Card",face |-> "Up", deployed |-> TRUE,active |-> TRUE] facility == [technique EXCEPT !.card = "a",!.face = "Down",!.active = FALSE] counter == [technique EXCEPT !.form = "Counter"] IN /\ Cardinality(CardTypes2) = 10 /\ CardTypes2 = SetupSideAKinds \cup SetupSideBKinds /\ \A kind \in SetupSideAKinds : CardTypeMetadataValid([kind |-> kind,side |-> "SideA"]) /\ \A kind \in SetupSideBKinds : CardTypeMetadataValid([kind |-> kind,side |-> "SideB"]) /\ ~CardTypeMetadataValid([kind |-> "ResourceUnit",side |-> "SideA"]) /\ ~CardTypeMetadataValid([kind |-> "Barrier",side |-> "SideB"]) /\ CardTypesForView(technique,data,FALSE) = {"Technique"} /\ CardTypesForView([technique EXCEPT !.active = FALSE],data,FALSE) = {"Technique"} /\ CardTypesForView(facility,data,FALSE) = {"Facility"} /\ CardTypesForView([technique EXCEPT !.face = "Down"],data,FALSE) = {} /\ CardTypesForView([technique EXCEPT !.face = "Down",!.deployed = FALSE],data,FALSE) = {"Technique"} /\ CardTypesForView(facility,data,TRUE) = {"Objective"} /\ CardTypesForView([technique EXCEPT !.deployed = FALSE,!.active = FALSE],data,TRUE) = {"Objective"} /\ CardTypesForView(counter,data,FALSE) = {} /\ CardTypesForView(counter,data,TRUE) = {} /\ CardTypeLayout("Barrier") = [position |-> "SchemaAtom096",rotationDegrees |-> 90, bold |-> TRUE,order |-> "SchemaAtom071"] /\ \A kind \in CardTypes2 \ {"Barrier"} : CardTypeLayout(kind).position = "SchemaAtom031" /\ CardTypeLayout(kind).rotationDegrees = 0 /\ CardTypeLayout(kind).bold SubtypeChecks == LET empty == [t \in {} |-> 0] sentry == PrintedSubtypeCounts({"Sentry"}) one == [Sentry |-> 1] two == [Sentry |-> 2] data == [p |-> [kind |-> "Technique",side |-> "SideB", printedSubtypes |-> {"SchemaAtom086","SchemaAtom073"}], a |-> [kind |-> "Facility",side |-> "SideA",printedSubtypes |-> {"SchemaAtom014"}]] technique == [card |-> "p",form |-> "Card",deployed |-> TRUE,face |-> "Up",active |-> TRUE] facility == [technique EXCEPT !.card = "a",!.face = "Down",!.active = FALSE] IN /\ [k \in CardTypes2 |-> Cardinality(SubtypesByPrintedType[k])] = [Profile |-> 15,Objective |-> 13,Facility |-> 25,Barrier |-> 21,Plan |-> 14, Attachment |-> 22,Action |-> 11,Equipment |-> 11,Technique |-> 14,Support |-> 17] /\ \A k \in CardTypes2 : SubtypesByPrintedType[k] \subseteq Subtypes2 /\ {"SchemaAtom030","SchemaAtom124","SchemaAtom143","SchemaAtom097"} \subseteq Subtypes2 /\ "SchemaAtom087" \notin Subtypes2 /\ PrintedSubtypeMetadataValid([kind |-> "Technique",printedSubtypes |-> {"SchemaAtom086","SchemaAtom073"}]) /\ PrintedSubtypeMetadataValid([kind |-> "Technique",printedSubtypes |-> {}]) /\ ~PrintedSubtypeMetadataValid([kind |-> "Technique",printedSubtypes |-> {"SchemaSymbol001"}]) /\ SubtypeFlagsConsistent([printedSubtypes |-> {"SchemaAtom086"},printedBarrierResponseCard |-> TRUE,printedAlliance |-> FALSE]) /\ ~SubtypeFlagsConsistent([printedSubtypes |-> {"SchemaAtom086"},printedBarrierResponseCard |-> FALSE,printedAlliance |-> FALSE]) /\ SubtypeFlagsConsistent([printedSubtypes |-> {"SchemaAtom013"},printedBarrierResponseCard |-> FALSE,printedAlliance |-> TRUE]) /\ ~SubtypeFlagsConsistent([printedSubtypes |-> {"SchemaAtom013"},printedBarrierResponseCard |-> FALSE,printedAlliance |-> FALSE]) /\ {t \in Subtypes2 : IntrinsicSubtypeRule(t) # "NoValue"} = {"SchemaAtom130","SchemaAtom045","SchemaAtom086"} /\ IntrinsicSubtypeRule("SchemaAtom130") = "SchemaAtom001" /\ IntrinsicSubtypeRule("SchemaAtom045") = "SchemaAtom002" /\ IntrinsicSubtypeRule("SchemaAtom086") = "SchemaAtom003" /\ SubtypeReference("SchemaAtom180",TRUE) = {"SchemaAtom180"} /\ SubtypeReference("SchemaAtom180",FALSE) = {} /\ SubtypeReference("SchemaAtom172",TRUE) = {} /\ SingleSubtypeChoiceAllowed(<<"SchemaSymbol001">>,"SchemaAtom016") /\ SingleSubtypeChoiceAllowed(<<"SchemaSymbol001">>,"Barrier") /\ ~SingleSubtypeChoiceAllowed(<<"SchemaSymbol001">>,"Technique") /\ ~SingleSubtypeChoiceAllowed(<<>>,"SchemaAtom016") /\ ~SingleSubtypeChoiceAllowed(<<"SchemaAtom180","SchemaAtom180">>,"SchemaAtom016") /\ ~SingleSubtypeChoiceAllowed(<<"SchemaAtom172">>,"SchemaAtom016") /\ SubtypeCountsValid(empty) /\ SubtypeCountsValid(two) /\ ~SubtypeCountsValid([Sentry |-> -1]) /\ IncrementSubtypeCount(one,"Sentry") = two /\ SubtypeCount(IncrementSubtypeCount(one,"SchemaSymbol001"),"Sentry") = 1 /\ SubtypeCount(IncrementSubtypeCount(empty,"SchemaSymbol001"),"SchemaSymbol001") = 1 /\ EffectiveSubtypes(sentry,one,one) = {"Sentry"} /\ EffectiveSubtypes(sentry,empty,one) = {} /\ EffectiveSubtypes(sentry,empty,two) = {} /\ EffectiveSubtypes(sentry,one,two) = {} /\ EffectiveSubtypes(sentry,two,two) = {"Sentry"} /\ \A b,g,l \in 0..3 : ("Sentry" \in EffectiveSubtypes([Sentry |-> b],[Sentry |-> g],[Sentry |-> l])) = (b+g > l) /\ CardSubtypesForView(technique,data,FALSE,empty,[SchemaSymbol001 |-> 1],empty) = {"SchemaAtom086","SchemaAtom073","SchemaSymbol001"} /\ CardSubtypesForView([technique EXCEPT !.active = FALSE],data,FALSE,empty,empty,empty) = {"SchemaAtom086","SchemaAtom073"} /\ CardSubtypesForView(facility,data,FALSE,empty,empty,empty) = {"SchemaAtom014"} /\ CardSubtypesForView([technique EXCEPT !.face = "Down"],data,FALSE,empty,empty,empty) = {} /\ CardSubtypesForView([technique EXCEPT !.face = "Down",!.deployed = FALSE],data,FALSE,empty,empty,empty) = {"SchemaAtom086","SchemaAtom073"} /\ CardSubtypesForView([technique EXCEPT !.form = "Counter"],data,FALSE,empty,empty,empty) = {} /\ CardSubtypesForView(facility,data,TRUE,empty,empty,empty) = {} /\ CardSubtypesForView(facility,data,TRUE,[Research |-> 1],empty,empty) = {"Research"} /\ CardWithoutSubtype(technique,{"SchemaAtom086","SchemaAtom073"},"SchemaAtom180") /\ ~CardWithoutSubtype(technique,{"SchemaAtom180","SchemaAtom073"},"SchemaAtom180") /\ ~CardWithoutSubtype([technique EXCEPT !.form = "Counter"],{},"SchemaAtom180") /\ SubtypeLayout.order = "SchemaAtom012" TextBoxChecks == LET ast1 == <<[tag |-> "SubtypeReference",token |-> "SchemaAtom180",bold |-> TRUE]>> ast2 == <<[tag |-> "SchemaAtom008",token |-> "SchemaAtom187",bold |-> FALSE]>> rules1 == TextSegment("SchemaAtom137","SchemaAtom185",FALSE,FALSE,ast1) rules2 == TextSegment("SchemaAtom137","SchemaAtom141",FALSE,FALSE,ast2) flavor == TextSegment("SchemaAtom072","SchemaAtom004",TRUE,FALSE,<<>>) reminder == TextSegment("SchemaAtom131","SchemaAtom005",TRUE,TRUE,<<>>) segments == <> IN /\ TextBoxMetadataValid(segments) /\ TextBoxMetadataValid(<<>>) /\ TextSegmentValid([rules1 EXCEPT !.italic = TRUE]) /\ ~TextSegmentValid([reminder EXCEPT !.parenthesized = FALSE]) /\ ~TextSegmentValid([flavor EXCEPT !.italic = FALSE]) /\ ~TextSegmentValid([flavor EXCEPT !.rulesAst = ast1]) /\ ~TextBoxMetadataValid(<>) /\ RulesTextProjection(segments) = <> /\ GameplayTextProjection(segments) = <> /\ GameplayTextProjection(<>) = <<>> /\ TextDirectlyReferenceable(rules1) /\ ~TextDirectlyReferenceable(flavor) /\ ~TextDirectlyReferenceable(reminder) /\ \A f \in {"SchemaAtom151","SchemaAtom152","SchemaAtom075"}, r \in {"SchemaAtom155","SchemaAtom156","SchemaAtom180"} : GameplayTextProjection(<>) = <> /\ TextAbilityActive(TRUE,TRUE,FALSE) /\ ~TextAbilityActive(TRUE,FALSE,FALSE) /\ TextAbilityActive(TRUE,FALSE,TRUE) /\ ~TextAbilityActive(FALSE,TRUE,TRUE) /\ ~TextAbilityActive(FALSE,FALSE,TRUE) /\ TextBoxLayout.position = "SchemaAtom033" TargetSiteIndicatorChecks == LET first == [triggerTargetSite |-> "SchemaAtom082"] rules == TextSegment("SchemaAtom137","SchemaAtom158",FALSE,FALSE,<>) back == [kind |-> "Profile",side |-> "SideA",profileFamily |-> "SelectableProfile", front |-> FALSE,targetSiteIndicator |-> "SchemaAtom120", title |-> "SchemaAtom111",subtitle |-> "SchemaAtom176", canonicalTitle |-> "SchemaAtom111",canonicalSubtitle |-> "SchemaAtom176", pronouns |-> "",textSegments |-> <>] front == [back EXCEPT !.front = TRUE,!.targetSiteIndicator = "NoValue"] other == [front EXCEPT !.profileFamily = "Other"] IN /\ TargetSiteIndicatorMetadataValid(back) /\ TargetSiteIndicatorMetadataValid(front) /\ TargetSiteIndicatorMetadataValid(other) /\ \A icon \in TargetSiteIndicatorIcons2 : TargetSiteIndicatorMetadataValid([back EXCEPT !.targetSiteIndicator = icon]) /\ ~TargetSiteIndicatorMetadataValid([back EXCEPT !.targetSiteIndicator = "NoValue"]) /\ ~TargetSiteIndicatorMetadataValid([front EXCEPT !.targetSiteIndicator = "SchemaAtom042"]) /\ ~TargetSiteIndicatorMetadataValid([other EXCEPT !.targetSiteIndicator = "SchemaAtom042"]) /\ ~TargetSiteIndicatorMetadataValid([back EXCEPT !.side = "SideB"]) /\ IndicatorTargetSiteHint("SchemaAtom120") = "SchemaAtom082" /\ IndicatorTargetSiteHint("SchemaAtom093") = "SchemaAtom129" /\ IndicatorTargetSiteHint("SchemaAtom042") = "SchemaAtom018" /\ IndicatorMatchesFirstAbility(back,first) /\ ~IndicatorMatchesFirstAbility([back EXCEPT !.targetSiteIndicator = "SchemaAtom042"],first) /\ IndicatorMatchesFirstAbility(front,first) /\ FirstAbilityCentralTargetSite(first) = "SchemaAtom082" /\ \A icon \in TargetSiteIndicatorIcons2 : CardRulesAstProjection([back EXCEPT !.targetSiteIndicator = icon]) = CardRulesAstProjection(back) /\ CanonicalName(back) # CanonicalName([back EXCEPT !.canonicalSubtitle = "SchemaAtom177"]) /\ TargetSiteIndicatorLayout = [position |-> "SchemaAtom116",purpose |-> "SchemaAtom181"] Block2Assertions == CASE block2 = 1 -> NameChecks [] block2 = 2 -> UniqueChecks [] block2 = 3 -> CostChecks [] block2 = 4 -> ProgressChecks [] block2 = 5 -> PointChecks [] block2 = 6 -> RetireCostChecks [] block2 = 7 -> StrengthChecks [] block2 = 8 -> CapacityPartChecks [] block2 = 9 -> LinkChecks [] block2 = 10 -> StartingCapacityUnitsChecks [] block2 = 11 -> MinimumChecks [] block2 = 12 -> ImportCostLimitChecks [] block2 = 13 -> AffiliationChecks [] block2 = 14 -> ImportCostChecks [] block2 = 15 -> CardTypeChecks [] block2 = 16 -> SubtypeChecks [] block2 = 17 -> TextBoxChecks [] block2 = 18 -> TargetSiteIndicatorChecks =============================================================================