alloy - 如何定义 Int 的范围

Question

我正在使用 Alloy 4.2 使用“for ... but...”语法来定义 Int 的范围，但看起来它无视我的请求。例如，给定以下简单模型:

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

第一个运行未找到任何实例，而第二个则找到一个实例。据我了解这些两个命令是等效的(除非有一些隐藏的签名，其范围是自动推断的)。

有人可以阐明这种行为吗？

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

编辑:(比评论更易读)

请注意

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

有效，并且

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

不起作用。

现在有趣的是

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

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

• 1 和 2 向我们表明事实实例是否找到，并不取决于您分配给签名 Int 的范围
• 3 让我猜测，如果您没有明确定义全局范围，则分析器“足够智能”，可以根据您正在运行的谓词来调整 seq/Int 的范围。