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

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)
}