如何定义 Int 的范围

Question

我使用 Alloy 4.2 来定义 Int 的范围，使用 'for ... but...' 语法，但是看起来 它无视我的要求。例如，给定以下简单模型：

sig A {
  y : seq A
}

run { some a : A | #(a.y) = 4} for 3 but 4 Int

run { some a : A | #(a.y) = 4} for 4 Int, 3 A

第一个 run 找不到实例，而第二个找到实例。据我了解这些 两个命令是等价的（除非有一些隐藏的签名，其范围是自动推断的）。

有人能解释一下这种行为吗？

Answer 1

假设用于“索引”序列 y 的 A 原子的原子由签名 Int 键入，这两个运行命令将是等效的。

虽然这个假设看起来足够合理，但事实并非如此，因为序列的索引是由签名“seq/Int”键入的。 因此，增加 Int 的范围不会影响序列的最大长度。

要完成您打算做的事情，您可以为“序列本身”分配一个范围。 这样做如下：

run { some a : A | #(a.y) = 4} for 3 but 4 seq

关于序列的答案和其他信息可以在这个地址找到： http://alloy.mit.edu/alloy/documentation/quickguide/seq.html

编辑：（比 cmets 更具可读性）

注意

1.run { some a : A | #(a.y) = 4} for 4

有效，并且

2.run { some a : A | #(a.y) = 4} for 3

没用。

现在有趣的是

3.run { some a : A | #(a.y) = 4}

works ，即使已知默认范围为 3。 从这些实验中，我们可以得出结论：

• 1 和 2 向我们展示了是否找到了事实实例，这与您分配给签名 Int 的范围无关
• 3 让我猜想分析器“足够聪明”，可以根据您正在运行的谓词调整 seq/Int 的范围，如果您没有明确定义全局范围。