# THE LIBRARY SYSTEM

# Entities of the system
{
	beloved, emma : BOOK
	peter, jane   : CUSTOMER
	mary          : LIBRARIAN
}

# Description of the initial state
{
    added(emma)
    available(emma)  
}

# Use cases description

#use case AddBook
UC AddBook(l:LIBRARIAN; b:BOOK)
pre not added(b)
post available(b) and added(b)

#use case RemoveBook
UC RemoveBook(l:LIBRARIAN; b:BOOK)
pre available(b)
post not available(b)

#use case Register
UC Register(c:CUSTOMER)
pre not registered(c)
post registered(c)

#use case Borrow
UC Borrow(c:CUSTOMER; b:BOOK)
pre registered(c) and available(b) and not exists(b2:BOOK) { has(c, b2) }
post not available(b) and has(c, b)

#use case Return
UC Return(c:CUSTOMER; b:BOOK)
pre has(c,b)
post available(b) and not has(c, b)