基数运算符 (#) 错误导致合金

Question

我正在使用 # 运算符来获取笛卡尔积 (A->B) 和并集 (A+B) 的基数。但它返回奇怪的负数，我不知道它们是什么！？

请查看下面的快照，其中显示了我的模型的 A->B 和 A+B 内容，以及 Alloy 使用 # 运算符为我提供的基数。 （我希望第一个得到 12，第二个得到 8，但我第一个得到 -4，第二个得到 -8）

有什么意见吗？！

如果有帮助，下面是我的规范：

打开实用程序/关系

签名一个{}

签名 B{}

sig C{r1: 一个 A,r2: 一个 B}

运行 {} 6

Answer 1

默认情况下，Alloy 整数是 4 位二进制补码值，因此可能值的范围从 -8 到 7。由于与设计和实现中的复杂权衡相关的原因，分析器处理有限的整数范围通过环绕。在您的示例中， A->B 的基数为 12，超出了可用范围；值环绕，求值器显示值 -4。

要允许高达 12 的基数，最简单的解决方法是确保 Int 的位宽大于 4，在范围规范中使用关键字 int。

具体而言：将run {} for 6 更改为run {} for 6 but 5 int。 （你当然可以使用大于 5 的位宽。）

Alloy 的较新版本还有一个禁止溢出选项，它可以防止在运行谓词或检查断言时出现虚假示例和反例。

另见最近的问题Why does Alloy tell me that 3 >= 10?