SE-561

Formal Methods in Software

Homework Assignment 5 (Due Thursday, Dec. 7)

Consider the following Petri net model for the five philosophers dining problem. Please convert it to a high-level Petri net model. Write down the set of token values for each place, the firing condition for each transition and the initial marking.

Legends:

    thi: philosopher i is thinking, i = 1, 2, 3, 4, 5

    ei: philosopher i is eating

    ci: chopstick i is available

    ai: philosopher i begins eating

    bi: philosopher i finishes eating

(Note that place c1 is duplicated in the model for nice graph.)