使用 Alloy 建模一个简单的库

Question

在“fact F4_All_wanted_books_are_had_by_someone”中，我试图让所有想要的书都借给某个赞助人。也就是说，如果顾客想要一本书，它必须处于加载状态（否则它可以借给想要它的顾客）。在“F7_Cannot_want_what_you_have”中，顾客不能想要他或她已经拥有的书。但是当我尝试执行代码时。它表明没有找到实例，但是，它应该找到了实例。

在我添加“fact F4”之前，实例仍然可以找到，但是在我添加F4之后，就再也找不到实例了。 “事实F4”有什么问题吗？以及我该如何解决。感谢您的帮助。

/**
 * The books in a library.
 */
some sig Book{}

/**
 * Patrons of the library, in general, have some books (on loan)
 * and want some other books.
 */
some sig Patron {
    has     : set Book,
    wants   : set Book
}

/**
 * The library has some books on reserve, some on the shelves,
 * and some on hold because patrons want them (are waiting for
 * them).
 *
 * Note: The books on loan are exactly those all the Patrons as
 *              a group "have".
 */
one sig Library {
    onReserve : set Book,
    onShelves   : set Book
}

/**
 *  All wanted books are on loan to some patron (that is,
 *  some patron has the wanted book). Note that a patron
 *  *MAY* have a book out that nobody else wants.
 */
fact F4_All_wanted_books_are_had_by_someone {
    all b : Patron | b.wants in b.has
}

/**
 *  Two different patrons cannot have the same book.
 */
fact F5_No_loan_conflicts {
    all disj b1, b2 : Patron | no (b1.has & b2.has)
}

/**
 *  A patron cannot want a book he or she already has.
 */
fact F7_Cannot_want_what_you_have {
    all b : Patron | no (b.wants & b.has)
}

run{
    some onReserve
    some onShelves - onReserve
    some wants
    some has
    some Patron.has - Patron.wants
    some Patron.has & Patron.wants
    some has.Book & wants.Book
} for exactly 3 Patron, exactly 8 Book

Answer 1

您的 F4 的含义是“对于所有顾客来说，他想要的每一本书都在他拥有的书中”。我建议

fact F4 {
    all p:Patron | p.wants in (Patron - p).has
}