Alloy book - Question on figure 2.6/page 14

Software Abstractions
1

Hi,
I just started reading the Software Abstractions book. I am on page 14, figure 2.6: Can anyone explain how to generate the chart at the bottom with the Alloy Analyzer?
When I am running the model, I am only seeing Book$0 and Book$1 but not Book2 or something like that. I would have expected seeing 3 books.
(what does the $ sign mean in this case? It is not shown in the book)

I were not able to figure out which settings to use to generate the chart above the two other frames.

I am using Alloy 5.1.

PS: may I suggest to add a category for questions about the book?

-zz

2

You should use the projection feature and project over Book.

image
image704×164 9.77 KB

The $ separates the sig name (Book) from the atom. All atoms get numbered. Atoms are not a part of the model but the instance/solution consists of atoms.

One incredible features of Alloy is the Evaluator. When you have a solution you can inspect this instance with a shell. You can execute Alloy expressions but these expressions include the atoms, which you cannot do in a model.
Name

┌─────┐
│Name⁰│
├─────┤
│Name¹│
├─────┤
│Name²│
└─────┘
Addr

┌─────┐
│Addr⁰│
├─────┤
│Addr¹│
└─────┘
addr

┌─────┬─────┬─────┐
│Book⁰│Name⁰│Addr⁰│
│     ├─────┼─────┤
│     │Name¹│Addr⁰│
│     ├─────┼─────┤
│     │Name²│Addr¹│
└─────┴─────┴─────┘
Book$0.addr

┌─────┬─────┐
│Name⁰│Addr⁰│
├─────┼─────┤
│Name¹│Addr⁰│
├─────┼─────┤
│Name²│Addr¹│
└─────┴─────┘
Book$0.addr[Name$0]

┌─────┐
│Addr⁰│
└─────┘
# Book = 1

true
3

Thanks @peter.kriens for your reply. I am already doing the projection on Books (the field right of the “Next” button says “Projection over Book”). I am using the assertion from page 13 where the Alloy Analyzer finds a counterexample.

When I am running this (“Execute”, “Show”), I am seeing only two Books (the drop down menu says “Book0” and “Book1”. I would expect it to show three books where the graphical representation of Book0 and Book1 are equal.

Thanks for the tip with the elevator. When I am typing univ, I am also seeing only 2 Books despite delUndoesAdd assertion refers to three books. (I am using the command: check delUndoesAdd for 3)

Figure 2.6 shows Book0, Book1, and Book2 (the third image in this figure) but with which settings?

When I am clicking a few times on the “Next” button, I am seeing counter examples with 3 books but I thought that Figure 2.6 refers to the first counterexample that Alloy Analyzer produced?

4

Are you using a specific run command or are you relying on the default.

The exact solver and other details can influence what the order is of the solutions. You can force the solution to have 3 books with the exactly keyword:

 check delUndoesAdd for 10 but exactly 3 Book
5

I am executing this example: addressBook1g.als.

The quantification in the delUndoesAdd declares b, b' and b''. I thought that those three variables are referred to in Figure 2.6 (the third graph shows the three books) and mapped to the atoms Book0, Book1 and Book2.

When running the command with exactly 3 Book, I am seeing three books. Yet, I am still a bit confused why Book1 does not have a mapping for {(Name0, Addr0)}. I thought that Book1 refers to the second step where an already present mapping is added to Book0 or am I missing something?

┌─────────┬───────────┐
│this/Book│addr       │
├─────────┼─────┬─────┤
│Book⁰    │Name⁰│Addr⁰│
├─────────┼─────┴─────┤
│Book¹    │           │
├─────────┼─────┬─────┤
│Book²    │Name⁰│Addr⁰│
└─────────┴─────┴─────┘
6

If you go to the Txt tab you will see that there are a number of skolem variables. Never really understood what skolem does but it is clever. Practically, they hold values for ‘variables’ in the instance:

 skolem $delUndoesAdd_b={Book$2}
 skolem $delUndoesAdd_b'={Book$2}
 skolem $delUndoesAdd_b''={Book$1}
 skolem $delUndoesAdd_n={Name$0}
 skolem $delUndoesAdd_a={Addr$0}

You can see that b and b' are Book² and b'' is Book¹. Book$0 is not in play at all. Since you’re not ordering Book, the order is random and you’re not forcing the b’s to be disjunct.

So this says that if you add Name⁰->Addr⁰ to Book².addr there is no change since this tuple was already there. So b and b' are identical. However, if you then remove this tuple, you remove the original tuple in addr. This is Book¹. And the assert fails since b''`` (Book¹.addr) is empty unlike b’' (Book¹.addr`).

It gets a little bit easier to track if you add to the top (after the module):

      open util/ordering[Book]

And change the quantification to:

     all disj b, b', b'': Book, n: Name, a: Addr |

The b b=Book⁰, b'=Book¹, b''=Book². This is of course purely cosmetic.

I apologize for now showing the skolem values on the Table tab. I should add them, they are really needed there.

7

Ok, thanks a lot. Now, I am understanding it a bit better, thanks! :slight_smile: