8

これは宿題で、私はそれで多くの問題を抱えています。ライブラリのモデリングに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
    }
}

しかし、それは機能していません...本は常に棚にあります。「すべての本について、貸し出されていない場合は棚にあります。そうでない場合は売り切れです」と言いたい。

訂正、例、およびヒントは大歓迎です。

4

5 に答える 5

4

すべての本が誰かに貸し出されているか、棚に置かれている必要がある場合、（a）貸し出しと棚の両方に本が置かれることはありません（「または」が排他的であると仮定すると）。オンシェルフセットは空になり、（b）本のセットはオンローンセットとオンシェルフセットの和集合に等しくなります。

いつでも貸し出されている本のセットは、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
}

または、意味によっては、少し異なることを言う必要があるかもしれません。これらの制約は、貸し出し中の本が単一の借り手に貸し出されていなければならないということではないことに注意してください。

于 2012-08-16T18:13:01.667 に答える
1

あなたfactは間違っています。あなたはすべての本のために何かを言いたいです（「いくつか」ではありません）。そして、それは基本的にXORです。

動作するものは次のとおりです。

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)
}
于 2012-07-29T21:01:11.880 に答える
1

私が間違っている場合は訂正してください。しかし、これはあなたが求めている事実だと思います。

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

そして少し説明。Library.on_shelvesリレーションの右側にある本のセットon_shelves、つまり棚にあるすべての本です。~loaned_toはタイプの逆の関係でありPerson -> Book、Person.~loaned_to任意の人に貸し出される本のセットです。

述語はdisj、2つのセットに共通のアトム（互いに素なセット）がないことを宣言します。

于 2012-11-13T17:43:56.050 に答える
0

私はAlloyにあまり詳しくありません。しかし、私はこれまたは同様のものがうまくいくと思います。

すべての本は棚にあるか、常連客に貸し出されています。

fact AllBooksLoanedOrOnShelves {
all b: Book | b in Library.on_shelves || b.loaned_to in Library.patrons
}
于 2012-02-10T11:40:53.287 に答える
0

この質問は現在6歳ですが、私はAlloyを学んでおり、解決策についての意見を述べたいと思いました。

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

これは、「棚にある本のセットと貸し出されている本のセットの交差点は空です」と読むことができます。

于 2018-03-27T08:09:17.233 に答える