• The due date is Thursday 21 November 2019, 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 (maximum) 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: Bentley James Oakes.
  
  

Petri Net Modelling, Simulation and Analysis of a Chat-Room Protocol

The assignment consists of two main parts - a) building the Petri Net model and b) its analysis.

Tool Installation and Usage Instructions:

PIPE v4.3.2

You will use the Petri net tool PIPE v4.3.2.

• Unzip the folder
• You MUST replace the pom.xml in the PIPE directory with this one. It updates the dependencies to allow PIPE to be built.
• Ensure that Maven is installed. On Linux, this is best done through the package manager as `maven`. Otherwise, check the Maven website.
• Use the command line within that folder to run `mvn install`.
• To run, execute the command `mvn exec:exec` on the command-line within the PIPE folder..

LoLA

LoLA is a command-line Petri Net analysis tool. Download it from here and see the README for compilation and install directions.

LoLA has a comprehensive manual available within the `doc` folder. This describes analysis possibilities and commands.

Converting PIPE Files to LoLA Format

LoLA uses a different file format than PIPE. To convert your files, you can use the Python scripts available here.

• LoLAConvert.py - takes a filename of a PIPE net as an argument, and produces the LoLA version.
• Example: `python LoLAConvert.py dining_philo.xml`
• LoLADraw.py - takes a filename of a LoLA net, and produces an SVG. Use this to verify correct conversion.
• Example: `python LoLADraw.py dining_philo.lola`

It is your responsibility to double-check that the produced LoLA net matches the PIPE version and make modifications. That said, please email Bentley if there are issues with the conversion process and include an example file.

Building the Petri Net using PIPE:

Build and document a Petri Net model of a chat room protocol.

You can use places, transitions, tokens, arcs, and weights, but you *MUST NOT* use priorities, capacities, inhibitor arcs! Note that the restriction on inhibitor arcs comes from the analysis tool LoLA, which cannot handle them.

Layout: You must make your net as readable as possible. Tips: a) Give your places and transitions meaningful names. b) Use annotations in your net. Right-click on annotations to make them transparent. c) Right-click on an arc to insert new points, so that your diagram is nicely laid out.

Documentation: Your report must explain the components of your Petri Net, and give an intuition to its behaviour.

The requirements for the chat room protocol are as follows:

1. (7 %) A chat room has three users who can send and receive messages. A sent message is received by all users except the sender;
2. (7 %) The sent messages are buffered by the chat room. The buffer has size 2;
3. (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 they 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;
4. (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 they can: when a user has a message to be sent (i.e., the user has something to say) and the buffer is not full;
5. (10 %) Implement "true" fairness: the order of interleaving of events (i.e., of firing of transitions) within one time slice is nondeterministic;
6. (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.

(10 %) Simulate the following cases and report on them, with explanatory text and figures:

• The first user and the third user send a message on the same time step. Both messages are buffered before being sent.
• The second user sends one message on one step, and another on the next step. Both messages are buffered before being sent.

Analysing the Petri Net using LoLA:

For each of the topics below, report the procedure you used to determine the results as well as the results themselves.

Some of the analyses below may run for a while on your solution. Consider the analysis to run forever if it has searched hundreds of thousands or millions of states. If this is the case, argue why this analysis could take forever as well as if/why this proves the analysis property. Hint: Section 5.2 of the LoLA manual discusses flags for early termination of analysis.

1. (5 %) Reachability:
• Argue why your solution would or would not produce an infinite reachability graph.
• Use the Reachability/Coverage module of PIPE to generate a reachability graph of a subset of the behaviour of your solution. For example, the possible states for the first and second users sending (or not) one message each. Report the subset of behaviour you selected, the graph, and what the regions of the graph represent.
2. (5 %) Boundedness: Use LoLA to analyse whether each place in your solution is bounded, and if so, what the k-boundedness is. Explain the formulas you ran, and analyse the results
• Hint: Use scripting to automate this checking;
• There is a Python script `LoLARunner.py` available here. It can loop through places and run a LoLA formula on them. Feel free to modify this file or write your own script.
3. (5 %) Deadlock: Use LoLA to determine if there is a deadlock.
• If there is, what firings cause the deadlock, and how can your solution be modified to make it deadlock-free? Hint: Section 8.1 and 8.2 of the LoLA manual specify flags for producing markings and paths for non-satisfied properties.;
• Run the command with and without the `--search='cover'` flag and analyse the results.
4. For the analyses below, add a new place to the solution such that only ten timecycles are executed.
5. (5 %) Buffer Overflow: Create and discuss a LoLA verification formula to determine whether or not the buffer can overflow in this restricted solution, and the results. What are the characteristics of your solution that allow or prevent this from happening?;
6. (2.5 % Restricted Deadlock: Use LoLA to determine if the restricted solution is deadlocked.
7. (2.5 %) Liveness: Pick an (interesting) transition in this restricted solution. Use LoLA to determine if this transition is live. If the transition is not live, explain the conditions in which it becomes not live;
8. (5 %) Invariants: Create and discuss an (interesting) LoLA invariant formula for this restricted solution. Argue why it is interesting and the result;
9. (5 %) Persistence: Choose (an interesting) pair of transitions in this restricted solution. Use LoLA's verification of CTL to check whether: a) a firing of transition X means that *there exists* a reachable marking where transition Y is non-live, and b) a firing of transition X means that *in all* subsequent reachable markings, transition Y is non-live. Discuss why this pair is interesting, the logic formulae you checked, and the results;

Report:

(10 %) Write a report (in PDF form) commenting on and illustrating all previous sections.