CMU MSE 15-761, Models of Software Systems, Fall 1995

Petri Nets

Garlan & Wing, Homework 13, Due: November 4, 1995

1. Consider the familiar situation of a student and a teacher:

The Student repeatedly does her homework, hands it in, and gets a pass or fail -- cheering when she passes and cursing when she fails.

The Teacher repeatedly collects the homework, (non-deterministically) assigns a pass/fail grade -- grumbling whenever he has to give out a failing grade.

Write a Petri Net description of the HW Process.

2. For the P/V Petri Net shown in Figure 15 of Peterson's article:

a. Construct the reachability tree.

b. Use this to argue that the design is correct: that it is not possible for the system to be simultaneously in the critical sections of both processes.

3. The Elevator Petri Net example discussed in Lecture 17 has the unfortunate property that if a user is not on the floor of the elevator the system will deadlock.

a. Write an improved version of the net so that this won't occur.
b. Explain why your Petri Net will not deadlock.
c. Is your Petri Net fair? (You may pick any notion of fairness that you like.)