书中的示例是否应该完善以避免结果不一致

Question

当书中示例的现有合金模型用于合金6.1时， 评估结果给出了加法运算的直观表示：

书籍实例中Book$0 Name$1与Addr$0相关， 但在书籍实例 Book$1 中，相同的 Name$1 与 Addr$1 相关。

就现实生活中的地址簿而言，我可以将这种情况解释为无意的 修改书籍条目。

如果我应用合金书示例中的建议是错误的？并添加附加约束b != b"，那么分析结果满足我的期望：添加后现有条目没有改变。

我们如何解释原始变体的分析结果，以及 为什么从一开始就没有使用附加约束 b != b" ？

该模型与地址簿示例中的完全相同：

module tour/addressBook1f ----- Page 12

sig Name, Addr { }

sig Book {
    addr: Name -> lone Addr
}

pred add [b, bn: Book, n: Name, a: Addr] {
   bn.addr = b.addr + n->a
}

pred showAdd [b, bm: Book, n: Name, a: Addr] {
   add [b, bm, n, a]
   #Name.(bm.addr) > 1
}

// This command generates an instance similar to Fig 2.5
run showAdd for 3 but 2 Book

Answer 1

首先，请注意，某些结果可能会与书中显示的有所不同，但没有错误，至少有 3 个原因：Alloy 中的代码更改修改了某些操作的顺序、对称性破缺以及使用这个或那个 SAT 求解器作为后端（例如，我在使用 Glucose41 时没有得到与您相同的实例）。但是，如果您一直按

New

直到筋疲力尽，您将沿着所有可能的非对称实例行走。

现在你的问题不是你想的那样。在您的实例中，如果您考虑

$showAdd_b

和

$showAdd_bm

的值，即在

this

实例中赋予

b

和 bm 的值，您会看到它们都对应于

Book$1

。您得到的实例实际上是正确的，但有点奇怪：它表明如果

Book$1

包含条目

Name$0->Addr$0

和

Name$1->Addr$1

，那么在添加

Name$1->Addr$1

（

$showAdd_n

和

$showAdd_a

的值）之后，它仍然包含相同的条目。换句话说，

Book$0

在这种情况下不起任何作用。

现在，如果您添加约束

b != bm

，那么 Alloy 将找到另一个实例，更加符合您的预期。

至于为什么从一开始就没有使用附加约束，我想说的是，如果你的规范不是太强，它通常被认为是好的，因为它允许更多的实例（=它涵盖了更多的情况）。在这里，找到的实例确实是一种可以接受的情况：它显示了一种情况，人们想要向地址簿添加一些条目，但由于它已经在这里，所以地址簿没有改变。棘手的部分是你认为

Book$0

参与其中，但事实并非如此。