module tour/addressBook2b

abstract sig Target {}
sig Addr extends Target {}
abstract sig Name extends Target {}

sig Alias, Group extends Name {}
sig Book {
	names: set Name,
	addr: names -> some Target
	}
	{
	no n: Name | n in n.^(addr)
	all a: Alias | one a.addr
	-- all g: Group | some g.addr
	}

pred add (b, b': Book, n: Name, t: Target) {b'.addr = b.addr + n->t}
pred del (b, b': Book, n: Name,t: Target) {b'.addr = b.addr - n->t}
fun lookup (b: Book, n: Name): set Addr {n.^(b.addr) & Addr}

assert delUndoesAdd {
	all b,b',b": Book, n: Name, t: Target |
		no n.(b.addr) and
			add (b,b',n,t) and del (b',b",n, t) implies b.addr = b".addr
	}
check delUndoesAdd for 3
check delUndoesAdd for 6 but 3 Book expect 0

assert addIdempotent {
	all b,b',b": Book, n: Name, t: Target |
		add (b,b',n,t) and add (b',b",n,t) implies b'.addr = b".addr
	}
check addIdempotent for 3

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

assert addLocal {all b,b': Book, n,n': Name, a: Addr |
	add (b,b',n,a) and n != n' => lookup (b,n') = lookup (b',n') }

check addLocal for 3 but 2 Book