Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel

Assignment 7
Spring 2003

General Information | Schedule | Assignments | Announcements
Assignment 7: Model Checking

Part I

Design an elevator controller, and verify that it satisfies certain temporal properties.

The SMV specification of the elevator is in elev.smv. (A looser specification is in elev-loose.smv.) It models the properties of a real-world, physical elevator. You must write an implementation of the controller module that satisfies all the specifications (SPECs) in the file. You should not modify any part of the file above the line, "Solution begins here."

SMV is installed as /usr/local/smv on shades and penguins; do man smv for detailed information, but basically you can just give the command
% smv elev.smv
to model-check your solution.

In fact, you can do it right now, even without implementing a controller, and you will find that smv complains that some of the temporal properties are not satisfied.

Hints. One problem is that when you start the system, you don't know where the elevator is! That's especially annoying when it starts between floors. While developing your solution, you could say "INIT e.f1.here & open" to postpone dealing with this problem.

I had to write about 45 lines of SMV code. I have two modules, one that is instantiated 3 times (one for each floor) and one for the global controller. I have three state variables per floor and two global state variables; when added to the elevator's 4 variables per floor and 7 globals, that's a total of 30 boolean variables in my solution, which is potentially quite a large state space! SMV checks my model (on the Sparcs) in about 544 seconds (it checks the looser model in 185 seconds).

Part II (optional)

Increase the number of floors from 3 to 4, and compare the amount of time and space that SMV takes to check the model.

Part III

I am interested in the following properties, but I don't believe they can be specified in CTL; they may require CTL*. Include in your file as a comment, an informal argument that
  1. Assuming the following conditions,
    1. Eventually the doorsensor will become 0 and stay 0;
    2. When the elevator stays movingup and not at a floor, eventually it will arrive at a floor;
    3. When the elevator stays movingdown and not at a floor, eventually it will arrive at a floor;
    4. When the elevator stays movingup and at a floor, eventually it will not be at a floor;
    5. When the elevator stays movingdown and at a floor, eventually it will not be at a floor;
    6. If the door stays closing, eventually it will be closed;
    7. If the door stays opening, eventually it will be open;
    then if any button for floor n is pushed, eventually the elevator will arrive at floor n and the door will be open.

  2. If at time t1 the elevator is at floor n, and the door is open, and from this time onwards nobody presses the buttons for floor n, then eventually there will come a time t2, such that after t2 the elevator will never again be at floor n with the door open.

Warning

FAIRNESS constraints seem to be buggy in smv. For example, you could look at this alternate version of the specification, elev-fair.smv, that uses FAIRNESS, but with the following trivial (and wrong) solution, smv claims that all properties are true. 
ASSIGN
  e.movingup   := 0;
  e.movingdown := 0;
  e.closing    := 1;
  e.opening    := 1;