The many uses of `disj`

Alloy 6
1

So we know that disj can used in quantifiers:

all disj x, y: Key |
   no x.lock & y.lock

But did you know you can add it to fields?

sig Key {
  lock: disj some Lock
}

This means the same as the above predicate. If lock was a var, this would hold true in every state, too.

More niche is that you can put the disj before the field name:

sig Lock {}
sig Key {
  , disj lock, lock2: one Lock 
}

Now lock and lock2 will be disjoint for each key.

Finally, you can use disj as a predicate:

all disj x, y, z, w: Key |
   disj[x.lock, y.lock, z.lock, w.lock]

disj takes any number of parameters.

3 Likes