module address

sig Time {}

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

sig Book {
        names: Name set -> Time,
        addr: Name -> some Target -> Time }

fact { all t:Time | all b:Book | b.addr.t.Target in b.names.t }

fact { all t:Time | all b:Book | no n: Name | n in n. ^(b.(addr.t)) }

fact { all t:Time | all b:Book | all a: Alias | #(a.(b.addr.t))=<1  }

pred add [b: Book, n: Name, a: Target, t,t': Time] {
        n in b.names.t
        b.addr.t' in b.addr.t + n->a }

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

-- run {}