合金书例子错了？

Question

阅读 Daniel Jackson 的软件抽象。尝试创建一个简单的模型，意识到它没有按我预期的方式工作。回到书中与我自己的 1:1 的最基本模型，并意识到它们也不起作用。 书本型号为：

sig Name, Addr {}
sig Book {addr: Name -> lone Addr}


 
pred add(b_a,b_b:Book, n: Name, a:Addr){
    b_b.addr = b_a.addr + n -> a
}

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

}

run showAdd for 3 but 2 Book

文本实例为：

---INSTANCE---
loop=0
end=0
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7, Addr$0, Addr$1, Book$0, Book$1, Name$0, Name$1}
Int={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2}
String={}
none={}
this/Name={Name$0, Name$1}
this/Addr={Addr$0, Addr$1}
this/Book={Book$0, Book$1}
this/Book<:addr={Book$0->Name$1->Addr$0, Book$1->Name$0->Addr$0, Book$1->Name$1->Addr$1}
skolem $showAdd_b_a={Book$1}
skolem $showAdd_b_b={Book$1}
skolem $showAdd_n={Name$1}
skolem $showAdd_a={Addr$1}

视觉表示（注意带下划线的地址名称是不同的，即使 Book1 应该是 Book0 的副本，但添加了新的 Name->Addr 映射）。

尝试去除多重性。本来他们看起来像

addr: lone Name -> some Addr

尝试删除

+ n -> a

以获得 Book0 和 Book1 的完整副本 - 没有用

明确一点，问题是：Instance Book1 应该是Book0 的副本，而Book1 还必须有一个额外的映射Name-> Addr。 相反，我们看到的是 Book1 映射到相同的地址，但通过不同的名称，这不应该发生

Answer 1

必须在谓词上设置

book_a != book_b

Answer 2

这里发生了两件事。首先，您获得的可视化与书中的可视化不匹配。这是因为这本书是为 Alloy 4.0 编写的，而我们现在是在 Alloy 6 上。这也是为什么你必须用

b'

替换

b_b

的原因，因为

b'

现在是 时间运算符。如果您查看示例模块（在

File

下），在

book > chapter2 > addressBook1f

下您会看到

b'

通常被重写为

b"

.

其次，假设“Book1 应该是 Book0 的副本”是不正确的。如果你看一下你的可视化，你会看到在

Book1

下面是

($showAdd_b_a, $showAdd_b_b)

。这意味着分析器为Book1和

b_a

选择了

b_b

！事实上，这正是 Software Abstractions 教程的下一步（介绍

delUndoesAdd

的那一步）将发现的确切错误。如果你想尝试的话，那就是

addressBook1g