Search code examples
modelingalloy

Unexpected Instance found for Alloy specification

I tried my first steps in modelling with Alloy and have come across a problem I cannot get my head around. I have the following spec:

module tour/AddressBook1

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

// operation: adds a (name, address) to the Book b, resulting in b'
pred add (b, b' : Book, n:Name, a:Addr) {
    b'.addr = b.addr + n->a
}

run add for 3 but 2 Book

So far nothing special. It is literally the example of the book 'Software abstraction' by Daniel Jackson.

It essentially models books, that have (name,address)-pairs associated with it. The add-predicate is supposed to grab a Book-instance b and create another Book-instance b' from it by adding (a potentially already existing) (name,address)-pair to it.

The first few examples found are easy and convincing but clicking through with the Next-button I end up with the following example (full view above, equivalent projection over books below)

Found instance

I see two books, the starting book Book0 with two pairs (Name0, Addr2) and (Name1, Addr1). From the annotions we can also see that the add operation is going to add the new duo (Name1, Addr2). When I now look at the result book Book1 I have {(Name0, Addr0),(Name1, Addr2)} instead of {(Name0, Addr2),(Name1, Addr1),(Name1, Addr2)}

Why is this considered a legal instance?

(Alloy Analyzer 4.2, Build date 2012-09-25 15:54 EDT)

Solution

  • There are two confusing things here:

    1. Book0 does not take part in the operation. Instead Book1 has the role of both b0 and b1.

    2. Adding n->a to a book does not assert that this is a new address. In the instance, Book1 has this address before and after add. This is because the operation

      b'.addr = b.addr + n->a

      uses set union. Broken down to a simpler example:

      {1, 2} = {1} + {2}

      is true. But

      {1, 2} = {1, 2} + {2}

      is also true. So in the original example, there is nothing that excludes n->a from already being a part of b.addr. And the Alloy Analyzer simply generates all instances that are consistent with the given constraints.

    You can improve this example by adding an assertion in add:

        b.addr[n] != a