4

My question is whether the semantics of () in the declaration of fields had changed in Alloy 4.2.

I read in "Software Abstractions" that

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

means that the relation addr associates at most one address with each address book and name pair but this does not hold when running Alloy 4.2

For instance, for 

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 finds a model instance which has for instance AddBX$2 with

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

If I use instead

addr : Book -> Name -> lone Addr

then no instance for the same run is found. This seems to indicate that in Alloy 4.2 this is how to declare that the relation addr associates at most one address with each address book and name pair but I would like to have a confirmation for this.

4

1 に答える 1

5

これは実際には v4.2 のバグです。正しい動作は Alloy4.1.10 が実装するものです。

この問題が修正された v4.2 のスナップショットを作成しました。ここからダウンロードできます。

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

このバグを報告していただきありがとうございます。

于 2013-01-28T17:00:01.330 に答える