alloy - 在一组或另一组中有一个对象，但不是两者都有？

Question

这是家庭作业，我遇到了很多麻烦。我正在使用 Alloy为图书馆建模。下面是对象的定义:

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

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

sig Person{}

然后我们需要有一个事实表明，每本书要么在书架上，要么被顾客取出。但是，它们不能同时出现在两个地方。

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

我试过这个...

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

但它不起作用……书总是在书架上。想说，“对于每一本书，如果它没有被借出，它就在书架上。否则，它就出局了。”

非常感谢更正、示例和提示。

Answer 1

如果每本书都必须借给某人或上架，那么 (a) 没有一本书既可以出借又上架(假设您的意思是“或”是排他性的)，因此借出集和上架集的交集onshelf set 将为空，并且 (b) book set 将等于 onloan set 和 onshelf set 的并集。

随时借出的套书是loaned_to的域关系。给定图书馆书架上的一套图书 L是 L.onshelves 的值;所有已知图书馆的书架上的这套书是 Library.onshelves .

所以你可能会说

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

或者你可能需要说稍微不同的事情，这取决于你的意思。请注意，这些限制并不是说借书簿必须借给单个借款人。