alloy - 在合金中运行命令范围

Question

在合金考虑

信号队列{链接：队列，元素：整数}

考虑到我有一些谓词 predicate-1，当我为 Queue <=1、int ={-3,-2,0,2} 运行 predicate-1 时，我将如何定义范围。我没有在这里列出谓词

为 1 个队列运行 predicate-1，此处为 int 范围

不知道 int 范围的语法是什么

Answer 1

语法是

run predicate1 for 1 Queue, 3 Int

整数的范围始终是位宽，因此您不能指定 Int 集正好包含 {-3。-2。0. 2}; 您只能指定一个位宽，并且将使用该位宽内的所有整数。在我上面的示例中，Int 集将包含从 -4 到 3 的所有整数。