不可满足的基数约束

Question

我无法让 Alloy 的基数运算符 (#) 按预期工作，即使在简单的示例中也是如此。

例如，下面的 Alloy 文件...

sig Y {}

sig X {r : Y -> Y} {
//#r = 2
}

run {} for exactly 1 X, 3 Y

... 给了我一个恰好包含 2 个 r 边的解决方案（见下图）。但是，如果我取消注释 #r = 2 行，Alloy 找不到任何解决方案！我做错了什么？

编辑。 我发现这个问题只影响 AlloyStar（相对于原版 Alloy）。使用 AlloyStar（版本 0.2）时，我得到

Executing "Run run for exactly 1 X, 3 Y"

Solver=minisatprover(jni) Bitwidth=1 MaxSeq=0 Symmetry=20

69 vars. 12 primary vars. 167 clauses. 923ms.

Instance found. Predicate is consistent. 21ms.

但是当我取消注释 #r = 2 时，我得到

Executing "Run run for exactly 1 X, 3 Y"

Solver=minisatprover(jni) Bitwidth=1 MaxSeq=0 Symmetry=20

0 vars. 0 primary vars. 1 clauses. 15ms.

No instance found. Predicate may be inconsistent. 1ms.

所以我想这个问题因此成为Alloy明星开发者的错误报告！

Answer 1

看来还得配置位宽：

Executing "Run run for exactly 1 X, 3 Y"

Solver=minisatprover(jni) Bitwidth=1 MaxSeq=0 Symmetry=20

0 vars. 0 primary vars. 1 clauses. 15ms.

No instance found. Predicate may be inconsistent. 1ms.

数字 2 不能用位宽 1 表示。我想这个例子在标准 Alloy 中工作，因为那里的默认位宽更高。

Answer 2

感谢您的错误报告。这里发生了几件事。基本上，所说的一切都是正确的，但完整的答案有点微妙。

首先，我假设您已将 "Forbid Overflows" 选项设置为 true，否则您将获得一个实例，而不管整数的指定范围（位宽）如何。

接下来，我们不要使用 "appended facts"，因为根据 "Enable Implicit This" 选项是否启用，附加的事实可以有不同的语义。因此，让我们假设以下 Alloy 模型：

sig Y {}
sig X {r: Y -> Y} 

fact { #r = 2 }

run {} for exactly 1 X, 3 Y

现在，在Alloy4.2中，当没有指定整数边界时，引擎用来表示整数表达式（例如基数表达式、整数常量等）的默认位宽为5；由于常量 2 可以用 5 位表示，因此不会发生溢出并找到一个实例。

另一方面，在Alloy*中，默认位宽为1，宽度不足以表示常量2，因此会发生溢出，找不到实例。为什么选择位宽 1 作为默认值？我不是 100% 确定，但这可能是因为添加了对位向量的支持，以及一些使用位向量的综合基准，所以在撰写本文时这样做很方便。

不可满足的基数约束

Cardinality constraints unsatisfiable

alloy