Alloy утверждение не работает, как ожидалось

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 
} 

Так что я хочу добавить, что два Assert Покровитель не может в настоящее время имеет ту же книгу. Вот утверждение я пришел с:

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{} for exactly 2 Book, exactly 2 Patron 

Кроме того, я прочитал, что добавление факта с отрицанием действительного утверждения, как предполагается, не дать ни одного примера. Я добавил, что:

fact sameBook2Patrons { 
    not (all disj p, p': Patron | all b: p.curbooks | b not in p'.curbooks) 
} 

Когда я запускаю модель, сплав находит действительный экземпляр.

Что я делаю неправильно? Спасибо.

Answer 1

Вы ошибочно используете команду проверки. Для того, чтобы проверить утверждение sameBook2Patrons вы должны использовать вместо

check sameBook2Patrons for exactly 2 Book, exactly 2 Patron 

т.е., без фигурных скобок. Если вы поместите скобки, утверждение, которое нужно проверить, - это выражение внутри фигурных скобок (в вашем случае пустое, что равно true), а sameBook2Patrons - это просто имя команды.