Hi to Everyone,

I've just started to experiment with (the last version of) the system and I am finding
a hard time understanding (mathematically speaking)
some of the several solutions presented by visualization tool:

Consider the following script (adapted from the model book (chapter 2) example:
/////////////////////////////////////////////////
module tour/addressBook1e ----- Page 11

sig Name, Addr { }

sig Book {
   addr: Name ->  Addr//I changed here...
}

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

assert addWorks{
all b, b': Book, n,n': Name, a: Addr |
      add [b, b', n, a] and (n'->a) in b.addr
      implies
        (n'->a) in b'.addr
}
// This command generates an instance similar to Fig 2.4
run add for 3 but 2 Book
check addWorks for 3

Executing 'run add' and going through the several solutions (using next + projection over Book+
magic layout) I observed the following:

1.First Solution:Ok

Book0: pre-state
Book1: pos-state

2. Second Solution: Ok (but)
Book0: pos-state
Book1: pre-state
(I thought Book0 would be always the pre-state)

3. Third Solution: Ok, but  again
Book0: pos-state
Book1: pre-state

4&5. Fourth and Fifth Solution are ok and the same,
showing the two states with the same tuples

6. Sixth Solution: Now we have a problem (at least to me)

In Book0, the pre-state, there is a link from Name0 to Address2 (which has the value "a"),
i.e., (Name0,a), but this tuple is gone in the pos-state (Book1), which has of course
the new link (Name1[(n),Addr2(a)).

In my script above I tried to check this with an assertion,which was found to be true by the
system.

Maybe the question is basic, but I would be grateful for any help on this.

All the best!

Alfio Martini

Executing the assert comand I received (as expected) that assertion holds,
that is to say, if I have a specific link to an address before add, then
adding a new link from a new