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

**URL:** <https://alloytools.discourse.group/t/alloy-6-running-examples-from-the-book-software-abstractions-and-getting-confused-by-the-visualisations/484>\
**Category:** Questions\
**Created:** [September 29, 2024, 12:24pm UTC](https://alloytools.discourse.group/t/alloy-6-running-examples-from-the-book-software-abstractions-and-getting-confused-by-the-visualisations/484 "2024-09-29T12:24:11Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![Modeller](https://avatars.discourse-cdn.com/v4/letter/m/d07c76/32.png) [@Modeller](https://alloytools.discourse.group/u/Modeller)\
**Post date:** [September 29, 2024, 12:24pm UTC](https://alloytools.discourse.group/t/alloy-6-running-examples-from-the-book-software-abstractions-and-getting-confused-by-the-visualisations/484/1 "2024-09-29T12:24:11Z")

</div>

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:

```auto
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](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/0b025bbb980a0bb1ef312aee4a5d4dfcbf49095c.png)

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!

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [September 29, 2024, 2:57pm UTC](https://alloytools.discourse.group/t/alloy-6-running-examples-from-the-book-software-abstractions-and-getting-confused-by-the-visualisations/484/2 "2024-09-29T14:57:05Z")

</div>

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):

```auto
---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](https://haslab.github.io/formal-software-design/), in which these kinds of issues are tackled earlier.

---

<div class="post-metadata">

**Author:** ![Modeller](https://avatars.discourse-cdn.com/v4/letter/m/d07c76/32.png) [@Modeller](https://alloytools.discourse.group/u/Modeller)\
**Post date:** [September 29, 2024, 7:18pm UTC](https://alloytools.discourse.group/t/alloy-6-running-examples-from-the-book-software-abstractions-and-getting-confused-by-the-visualisations/484/3 "2024-09-29T19:18:52Z")

</div>

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!