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?
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
.