合金中的基数运算符(#)错误结果

Question

我使用#manrator获得笛卡尔积(A-> B)和Union(A + B)的基数.但它返回奇怪的负数,我不知道它们是什么!？

请看下面的快照,显示我的模型的A-> B和A + B内容以及Alloy给我使用#manrator的基数.(我希望第一个获得12个,第二个获得8个,但第一个获得-4而第二个获得-8)

任何意见？!

如果它有帮助,波纹管是我的规格:

打开util/relation

sig A {}

sig B {}

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

运行{} 6

Answer 1

默认情况下,合金整数是4位二进制补码值,因此可能值的范围从-8到7.由于与设计和实现中的复杂权衡相关的原因,分析器通过包装处理有限的整数范围 - 周围.在您的示例中,A-> B的基数为12,溢出可用范围; 值环绕并且赋值器显示值-4.

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

具体地说:run {} for 6改为run {} for 6 but 5 int.(您当然可以使用大于5的位宽.)

较新版本的Alloy还具有Forbid Overflow选项,可防止在运行谓词或检查断言时显示虚假示例和反例.

另见最近的问题为什么Alloy告诉我3> = 10？