基数运算符 (#) 错误结果 Alloy
cardinality operator (#) wrong results in Alloy
我正在使用 # 运算符获取笛卡尔积 (A->B) 和并集 (A+B) 的基数。但它 returns 奇怪的负数，我不知道它们是什么！？
请查看下面的快照，其中显示了我的模型的 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
默认情况下，Alloy 整数是 4 位二进制补码值，因此可能值的范围 运行s 从 -8 到 7。出于与设计中复杂权衡相关的原因和实现，分析器通过环绕处理有限范围的整数。在您的示例中，A->B 的基数为 12，超出了可用范围；值回绕，计算器显示值 -4。
要允许高达 12 的基数，最简单的解决方法是确保 Int 的位宽大于 4，在范围规范中使用关键字 int。
具体来说：将run {} for 6改为run {} for 6 but 5 int。 （你当然可以使用大于 5 的位宽。）
较新版本的 Alloy 也有一个禁止溢出选项，它可以防止在 运行 或检查断言时出现虚假示例和反示例。
另见最近的问题
我正在使用 # 运算符获取笛卡尔积 (A->B) 和并集 (A+B) 的基数。但它 returns 奇怪的负数，我不知道它们是什么！？
请查看下面的快照，其中显示了我的模型的 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
默认情况下，Alloy 整数是 4 位二进制补码值，因此可能值的范围 运行s 从 -8 到 7。出于与设计中复杂权衡相关的原因和实现，分析器通过环绕处理有限范围的整数。在您的示例中，A->B 的基数为 12，超出了可用范围；值回绕，计算器显示值 -4。
要允许高达 12 的基数，最简单的解决方法是确保 Int 的位宽大于 4，在范围规范中使用关键字 int。
具体来说：将run {} for 6改为run {} for 6 but 5 int。 （你当然可以使用大于 5 的位宽。）
较新版本的 Alloy 也有一个禁止溢出选项，它可以防止在 运行 或检查断言时出现虚假示例和反示例。
另见最近的问题