[Alloy 6] Running examples from the book Software Abstractions and getting confused by the visualisations

Questions
1

Hi everybody, I am new with Alloy and I purchased the book Software Abstractions, based on Alloy 4.

However, I’m using Alloy 6 and it looks like I get different results than in the book.

For example, this code:

module tour/addressBook1

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

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

pred show (b: Book) {
	#b.addr > 1
	#Name.(b.addr) > 1
}

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

run showAdd for 3 but 2 Book

generates these two diagrams (projections are over Book)

image
image692×1224 47.4 KB

Why would the union operator cause to change the mappings instead of just adding a new one like in the book?

Thank you very much in advance!

2

First, depending on the exact version of Alloy and the exact version of the underlying SAT solver, you may not get instances in the same order as Daniel when he wrote the book. This is because the solving process may vary a lot even with small changes in the solving algorithms. However, up to possible bugs in Alloy or SAT solvers, if you kept hitting the New button in the Visualizer, yielding new possible instances, you would end up with the same set of instances.

So, here, you get an instance different from the book but this is a possibility for the reason explained above. That is, provided the unexpected instance is indeed correct. And to say the truth, it looks wrong, right?

Well, this is because, as you will learn when reading the book, the specification does not say at least two things that we may expect as end-users:

  1. that b and b1 will be shown by the Visualizer in that order,
  2. that b and b1 are two different books.

Which means we can get instances where the second item isn’t verified, and these instances are correct with respect to the specification.

Let’s check this. In the Visualizer, click the “Txt” button (which gives another, textual, view of the instance). This is what I get (ignore the “skolem” wording for the moment):

---INSTANCE---
...
skolem $showAdd_b={Book$1}
skolem $showAdd_b1={Book$1}
skolem $showAdd_n={Name$1}
skolem $showAdd_a={Addr$1}

And here we have our explanation: the instance is one where both b and b1 are mapped to the same atom Book$1! And of course, provided Book$1.addr contains a pair n->a, we indeed have: Book$1.addr = Book$1.addr + n->a. This is admittedly confusing but correct in the sense that nothing forbids such an instance.

To continue, I would advise you to either trust the examples printed in the book (then at some point the book will make clear why such instances appear and how we can constrain them more), or to consider first reading the tutorial of Alloy 6 available here, in which these kinds of issues are tackled earlier.

3

Thanks for taking the time to answer to me and for your clear explanation.
I’m not sure whether the author of the book cheated on the images to avoid overloading the reader or the tool changed so that now more specifications are needed to reach the same result, but it really confused me.
I’m going to do the tutorial first and the book after. Thanks for your valuable advice!