Princeton University Computer Science Dept.

Computer Science 496 Automated Theorem Proving Andrew W. Appel

Spring 2001

Part I

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)

Announcements

ASSIGN
  e.movingup   := 0;
  e.movingdown := 0;
  e.closing    := 1;
  e.opening    := 1;

(April 3, 2001, 1:35 p.m.) The last two specifications,

  SPEC  (AG ((AF ! (doorsensor & open)) &
             (AF ! (movingup & at_a_floor)) &
             (AF ! (movingdown & at_a_floor)) &
             (AF ! (movingup & !at_a_floor)) &
             (AF ! (movingdown & !at_a_floor)) &
             (AF ! (closing & !closed)) &
             (AF ! (opening & !open)))) ->
        AG (f1.anybutton -> (AF AG !doorsensor) -> (AF open & f1.here))
  SPEC AG ((f1.here & open & AG !f1.anybutton) -> AF (AG !(f1.here & open)))

I would like you to 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 t₁ 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 t₂, such that after t₂ the elevator will never again be at floor n with the door open.