1

我有两个类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
}

其中包含 this和 thatB之间存在关系以及数据类型为 的所有实例。ABTrue

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

上述文本的正式版本
（来源：dropproxy.com）

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

到目前为止，我尝试的是定义 a fun trueR(a : A)which 应该返回所有R's for whichR.a = a and r.data = True和 a fact allbIsRTruewhich 声明 for eachA allb应该是R.b's 返回的总和 by trueR。

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

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

4

1 回答 1

3

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

{x: X | f(x)}

上面的表达式计算为一组X'sf(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“连接”那些精确的a和b和r.data的True。

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

  • 我做了Boolsig 抽象因为你可能不想要既不是True也不是的布尔值False

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

  • 我重命名了关系a和btora和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
}
于 2012-10-19T16:33:22.880 回答