Alloy draws the example that breaks a claim
Alloy is a tool for checking a model made of sets of things and the links between them. It looks for a small example that breaks a claim, and prints that example as things and links.
Reading that example is how you learn what your model forgot to forbid.
By the end of this lesson
Note
I can read the counterexample Alloy gives for a claim about a model.
Key words
| Word | What it means | Example |
|---|---|---|
| Signature | a set of things in the model | sig Student |
| Relation | links from one set of things to another | |
| Fact | a rule the model always obeys | |
| Assertion | a claim you ask Alloy to check | |
| Scope | the most things of each kind Alloy tries | |
| Counterexample | an example that breaks the claim |
The cells students fill in are left blank in this preview.
A model is sets and relations
Alloy needs no steps. You list the kinds of thing, how they link, and the rules. A sig is a set of things. A field inside it is a relation.
Here a student has at most one mentor, written lone. A fact is a rule. An assert is a claim, and check asks Alloy to look for a counterexample.
Worked example: the mentor model line by line
| Line | What it says |
|---|---|
| sig Student { mentor: lone Student } | students, each with at most one mentor |
| fact noSelfMentor { no s: Student | s.mentor = s } | nobody is their own mentor |
| assert NoLoops { no s: Student | s in s.^mentor } | claim: nobody is in their own chain of mentors |
| check NoLoops for 4 | search for a counterexample with up to 4 students |
| run Pair { some mentor } for 3 | show any example where somebody has a mentor |
The cells students fill in are left blank in this preview.
Write the model
printf '%s\n' 'sig Student { mentor: lone Student }' 'fact noSelfMentor { no s: Student | s.mentor = s }' 'assert NoLoops { no s: Student | s in s.^mentor }' 'check NoLoops for 4' 'run Pair { some mentor } for 3' > mentor.alsShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Run both commands
alloy mentor.als | head -n 2Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
For a check, SAT means a counterexample
Alloy prints SAT when it found an instance and UNSAT when it found none. For a run, SAT is good news: here is an example. For a check, SAT is bad news: the claim has a counterexample.
The mark ^ means "follow the link one or more times". So s.^mentor is every student you reach from s by going up the chain of mentors.
Read the counterexample
alloy mentor.als | grep -A 3 'found by NoLoops'Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Repair the model with a real rule
The model forgot the real rule: a mentor is in a later year than their student. Adding it as a fact rules out every loop, because years cannot go up for ever around a circle.
Do not copy the assertion into a fact. That passes the check and says nothing new about students. The next Runs add a year and the rule.
Write the repaired model
printf '%s\n' 'sig Student { mentor: lone Student, year: one Int }' 'fact noSelfMentor { no s: Student | s.mentor = s }' 'fact seniorMentors { all s: Student | some s.mentor implies s.mentor.year > s.year }' 'assert NoLoops { no s: Student | s in s.^mentor }' 'check NoLoops for 4' 'run Pair { some mentor } for 3' > senior.alsShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Run the repaired model
alloy senior.als | head -n 2Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A common mistake
Warning
Many people think UNSAT for a check proves the claim for any number of students. Alloy only searched up to the scope, here 4. Most faults show up in a small example, so a clean check is strong evidence. It is not a proof for every size.