集合并集的累积

Question

我有两个类 A 和 B 以及它们与类 R 的额外数据的关系。

所以，A 和 B 通过 R 相互关联。

sig A {}
sig B {}

sig R {
    a : A,
    b : B,
    data : Bool
}

这里，Bool 定义为：

sig Bool {}
sig True, False extends Bool {}

现在，我像这样扩展A：

sig A{
    allb : some B
}

其中包含B 的所有实例，其中A 和B 之间存在关系，并且数据类型为True。

我想将以下逻辑陈述表达为合金事实：

_{（来源：dropproxy.com）}

我在这里假设True == 1 和False != 1 以及集合A 和R 分别包含A 和R 的所有实例。

到目前为止，我尝试定义一个 fun trueR(a : A)，它应该返回所有 R 的 R.a = a and r.data = True 和一个 fact allbIsRTrue，它声明每个 A allb 应该是R.b 由 trueR 返回的总和。

但是，这就是我卡住的地方，我找不到正确的构造来对引用中的集合求和，并尝试使用 sum 导致语法错误。

如何将我的正式约束指定为合金事实？

Answer 1

我认为你想使用集合推导。在 Alloy 中，这是集合理解的语法

{x: X | f(x)}

上面的表达式计算为一组X，f(x) 对其成立。

在您的示例中，要表达allB 的事实，您可以编写类似

fact fAllB {
    all a: A | 
        a.allB = {b: B | 
            some r: R | r.ra = a and r.rb = b and r.data = True}
}

在英语中，这个事实读作“对于集合A 的所有a，a.allB 是所有B 的集合，因此存在一些r，它们“连接”那些确切的@987654331 @ 和 b，其中 r.data 是 True。

请注意我对模型其余部分所做的以下修改：

• 我制作了Bool sig 抽象，因为您可能不想要既不是True 也不是False 的布尔值

• 我制作了 True 和 False sigs 单例 sigs（即 one sig），因为您可能希望它们中的每一个都只有一个原子

• 我将关系 a 和 b 重命名为 ra 和 rb 以避免名称别名和潜在的混淆

这是我用于此示例的模型的其余部分

abstract sig Bool {}
one sig True, False extends Bool {}

sig A {
  allB: set B
} 
sig B {}
sig R {
  ra : A,
  rb : B,
  data : Bool
}