如何在Alloy奥运奖牌模型中约束子类实例数量？

Got it, let's work through adding the required constraints to your Alloy model. Your base sig definitions are already solid—we just need to add a fact that enforces the two mutually exclusive medal scenarios you outlined.

Complete Alloy Code #

Here's the full model with the constraint fact included:

sig Medal {}
sig GoldMedal extends Medal {}
sig SilverMedal extends Medal {}
sig BronzeMedal extends Medal {}
sig Event { medals: set Medal }

fact MedalConstraints {
    // Scenario 1: Exactly 1 gold, 1 silver, and at least 1 bronze
    (one GoldMedal and one SilverMedal and some BronzeMedal)
    // Scenario 2: Exactly 1 gold, at least 2 silvers, and no bronzes
    or (one GoldMedal and #SilverMedal >= 2 and no BronzeMedal)
}

Breakdown of the Constraint Fact #

Let's break down what each part does to make it clear:

• one GoldMedal: Both scenarios require exactly 1 gold medal. While we included this in both branches for clarity, you could also pull it outside the or (like one GoldMedal and (...) or (...)) to avoid repetition—it works either way.
• Scenario 1 specifics:
  • one SilverMedal: Enforces exactly 1 silver medal instance.
  • some BronzeMedal: Ensures there's at least 1 bronze medal (this is Alloy shorthand for #BronzeMedal >= 1).
• Scenario 2 specifics:
  • #SilverMedal >= 2: Requires 2 or more silver medal instances.
  • no BronzeMedal: Guarantees there are zero bronze medal instances (equivalent to #BronzeMedal = 0).
• The or operator ensures the model will only satisfy one of the two scenarios—they're mutually exclusive, which makes sense for your use case.

Testing Each Scenario #

To verify the constraints work as expected, you can use dedicated run commands for each scenario:

Test Scenario 1 #

run VerifyScenario1 for 5 Medal, 1 Event {
    one GoldMedal and one SilverMedal and some BronzeMedal
}

This will generate instances that match your first scenario (1 gold, 1 silver, 1+ bronze).

Test Scenario 2 #

run VerifyScenario2 for 5 Medal, 1 Event {
    one GoldMedal and #SilverMedal >= 2 and no BronzeMedal
}

This will generate instances for your second scenario (1 gold, 2+ silver, 0 bronze).

内容的提问来源于stack exchange，提问作者Sonja Brits