search
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
cs-486:homework-2 [2017/01/27 13:00] egm [Problems] |
cs-486:homework-2 [2018/09/04 12:38] egm [Problems] |
||
|---|---|---|---|
| Line 26: | Line 26: | ||
| do | do | ||
| :: schedToCons[me]?task(you) | :: schedToCons[me]?task(you) | ||
| + | :: timeout -> break | ||
| od | od | ||
| } | } | ||
| Line 46: | 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. | ||
