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-2 [2017/10/09 22:05]
egm [Problems]
cs-486:homework-2 [2018/09/04 18:38] (current)
egm [Problems]
Line 47: Line 47:
  
 '''​4. (50 points)'''​ Write a PROMELA verification model for [https://​www.risc.jku.at/​software/​daj/​TermDetect/​ Dikstra'​s Token Termination Algorithm] (another [http://​people.cs.aau.dk/​~adavid/​teaching/​MVP-10/​17-Termination-lect14.pdf presentation]) and use SPIN to prove that the verification model is correct. Make the verification model be parameterized by '''​N'''​ the number of nodes participating in the system. '''​4. (50 points)'''​ Write a PROMELA verification model for [https://​www.risc.jku.at/​software/​daj/​TermDetect/​ Dikstra'​s Token Termination Algorithm] (another [http://​people.cs.aau.dk/​~adavid/​teaching/​MVP-10/​17-Termination-lect14.pdf presentation]) and use SPIN to prove that the verification model is correct. Make the verification model be parameterized by '''​N'''​ the number of nodes participating in the system.
 +* '''​(25 points)'''​ All nodes are passive, the token goes one-time around, and the system terminates
 +* '''​(10 points)'''​ Exactly one node is active, but it does not send any messages, and when it receives the token, it switches to passive and sends the token out black
 +* '''​(10 points)'''​ The one active node may send at most one message total, and that message can be to to any other node; if a node receives a message causing it to become active, then it too may only send at most one message even if it is again activated by an incoming message; in this way, there can never be more than '''​N'''​ messages ever sent. The node non-deterministically chooses if it will send a message or not. 
 +* '''​(5 points)'''​ Any node may start active (one message bound still applies)
 +Please note that messages related to the token do not count in the send/​receive counters. Also note that a node becomes passive once it receives a token.
cs-486/homework-2.txt ยท Last modified: 2018/09/04 18:38 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