Specification and Verification Tools Seminar
			      Homework 5
		     $Date: 2008/11/06 04:45:58 $


For 19 November 2008. 

Download and install Spin from http://spinroot.com/spin/Man/README.html . 

As mentioned in the instructions, you can also install the graphical
front-end, XSpin.  However, this is not necessary and its not that
difficult to use Spin from the command line.

You may find the following links helpful:

Basic Spin manual: http://spinroot.com/spin/Man/Manual.html Concise
Promela Reference: http://spinroot.com/spin/Man/Quick.html Building
and Verifying Spin Models: http://spinroot.com/spin/Man/Roadmap.html
(This discuses the various options that can be given to the spin
command, when compiling the verifier (pan.c) generated by spin, and
also when running 'pan'.)


PROBLEM

The homework problem is about writing and checking properties of a
Promela model of an elevator system. The model handed out in class can
be downloaded from: http://spinroot.com/spin/Doc/course/elevator.pml

Specify and check any one (or all!) of the following properties: 

a) The elevator never moves with its doors open.
b) A passenger cannot get stuck at either W1 or W2 at a permanently
   false wait-condition. 
c) If there is at least one request, the controller will eventually
   service at least one request. 

Note: On my Linux machine, trying to execute 'pan' (after compiling
pan.c) gave the message "error: max search depth too small". So, I
increased the search depth using the option -m. '$ ./pan -m1000000'
worked for me.


Note: This problem is due to Gerard Holzmann ( http://spinroot.com/gerard/ )
and the homework was selected by Faraz Hussain.