Simple book examples don't work(?)

Questions
1

Am I missing something?

What I expect for is:

  • two instances of Book to be created (Book1, Book0)
  • Book1 has all of the same Name → Addr mappings as Book0
  • Book1 additionally must also have a NEW mapping Name → Addr

What I get:

  • Book0 that maps Name1 → Addr0
  • Book1 maps Name0 → Addr0 (wrong!) and Name1 → Addr1 (a new mapping)

The model:

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


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

 
run add for 3 but 2 Book

Visual example:
WF8wq

2

Okay, it’s because I didn’t set b_a != b_b