Search code examples
alloy

What am I missing here? (Confusion over witness labels)

I'm going through the Alloy book, and looking at the snippet of code below from chapter 2.

module tour/addressBook1

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

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

run show for 3 but 1 Book

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

run add for 3 but 2 Book

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

run showAdd for 3 but 2 Book

When I execute the run showAdd for 3 but 2 Book, and project over Book, I get the following two images

Book0

Book1

And that output makes a lot of sense. Book1 has Name0 -> Addr added to it, and those two elements are marked as the witnesses to showAdd.

However, if I stop projecting over Book, I get this image:

No Projection

And this is where I'm confused. If I'm reading it correctly, it's telling me that Book1 is used as both b and b', i.e. it's the witness to both of those arguments of the predicate showAdd.

Shouldn't that final image have labelled Book0 with $showAdd_b? If not, where's my misunderstanding?

Solution

  • I think both would be valid instances: using Book0 or Book1 as b. Note: there is no precondition that b does not already contain the given name.

    You can improve the add predicate by adding such a precondition.