合金中两个签名的不相交并集

Question

我已经询问了关于 Alloy here 中的笛卡尔积和不相交联合。在那里，我将集合视为一元定义的谓词。

如果我想将 Alloy 中的两个简单签名不相交怎么办。

假设我有以下签名：

sig A {}
sig B {}

我想定义从 A 到 B Û B 的关系，其中我使用 Û 表示 disjoint union。这可以直接用合金制成吗？

Answer 1

我可以想到两种方法。 （但我意识到，重新阅读您的问题，我不知道您的最后一段是什么意思。所以也许这与您的目标无关。）

首先：不相交的联合使用标志标记每个成员，以便您知道它来自哪个父集，并且不相交的联合中的任何元素都不在两个父集中。如果练习的目的是确保您知道不相交并集的每个成员来自哪个父集，并确保不相交并集的任何成员都来自多个父集，那么在这种情况下，正常并集似乎做你需要的。在您的示例中，签名 A 和 B 已经不相交，并且始终可以判断给定原子是在 A 中还是在 B 中。所以第一种方法就是使用表达式 A + B。

第二：如果A + B 不这样做，由于问题中没有给出的原因，并且你真的很想要一组对，那么定义那组对。在每一对中，第一个元素来自 A，第二个元素是 1（或其他标志），或者第一个元素来自 B，第二个元素是 2（或其他标志）。

一种写法是：

{v : X + Y, n : Int | (v in X and n = 1) or (v in Y and n = 2) }

另一种等效的方法是：

{x : X, y : Int | y = 1}
+
{x : Y, y : Int | y = 2}

第三种方法更简单：

{v : X, n : 1} + {v : Y, n : 2}

而且更简单：

(X -> 1) + (Y -> 2) 

像任何表达式一样，这可以封装在一个函数中：

fun du[Left, Right : set univ] : (Left + Right) -> Int {
  (Left -> 1) + (Right -> 2)
}

然后A和B的不相交并集可以写成du[A, B]。

我重复我的建议，花一些时间学习理解。