首页 文章

合金中两个签名的不相交联合

提问于
浏览 次
1

我已经问过合金here中的笛卡尔积和不相交的联合 . 在那里，我认为集合是一元定义的谓词 .

如果我简单想要在Alloy中取消联合两个简单的签名，该怎么办？

假设我有以下签名：

sig A {}
sig B {}

我想定义从A到 B Û B 的关系，其中我使用 Û 作为disjoint union . 这可能直接用合金制成吗？

alloy

1 回答

  • 3

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

    第一：不相交联合用标志标记每个成员，以便您知道它来自哪个父集，并且不相交联合中的任何元素都不在父集中 . 如果练习的目的是确保你知道不相交联盟的每个成员来自哪个父集，并确保没有不相交联盟的成员来自多个父集，那么在这种情况下，正常联合似乎做你需要的 . 在您的示例中，签名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] .

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

    回复于

相关问题