オブジェクトを1つのセットに入れるか、別のセットに入れるかを選択できます。

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が間違っています。あなたはすべての本（何かではない）のために何かを言いたいと思う。それは基本的に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) 
} 

Answer 2

私はあまり合金に精通していません。 しかし、私はこれまたは類似のものがうまくいくと思います。

すべての書籍は棚に置かれているか、またはお客様に貸し出されています。

fact AllBooksLoanedOrOnShelves { 
all b: Book | b in Library.on_shelves || b.loaned_to in Library.patrons 
} 

Answer 3

をすべての本は、ローンの誰かにまたは棚にどちらかでなければならない場合に、（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 
} 

を言うかもしれないか、あなたは意味だけで何に応じて、若干異なる事を言う必要があります。これらの制約は、貸出先の書籍が単一の借り手に貸与されている必要があるとは言いません。

Answer 4

[OK]を私が間違っているなら、私を修正し、私は、これはあなたが後にしている事実であると信じて：

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

そして少し説明。 Library.on_shelvesは、on_shelvesの関係の右側にある書籍のセット、つまり棚にあるすべての書籍です。 ~loaned_toはタイプPerson -> Bookの逆の関係であり、Person.~loaned_toは誰にも貸与された本のセットです。

述語は、2つの集合に共通の原子がないことを宣言します（互いに素な集合）。