为什么 Alloy 告诉我 3 >= 10？
Why does Alloy tell me that 3 >= 10?
在调试 Alloy 中的一个令人费解的问题时，我使用求值器做了 3 > 10 并得到了结果 true。我错过了什么吗？！
Alloy 整数通常按照正常标准非常窄，并且它们通常具有某种 'wraparound' 语义。在默认作用域中，in Alloy 4.2 Int取值范围为-8到7，字面量8、9、10与字面量-8、-7、-6没有区别。 （像字面量10这样的超出范围的值的使用静态是检测不到的，因为原则上Alloy模型可以是无限的；Int的大小静态是不知道的，是动态知道的，所以应该是Int 范围之外的文字可能引发动态错误；我不知道他们为什么不这样做。如果他们这样做的话，肯定会让一些用户的生活不那么混乱。）
如果您想要像 #x > 10 这样的约束，您需要为 Int 指定更大的范围。 N.B。为 Int 或 int 指定的范围指定用于整数的二进制补码表示的位宽，而不是宇宙中 Int 原子的数量。
有一个禁止溢出选项，这可能会有所帮助（但请参阅 this question，这表明可能存在并发症）。
考虑在 Alloy 中使用整数时，值得思考一下 Jackson 在 软件抽象 中所说的话（第 2.3.2 节之后的讨论）：
Can you really work without interpreted atoms such as the integers?
Yes, almost all the time. And it turns out that on most occasions that you might think you need integers, it's cleaner and more abstract to use atoms of an uninterpreted type with some relations to give whatever interpretation is needed. Alloy does actually support integers, albeit in a restricted way (due to the limitations of finite bounds).
和（4.8后讨论）：
Why leave integers to the end?
Integers are actually not very useful. If you think you need them, think again; there is often a more abstract description that matches the problem better. Just because integers appear in the problem domain does not mean that they should be modeled as such. To figure out whether integers are necessary, ask yourself what properties are actually relied upon. For example, a communications protocol that numbers its messages may rely only on the numbers being distinct; or it may relay on them increasing; or perhaps even being totally ordered. In none of these cases should integers be used. Of course, if you have a heavily numerical problem, you're likely to need integers (and more), but then Alloy is probably not suitable anyway.
祝你好运。
在调试 Alloy 中的一个令人费解的问题时，我使用求值器做了 3 > 10 并得到了结果 true。我错过了什么吗？！
Alloy 整数通常按照正常标准非常窄，并且它们通常具有某种 'wraparound' 语义。在默认作用域中，in Alloy 4.2 Int取值范围为-8到7，字面量8、9、10与字面量-8、-7、-6没有区别。 （像字面量10这样的超出范围的值的使用静态是检测不到的，因为原则上Alloy模型可以是无限的；Int的大小静态是不知道的，是动态知道的，所以应该是Int 范围之外的文字可能引发动态错误；我不知道他们为什么不这样做。如果他们这样做的话，肯定会让一些用户的生活不那么混乱。）
如果您想要像 #x > 10 这样的约束，您需要为 Int 指定更大的范围。 N.B。为 Int 或 int 指定的范围指定用于整数的二进制补码表示的位宽，而不是宇宙中 Int 原子的数量。
有一个禁止溢出选项，这可能会有所帮助（但请参阅 this question，这表明可能存在并发症）。
考虑在 Alloy 中使用整数时，值得思考一下 Jackson 在 软件抽象 中所说的话（第 2.3.2 节之后的讨论）：
Can you really work without interpreted atoms such as the integers?
Yes, almost all the time. And it turns out that on most occasions that you might think you need integers, it's cleaner and more abstract to use atoms of an uninterpreted type with some relations to give whatever interpretation is needed. Alloy does actually support integers, albeit in a restricted way (due to the limitations of finite bounds).
和（4.8后讨论）：
Why leave integers to the end?
Integers are actually not very useful. If you think you need them, think again; there is often a more abstract description that matches the problem better. Just because integers appear in the problem domain does not mean that they should be modeled as such. To figure out whether integers are necessary, ask yourself what properties are actually relied upon. For example, a communications protocol that numbers its messages may rely only on the numbers being distinct; or it may relay on them increasing; or perhaps even being totally ordered. In none of these cases should integers be used. Of course, if you have a heavily numerical problem, you're likely to need integers (and more), but then Alloy is probably not suitable anyway.
祝你好运。