Have an object in one set or another, but not both?

Question

This is homework and I'm having a lot of trouble with it. I am using Alloy to model a library. Here are the definitions of the objects:

sig Library {
    patrons : set Person,
    on_shelves : set Book,
}

sig Book {
    authors : set Person,
    loaned_to : set Person,
}

sig Person{}

Then we need to have to have a fact that states, every book is either on the shelf, or taken out by a patron. However, they cannot be in both places.

// Every book must either be loaned to a patron or
// on the shelves.
fact AllBooksLoanedOrOnShelves {}

I have tried this...

fact AllBooksLoanedOrOnShelves {
    some b : Book {
        one b.loaned_to =>
            no (b & Library.on_shelves)
        else
            b in Library.on_shelves
    }
}

But it's not working... the books always are on the shelves. want to say, "For every book, if it is not being loaned, it is on the shelf. Otherwise, it's out."

Corrections, examples, and hints are greatly appreciated.

Answer 1

If every book must be either on loan to someone or on the shelves, then (a) no book will be both on loan and on the shelves (assuming you mean that "or" as exclusive), so the intersection of the onloan set and the onshelf set will be empty, and (b) the set of books will be equal to the union of the onloan and onshelf sets.

The set of books on loan at any time is the domain of the loaned_to relation. The set of books on the shelf in a given library L is the value of L.onshelves; the set of books on the shelves in all known libraries is Library.onshelves.

So you might say

fact in_or_out_not_both {
  no Library.onshelves & loaned_to.Person 
}
fact all_books_in_or_out {
  Book = Library.onshelves + loaned_to.Person
}

Or you might need to say slightly different things, depending on just what you mean. Note that these constraints don't say that a book on loan must be on loan to a single borrower.

Answer 2

Your fact is wrong. You want to say something for all books (not "some"). And that something is basically an XOR.

Here's one that works:

fact AllBooksLoanedOrOnShelves{
  all b : Book|
    (b in Library.on_shelves and no p:Person | p in b.loaned_to)
    or
    (not b in Library.on_shelves and one p:Person | p in b.loaned_to)
}