4.2中的语义变化？

Question

我的问题是,合金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

然后找不到同一次运行的实例.这似乎表明在合金4.2中,这是如何声明关系addr 最多将一个地址与每个地址簿和名称对关联,但我想对此进行确认.

Answer 1

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

我创建了v4.2的快照,修复了这个问题,你可以在这里下载它:

感谢您报告此错误.