• Due Date: Wednesday 30 November 2022, before 23:59.
• Team Size: 2 (pair design/programming)!
  Note that as of the 2017-2018 Academic Year, each International student should team up with "local" (i.e., whose Bachelor degree was obtained at the University of Antwerp).
• Submission Information: Only one member of each team submits a full solution. This must be a compressed archive (ZIP, RAR, TAR.GZ...) that includes your report and all models, images, code and other sources that you have used to crate your solution. Do not submit any executables. The report may be either HTML or PDF and must be accompagnied by all images. When an image is unreadable in your report and missing from your submission archive, you will not receive any points for that task. Make sure to mention the names and student IDs of both team members. The other team member must submit a single HTML file containing only the coordinates of both team members. You may use this template. This will allow us to put in grades for both team members in BlackBoard.
• Submission Medium: BlackBoard Ultra. Beware that BlackBoard's clock may differ slightly from yours. If BlackBoard is not reachable due to an (unpredicted) maintenance, you submit your solution via e-mail to the TA. Make sure all group members are in CC!
• Contact / TA: Randy Paredis.

In this assignment, you will learn how Petri-Nets can be used for safety analysis. You will learn how they can be built, as well as how properties, and in particular, temporal patterns (over behaviour traces) can be specified in the CTL property language. You will use the TAPAAL tool.

Make sure to clearly indicate which files implement which models in your report! This assignment expands on the nautical engineering case from the first two assignments, albeit at a different level of abstraction/detail and with different properties of interest. Carefully read and understand the full assignment before starting your solution!

Note: building Petri Net models by hand is time consuming and error prone. In the Model Driven Engineering (MDE) course, we start from a domain-specific visual notation and generate Petri Net models automatically by means of graph transformation.

The figure below shows you what we mean by a confluence. It is similar to an intersection in a road traffic network.

We can describe the confluence as follows:

• A confluence has two inputs (South and West) and two outputs (North and East).
• There can be at most one watercraft at an output, but the number of watercraft at an input is unbounded. The inputs and outputs act as the environment of our System under Studay.
• The total number of watercraft that can be present in a confluence at any time (its capacity, i.e., the sum of the number of vessels going North and East, excluding the ones on the in- and outputs) is limited. By default, let's assume this capacity is 1 (to prevent collisions in a small confluence which can only hold one watercraft at a time).
• Watercraft will go straight through the confluence (they don't turn corners): If a watercraft enters on the South input, it should exit on the North output. Similarly, if a watercraft enters on the West input, it can only exit on the East output.
• If there is a watercraft on an output, no other watercraft can leave on that output. For instance, if there is a vessel on the North output and another vessel enters on the South input, then the second vessel will remain in the confluence until the North output is free. The same is true for the West-East trajectory.
• We can model the evolution over time of our System under Study by modelling a discrete "clock". Every time this clock "ticks", a single "step" is executed. What happens to the confluence during a single (macro-)"step" is defined by the following set of "micro-steps" (in no particular order).
  • On every input, a new watercraft may spontaneously appear, or not (non-deterministically).
  • On every output that contains a watercraft, the watercraft present can spontaneously disappear, or not (non-deterministically).
  • If the confluence contains a watercraft that should move to some output Y (Y being North or East), and that output Y does not contain a watercraft, the watercraft moves from the confluence to that output (deterministically). If there is a watercraft waiting to move to the North output and another is waiting for the East output and both outputs are empty, both watercrafts should move (in no particular order).
  • If the confluence may still accept a watercraft (i.e., it still has remaining capacity or "slack") and a watercraft is waiting on some input X (X being South or West), that watercraft should enter the confluence (deterministically). If there is a watercraft waiting to enter on the South input and another is waiting on the West input and there is capacity for both watercraft, they both should enter (in no particular order).
  • The total number of clock "ticks" upto now (in essence, a counter) is increased.
  Note that these "micro-steps" are NOT given in a predefined order. It is important that each watercraft only moves a single position in every clock tick (unless it can not move in which case, it doesn't).

To construct a Petri-Net of the given confluence, you will use TAPAAL with its modelling, simulation and analysis features. When creating a model, it is not allowed to use time or game semantics. In other words, you are only allowed to use Places, Transitions, (Inhibitor) Arcs and Tokens. Make sure to check that "timed" and "game" are set to "No" in the bottom-right corner of the GUI. When creating a new model, you can select this as well from the pop-up modal window.

You can (and are encouraged to) make use of Global Constants for arc weights whenever your weight is larger than 1. Additionally, you can also use multiple "components" to describe your system. Each component should contain a representative subset of the system you are building, but make sure to not overdo this (i.e., do not create a component for every place). This allows you to maintain an overview, whilst also creating much cleaner nets. Use Shared Places to define interactions between multiple components. Do not use Shared Transitions!
Hint: If you do not see the "Components", "Shared Places and Transitions" and "Global Constants" sections on the lefthand-side of your screen, select "View" > "Show advanced workspace". Alternatively, you can enable these sections by checking the corresponding boxes in the "View" menu.

You will need to perform the following tasks step by step. Store (and submit) a copy of your model after each finished (sub-)task. Provide an answer to all the questions asked.

1. Create and describe a Petri-Net for the confluence. Clearly identify all the aspects of the system and all used components.
   • (5%) Describe and validly construct an input and an output for the confluence.
   • (5%) Describe and validly construct the core unit of the confluence.
   • (10%) Construct the full confluence by linking your inputs and outputs to the core. Make sure to clearly denote (by appropriate naming) which input/output is which.
   • (15%) Introduce the clock into your model. Make sure the required events (see above) only happen exactly once for each "tick". Clearly describe what constructs used for the introduction of the clock. Add a place that holds the number of clock ticks that have happened.
2. (10%) Provide a (simulation) trace for the following scenarios. Make sure to describe the full clock tick. The confluence's capacity is 1 (to start with). You may assume that a watercraft will always exit the system when it is able to.
   • Two watercraft arrive at the confluence in the same step. The simulation ends as soon as both watercraft have fully exited the confluence.
   • Three watercraft arrive on the South input, enter the confluence and try to exit. However, there is a watercraft which blocks the North output. The execution ends after the third watercraft has arrived.
3. (10%) Redo the scenarios from the previous task, but this time, the confluence's capacity is 2.
4. Use this Python script to do some preliminary analysis for the system. Take a look at the documentation at the top of the file for more info on how to execute the script. Clearly indicate which commands were used to generate your results.
   Note: The -g flag overrides the creation of a reachability/coverability graph to create an image of the Petri-Net itself.
   • (5%) Reachability / Coverability:
     • Argue why your solution would (not) produce an infinite reachability graph.
     • Generate the reachability graph and discuss any patterns you identify. If your reachability graph is infinite, generate the graph for a representative variant of your model instead.
     • Can you add/remove one/multiple place(s)/transition(s)/arc(s) such that the reachability graph becomes finite if it was infinite (or vice-versa)? Your new model does not have to conform to the requirements.
     • Generate the coverability graph and discuss any patterns you identify.
   • (5%) Invariant Analysis:
     • Generate the P(place)-invariants for the model and explain what they mean in terms of the confluence's dynamics.
     • Which invariants did you expect? Which ones are surprising? Why?
     • Can you add a single place/transition/arc to the model that changes these invariants (for better or worse)? Your new model does not have to conform to the requirements.
5. Use queries in TAPAAL to analyze the following aspects of the confluence:
   • (6%) Boundedness:
     • You may use the "Check Boundedness" feature in the Query modal to analyze the model's boundedness. (Logical) queries are expressed as CTL (Computation Tree Logic) formulas. There used to be a bug in TAPAAL that breaks this feature. Starting from TAPAAL 3.9.3, the issue seems to be resolved. "Number of extra tokens" identifies how many additional tokens may be used in the analysis. For instance, if the net contains 7 tokens and this value is set to 3, the 10-boundedness is analyzed. Is the result what you expected? Why (not)?
     • Use one or multiple queries to check the boundedness of your net. You may use logic, reasoning and the already obtained P-invariants to simplify/minimize your queries, as long as you clearly describe your reasoning. Is the result what you expected? Why (not)?
   • (6%) Deadlock:
     • When enabling "Some Trace" in the "Trace Options" (when possible), a simulation trace is opened/shown after verification if it found a sequence of firings that caused the query to be satisfied.
     • Use a query to find whether or not there is a deadlock in your net. What firing sequence cause this? What does this mean for the confluence?
     • If there is a deadlock, describe how you can modify your net to make it deadlock-free. Can you identify this deadlock in the Reachablity/Coverability graph?
     • If there is no deadlock, describe why there is no deadlock. What would a deadlock look like in the Reachability/Coverability graph?
   • (6%) Liveness:
     • Pick interesting transitions in your net and determine their liveness using queries.
     • Can you add a single place/transition/arc to alter this result?
   • (6%) Fairness:
     • Argue convincingly that you've implemented "true" fairness.
     • This means that for each clock event can only happen once for every clock tick. For instance, it is not possible for a watercraft to move through the entire confluence in a single clock tick.
     • Your argument may consist of examples, queries, logical statements... As long as you can validly and objectively argue that there is "true" fairness, this will be accepted.
   • (6%) Safety:
     • Can two watercraft crash? This happens if there are more watercraft in the confluence than its capacity allows. Why (not)?
     • Provide a trace in which the watercraft do crash. If they can't, prove (using queries, logic reasoning, already obtained results...) that this is impossible in your net.
     • Can you find an acceptable initial marking such that there is a collision?
     • Can you find a way to add/remove one transition/place/arc such that there is a possibility for crashes? Your new net does not have to conform to the given requirements.
6. (5%) Write a report that explains your solution for this assigment. Include your models and discuss them. Also clearly indicate which models can be found in which files. Make sure to mention all your hypotheses, assumptions and conclusions. See also the "submission information" at the top of this page. Make sure to have a new model (or set thereof) for every sub-solution of this assignment; and to have an answer to all the questions posed here.

Take pride in your work. Make sure your report and all models and images are clearly readable. In TAPAAL, you can make use of annotations to identify sections of your models. You will not lose points for doing too much, but you will lose points if you do too little.

• This assignment is to be solved with TAPAAL.
• Reachability, coverability and P-invariant analysis are not part of TAPAAL, but should be solved by using this Python 3.6+ script. The documentation at the top of the file provides the required information on how to use it. Note that TAPAAL sometimes introduces inconsistencies in large models. They can cause the warning "No such place %s reachable from %s. Please recreate both to make your model valid." to appear. To solve this issue, delete and recreate both listed transitions. Use the -g or --graphviz flag to create a GraphViz file for the internal net to verify inconsistency issues. If you found a bug or experience any issues with the script, please contact the TA.