Alloy assertion does not work as expected

Question

Here is my alloy code:

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
}

So I want to add an assert that two Patron cannot currently have the same book. Here is the assertion I came with:

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

So when check the assertion with:

check sameBook2Patrons{} for exactly 2 Book, exactly 2 Patron

Alloy does not find any counter-example. But when I use the run command, Alloy gives me plenty of counter example:

run{} for exactly 2 Book, exactly 2 Patron

Also, I read that adding a fact with the negation of a valid assertion is supposed to give no instance. I added that:

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

When I run the model, Alloy finds valid instance.

What am I doing wrong? Thank you.

note that using the run command does not produce counter examples but instances satisfying your alloy specification. — Loïc Gammaitoni

Alcino Cunha Alcino Cunha · Accepted Answer · 2016-02-21T08:04:05

You are using the check command wrongly. To check the assertion sameBook2Patrons you should instead use

check sameBook2Patrons for exactly 2 Book, exactly 2 Patron

i.e, without curly braces. If you put the braces, the assertion to be checked is the expression inside the braces (in your case, empty, which is equivalente to true) and sameBook2Patrons is just the name of the command.

Alloy assertion does not work as expected

1 Answers