##### Differences

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

 cs-486:homework-2 [2017/10/09 16:05]egm [Problems] cs-486:homework-2 [2018/09/04 12:38]egm [Problems] Both sides previous revision Previous revision 2018/09/04 12:38 egm [Problems] 2017/10/09 16:05 egm [Problems] 2017/01/27 13:00 egm [Problems] 2017/01/26 09:36 egm 2017/01/11 11:46 egm [Problems] 2017/01/11 11:36 egm [Problems] 2017/01/11 11:25 egm 2017/01/11 10:28 egm 2017/01/11 10:20 egm 2014/09/02 10:27 egm created 2018/09/04 12:38 egm [Problems] 2017/10/09 16:05 egm [Problems] 2017/01/27 13:00 egm [Problems] 2017/01/26 09:36 egm 2017/01/11 11:46 egm [Problems] 2017/01/11 11:36 egm [Problems] 2017/01/11 11:25 egm 2017/01/11 10:28 egm 2017/01/11 10:20 egm 2014/09/02 10:27 egm created 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.