CSSE 373 Formal Methods in Specification and Design

HW2

Purpose: dust off some more discrete math skills, experiment with the Alloy Analyzer

1. Keep track of how much time you spend on this assignment. You will submit your answers as a pdf file at the end of the homework.

2. The problems on this homework are based on A.1.1 from Software Abstractions. Enter the following Alloy model in the Analyzer:

   module homework/HW2
   
   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.

3. Add a fact to the model stating that at least 4 Person atoms exist. Copy and paste that fact into your answers for this homework.

4. 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.)

   1. nonempty: __________________________________
   2. transitive: a friend of my friend is my friend
   3. irreflexive: __________________________________
   4. symmetric: Barney says, "I love you, you love me..."
   5. functional: __________________________________
   6. injective: Only liked by one. Also, "a face only a mother could love"
   7. total: __________________________________
   8. onto: __________________________________

5. 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.)

   1. dropping nonempty: __________________________________
   2. dropping transitive: __________________________________
   3. dropping irreflexive: __________________________________
   4. dropping symmetric: __________________________________
   5. dropping functional: __________________________________
   6. dropping injective: __________________________________
   7. dropping total: __________________________________
   8. dropping onto: __________________________________
6. Turn in your work by committing a pdf file containing your answers to the HW2 folder in your individual subversion repository for this course.
7. Please complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)