基数约束不可满足答案

【问题标题】：Cardinality constraints unsatisfiable基数约束不可满足
【发布时间】：2016-03-25 09:10:13
【问题描述】：

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

比如下面这个合金文件……

sig Y {}

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

run {} for exactly 1 X, 3 Y

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

编辑。我发现这个问题只影响AlloyStar（与香草合金相反）。使用 AlloyStar（0.2 版）时，我得到了

执行“运行 run$1 for 1 X, 3 Y”

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

69 个变量。 12个初级变量。 167 条。 923 毫秒。

找到实例。谓词是一致的。 21 毫秒。

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

执行“运行 run$1 for 1 X, 3 Y”

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

0 变量。 0 个主要变量。 1 条款。 15 毫秒。

没有找到实例。谓词可能不一致。 1 毫秒。

所以我猜这个问题已成为 AlloyStar 开发人员的错误报告！

【问题讨论】：

标签： alloy

【解决方案1】：

看来你得配置位宽：

执行“运行 run$1 for 1 X, 3 Y”

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

0 变量。 0 个主要变量。 1 条款。 15 毫秒。

没有找到实例。谓词可能不一致。 1 毫秒。

数字 2 不能用位宽 1 来表示。我想该示例适用于标准合金，因为那里的默认位宽更高。

【讨论】：

【解决方案2】：

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

首先，我假设您将“禁止溢出”选项设置为 true，否则您将获得一个实例，而不管整数的指定范围（位宽）如何。

接下来，我们不要使用“附加事实”，因为附加事实可能具有不同的语义，具体取决于是否启用了“启用隐式此”选项。所以让我们假设以下合金模型：

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% 确定，但这可能是因为添加了对位向量的支持，以及一些使用位向量的合成基准，所以在撰写本文时这样做很方便。

【讨论】：