合金 - 设置差异导致 vars 和从句，设置并没有

Question

我很好奇什么时候开始计算，显然某些运算符被转换为子句而不是被计算：

abstract sig Element {}
one sig A,B,C extend Element {}

one sig Test {
  test: set Element
}

pred Test1 { Test.test = A+B }
pred Test2 { Test.test = Element-C }

分别为Test1 和Test2 运行它会给出不同数量的变量/子句，具体来说：

Test1: 0 vars, 0 primary vars, 0 clauses
Test2: 5 vars, 3 primary vars, 4 clauses

因此，尽管 Element 是 abstract 并且它的所有成员及其基数都是已知的，但似乎没有提前计算差异，而总和是。我不想做任何假设，所以我对为什么会这样感兴趣。 + 操作符是特殊的吗？

为了提供一些上下文，我尝试限制关系的域并发现仅使用 + 似乎更有效，即使事先完全知道集合。

Answer 1

为了提供一些上下文，我尝试限制关系的域并发现仅使用 + 似乎更有效，即使事先完全知道集合也是如此。

这几乎是正确的结论。原因是合金分析器试图从某些合金习语推断关系界限。它使用保守的近似值，对于集合并集和乘积总是合理的，但对于集合差则不然。这就是为什么对于上面示例中的Test1，Alloy Analyzer 推断出test 关系（this/Test.test: [[[A$0], [B$0]]]）的固定界限，因此不需要调用求解器；对于Test2，test 关系的边界不能缩小，因此设置为最宽松的 (this/Test.test: [[], [[A$0], [B$0], [C$0]]])，因此需要调用求解器来找到满足给定边界约束的解决方案。