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

Answer 2

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 3

Ok correct me if I'm wrong, but I believe this is the fact you're after:

fact {
  disj[Library.on_shelves, Person.~loaned_to]
}

And a little explanation. Library.on_shelves is the set of books on the right side of the on_shelves relation, i.e. all the books that are on the shelves. ~loaned_to is the reverse relation of type Person -> Book and Person.~loaned_to is the set of books loaned to any person.

The disj predicate declares that the two sets have no common atoms (disjoint sets).

Answer 4

I am not very familiar with Alloy. But I think this or something similar would work.

Every book is either on the shelves or is loaned to a a patron.

fact AllBooksLoanedOrOnShelves {
all b: Book | b in Library.on_shelves || b.loaned_to in Library.patrons
}

Answer 5

This question is 6 years old now, but I'm learning Alloy, and I wanted to offer my take on a solution.

fact AllBooksLoanedOrOnShelves {
    no (Library.on_shelves & loaned_to.Person)
}

This can be read as "the intersection of the set of books that are on shelves and the set of books that are loaned out, is empty".