《软件抽象》中Alloy Book示例异常？实例未符合预期逻辑

我在阅读Daniel Jackson所著的《Software Abstractions》时，实现书中的Book模型后发现运行结果不符合预期。

原模型代码 #

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}

预期中Book$1应该是Book$0的副本并新增一组Name->Addr映射，但实际实例里b_a和b_b指向同一个Book$1，且Book$1的addr关系和Book$0没有继承关联，完全不符合预期。

问题原因 #

1. 未约束实例唯一性：showAdd谓词没有限制b_a和b_b是不同的Book实例，Alloy允许两者指向同一个对象，导致add操作失去了“基于原Book创建新Book并添加映射”的意义。
2. 缺乏新增映射的约束：原代码只要求b_b的addr关联至少两个Name，但没有确保新增的n->a是在b_a的addr基础上添加的——当b_a和b_b为同一个对象时，这个操作本身无意义，因为sig的字段是静态不可变的。

修正方案 #

修改showAdd谓词，添加实例唯一性约束，可选新增“Name未存在于原Book映射中”的约束（避免覆盖原有映射，更贴合“新增”的预期）：

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]
    b_a != b_b  // 强制两个Book实例不同
    #Name.(b_b.addr) > 1
    n not in dom b_a.addr  // 可选：确保新增的Name未在原Book中存在，避免覆盖
}

run showAdd for 3 but 2 Book

修正效果 #

运行修正后的代码，会生成符合预期的实例：b_a为初始Book（如Book$0，addr包含Name$1->Addr$0），b_b为新Book（如Book$1，addr包含Name$1->Addr$0和新增的Name$0->Addr$1），完美实现“基于原Book副本新增映射”的逻辑。

内容的提问来源于stack exchange，提问作者user21808955