是否应优化Alloy通讯录示例以避免分析结果不一致？

问题描述 #

在Alloy 6.1中运行《Address Book Example》的通讯录示例模型时，add操作的分析结果出现违反直觉的表现：

• 实例Book$0中，Name$1关联Addr$0；但在实例Book$1中，同一个Name$1却关联Addr$1
• 从现实通讯录逻辑看，这相当于原有条目被意外修改
• 若给add谓词添加约束b != bn，分析结果就符合预期：添加操作后原有条目未被修改

疑问：

1. 如何解释原模型的分析结果？
2. 为何最初的模型没有加入b != bn这个约束？

原模型代码 #

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

结果解释 #

1. 原模型分析结果的原因 #

Alloy的关系运算符+在这里的行为是覆盖而非追加：当n在b.addr中已经有对应地址时，b.addr + n->a会直接用新的n->a替换原有的关联关系，而不是保留旧关联再添加新的。

原模型的add谓词只定义了bn.addr等于b.addr + n->a，没有限制n在b.addr中是否已存在关联。所以Alloy会生成所有满足这个等式的实例，包括n已有地址、被新地址覆盖的情况——这就是你看到的“原有条目被修改”的反直觉结果。

另外，原模型没有限制b != bn，理论上还可能生成b和bn是同一个实例的情况（比如当n->a已经存在于b.addr中时，b.addr + n->a等于自身），不过你的showAdd里加了#Name.(bm.addr) > 1，过滤掉了这种无变化的情况，但覆盖原有条目的情况依然会被保留。

2. 最初模型未加b != bn的原因 #

《Address Book Example》作为入门示例，核心是演示关系更新的基本语法，而非严格定义“添加操作”的业务语义。

• 从教学角度，先展示最基础的关系运算逻辑，让读者理解+运算符的行为，再逐步引入业务约束（比如禁止覆盖、禁止无变化），符合循序渐进的学习路径。
• 从Alloy的建模思想来看，模型默认会生成所有满足谓词的实例，包括边界情况。这种设计能帮助用户发现模型中的隐含假设——比如你遇到的问题，正是在提示你需要明确“添加操作不应修改原有条目”的业务规则，从而完善模型。

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