我使用#manrator获得笛卡尔积（A-> B）和Union（A B）的基数 . 但它返回奇怪的负数，我不知道它们是什么！？
请看下面的快照，显示我的模型的A-> B和A B内容以及Alloy给我使用#manrator的基数 . （我希望第一个获得12个，第二个获得8个，但第一个获得-4而第二个获得-8）
任何意见？！
如果它有帮助，波纹管是我的规格：
open util / relation sig A {} sig B {} sig C {r1：one A，r2：one B} run {} for 6
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选项，可防止在运行谓词或检查断言时显示虚假示例和反例 .
另见最近的问题Why does Alloy tell me that 3 >= 10?