alloy - 4.2 中的语义变化？

Question

我的问题是，Alloy 4.2 中字段声明中 () 的语义是否已更改。

我在“软件抽象”中读到

addr: (Book -> Name) -> lone Addr

表示关系地址关联 最多 每个地址簿和姓名对都有一个地址，但在运行 Alloy 4.2 时不成立

例如，对于

sig Book, Name, Addr  {}
sig AddBX {
  addr : (Book -> Name) -> lone Addr
}

run XRun {
  some B : Book, N : Name, X : AddBX | #X.addr[B][N] = 2
} 

Alloy 4.2 找到一个模型实例，例如 AddBX$2 与

Book$1 ->Name$0 ->Addr$0
Book$1 ->Name$0 ->Addr$1
Book$1 ->Name$0 ->Addr$2

如果我改用

addr : Book -> Name -> lone Addr

然后找不到相同运行的实例。这似乎表明，在 Alloy 4.2 中，这是如何声明关系 addr 关联 最多 每个地址簿和姓名对都有一个地址，但我想对此进行确认。

Answer 1

这实际上是 v4.2 中的一个错误，正确的行为是 Alloy4.1.10 实现的。

我创建了 v4.2 的快照，其中修复了此问题，您可以在此处下载:

http://alloy.mit.edu/alloy/downloads/alloy4.2_2013-01-28.jar

感谢您报告此错误。