合金约束如何将一个集合放入其子集中？

Question

以下合金代码表示每个酒店房间都有一组钥匙：

sig Key {}

sig Room {
    keys: set Key
}

keys 关系需要受到约束。就目前而言，它允许这样的情况：在一堆房间中使用密钥 K1。哎哟!我们不希望那样。我们希望每把钥匙只能用于一个房间。下图展示了所有有效实例（以及我们实际希望允许的实例子集）：

我们真正想要的实例集可以用这个合金代码很好地表达：

Room lone -> Key

该合金代码的实例在上图中用小圆圈表示。

那么，我们如何约束keys？一个答案是这样的：创建一个合金事实，它说：

keys in Room lone -> Key

想一想那是用图形表达的意思。就是说大圆圈必须在小圆圈内（见下文）。这不是很奇怪吗？一个圆怎么能在它的子圆里面呢？有人可以给我一些直觉吗？看起来很奇怪。

Answer 1

• 如果您只有 sig Room {keys: set Key} 而没有任何其他事实/约束，则 keys 关系的域是大圆圈；

• 您可以决定添加一些约束（如keys in Room lone -> Key），以缩小keys 关系的域（使其变成小圆圈）。

所以正确的思考方式不是大圆圈必须在小圆圈内（？！）；相反，将其视为使用小圆圈而不是大圆圈作为keys 的域（所有有效值的集合）。