module analysis/addressBook

sig Addr, Name {}
sig Book {addr: Name -> (Name + Addr)}
fact Acyclic {all b: Book | no n: Name | n in n.^(b.addr)}
pred add (b, b': Book, n: Name, t: Name + Addr) {
	b'.addr = b.addr + n->t
	}
run add for 3 but 2 Book
fun lookup (b: Book, n: Name): set Addr {n.^(b.addr) & Addr}
assert addLocal {
	all b,b': Book, n,n': Name, t: Name + Addr |
		add (b,b',n,t) and n != n' => lookup (b,n') = lookup (b',n')
	}
check addLocal for 3 but 2 Book

assert AddTotal {
	all b: Book, n: Name, a: Addr |
		some b': Book | add (b, b', n, a)
	}
check AddTotal for 2