Petri Net assignment

General Information

Update

Due to problems with pipe2, you do not need to provide the reachability/coverability graph. You do however need to compute (with pipe2) place invariants and draw conclusions, and this will be worth the same amount as was given to the previous task.

The assignment: Petri Net modelling, simulation and analysis of a simple traffic system

  1. [50%] Modelling a simplified traffic intersection + analysis: The system depicted below is a four-direction (North, East, South and West) traffic intersection. Each direction has two lanes, i.e. an entrance and an exit.
    There are some constraints about the system as follows:
    1. [8%] At most one car is allowed to be present at the center of the intersection at any moment;
    2. [8%] No U-turns are allowed, e.g. a car entering from North is not allowed to exit to the North;
    3. [8%] The number of cars to enter the intersection from any direction can be infinite;
    4. [8%] Before a car enters the intersection, the direction in which it will exit is determined randomly.
    5. [8%] The progression of cars must be fair.

    (1) [40%] Using the tool pipe2, build and document a Petri Net model of the behaviour of this system. Documentation must describe how the different constraints given above were addressed. Include an image of the model in your solution.

    (2) [10%] Build the coverability graph for this Petri Net and draw some conclusions, including what is conserved in the system.

  2. [50%] Modelling a simplified traffic roundabout (traffic circle) + analysis: The roundabout depicted below is very similar to the intersection. It has four directions (North, East, South, and West) and each one has two lanes: an entrance and an exit. However, there are four arcs at the center of the roundabout.
    There are some constraints about the system as follows:
    1. [7%] At most one car is allowed to be present in each arc of the roundabout at any moment;
    2. [7%] U-turns or circling are allowed, e.g. a car entering from the North may exit to the North;
    3. [7%] Cars may not loop beyond their entry point;
    4. [7%] The number of cars to enter the roundabout from any direction can be infinite;
    5. [7%] Before a car enters the roundabout, the direction in which it exits is determined randomly;
    6. [7%] The progression of cars must be fair.

    (1) [42%] Using the tool pipe2, build and document a Petri Net model of the behaviour of this system. Documentation must describe how you've addressed the different constraints given above. Include an image of this model in your solution.

    (2) [8%] Build the coverability graph for this Petri Net and draw some conclusions, e.g. what is conserved in the system.

Modelling, Simulation, and Analysis

You should use the tool pipe2 which can be downloaded from sourceforge.

Modified Assignment for those who took COMP 763

The assignment remains the same. Instead of doing un-timed modelling with Place/Transition nets, you should use some form of Petri Nets with time (such as Generalized Stochastic Petri Nets -- GSPN). The latter is supported by the tool pipe2. You can learn more about GSPN by downloading the book modelling with generalized stochastic petri nets. Note that fairness will be a direct result of the timing information you will add to the models.