我创建了一个测试来比较一个空字段中的值的数量与一个数字。我对结果感到惊讶。
首先，我创建了一个带有字段 f 的签名，可以选择将一个 A 原子映射到另一个 A 原子：
sig A {f: lone A}
然后我创建了这个表达式：如果 f 为空，则 f 映射的 A 原子数的计数小于 8：
check {
no A.f =>
# A.f < 8
}
我运行了检查命令，合金分析仪找到了一个反例。这让我大吃一惊。
我打开了评估工具并输入了这个：
我输入：A
评估员回复：{}
我输入：no A.f
评估员回复：true
我输入：# A.f
评估员回复：0
我输入：# A.f < 8
评估员回复：false
嗯？
为什么0 < 8 是假的？
【问题讨论】：
标签： alloy
Alloy 只有一组有限的整数，因为每个整数在找到解决方案时相对昂贵。默认情况下，此设置为：
Int
┌──┬──┬──┬──┬──┬──┬──┬──┬─┬─┬─┬─┬─┬─┬─┬─┐⁻¹
│-8│-7│-6│-5│-4│-3│-2│-1│0│1│2│3│4│5│6│7│
└──┴──┴──┴──┴──┴──┴──┴──┴─┴─┴─┴─┴─┴─┴─┴─┘
当你做 7+1 时，你实际上得到 -8！
试试看...只需在评估器中输入 8：
8
-8
这实际上不仅限于 Alloy、C、C++、Java 和大多数其他语言也是如此，您通常不会注意到它的原因是因为环绕点要高得多。对于 Java int，它超过 20 亿。原因是整数被存储为一组位。一旦达到最大值，添加将需要额外的位。由于该位不存在，它被默默地忽略。 （实际上，意识到到目前为止我从未见过任何处理此溢出的代码是一个非常可怕的想法。）
因此，当你的最大数字是 7 时，Alloy 中的默认值，而你使用 8 它实际上是 -8！
# A.f < -8
我们有这种恐惧的原因是，在 Alloy Int 中，当它被提供给 SAT 求解器时，它也包含在一个位集合中。
Alloy 一直在努力解决这个问题，并且有一个选项可以防止溢出。起初我以为这是上天送来的礼物，但因为我意识到它是如何工作的，所以我禁用了它。问题是它删除了可能有效的解决方案。找到解决方案并不算太糟糕，因为您会注意到什么时候什么都没有，但是对于断言来说是非常糟糕的，因为断言可能会说模型实际上有没有解决方案。这让我不寒而栗，因为我想依赖一个断言。查看实际用例，我决定我宁愿在我的模型中明确处理溢出，因为它们实际上也是最终产品中的一个问题。许多已知的错误是由意外溢出引起的。所以隐藏它们的模型不是很有用。
那么你如何处理这个问题？这个语法有点奇怪。您必须指定整数编码的位宽。因此，您可以将模型更改为：
sig A {f: 孤独的 A}
check {
no A.f =>
# A.f < 8
} for 5 int
for 5 int 将 SAT 编码的位宽设置为 5 位。 5 位 = 5^2=32。那么你有整数 -16..15。
这显然是一个巨大的绊线。幸运的是，为了让 Alloy 在 SMT 求解器上运行，正在进行出色的工作。 SMT 求解器将具有比 Alloy 更自然的数字处理能力，这不会让您失望。
也就是说，如果您使用不适合可用 Int 集合的常量整数，我至少可以尝试生成错误。也许你可以提交一个错误？
【讨论】：