Search code examples
alloy

Find the number of subclass instances in Alloy model

I have to make a simple model of the Olympics on Alloy, but I am struggling to understand how to constrain the number of subclass instances in the model.

sig Medal {}

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

sig Event {
    medals: set Medal
}

Now I want to make a fact that constrains the number of each type of medal for the following cases:

  • Case 1: 1 Gold medal, 1 Silver medal, >=1 Bronze medal
  • Case 2: 1 Gold medal, >=2 Silver medal, no Bronze medal
  • Case 3: >=3 Gold medal, no Silver, no Bronze

So far, I know how to enforce the case where we have exactly one medal of each type, as follows:

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 }

This gives the expected model as follows:

enter image description here

However I do not know how to find the number of subclass instances in the e.medals set. I want something like the following:

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

  • You can take the intersection of medals and the sub-type. I.e. 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¹│    │
└──────────┴────────────┴────┘