0

这是我的合金代码:

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
}

所以我想添加一个断言,即两个 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

合金没有找到任何反例。但是当我使用 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 会找到有效的实例。

我究竟做错了什么?谢谢你。

4

1 回答 1

1

您错误地使用了检查命令。要检查断言sameBook2Patrons,您应该改用

check sameBook2Patrons for exactly 2 Book, exactly 2 Patron

即,没有花括号。如果您放置大括号,则要检查的断言是大括号内的表达式(在您的情况下,为空,相当于 true)并且sameBook2Patrons只是命令的名称。

于 2016-02-21T08:04:05.453 回答