Homework 3
Assigned 11/27. Due 12/11
2. Petri Nets.
2a. Consider the diner/waiter Petri net example in slide 5-16. Modify the Petri net to include the action that once the diner receives the food, he/she can return the food (e.g., to have it cooked more), with the waiter then later returning the food.3. Protocol Specification/Verification Using Temporal Logic. Consider the sender's timer in the data transfer protocol shown on notes page page 5-23. The timer will have three states: running, stopped, and timed out.
2b. Modify the Petri net in Figure 5-17 so the timer events will only fire when a message associated with the timer has been lost.
3a. Give the temporal logic statement that states that if the timer is running and is never canceled, then the timer will eventually timeout. Note that your statement should only contain the three timer states identified above, and various logical operators.
3b. What are the specifications for the timer's three services (timer,start, timer.cancel, timeout)? These specifications should be given in terms of temporal logical operators, other logical operators, and timer state values. See, e.g., the pre-post- and liveliness conditions for the medium on page 60 (bottom of column) of Hailpern's paper (although note there is no explicit state variable involved for the medium).
4. Self-Stabilization. Consider the sample execution
of the diffusing computation on page 6-7 in the notes, and consider the
second tree in the third row (the root is red, both children of the root
are red, and the left-child of each root-child is red and the right-child
of each root-child is green). Given two examples (which differ in the order
and nature of state transitions) that show the sequence of state transitions
that result in the self stabilizing computation eventually turning the
tree all green. For each transition, indicate which event (s1, s2,
or s3 on page 6-6 is executed at which node, and the corresponding value
of sn.j a that node).
As I noted in class, I left out an important sentence from the homework
problem statement above. You can do the above question (which is
trivial given the missing sentence), or do the following version of the
problem for extra credit. You only need to do either the question
4 above or question 4 below. The missing sentence is shown in red
below
4. Self-Stabilization. Consider the sample execution of the diffusing computation on page 6-7 in the notes, and consider the second tree in the third row (the root is red, both children of the root are red, and the left-child of each root-child is red and the right-child of each root-child is green). Now suppose that the state in the left-child of the root is corrupted so that its color changes spontaneously from red to green. Given two examples (which differ in the order and nature of state transitions) that show the sequence of state transitions that result in the self stabilizing computation eventually turning the tree all green. For each transition, indicate which event (s1, s2, or s3 on page 6-6 is executed at which node, and the corresponding value of sn.j a that node).