module email
open std/ord
sig Target {}
part sig Addr, Name extends Target {}
part sig Alias, Group extends Name {}
sig AddrBook {names: set Name, map: names ->+ Target}
fun lookup (b: AddrBook, n: Name): set Addr {
	result = n.^(b.map) & Addr }
fun add (b, b': AddrBook, n: Name, a: Target) {
	a in Addr or some lookup(b,a)
	b'.map = b.map + n->a}
assert namesok {
	all b, b': AddrBook, n: Name, a: Addr |
		add (b,b',n,a) => b'.names = b.names + n
	}
check namesok
fun del (b, b': AddrBook, n: Name) {b'.map = b.map - n->Addr}
fun init (b: AddrBook) {no b.map}
fact traces {
	all b: AddrBook - Ord[AddrBook].last | let b' = OrdNext(b) |
		some n: Name, a: Target | add (b, b', n, a) or del (b, b', n)
	init (Ord[AddrBook].first) }
assert lookupYields {all b: AddrBook, n': b.names | some lookup(b,n')}
check lookupYields for 3 but 4 AddrBook