Please may attention to the following to get you up and running for
your Spin assignment.

1. Install jSpin and not Spin. You are free to use Spin if you please
but jSpin provides a graphical interface which I believe will simplify
your work.

Download jSpin from this link: http://code.google.com/p/jspin/

2. There is a very ice tutorial on Promela at this link which i
believe will help you out:

http://spinroot.com/spin/Man/Manual.html

3. If you choose to model the properties with assert, progress or
accept, please put the model for each property in a different file and
dont but the asserts, etc for different properties in one file. For
instance, if you are using assert to verify property P1 for
one-light.pml, put you model in a file named P1-one-light.pml so I
would now this model is for one-light along with assertions verifying
property P1.