##### Differences

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

 cs-486:homework-0 [2020/01/06 11:23]egm [Problems] cs-486:homework-0 [2020/01/11 19:47] (current)egm [Problems] Both sides previous revision Previous revision 2020/01/11 19:47 egm [Problems] 2020/01/11 17:27 egm [Problems] 2020/01/11 16:55 egm [Problems] 2020/01/06 11:23 egm [Problems] 2017/01/10 16:57 egm [Problems] 2017/01/10 16:54 egm created Next revision Previous revision 2020/01/11 19:47 egm [Problems] 2020/01/11 17:27 egm [Problems] 2020/01/11 16:55 egm [Problems] 2020/01/06 11:23 egm [Problems] 2017/01/10 16:57 egm [Problems] 2017/01/10 16:54 egm created 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 -?'''​ - # ('''​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. + # ('''​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.