SE-561

Formal Methods in Software

Homework Assignment 4 (Due Thursday, Nov. 30)

1. Consider the Petri net in lecture slide FM-10 4.
       a. How many times can transition t3 fire?
       b. What is the final marking?
 

2. Modify the Petri net model slide FM-10 17 such that a new mail can be 

    sent to the mailbox only if the mailbox is empty.

 

3. Consider the river-crossing puzzle. Suppose that
    -- the wolf will eat the goat if, and only if, the wolf and goat are on the same
       bank while the man is on the other bank; and

    -- the goat will eat the cabbage if, and only if, the the goat and cabbage are

       on the same bank while the man and wolf are on the other bank.

    Please model all these possible meal events in one Petri net using a tool,

    and print out the screenshot.