验证两种确保酒店客人获得唯一密钥集方法的等价性

更新：特别感谢@Loïc Gammaitoni提供的解答思路！顺着他的方向，我创建了如下Alloy模型，用来验证两种确保酒店房间密钥集互不重叠方法的等价性：

sig Key {}
sig Room { keys: set Key }

// 第一种约束方式：通过关系限定每个密钥仅归属最多一个房间
pred DisjointKeySet_v1 { keys in Room lone -> Key }

// 参考《Software Abstractions》第274页的说明
> 《Software Abstractions》第274页指出：`sig S {f: disj e}` 等价于约束 `all a,b: S | a != b => no a.f & b.f`

// 第二种约束方式：直接断言不同房间的密钥集无交集
pred DisjointKeySet_v2 { all r, r': Room | r != r' => no r.keys & r'.keys }

这两种约束的核心逻辑都是保证不同房间的密钥集合没有重叠，只是表达方式不同：

• DisjointKeySet_v1 利用Alloy的关系运算符lone->，直接限定Key和Room的映射是“至多一个房间对应一个密钥”，从关系层面确保密钥集的唯一性。
• DisjointKeySet_v2 则是用更直观的一阶逻辑来描述：任意两个不同的房间，它们的密钥集合完全没有交集。

根据书中的理论，这两种约束是完全等价的，你可以通过Alloy的模型检查器添加断言assert Equivalence { DisjointKeySet_v1 <=> DisjointKeySet_v2 }，然后运行检查来验证这一点。

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