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

Both sides previous revision Previous revision | |||

cs-486:homework-2 [2017/10/09 16:05] egm [Problems] |
cs-486:homework-2 [2018/09/04 12:38] 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. |