/*
** Address book example
** GS03/4023 Validation and Verification
** Jonathan Bowen and Anthony Hall
** University College London
** 2006/2007
*/


/* An email address book */

/* State */

sig Name, Addr {}

sig Book {
	addr: Name ->  Addr
}

/* Invariant */

pred invBook (b:Book){
	all n:Name | # b.addr[n] =<1
}


/* A simple example */

pred show(b:Book){
	invBook[b]
}

/* run show for 3 but 1 Book */


/* Specifying the initial state */

pred init (b : Book) {
	no b.addr
}

/* run init */

/* run init for 3 but 1 Book */

assert initOK {
	all b : Book | init[b] implies invBook[b]
}

/* check initOK for 3 */


/* Specifying an operation */

/*
pred add (b, b' : Book, n : Name, a : Addr){
	b'.addr = b.addr + n -> a
}
*/

/* A fix for the "add" operation */

pred add (b, b' : Book, n : Name, a : Addr){
	b'.addr = b.addr ++ n -> a
}

/* run add for 3 but 2 Book */


/* Does the operation respect the invariant? */

assert addOK{
	all b, b' : Book, n : Name, a:Addr |
		invBook[b] and add[b,b',n,a] implies invBook[b']
}

/* check addOK for 3 */


/* Looking up a name */

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

assert lookupOK{
	all b, b' : Book, n : Name, a : Addr |
		add[b,b',n,a] implies lookup[b',n] = a
}

/* check lookupOK for 3 */


/* Deleting an entry */

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


/* Is this a property that should hold? */

assert delUndoesAdd {
	all b, b', b'' : Book, n: Name, a : Addr |
		add[b,b',n, a] and del[b', b'', n] implies
			b.addr = b''.addr
}

check delUndoesAdd for 3