module addressBook
open std/ord [Book]

abstract sig Target {}
sig Addr extends Target {}
abstract sig Name extends Target {}
sig Alias, Group extends Name {}

sig Book {
	names: set Name,
	addr: names ->+ Target}

fact {all b: Book | no n: Name | n in n.^(b.addr)}

pred add (b, b': Book, n: Name, t: Target) {
	-- almost fix the AddLocal problem
	t in Addr or some lookup(b,t)
	b'.addr = b.addr + n->t
	}

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

fun lookup (b: Book, n: Name): set Addr {
	n.^(b.addr) & Addr
	}

pred init (b: Book) {no b.addr}
fact traces {
	all b: Book - last() | let b' = next(b) |
		some n: Name, t: Target | add (b, b', n, t) or del (b, b', n)
	init (first ()) }

assert lookupYields {all b: Book, n: b.names | some lookup(b,n)}
check lookupYields for 3 but 4 Book