r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

SchemaChecksMC¶

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.

This model/fact module also contains 31 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

AffiliationChecks · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AffiliationGroup, AffiliationLogoCorners, AffiliationMetadataValid, AffiliationPresentation, MajorSideBAffiliations2, MiniSideBAffiliations2, SchemaSymbol002, SideAAffiliations2, StandardProfileAffiliationValid

BarrierCost · operator

reference-profile · input revision 2 · CC0 1.0

BarrierCost == CostExample("Barrier",NoNumber,NoNumber,NumberPart(TRUE,3))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CostExample, NoNumber, NumberPart

Block2Assertions · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AffiliationChecks, CapacityPartChecks, CardTypeChecks, CostChecks, ImportCostChecks, ImportCostLimitChecks, LinkChecks, MinimumChecks, NameChecks, PointChecks, ProgressChecks, RetireCostChecks, StartingCapacityUnitsChecks, StrengthChecks, SubtypeChecks, TargetSiteIndicatorChecks, TextBoxChecks, UniqueChecks, block2

CapacityPartChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ModifiedCost, CapacityCostLayout, CapacityCostMetadataValid, CapacityCostPart, CardResourceUnitCost, NoNumber, NumberPart, XNumber

CardTypeChecks · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardTypeLayout, CardTypeMetadataValid, CardTypes2, CardTypesForView, SetupSideAKinds, SetupSideBKinds

CostChecks · operator

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ModifiedCost, BarrierCost, CostExample, EventCost, FacilityCost, TechniqueCost, CardResourceUnitCost, CostPartLayout, NoNumber, NumberPart, NumberPartValid, PrintedCostMetadataValid, PrintedCostPart, XNumber

CostExample · operator

reference-profile · input revision 2 · CC0 1.0

CostExample(kind, play, deploy, activation) ==
    [kind |-> kind,playCost |-> play,deployCost |-> deploy,activationCost |-> activation]

Exact module download · Source bundle and reproduction instructions

EventCost · operator

reference-profile · input revision 2 · CC0 1.0

EventCost == CostExample("Action",NumberPart(TRUE,5),NoNumber,NoNumber)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CostExample, NoNumber, NumberPart

ExampleNames · operator

reference-profile · input revision 2 · CC0 1.0

ExampleNames == [id \in 1..4 |-> IF id \in {1,2} THEN CanonicalName(NameCard)
                    ELSE IF id = 3 THEN CanonicalName(NameTechnique) ELSE <<"Other">>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NameCard, NameTechnique, CanonicalName

FacilityCost · operator

reference-profile · input revision 2 · CC0 1.0

FacilityCost == CostExample("Facility",NoNumber,NoNumber,NumberPart(TRUE,0))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CostExample, NoNumber, NumberPart

ImportCostChecks · operator

reference-profile · input revision 2 · CC0 1.0

ImportCostChecks ==
    LET zero == [side |-> "SideA",affiliation |-> "SchemaAtom112",printedAlliance |-> FALSE,
                 printedImportCost |-> NumberPart(TRUE,0),
                 importCostSlots |-> <<FALSE,FALSE,FALSE,FALSE,FALSE>>]
        alliance == [zero EXCEPT !.printedAlliance = TRUE,
                     !.printedImportCost = NumberPart(TRUE,2),
                     !.importCostSlots = <<TRUE,FALSE,TRUE,FALSE,FALSE>>]
        none == [zero EXCEPT !.printedImportCost = NoNumber,!.importCostSlots = <<>>]
        full == [zero EXCEPT !.printedImportCost = NumberPart(TRUE,5),
                 !.importCostSlots = <<TRUE,TRUE,TRUE,TRUE,TRUE>>]
    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 = <<FALSE,FALSE,FALSE,FALSE,FALSE>>])
       /\ 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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ImportCostBarLayout, ImportCostEligibleOutOfAffiliation, ImportCostLegalityInput, ImportCostMetadataValid, ImportCostPartForContext, NoNumber, NumberPart, XNumber

ImportCostLimitChecks · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ImportCostLimitExample, ImportCostLimitLayout, ImportCostLimitMetadataValid, ImportCostLimitPart, ImportCostWithinLimit, NoNumber, NumberPart

ImportCostLimitExample · operator

reference-profile · input revision 2 · CC0 1.0

ImportCostLimitExample(front, part) == [kind |-> "Profile",front |-> front,importBudget |-> part]

Exact module download · Source bundle and reproduction instructions

Init2 · operator

reference-profile · input revision 2 · CC0 1.0

Init2 == block2 \in 1..18

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block2

LinkChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BaseLinkLayout, BaseLinkMetadataValid, BaseLinkPart, LinkValue, NoNumber, NumberPart, XNumber

MinimumChecks · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimumExample, MinimumDeckLayout, MinimumDeckMetadataValid, MinimumDeckSatisfied, NoNumber, NumberPart, StandardMinimumBound

MinimumExample · operator

reference-profile · input revision 2 · CC0 1.0

MinimumExample(kind, front, part) == [kind |-> kind,front |-> front,minDeckSize |-> part]

Exact module download · Source bundle and reproduction instructions

NameCard · operator

reference-profile · input revision 2 · CC0 1.0

NameCard == [kind |-> "Profile",title |-> "SchemaAtom123",subtitle |-> "SchemaAtom070",
             canonicalTitle |-> "SchemaAtom123",canonicalSubtitle |-> "SchemaAtom070",pronouns |-> "SchemaAtom189"]

Exact module download · Source bundle and reproduction instructions

NameChecks · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExampleNames, NameCard, NameTechnique, CanonicalName, CopiesOfName, DifferentCanonicalNames, NameMetadataValid, NameParts, NamePlacement, NameReference

NameTechnique · operator

reference-profile · input revision 2 · CC0 1.0

NameTechnique == [kind |-> "Technique",title |-> "SchemaAtom122",subtitle |-> "",
                canonicalTitle |-> "SchemaAtom162",canonicalSubtitle |-> "",pronouns |-> ""]

Exact module download · Source bundle and reproduction instructions

Next2 · operator

reference-profile · input revision 2 · CC0 1.0

Next2 == UNCHANGED block2

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: block2

PointChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoNumber, NumberPart, ObjectivePlacement, ObjectivePointLayout, ObjectivePointsMetadataValid, ObjectivePointsPart

ProgressChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProgressExample, NoNumber, NumberPart, ProgressLayout, ProgressMetadataValid, ProgressPart, ProgressThresholdMet, ResolvedNumberPart, XNumber

ProgressExample · operator

reference-profile · input revision 2 · CC0 1.0

ProgressExample == [kind |-> "Objective",progressRequirement |-> NumberPart(TRUE,3)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NumberPart

RetireCostChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoNumber, NumberPart, RetireCostLayout, RetireCostMetadataValid, RetireCostPart, XNumber

Spec2 · operator

reference-profile · input revision 2 · CC0 1.0

Spec2 == Init2 /\ [][Next2]_block2

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Init2, Next2, block2

StartingCapacityUnits · operator

reference-profile · input revision 2 · CC0 1.0

StartingCapacityUnits(kind,side,part) == [kind |-> kind,side |-> side,startingCapacityUnits |-> part]

Exact module download · Source bundle and reproduction instructions

StartingCapacityUnitsChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StartingCapacityUnits, CapacityLimitWithBase, NoNumber, NumberPart, ProfileStartingCapacity, StartingCapacityLayout, StartingCapacityMetadataValid

StrengthChecks · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: StrengthExample, NoNumber, NumberPart, StrengthLayout, StrengthMetadataValid, StrengthPart, StrengthThresholdMet, XNumber

StrengthExample · operator

reference-profile · input revision 2 · CC0 1.0

StrengthExample(kind, generalDemand, part) ==
    [kind |-> kind,printedBarrierResponseCard |-> generalDemand,strength |-> part]

Exact module download · Source bundle and reproduction instructions

SubtypeChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardSubtypesForView, CardTypes2, CardWithoutSubtype, EffectiveSubtypes, IncrementSubtypeCount, IntrinsicSubtypeRule, PrintedSubtypeCounts, PrintedSubtypeMetadataValid, SingleSubtypeChoiceAllowed, SubtypeCount, SubtypeCountsValid, SubtypeFlagsConsistent, SubtypeLayout, SubtypeReference, Subtypes2, SubtypesByPrintedType

TargetSiteIndicatorChecks · operator

reference-profile · input revision 2 · CC0 1.0

TargetSiteIndicatorChecks ==
    LET first == [triggerTargetSite |-> "SchemaAtom082"]
        rules == TextSegment("SchemaAtom137","SchemaAtom158",FALSE,FALSE,<<first>>)
        back == [kind |-> "Profile",side |-> "SideA",profileFamily |-> "SelectableProfile",
                 front |-> FALSE,targetSiteIndicator |-> "SchemaAtom120",
                 title |-> "SchemaAtom111",subtitle |-> "SchemaAtom176",
                 canonicalTitle |-> "SchemaAtom111",canonicalSubtitle |-> "SchemaAtom176",
                 pronouns |-> "",textSegments |-> <<rules>>]
        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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanonicalName, CardRulesAstProjection, FirstAbilityCentralTargetSite, IndicatorMatchesFirstAbility, IndicatorTargetSiteHint, TargetSiteIndicatorIcons2, TargetSiteIndicatorLayout, TargetSiteIndicatorMetadataValid, TextSegment

TechniqueCost · operator

reference-profile · input revision 2 · CC0 1.0

TechniqueCost == CostExample("Technique",NoNumber,NumberPart(TRUE,0),NoNumber)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CostExample, NoNumber, NumberPart

TextBoxChecks · operator

reference-profile · input revision 2 · CC0 1.0

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 == <<rules1,reminder,rules2,flavor>>
    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(<<flavor,rules1>>)
       /\ RulesTextProjection(segments) = <<rules1,rules2>>
       /\ GameplayTextProjection(segments) = <<ast1,ast2>>
       /\ GameplayTextProjection(<<flavor,reminder>>) = <<>>
       /\ TextDirectlyReferenceable(rules1)
       /\ ~TextDirectlyReferenceable(flavor)
       /\ ~TextDirectlyReferenceable(reminder)
       /\ \A f \in {"SchemaAtom151","SchemaAtom152","SchemaAtom075"},
             r \in {"SchemaAtom155","SchemaAtom156","SchemaAtom180"} :
            GameplayTextProjection(<<rules1,[reminder EXCEPT !.text = r],
                                     rules2,[flavor EXCEPT !.text = f]>>) = <<ast1,ast2>>
       /\ TextAbilityActive(TRUE,TRUE,FALSE)
       /\ ~TextAbilityActive(TRUE,FALSE,FALSE)
       /\ TextAbilityActive(TRUE,FALSE,TRUE)
       /\ ~TextAbilityActive(FALSE,TRUE,TRUE)
       /\ ~TextAbilityActive(FALSE,FALSE,TRUE)
       /\ TextBoxLayout.position = "SchemaAtom033"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: GameplayTextProjection, RulesTextProjection, TextAbilityActive, TextBoxLayout, TextBoxMetadataValid, TextDirectlyReferenceable, TextSegment, TextSegmentValid

UniqueChecks · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: UniqueMetadataValid, UniquePrefix, UniqueSymbolPlacement

block2 · variable

reference-profile · input revision 2 · CC0 1.0

block2

Exact module download · Source bundle and reproduction instructions