这是我的合金代码：
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
}
所以我想添加一个断言，两个赞助人目前不能拥有相同的书 . 这是我带来的断言：
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找到有效的实例 .
我究竟做错了什么？谢谢 .
1 回答
您错误地使用了check命令 . 要检查断言
sameBook2Patrons，您应该改为使用即没有花括号 . 如果你把大括号，要检查的断言是大括号内的表达式（在你的情况下，为空，等于true），
sameBook2Patrons只是命令的名称 .