module addressBook
open std/ord

sig Target {}
part sig Addr, Name extends Target {}
part 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)}

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

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

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

fun init (b: Book) {no b.addr}
fact traces {
	all b: Book - Ord[Book].last | let b' = OrdNext(b) |
		some n: Name, a: Target | add (b, b', n, a) or del (b, b', n)
	init (Ord[Book].first) }

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