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) 没有一本书既是外借的又是上架的（假设你的意思是“或”是排他性的），所以外借集的交集和onshelf 集将是空的，并且 (b) book set 将等于 onloan 集和 onshelf 集的并集。

任何时候借出的账套都是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 {
  disj[Library.on_shelves, Person.~loaned_to]
}

还有一点解释。Library.on_shelves是关系右侧的书集on_shelves，即所有在书架上的书。~loaned_to是类型的反向关系，Person -> Book是Person.~loaned_to借给任何人的账套。

谓词声明这disj两个集合没有公共原子（不相交集合）。

于 2012-11-13T17:43:56.050 回答
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)
}
于 2012-07-29T21:01:11.880 回答
0

我对合金不是很熟悉。但我认为这个或类似的东西会起作用。

每本书要么在书架上，要么借给顾客。

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

这个问题现在已经 6 岁了，但我正在学习合金，我想提供我的解决方案。

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

这可以理解为“上架的书集和借出的书集的交集是空的”。

于 2018-03-27T08:09:17.233 回答