我正在使用＃运算符来获取笛卡尔乘积(A-> B)和联合(A + B)的基数。但是它返回奇怪的负数，我不知道它们是什么!
请查看下面的快照，其中显示了我的模型的A-> B和A + B内容，以及Alloy的基数使用＃运算符提供给我。 (我希望第一个得到12，第二个得到8，但是我得到-4，然后得到-8)
任何意见？!
波纹管是我的规格，如果它可以帮助:
最佳答案
默认情况下，Alloy整数是4位二进制补码值，因此可能的值范围是-8到7。由于设计和实现中的复杂权衡取舍，分析器通过自动换行处理有限的整数范围周围。在您的示例中，A-> B的基数为12，这超出了可用范围；值将环绕并且评估器显示值-4。
若要允许基数高达12，最简单的解决方法是使用范围规范中的关键字int确保Int的位宽大于4。
具体来说:将run {} for 6更改为run {} for 6 but 5 int。 (您当然可以使用大于5的位宽。)
较新版本的Alloy也具有“禁止溢出”选项，该选项可防止在运行谓词或检查断言时显示虚假示例和反示例。
另请参阅最近的问题Why does Alloy tell me that 3 >= 10?
关于alloy - 基数运算符(＃)错误导致Alloy，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/29335376/