assertion - Alloy アサーションが期待どおりに機能しない

Question

ここに私の合金コードがあります:

one sig Library {
    books: set Book,    // set of the library's books
    patrons: set Patron,    // set of the library's patrons
    circulation: Patron lone -> some Book   // books in circulation
}

// set of books in the Library
sig Book {
}

// set of patrons
sig Patron {
    curbooks: set Book // books currently checked out by a patron
}

したがって、2 人の Patron が現在同じ本を持つことはできないという主張を追加したいと思います。これが私が持ってきた主張です：

assert sameBook2Patrons {
    all disj p, p': Patron | all b: p.curbooks | b not in p'.curbooks
}

したがって、アサーションを次のようにチェックします。

check sameBook2Patrons{} for exactly 2 Book, exactly 2 Patron

Alloyは反例を見つけません。しかし、run コマンドを使用すると、Alloy は多くの反例を示します。

run{} for exactly 2 Book, exactly 2 Patron

また、有効なアサーションを否定して事実を追加しても、インスタンスが得られないことになっていることを読みました。私はそれを追加しました：

fact sameBook2Patrons {
    not (all disj p, p': Patron | all b: p.curbooks | b not in p'.curbooks)
}

モデルを実行すると、Alloy は有効なインスタンスを見つけます。

私は何を間違っていますか？ありがとうございました。