我有两个类 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
.
我想将以下逻辑语句表达为Alloy事实:
Formal version of text above http://dropproxy.com/f/3B
我在这里假设 True == 1
和 False != 1
并且集合 A
和 R
分别包含 A
和 R
的所有实例 .
到目前为止我所尝试的是定义一个 fun trueR(a : A)
,它应该返回所有 R
的 R.a = a and r.data = True
和一个 fact allbIsRTrue
,它表明每个 A
allb
应该是 trueR
返回的 R.b
的总和 .
但是,这里是我卡住的地方,我找不到正确的构造来对引用中的集合求和,并尝试 sum
导致语法错误 .
如何将我的正式约束指定为Alloy事实?
1 回答
我想你想用set comprehension . 在Alloy中,这是set comprehension的语法
上面的表达式计算为
f(x)
为f(x)
持有的一组X
.在您的示例中,为了表达
allB
的事实,您可以编写类似的内容在英语中,这个事实是“为所有
a
设置A
,a.allB
是所有B
的集合,因此存在一些r
,"connects"那些确切的a
和b
,其中r.data
是True
.请注意我对您模型的其余部分所做的以下修改:
我做了
Bool
sig摘要,因为你可能不希望bool既不是True
也不是False
我制作了
True
和False
sigs singleton sigs(即one sig
)因为你可能想要每个都只有一个原子我将关系
a
和b
重命名为ra
和rb
以避免名称别名和潜在的混淆以下是我用于此示例的模型的其余部分