assertion - 合金断言没有按预期工作

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
}

所以我想添加一个断言，即两个 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 会找到有效的实例。

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

Answer 1

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

check sameBook2Patrons for exactly 2 Book, exactly 2 Patron

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