Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
cs-486:homework-0 [2017/01/10 23:57]
egm [Problems]
cs-486:homework-0 [2020/01/12 02:47] (current)
egm [Problems]
Line 6: Line 6:
  
 # ('''​5 points'''​) Download and install the [http://​spinroot.com SPIN model checker]. See the [[Tools]] page for some suggestions. Submit a screen shot from the command '''​spin -?'''​ # ('''​5 points'''​) Download and install the [http://​spinroot.com SPIN model checker]. See the [[Tools]] page for some suggestions. Submit a screen shot from the command '''​spin -?'''​
-# ('''​points'''​) ​Find and run a PROMELA ​file in both simulation ​and verification mode. Capture ​the output ​in a file and submit it for the answer to this problem.+# ('''​20 points'''​) ​Write a PROMELA ​model that starts no more than '''​N'''​ processes randomly where '''​N'''​ is given with a '''#​define'''​. Here the ''​init''​ process is not part of '''​N'''​. Each of the '''​N'''​ processes should output its process ID in the order of creation. After that, each process should then output its process ID in reverse order of creation ​and then exit before the next process reports its ID and exits. Report the number of states found for '''​N = 5'''​ in verification mode.  
 +# Try a variant of the previous model where the '''​N'''​ processes actually exit in the actual order of creation. Explain what happens in this variant of the model? 
 + 
 + 
 +Upload the final file to learning suite.
cs-486/homework-0.1484092622.txt.gz · Last modified: 2017/01/10 23:57 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