合金 - 自反传递闭包包括外来元素答案

【问题标题】：Alloy - reflexive-transitive closure includes foreign elements合金 - 自反传递闭包包括外来元素
【发布时间】：2014-12-12 19:08:19
【问题描述】：

所以我有这个mwe：

abstract sig S { r: set S }
one sig A, B extends S {}
one sig C  { }
run { r = A->B and A->A + B->B + A->B = *r }

我希望自反传递闭包是A->A + B->B + A->B，这将是传递和自反的最小封闭关系，包含它定义的域中的所有元素 (S = A+B)。然而，事实并非如此。

在语言参考中它说

关系的自反-传递闭包是传递和自反的最小封闭关系（即包括恒等关系）。

然而，括号中的加法似乎是字面意思，意思是C->C 在关系的自反传递闭包中，为S->S 定义。我想知道为什么会这样......因为它在技术上不在数学中定义的“真正的”自反传递闭包中。

*r = ^r + iden & S->S 不是更好吗？特别是，因为C->C in *r 会引发警告。我认为这表明*r 确实意味着 限于S->S，但不实际上 限于S->S。

【问题讨论】：

标签： alloy

【解决方案1】：

是的，这是关于 Alloy 的 * 运算符的一件事，有时令人惊讶。 Jackson 在 Software Abstractions 的第 3.4.3.5 节之后的问题中讨论了它（修订版中的第 65-66 页）。那里提供的解释是：

虽然这看起来很奇怪，但它自然地遵循自反传递闭包和身份关系的定义。另一种方法是让集合与每个关系隐式关联，这些关系代表其域和范围的可能成员，这会使逻辑复杂化。

他接着指出，这在实践中很少出现问题，因为在导航表达式中使用传递闭包时，不相关的元组将在连接中消失，而当不相关时，编写 S <: *r 也会过滤掉非 S 元组。我的经验，例如，证实了杰克逊的说法：我记得这一点，因为它让我非常惊讶，有一次我在实践中遇到了这个问题。八年一次（诚然，我并没有把所有时间都花在编写合金模型上）似乎是一个相当温和的发生率。（翻译：是的，这很令人惊讶。但你可以学会忍受它。我保证。）

我推断C->C in *r 上的警告并不表明* 旨在排除不相关的三元组；这可能是承认（如 3.4.3.5 中的讨论）许多用户对在关系的传递闭包中发现意外配对感到有点吃惊。

我希望这会有所帮助。

【讨论】：

我明白了。我没有真正的书，只有语言参考。这对我来说似乎是一个反复出现的主题。

【解决方案2】：

为 CMS 的好答案加一分...

你问

*r = ^r + iden & S->S 不是更好吗？

但这不是一个选择——至少不是很明显。原因是我们不知道 S 是什么，所以要么需要推断它（这可能会产生一些奇怪的情况），要么需要明确给出。

【讨论】：