4.2 中的语义变化？

Question

我的问题是字段声明中 () 的语义是否在 Alloy 4.2 中发生了变化。

我在“软件抽象”中读到

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

表示关系 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 中的一个 bug，正确的行为是 Alloy4.1.10 实现的。

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

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

感谢您报告此错误。