合金-处理无界的通用量词

Question

下午好，

我在处理无界通用量词时遇到了Alloy的问题。正如Daniel Jackson的《软件摘要》一书(第5.3节"无界通用量词")中所解释的，Alloy在通用量词和断言检查方面有一个微妙的限制。Alloy在某些情况下会产生虚假的反例，例如下一个检查集合是否在并集下闭合的反例(如前书所示)：

sig Set {
elements: set Element
}
sig Element {}
assert Closed {
all s0, s1: Set | some s2: Set |
s2.elements = s0.elements + s1.elements
}
check Closed for 3

产生反例，例如：

Set = {(S0),(S1)}
Element = {(E0),(E1)}
s0 = {(S0)}
s1 = {(S1)}
elements = {(S0,E0), (S1,E1)}

其中分析器没有用足够的值填充Set(缺少Set原子S2，包含S0和S1的并集)。

这本书提出了两种解决这一普遍问题的方法：

1) 声明生成器公理以强制Alloy生成所有可能的实例。例如：

fact SetGenerator{
some s: Set | no s.elements
all s: Set, e: Element |
some s': Set | s'.elements = s.elements + e
}

然而，这种解决方案会产生范围爆炸，也可能导致不一致。

2) 省略了生成器公理，并使用约束的有界通用形式。也就是说，量化变量的边界表达式并没有提到生成的签名的名称。然而，并不是每一个断言都可以用这样的形式表达

我的问题是：有没有具体的规则来选择这些解决方案？我从书中看不清楚。

谢谢。

Answer 1

不，没有特定的规则(或者至少我没有想出任何规则)。在实践中，这种情况并不经常出现，所以我会处理每一个出现的案例。你有一个特别的例子吗？

此外，请记住，有时你可以用高阶量词(即集合或关系上的量词)来表述你的问题，在这种情况下，你可以使用Alloy*，Alloy的一个扩展，支持高阶分析。