Search code examples
alloy

How Can I Specify All Members of a Set Are Unique in Alloy?

I have an alloy model. In the spirit of a small reproduction example, I've extracted the following:

sig SearchTerm {}
sig Document{
    keyword: set SearchTerm
}

assert keywordsAreUniqueForDocument {
    all k, k' : Document.keyword | k != k'
}

check keywordsAreUniqueForDocument for 5

What I'm trying to achieve is that the set of keywords associated with a particular document should be unique. But this is immediately showing me a trivial counterexample.

How can I specify that there should be no duplicated elements in a set?

Solution

  • document.keyword is a set and, by the set definition, is only unique elements. You're getting a counterexample where k = k'. If you instead write all disj k, k' : Document.keyword | k != k', it will trivially pass.

    If you instead intended that no two documents share keywords, that'd be all disj d, d': Document | no d.keywork & d'.keyword.