Differences

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

Link to this comparison view

Both sides previous revision Previous revision
cs-486:homework-6 [2017/03/07 21:21]
egm [Problems]
cs-486:homework-6 [2017/03/10 22:54] (current)
egm
Line 17: Line 17:
 '''​4. (20 points)'''​ Consider again [[Homework 2 | Homework 2 Problem 4]] to model Dijkstra'​s Token Termination algorithm. Verify the following properties using never claims on your model. Modify the model as needed so the algorithm passes verification. Check each property for several number of nodes '''​N'''​ and messages '''​M'''​. ​ '''​4. (20 points)'''​ Consider again [[Homework 2 | Homework 2 Problem 4]] to model Dijkstra'​s Token Termination algorithm. Verify the following properties using never claims on your model. Modify the model as needed so the algorithm passes verification. Check each property for several number of nodes '''​N'''​ and messages '''​M'''​. ​
 * A process when black eventually becomes white * A process when black eventually becomes white
-* A process only turns black if it receives a message+* A process only turns black if it receives a message ​or sends a message to a process with a smaller ID
 * A process receiving a token eventually sends out the token * A process receiving a token eventually sends out the token
 * The system only terminates when there are no outstanding messages * The system only terminates when there are no outstanding messages
  
 '''​5. (20 points)'''​ Explain the difference between the ''​accept''​ and ''​progress''​ labels. Write a PROMELA verification model to illustrate the difference and show the output from SPIN.  '''​5. (20 points)'''​ Explain the difference between the ''​accept''​ and ''​progress''​ labels. Write a PROMELA verification model to illustrate the difference and show the output from SPIN. 
cs-486/homework-6.txt ยท Last modified: 2017/03/10 22:54 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