Home Articles

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

Asked
Viewed 1049 times
2

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

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

任何意见?!

enter image description here

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

open util / relation sig A {} sig B {} sig C {r1:one A,r2:one B} run {} for 6

1 Answer

  • 5

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

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

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

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

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

Related