使用"Forbid Overflow: Yes"的合金整数比较语义

Question

我有以下合金模块和运行命令：

sig A { x : set A }
run {all a: A| #a.x<3 and #a.x>1} for exactly 2 A, 2 int

"禁止溢出：no"合金分析仪4.2（构建日期：2012-09-25）找不到实例。我相信原因是，由于常数3的溢出，运行谓词读取{all a: A| #a.x<-1 and #a.x>1}。

使用"禁止溢出：是"合金分析仪找到一个实例。

---INSTANCE---
integers={-2, -1, 0, 1}
univ={-1, -2, 0, 1, A$0, A$1}
Int={-1, -2, 0, 1}
seq/Int={0}
String={}
none={}
this/A={A$0, A$1}
this/A<:x={A$0->A$0, A$0->A$1, A$1->A$0, A$1->A$1}

合金评估器告诉我，运行命令中使用的谓词{all a: A| #a.x<3 and #a.x>1}评估为false。

有人可以解释这种行为吗？评估器和分析仪中整数比较的半数有差异？

编辑：我注意到最新的实验版本中的行为不同：合金4.2_2014-03-07。它找不到实例。这种行为是预期的。

Answer 1

您已经在问题中提供了所有正确的答案，因此我只能快速重申它们

• 预期行为（无实例）是该模型的"正确"行为;
• 版本4.2有一些有关处理溢出的已知错误，因此这就是它找到一个实例的原因（应在最新版本中固定这些错误，因此该模型的正确行为）;
• 在整数的"环绕式"语义下（关闭溢出检测），仍然没有实例，完全是出于您描述的原因（-3被视为-1）;
• 评估者仍然存在一些问题（即使在最新版本中），因此有时它将仅使用环绕语义。