• The due date is Monday 7 December 2020, 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: Randy Paredis.
  
  

Petri Net Modelling, Simulation and Analysis of an Assembly Line

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 visualization of it. 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 Randy 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 an assembly line.

You can use places, transitions, tokens, arcs, and weights, but you MUST NOT use priorities, timed transitions, capacities or 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. d) Scrolling over a place increases/decreases its number of tokens, while scrolling over a transition rotates it.

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

The assembly line structure and dynamics is as follows:

• (7 %) Cubes and cylinders arrive at an assembly line. The Assembler merges two cubes and one cylinder into a single assembly.
• (7 %) The Assembler passes the assembly on to an Inspector, who decides if the assembly is to be accepted, trashed or remade/fixed. Assemblies to be remade are sent back to the Assembler. How they are ordered w.r.t. the arriving shapes is up to you, but make sure you clearly describe which choice you've made and why.
• (7 %) Both the Assembler and the Inspector can only handle a single assembly at a time.
• (10 %) The system makes use of a clock. The following logic happens every "timestep":
  1. A new shape arrives (either a cube or a cylinder).
  2. If the Assembler is busy, shapes are enqueued.
  3. If the Assembler is idle, it may start making/reassembling an assembly.
  4. If the Inspector is busy, assemblies are enqueued.
  5. If the Inspector is idle, it may start inspecting an assembly
• (7 %) The Assembler takes at least four time-units, whereas the Inspector needs a minimum of two.
• (7 %) 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, the amount of accepted assemblies, the amount of trashed assemblies and the amount of times an assembly was sent for "fixing".
• (10 %) Simulate the following cases and report on them, with explanatory text and figures:
  • The Assembler finished an assembly at the exact same timestep the Inspector marks an assembly for reassembly.
  • There is an assembly waiting for reassembly (i.e., it is to be fixed) and at that exact time the third component of an assembly arrives.

Analysing the Petri Net using PIPE:

For each of the topics below, report the procedure you used to determine the results as well as the results themselves. Do make sure your PIPE results correspond to the asked requirement.

• (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 two cylinders and a cube arriving. Report the subset of behaviour you selected, the graph, and what the regions of the graph represent.
• (5 %) Invariant Analysis: Use the Invariant Analysis module to obtain information about the invariants in your system.
  • Which invariants did you expect? Which ones are surprising? Why?
  • Can you add a single state that changes these invariants (for the better or worse)?
  • Include the generated HTMLs of the analysis in your submission.

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.

• (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.
• (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.
• (2.5 %) Queue Overflow: Create and discuss a LoLA verification formula to determine whether or not a queue in the system can overflow. Such an overflow happens if there are more than 10 items waiting to be processed by an Assembler/Inspector. What are the characteristics of your solution that allow or prevent this from happening?
• (2.5 %) Liveness: Pick an (interesting) transition in your 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.
• (3 %) Fairness: Prove that you've implemented "true" fairness

Now, add a predefined stock of 53 cubes and 18 cylinders and redo the analysis. What remains consistent? What changes? Why?

Report:

(10 %) Write a report (in PDF form) commenting on and illustrating all previous sections. Make sure you include images and traces of all your models!