you can run the nifty interface to SPIN by typing: ~jones/bin/xspin. Or if you have ~jones/bin in our path, you can just type xspin. There are some promela models in ~jones/Test/. Have fun!