Purpose: dust off some more discrete math skills, experiment with the Alloy Analyzer
This is a team homework assignment. All work must be done by the team members together. All team members should understand all work submitted. If you have concerns about your own understanding or that of your teammates, please let me know. I want everyone to learn all they can in this course!
Do your work in your Homework Team SVN repository for the course. Your team number and the SVN repository URL are listed in the slides for session 7.
The first set of problems on this homework is based on A.1.1 from Software Abstractions. I modified it a bit to be, uh, less abstract.
Enter the following Alloy model in the Analyzer:
module homework/hw02_1
sig Person { likes: set Person }
pred show {
some likes -- nonempty
likes.likes in likes -- transitive
no iden & likes -- irreflexive
~likes in likes -- symmetric
~likes.likes in iden -- functional
likes.~likes in iden -- injective
Person in likes.Person -- total
Person in Person.likes -- onto
}
run show for 4
Each constraint in the show predicate constrains the likes relation according to one standard property of a binary relation. All of these properties cannot hold at once, so if you execute the run command, Alloy should report No instance found.
fact to the model stating that at least 4 Person atoms exist. Copy and paste that fact into your answers for this homework.
Comment out all but one constraint within the show predicate. (You can use /* ... */ for block comments.) Execute the run command and visualize the results. Use Next to step through the results.
For each constraint, give a plain-English analogy for the corresponding property. A couple of examples are given below to get you started. (You can also use other sources to look up the properties. Please indicate any external sources used, and please try to see how the Alloy results correspond to the property.)
Next you’ll try eliminating one constraint at a time. Uncomment all the constraints. Comment out a single constraint. (You can use -- or // for single line comments.) Execute the run command and see if the constraints can be satisfied with just that single constraint eliminated. Try this for each constraint.
For each constraint indicate either that the remaining properties are still not satisfiable, or if they are satisfiable, give an example of a satisfying relation. (You can use the Evaluator in the Visualizer to get a textual representation of the likes relation.)
The second set of problems is based on A.1.2 from Software Abstractions, modified as above.
In part 2 above, the non-emptiness property was written in relational calculus style as some likes. This says the likes relation has some things in it. Those things are pairs of Persons.
For this problem, your task will be to write the properties from above in predicate calculus style. Recall (from p. 33–35 of the text) that this style involves identifying some elements and relations and making statements about tuples formed from the elements.
For example, the non-emptiness property in relational calculus style would be written:
some p1, p2: Person | p1->p2 in likes
This says that p1 and p2 are Persons and that there is a pair (p1,p2) in the likes relation. Thus, the likes relation is non-empty.
A cool property of Alloy is that it can check your answers for you. You’ll see how to do that below.
Enter the following Alloy model in the Analyzer:
module homework/hw02_2
sig Person { likes: set Person }
assert NewNonEmptinessOK {
some likes iff
(some p1, p2: Person | p1->p2 in likes)
}
check NewNonEmptinessOK
assert NewTransitivenessOK {
(likes.likes in likes) iff
(no likes) // replace constraint with your answer
}
check NewTransitivenessOK
assert NewIrreflexiveOK {
(no iden & likes) iff
(no likes) // replace constraint with your answer
}
check NewIrreflexiveOK
assert NewSymmetricOK {
(~likes in likes) iff
(no likes) // replace constraint with your answer
}
check NewSymmetricOK
assert NewFunctionalOK {
(~likes.likes in iden) iff
(no likes) // replace constraint with your answer
}
check NewFunctionalOK
assert NewInjectiveOK {
(likes.~likes in iden) iff
(no likes) // replace constraint with your answer
}
check NewInjectiveOK
assert NewTotalOK {
(Person in likes.Person) iff
(no likes) // replace constraint with your answer
}
check NewTotalOK
assert NewOntoOK {
(Person in Person.likes) iff
(no likes) // replace constraint with your answer
}
check NewOntoOK
Notice the first assertion at the top of the model, named NewNonEmptinessOK. The body of this assertion is:
some likes iff (some p1, p2: Person | p1->p2 in likes)
This asserts that the non-emptiness property expressed in the relational calculus style as:
some likes
is equivalent to the property expressed in the predicate calculus style as:
(some p1, p2: Person | p1->p2 in likes)
The check NewNonEmptinessOK command tells Alloy to look for counterexamples that disprove the assertion. In Alloy, use the Execute menu to execute the NewNonEmptinessOK check. You should see something like this in the output pane:
Executing "Check NewNonEmptinessOK" Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 91 vars. 12 primary vars. 163 clauses. 4ms. No counterexample found. Assertion may be valid. 0ms.
(no likes) constraint with an appropriate predicate calculus style one. Execute the check in Alloy to verify that your predicate calculus style constraint is equivalent to the relational calculus one on the left-hand side of the iff.