• The due date is Sunday 16 November 2014, before 23:55.
  
  
• Submissions must be done via Blackboard. Beware that Blackboard's clock may differ slightly from yours.
  
  
• The assignment must be made in groups of two students.
  
  
• 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 !
  
  
• Contact: Bart Meyers.
  
  

Petri Net modelling, simulation and analysis of a chat room protocol

You will use the Petri net tool Pipe2 v. 2.5 (don't use the latest Pipe2 version; there are numerous bugs). To start Pipe2, run pipe.bat (Windows) or pipe.sh (Linux/Mac).

The assignment consists of four parts.

1. Build and document a Petri Net model of a chat room protocol. You can use places, transitions, tokens, arcs, inhibitor arcs and weights, but not priorities! Give your places and transitions meaningful names, to make your net readable. You can also use comments in your net. The requirements for the protocol are as follows:
• (7 %) A chat room has three users who can send and receive messages. A sent message is received by all users except the sender;
• (7 %) The sent messages are buffered by the chat room. The buffer has size 2;
• (7 %) A sent message is cleared from the buffer when all users (except for the sender, who should not receive a copy of the message s/he sent) have received *that* message. Messages from one sender arrive in the same order as they have been sent. The order among different senders may be changed upon arrival;
• (7 %) The messages are sent in a fair way: every user has exactly one chance per time cycle to send a message. A user *must* send a message if s/he can: when a user has a message to be sent (i.e., the user has something to say) and the buffer is not full;
• (10 %) Implement "true" fairness: the order of interleaving of events (i.e., of firing of transitions) within one time slice is nondeterministic;
• (7 %) To be able to analyse performance, the following counters must be modelled: the number of time cycles, how many messages each user sent, and how many messages each user received.
2. (10 %) Perform an appropriate number of simulation steps of this protocol so that its possibilities are illustrated, and comment.
3. Analyse your Petri net in terms of:
   • (5 %) boundedness: if your net is bounded, argue why. If not, argue what can be modified to make it bounded;
   • (5 %) deadlock: if your net is deadlock free, argue why. If not argue what can be modified to make it deadlock free;
   • (5 %) reachability: which (partial) states are reachable and which are not?
   • (5 %) liveness: what is the liveness level for each transition?
   • (5 %) persistence: argue for each transition whether it is persistent;
   • (5 %) invariants: what are the invariants in the system, and what do each of them mean?
   • (5 %) can the buffer overflow? Argue why (not).
4. (10 %) Write a report commenting on and illustrating all previous sections.