**This is an old revision of the document!**


  • Download and install SPIN
  • Run a few simple examples with SPIN


  1. (5 points) Download and install the SPIN model checker. See the Tools page for some suggestions. Submit a screen shot from the command spin -?
  2. (20 points) Write a PROMELA model that starts no more than N processes randomly where N is given with a #define. The created processes should exit in the order in which they are created. None of the created processes should run until all the processes are created. Run the model in both simulation and verification mode. Report the number of states found for N = 5 in verification mode. Put that in a comment block in the model.
cs-486/homework-0.1578334995.txt.gz · Last modified: 2020/01/06 11:23 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0