Alloy book example is wrong?

Question

Reading Software Abstractions by Daniel Jackson. Tried creating a simple model, realized it's not working the way I intend. Came back to the most basic models in the book which are 1:1 to my own, and realized they don't work either. The book model is:

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


 
pred add(b_a,b_b:Book, n: Name, a:Addr){
    b_b.addr = b_a.addr + n -> a
}

pred showAdd(b_a,b_b:Book, n: Name, a:Addr){
    add [b_a, b_b, n, a]
    #Name.(b_b.addr) > 1

}

run showAdd for 3 but 2 Book

The text instance is:

---INSTANCE---
loop=0
end=0
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7, Addr$0, Addr$1, Book$0, Book$1, Name$0, Name$1}
Int={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2}
String={}
none={}
this/Name={Name$0, Name$1}
this/Addr={Addr$0, Addr$1}
this/Book={Book$0, Book$1}
this/Book<:addr={Book$0->Name$1->Addr$0, Book$1->Name$0->Addr$0, Book$1->Name$1->Addr$1}
skolem $showAdd_b_a={Book$1}
skolem $showAdd_b_b={Book$1}
skolem $showAdd_n={Name$1}
skolem $showAdd_a={Addr$1}

Visual representation (notice that underlined address Names are different, even though the Book1 should be a copy of Book0, with the addition of a new Name->Addr mapping). Visual represantation

Tried removing multiplicities. Originally they looked something like addr: lone Name -> some Addr Tried removing + n -> a in order to achieve full copy of Book0 and Book1 - didn't work

To be clear, the problem is: Instance Book1 should be a copy of Book0, while Book1 must also have an additional mapping Name-> Addr. What we see instead, is that Book1 maps to the same Addrs, but through different Names, which should not happen

Answer 1

Had to set book_a != book_b on predicate

Answer 2

There's two things going on here. First, the visualizations you get don't match the book visualizations. This is because the book was written for Alloy 4.0, and we're now on Alloy 6. That's also why you had to replace b' with b_b, as b' now is a temporal operator. If you look at the sample modules (under File), under book > chapter2 > addressBook1f you'll see that b' is commonly rewritten as b".

Second, the assumption "Book1 should be a copy of Book0" is incorrect. If you look at your visualization, you'll see that under Book1 is ($showAdd_b_a, $showAdd_b_b). This means that the analyzer picked Book1 for both b_a and b_b! And in fact this is the exact error that the next step in the Software Abstractions tutorial, the one that introduces delUndoesAdd, will uncover. That's addressBook1g if you want to try it.

Answer 3

Remember also that exactly which instances Alloy generates for a particular model is non-deterministic, and depends on the solver!

Alloy uses symmetry breaking to avoid generating instances that are isomorphic (that is, essentially equivalent because you can rename one to the other) but the symmetry breaking isn't perfect so occasionally you get two solutions that are essentially the same.