首页 文章

集合联合的积累

提问于
浏览
1

我有两个类 AB 以及与它们的类 R 的额外数据的关系 .

所以, AB 通过 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 的所有实例,其中 AB 之间存在关系,数据类型为 True .

我想将以下逻辑语句表达为Alloy事实:

Formal version of text above http://dropproxy.com/f/3B

我在这里假设 True == 1False != 1 并且集合 AR 分别包含 AR 的所有实例 .

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

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

如何将我的正式约束指定为Alloy事实?

1 回答

  • 3

    我想你想用set comprehension . 在Alloy中,这是set comprehension的语法

    {x: X | f(x)}
    

    上面的表达式计算为 f(x)f(x) 持有的一组 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 设置 Aa.allB 是所有 B 的集合,因此存在一些 r ,"connects"那些确切的 ab ,其中 r.dataTrue .

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

    • 我做了 Bool sig摘要,因为你可能不希望bool既不是 True 也不是 False

    • 我制作了 TrueFalse sigs singleton sigs(即 one sig )因为你可能想要每个都只有一个原子

    • 我将关系 ab 重命名为 rarb 以避免名称别名和潜在的混淆

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

    abstract sig Bool {}
    one sig True, False extends Bool {}
    
    sig A {
      allB: set B
    } 
    sig B {}
    sig R {
      ra : A,
      rb : B,
      data : Bool
    }
    

相关问题