如何在Alloy中表示一对一关系？
How to represent one-to-one relationship in Alloy?
假设我有
信号 A{}
签名 B{e:A}
我想表示 A 和 B 之间的 1-1 映射，因此对于每个 B，只有一个 A 对应于：
{all b:B | one a : A | b.e = a}
是否有其他方法可以做到这一点，例如使用多重性？
您可以编写以确保每个 B 都与一个 A 相关：
sig B{
e: one A
}
编辑：
要确保每个 A 都与一个 B 相关，您可以在 A 的签名声明中添加一个签名事实
sig A{
}{
one this.~e
}
为什么这样做：
签名A下的签名事实被Alloy处理为：
fact{
all a:A | one a.~e
}
其中：
e 是签名 B 中定义的字段。因此它定义了类型 B -> A 的关系.
~ 运算符产生该关系的逆（因此类型变为 A -> B ）。
a 和那个关系 (A.A->B 之间的“点连接”产生所有 B 元素 B.e=a.
最后用one关键字表示只有一个这样的B元素（for all a） .
假设我有 信号 A{} 签名 B{e:A} 我想表示 A 和 B 之间的 1-1 映射，因此对于每个 B，只有一个 A 对应于：
{all b:B | one a : A | b.e = a}
是否有其他方法可以做到这一点，例如使用多重性？
您可以编写以确保每个 B 都与一个 A 相关：
sig B{
e: one A
}
编辑：
要确保每个 A 都与一个 B 相关，您可以在 A 的签名声明中添加一个签名事实
sig A{
}{
one this.~e
}
为什么这样做：
签名A下的签名事实被Alloy处理为：
fact{
all a:A | one a.~e
}
其中：
e 是签名 B 中定义的字段。因此它定义了类型 B -> A 的关系.
~ 运算符产生该关系的逆（因此类型变为 A -> B ）。
a 和那个关系 (A.A->B 之间的“点连接”产生所有 B 元素 B.e=a.
最后用one关键字表示只有一个这样的B元素（for all a） .