如果结果不符合预期，如何调试Alloy？

Question

当 Alloy 说“未找到实例”时。我如何寻找更多细节来了解为什么结果不如预期？

我使用合金分析仪6.1.0

我的代码是，

sig State, Node {}
sig List {
  header: Node ->one State
}
pred test( l: List, n: Node ){
 #l.header = 1 and #n.(l.header) = 1
}
run test for  exactly 2 List, exactly 2 State, exactly 2 Node

我的期望是，

但是合金的输出是，

执行“为正好 2 个列表、正好 2 个状态、正好 2 个节点运行 run$1” 求解器=sat4j 位宽=4 MaxSeq=4 SkolemDepth=1 对称性=20 模式=批处理 106 变种8 个主要变量。 195 个条款。 124 毫秒。 未找到实例。谓词可能不一致。 3毫秒。

我查看了解析树，但仍然不知道为什么没有找到实例。

但是，如果我将

exactly 2 Node

更改为

exactly 1 Node

，则 Alloy 会显示“已找到实例”。像这样，

我不明白如何解释这种差异。

Answer 1

Alloy 中“调试”主要有两种方法。

我首先讨论最重要的一个，就像是一名侦探：你必须自己寻找足以使你的模型不一致的约束：

• 这是通过用新的眼光重新阅读您的模型，尝试找到可能相互排斥的约束来完成的。不一致的典型来源是以不兼容的方式影响 sig 或字段的基数的约束。
• 您可以通过重写（或注释掉）模型的小部分来评估您对当前问题的评估，看看它是否可以令人满意。如果是这样，您发现了一个与您更改的内容相关联的问题，这会给您一个提示。

例如，您的模型可以重写如下：

sig State, Node {}
sig List {
  header: Node ->one State
}
pred test( l: List, n: Node ){
 one l.header 
 one l.header[n] // can be removed
}
run test for  exactly 2 List, exactly 2 State, exactly 2 Node

然后你可能会意识到

one l.header[n]

没有用，因为

header

的类型已经表明每对列表和节点都有一个状态。所以你可以删除它并看到它仍然是 UNSAT。

现在，您基本上有 3 个约束：

one

类型中的

header

、

one

中的

test

以及范围规范。

header

的类型表示列表和节点的每个组合都映射到唯一的状态。由于范围的原因，这意味着

header

在排列范围内应等于

{ l1->n1->?, l1->n2->?, l2->n1->?, l2->n2->? }

（对于每个元组，

?

为

s1

或

s2

）。然后，在

test

中，您说

l

（无论是

l1

或

l2

）与一对 single 节点和状态相关联。砰！

所以我们看到问题来自 3 个约束的组合。

如果您确实只考虑一个节点，那么

header

将仅包含形状为

{ l1->n1->?, l2->n1->? }

的元组，这一次将满足

test

。

但是解决问题的另一种方法是删除

test

！或者删除

one

类型中的

header

！ 通常有多种方法可以解决不一致问题。 您对该领域的了解将使您更喜欢一种解决方案而不是另一种解决方案。

为了完整起见，还有第二种方法可以补充前一种方法并且是自动化的，但有时很难解释。这个想法是要求 Alloy 生产所谓的“UNSAT 核心”，这是一组足以导致不一致的约束。为此，您必须依赖可以生成此类核心的 SAT 求解器，例如选项菜单中的“Minisat with Unsat Cores”。然后，您运行分析，如果与示例中的情况不一致，则会出现 Core 可点击文本，突出显示模型中的“可疑”部分。根据选项的不同，核心的计算速度会或多或少地快，并且突出显示的范围也会或多或少地大。

在您的示例中，如果我使用

Slow minimization

和粒度

Expand quantifiers

，那么 Alloy 将仅突出显示

one l.header

。事实上，您可以放松或删除此约束以使模型可满足。但正如您从上面的讨论中看到的，其他修改也可能有效，并且使用这些选项进行 UNSAT 核心提取不会显示它们。至少，使用这种技术绝不会妨碍您依赖自己对情况的分析！