CSSE 373 Formal Methods in Specification and Design

HW5

Purpose: practice reading and describing Alloy models, demonstrate individual understanding of your project so far

This homework assignment includes questions about your project; however, it is still an individual assignment.

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. Download my time-based solution to P1, liftPrelimT.als. Open the model in Alloy and execute the included check OnlyValid for 5 but exactly 5 Floor, 25 Time command. Alloy should find no counterexamples.
3. Answer the following questions about the provided solution:
   1. Suppose a lift l had no planned direction at time t. What would be the value of l.plannedDirection[t]?
   2. Why is requestsPending defined as a separate function?
   3. What is the purpose of the initTime predicate?
   4. A valid transition between two successive instances of Time, is defined (in the ValidTransitions predicate) as any transition allowed by the someChange predicate. What four predicates are used by someChange to define the valid transitions?
   5. A valid instance in time is defined by the Valid predicate. In English, what must be true at an instance in time for it to be valid? (That is, describe the conditions that hold, don’t just say that ValidIndicators and ValidRequestLights must both be true.)
   6. Each of the operation predicates (move, requestFloor, openDoors, and closeDoors) call a set of helper predicates, no…ChangeExcept. What is the purpose of the calls to these helper predicates?

   7. The OnlyValid assertion says that if the system configuration is valid at one instance in time, then it is also valid at the next instance in time.

      • What constraint could we add to OnlyValid to assert that the first instance in time is valid?
      • Add your constraint to the model; the improved assertion should still hold.
      • Comment out some lines from initTime to cause the improved assertion to have a counterexample. What lines did you comment out? (Be sure to uncomment them when you’re done.)
   8. Since OnlyValid checks all allowed transitions, what use are assertions like OnlyValid_Move and OnlyValid_Open that just check specific operations and constraints?

4. Compare my provided solution to the one you (and your team) developed for P1. Describe the major differences between my model and yours. For each major difference, indicate whether you think the difference is significant (i.e., makes one model more expressive than the other) or just incidental (i.e., a matter of style or personal preference).

   I’ll evaluate your description based on:

   • the level of understanding of the two models that you demonstrate, and
   • the clarity and conciseness of your writing.

   Please include (small) code snippets in your description if that helps you make your point.

5. Turn in your work by committing a pdf file containing your answers to the appropriate HW folder in your individual subversion repository for this course.