alloy - 基数运算符 (#) 在 Alloy 中产生错误结果

Question

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

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

有什么意见吗？!

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

open util/relation

sig A {}

sig B{}

sig C{r1: one A,r2:one B}

run {} for 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?