查找合金模型中子类实例的数量

Question

我必须在 Alloy 上制作一个简单的奥运会模型，但我很难理解如何限制模型中子类实例的数量。

sig Medal {}

sig GoldMedal extends Medal {}
sig SilverMedal extends Medal {}
sig BronzeMedal extends Medal {}

sig Event {
    medals: set Medal
}

现在我想为以下情况做一个限制每种奖牌数量的事实：

• 案例 1：1 枚金牌，1 枚银牌，>=1 枚铜牌
• 案例 2：1 枚金牌，>=2 枚银牌，没有铜牌
• 案例 3：>=3 金牌，没有银牌，没有铜牌

到目前为止，我知道如何执行每种类型只有一个奖章的情况，如下所示：

fact oneOfEachMedal{ all e:Event | one g:GoldMedal | one s:SilverMedal | one b:BronzeMedal | g in e.medals and s in e.medals and b in e.medals }

这给出了预期的模型如下：

但是我不知道如何在e.medals 集合中找到子类实例的数量。我想要以下内容：

fact caseOne {all e:Event | #(GoldMedal in e.medals) = 1 and #(SilverMedal in e.medals) = 1 and #(BronzeMedal in e.medals >=2 }

Answer 1

你可以取medals和子类型的交集。 IE。 no (GoldMedal & medals).

sig Medal {}

sig GoldMedal extends Medal {}
sig SilverMedal extends Medal {}
sig BronzeMedal extends Medal {}

sig Event {
    medals  : set Medal,
    case    : Int
} {

    case > 0
    case <= 3

    case=1 => {
        // Gold medal, 1 Silver medal, >=1 Bronze medal
        one (GoldMedal & medals )
        one (SilverMedal & medals )
        some (BronzeMedal & medals )
    } else case =2  => {
        // 1 Gold medal, >=2 Silver medal, no Bronze medal
        one (GoldMedal & medals )
        # (SilverMedal & medals ) >= 2
        no (BronzeMedal & medals )
    } else case = 3 => {
        // >=3 Gold medal, no Silver, no Bronze
        # (GoldMedal & medals ) >= 3
        no (SilverMedal & medals )
        no (BronzeMedal & medals )
    }
}

run { Event.case = 1+2+3} for 10


┌──────────┬────────────┬────┐
│this/Event│medals      │case│
├──────────┼────────────┼────┤
│Event⁰    │GoldMedal⁰  │3   │
│          ├────────────┼────┤
│          │GoldMedal¹  │    │
│          ├────────────┤    │
│          │GoldMedal²  │    │
│          ├────────────┤    │
│          │Medal¹      │    │
├──────────┼────────────┼────┤
│Event¹    │GoldMedal¹  │2   │
│          ├────────────┼────┤
│          │SilverMedal⁰│    │
│          ├────────────┤    │
│          │SilverMedal¹│    │
├──────────┼────────────┼────┤
│Event²    │BronzeMedal⁰│1   │
│          ├────────────┼────┤
│          │GoldMedal⁰  │    │
│          ├────────────┤    │
│          │SilverMedal¹│    │
└──────────┴────────────┴────┘