在 Alloy 模型中查找子类实例的数量

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和sub-type的交集。 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¹│    │
└──────────┴────────────┴────┘

在 Alloy 模型中查找子类实例的数量

Find the number of subclass instances in Alloy model

alloy