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.
