Should the book example be refined to avoid inconsistent results

Question

When existing Alloy models of the book example are used in Alloy 6.1, the evaluation results give contr-intuitive representation of add operation:

In the book instance Book$0 Name$1 is related to Addr$0, but in the book instance Book$1 the same Name$1 is related to Addr$1.

In terms of the real-life address book, I can interpret such situation as unintended modification of book entries.

If I apply suggestion from Alloy book example is wrong? and add additional constraint b != b", then the analysis results satisfy my expectations: existing entries are not changed after add.

How we can interpret the results of analysis for the original variant, and why additional constraint b != b" was not used from the beginning ?

The model is exactly the same as in the Address Book Example:

module tour/addressBook1f ----- Page 12

sig Name, Addr { }

sig Book {
    addr: Name -> lone Addr
}

pred add [b, bn: Book, n: Name, a: Addr] {
   bn.addr = b.addr + n->a
}

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

// This command generates an instance similar to Fig 2.5
run showAdd for 3 but 2 Book

Answer 1

First, notice that some results may appear different than in the book, without being wrong, for at least 3 reasons: a code change in Alloy that modified the order of some operations, symmetry breaking, and using this or that SAT solver as a backend (for instance, I don't get the same instance as you when using Glucose41). But, if you keep pressing New until exhaustion, you shall walk along all possible non-symmetric instances.

Now your issue isn't what you think. If, in your instance, you consider the value of $showAdd_b and $showAdd_bm, which are the values given to b and bm in this instance, you'll see that they both correspond to Book$1. The instance you get is in fact correct but a bit peculiar: it shows that if Book$1 contains entries Name$0->Addr$0 and Name$1->Addr$1, then after adding Name$1->Addr$1 (the value for $showAdd_n and $showAdd_a), it still contains the same entries. Said otherwise, Book$0 doesn't play any role in this instance.

Now if you add the constraint that b != bm, then Alloy will find another instance, more as you expected.

As to why the additional constraint was not used from the beginning, I'd say that it usually considered good if your specification is not too strong because it allows more instances (= it covers more situations). And here, the instance found is indeed an acceptable situation: it shows a situation where one wants to add some entry to an address book, but as it's already here, the address book is unchanged. The tricky part was that you thought that Book$0 was involved while it wasn't.