如何指定一个集合的所有成员在合金中是唯一的？

Question

我有一个合金模型。本着一个小型复制示例的精神，我提取了以下内容：

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

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

check keywordsAreUniqueForDocument for 5

我想要实现的是与特定文档相关联的一组关键字应该是唯一的。但这立即向我展示了一个微不足道的反例。

如何指定集合中不应有重复的元素？

Answer 1

document.keyword 是一个集合，根据集合的定义，它只是唯一的元素。你得到了一个反例k = k'。如果你改为写 all disj k, k' : Document.keyword | k != k'，它会很容易通过。

如果您希望没有两个文档共享关键字，那就是all disj d, d': Document | no d.keywork & d'.keyword。