有一个或另一个对象,但不是两个？

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

你fact的错了。您想为所有书籍（而不是“某些”）说些什么。这基本上就是一个异或运算。

这是一个有效的方法：

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