module tour/addressBook3
open util/ordering [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 -> some Target
	}
	{
	no n: Name | n in n.^(addr)
	all a: Alias | lone a.addr
	}

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

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

pred del (b, b': Book, n: Name, t: Target) {
	-- removing this binding of n to t doesn't leave any group or alias empty
	no b.addr.n or some n.(b.addr) - t
	b'.addr = b.addr - n->t
	}

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

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

pred show () {}
run show for 4

-- replay example from early draft of book
pred showDraftExample () {
	let b0 = first (), b1 = next(b0), b2 = next (b1), b3 = next (b2) {
		b1.addr in Group -> Addr
		#b2.addr.Addr & Group = 2
		let a = b3.addr | some a.a
	}
}
run showDraftExample for 4


assert lookupYields {
	all b: Book, n: b.names |
		some lookup(b,n)
	}

check lookupYields for 3 but 3 Book
check lookupYields for 3 but 4 Book
check lookupYields for 6