module others/addressBook
sig User, Host, Target {}
sig Name extends Target {}
sig Address extends Target {
	user: User,
	host: lone Host}
sig Book {
	addr, addri: Name -> Target,
	local: lone Host}
	{
	addri = ^addr
	}
pred inv (b: Book) {
	all a: Name.(b.addri) & Address | some a.host
	no b.addri & iden
	}
fun lookup (b: Book, n: Name): set Address {
	n.(b.addri) & Address
	}
pred add (b, b': Book, n: Name, a: Address) {
	some x: Address {
		x.user = a.user
		x.host = if some a.host then a.host else b.local
		b'.addr = b.addr + n -> x
		}
	b'.local = b.local
	}
assert addOK {
	all b, b': Book, n: Name, a: Address |
		add (b, b', n, a) and inv (b) => inv (b')
	}
check addOK