module addressBook

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

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

run add for 3 but 2 Book

pred addPlay  (b, b': Book, n: Name, a: Addr) {
	add (b, b', n, a)
	b != b'
	b.addr != b'.addr
	}

run addPlay for 3 but 2 Book