• UPDATED The due date is Friday 16 December 2011, before 23:55.
  
  
• Submissions must be done via BlackBoard. Beware that BlackBoard's clock may differ slightly from yours. All results must be uploaded to BlackBoard and accessible from links in the index.html file. There is no need to upload pipe2.
  
  
• The assignment must be made in groups of maximum 2 people. It is understood that all partners will understand the complete assignment (and will be able to answer questions about it). Clearly identify who did what.
  
  
• Grading will be done based on correctness and completeness of the solution. Do not forget to document your requirements, assumptions, design, implementation and modelling and simulation results in detail!
  
  
• Extensions, if given, will involve extending not only the alotted time, but also the assignment !
  
  

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. Note that this means you'll have to introduce some notion of (Petri net model of) time.

   (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.
   update: due to limitations in pipe2, you should only generate the coverability graph for a simplified model (1 car from each direction). Note that pipe2 will be able to determine invariants as it calculates without explicitly building the coverability graph

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. Note that this means you'll have to introduce some notion of (Petri net model of) time.

   (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.

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