在Alloy 中调试一个令人费解的问题时，我使用评估器执行3 > 10 并得到结果true。我错过了什么吗？！
【问题讨论】：
run 设置为要求#x > 10 并没有达到我的预期。我告诉评估员评估3 > 10 并得到true。显然，3 > 10 并不意味着“3 大于 10”。反对票在哪里？
标签： alloy
按照正常标准，合金整数通常非常窄，并且它们通常具有某种“环绕”语义。在默认范围内，Alloy 4.2 中的 Int 范围从 -8 到 7，文字 8、9、10 与文字 -8、-7、-6 无法区分。 （不能静态检测到像字面值 10 这样的超出范围值的使用，因为原则上合金模型可以是无限的； Int 的大小不是静态知道的。它是动态知道的，所以对于外面的字面量应该是可能的引发动态错误的 Int 范围；我不知道他们为什么不这样做。如果他们这样做，肯定会让一些用户的生活不那么混乱。）
如果您想要像#x > 10 这样的约束，您需要为 Int 指定更大的范围。注：为 Int 或 int 给出的范围指定用于整数的二进制补码表示的位宽，而不是宇宙中 Int 原子的数量。
有一个禁止溢出选项，这可能会有所帮助（但请参阅this question，这表明可能会出现并发症）。
当考虑在 Alloy 中使用整数时，值得考虑一下 Jackson 在 软件抽象 中所说的话（在第 2.3.2 节之后进行讨论）：
你真的可以在没有解释原子（例如整数）的情况下工作吗？
是的，几乎一直如此。事实证明，在大多数情况下，您可能认为您需要整数，使用具有某些关系的未解释类型的原子来提供所需的任何解释会更简洁、更抽象。 Alloy 实际上确实支持整数，尽管方式受到限制（由于有限边界的限制）。
和（4.8后讨论）：
为什么要把整数留到最后？
整数实际上不是很有用。如果您认为自己需要它们，请再想一想；通常有更抽象的描述可以更好地匹配问题。仅仅因为整数出现在问题域中并不意味着它们应该被建模。要弄清楚整数是否必要，问问自己实际依赖哪些属性。例如，对其消息进行编号的通信协议可能仅依赖于不同的编号；或者它可能会继续增加它们；或者甚至完全被命令。在这些情况下，都不应使用整数。当然，如果你有一个严重的数值问题，你可能需要整数（甚至更多），但是 Alloy 可能并不适合。
祝你好运。
【讨论】：