这是我的合金代码:
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 会找到有效的实例。
我究竟做错了什么?谢谢你。