• Due Date: Tuesday, 26 November 2024, before 23:59.
• Team Size: 2 (pair design/programming)!
  As of the 2017-2018 Academic Year, each International student should team up with a "local" student (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 create your solution.
  • The report must be in HTML or PDF and must be accompanied by all images.
  • Images that are too large to render on one page of the PDF must still be rendered on the PDF (even though unclear), and the image label should mention the appropriate file included in the submission archive.
  • Make sure to mention the names and student IDs of both team members.
  • The other team member must submit a single HTML file containing the coordinates of both team members using this template.
• 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 should submit your solution via e-mail to the TA. Make sure all group members are in CC!
• Contact / TA: Rakshit Mittal.

In this assignment, You will use the TAPAAL tool to model the queueing system of a seaport. You will learn:

1. How to build Petri nets and use them for safety analysis of Cyber-Physical Systems
2. How properties, and in particular, temporal patterns (over behaviour traces) can be specified in the CTL property language.

Make sure to clearly indicate which files implement which models in your report! This assignment expands on the port/container-terminal 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.

You will use TAPAAL with its modelling, simulation and analysis features to accomplish the tasks of this assignment.

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. You can do this in 2 ways:

• 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 "No" from the 'Create a New Petri Net' dialog box.

Figure 1: Two methods to ensure time or game semantics are not used in your assignment solution.

• You can (and are encouraged to) make use of Global Constants for arc weights whenever your weight is larger than 1.
• You can also use multiple "components" to describe your system. Each component should contain a representative subset of the system you are building.
  • 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!
  • 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.

Figure 2: Menu options to view the advanced workspace for making components in your Petri net.

In the previous assignments the system-under-study was the gantry system. We will continue with the theme of the seaport. However, now, our property of interest is related to the efficiency of the port in handling the ships that arrive and depart. Hence, our system will be the whole seaport itself, and we will model it using Petri nets, since that is the most appropriate abstraction to reason about our current properties of interest.

Figure 3: Map of the Port of Antwerp-Bruges

Figure 4: Simplified port that you will use for the case-study. Notice that there are 2 berths where ships can dock, and be served (containers loaded/unloaded). Each berth has a dedicated entry and exit path. That means there can be a maximum of 9 ships 'within' the port as shown in the figure.

The precise textual description of the above system is as follows:

Waiting area and common passage

• There is an area for ships that arrive (are generated) to wait.
• There is a common passage leading into the port, that is used for movement in both directions entry and exit. This passage can accommodate upto $m$ ships. We will work $m=1$ and $m=3$
• The number of ships at the input (the waiting area) is unbounded. Ships do not wait at the output after they have exited the port and disappear immediately. You will receive a BONUS if you accumulate serviced ships in a single place at the output to act as a counter for the number of ships serviced. NOTE: By input, we mean the producer/generator pattern (as described in the lectures) and by output we mean the consumer/sink pattern (as described in the lectures).
• These inputs and outputs model the environment of our System under Study.

Entries and exits for the 2 berths

• The common passage is connected to the berths via dedicated uni-directional passages for both entry and exit.
• Each such passage can accommodate maximum one ship.

Berths and workers

• There are 2 berths where ships can dock and be serviced.
• There is a pool of $n$ workers. We will work with $n=1$ and $n=4$.
• Ships docked at both berths are serviced by this pool of workers. One worker can only service one ship in a clock cycle.

Clock and semantics

• We can model the evolution over time of our System under Study (the port) by modelling a discrete "clock". Every time this clock "ticks", a single "step" is executed. What happens to the port during a single (macro-)"step" is defined by the following set of "micro-steps" (in no particular order).
  • An unbounded number of new ships may appear or not (non-deterministic) in the waiting zone.
  • If a ship was in the waiting area in the previous tick, and if there is space in the common passage, the ship (possibly more than one), will move into the common passage (deterministic).
  • If a (yet-to-be-serviced) ship was in the common passage in the previous tick, and if there is space in any of the berth input passages, the ship will move into the empty berth input passage. Note that if both entry passages are empty, the ship can choose either one non-deterministically.
  • If a ship was in a berth input passage in the previous tick, and if the corresponding berth is empty, the ship will move into that berth (deterministic).
  • If a ship moved into a berth in the previous tick, and if there is an available worker, the ship will be serviced.
  • If there are 2 ships to be serviced, i.e. one in each berth, the order of service can be randomly chosen. This does not matter if there are more than one workers. BONUS if you can explain why the output will be different if there is only one worker with supporting traces.
  • You will get a BONUS if you correctly implement fairness in your model, i.e. ships are serviced alternately.
  • If a ship has been serviced, it will leave the berth, and move into the corresponding exit passage if it is free (deterministic).
  • If a ship is in the exit passage, it will move into the common passage if there is space in the common passage (deterministic).
  • A serviced ship in the common passage will leave. Multiple ships can and will leave the port (deterministic).
  • The total number of clock "ticks" upto now (in essence, a counter) should be incremented.

NOTE: The above "micro-steps" are NOT given in a predefined order. The clock is important because it restricts the movement of each vehicle to a single position in every major clock tick (unless the vehicle can/does not move). Later in the assignment is described how you can model this clock easily.

NOTE: We encounter 2 notions of fairness:

1. Ships are serviced alternately (this is a BONUS)
2. Ships can only move a maximum of one step in every clock tick. This is mandatory and you will implement this by careful design of the clock.

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 above simplified port system. Clearly identify all the aspects of the system and all used components.
• (5%) Describe and validly construct the inputs and outputs for the port.
• (5%) Describe and validly construct the other elements of the port.
• Note: You will get a BONUS for giving meaningful names to all the places and transitions in your Petri nets for the assignment.
• (10%) Construct the full port 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 as described for each "tick".
• Clearly describe what constructs are used for the introduction of the clock.
• Add a place that holds the number of clock ticks that have happened -> the clock counter.
2. (10%) Provide a (simulation) trace for the following scenarios. Make sure to describe the full clock tick. You will have to do this manually.
• $m=1$ and $n=1$. 10 ships are waiting to enter the port. No new ships arrives during the simulation. The simulation ends as soon as all ships have fully exited the port or if there is no possible movement for ships. Is there a livelock or a deadlock? Describe the race in your report.
• $m=3$ and $n=4$. There are no ships waiting initially. 1 ship arrives in each clock cycle for 3 cycles. The simulation ends as soon as all ships have fully exited the port or if there is no possible movement for ships. Is there a livelock or a deadlock? Describe the race in your report.
3. 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.
   • For the rest of the tasks you will assume that $m=3$ and $n=1$ and there are no ships in the initial state of the system.
   • (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-invariants (place-invariants) for the model and explain what they mean in terms of the port system'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.
4. Use queries in TAPAAL to analyze the following aspects of the port system:
• (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 caused this? What does this mean for the port system?
• 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?
• What would a deadlock look like in the Reachability/Coverability graph?
• If there is no deadlock, describe why there is no deadlock.
• (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 each clock event can only happen once for every clock tick.
• For instance, it is not possible for a ship to move through the entire port system 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 ships crash?
• This happens if there are more ships in any part of the port than its capacity allows.
• Why (not)? Your argument may consist of examples, queries, logical statements...
• Provide a trace in which the ships do crash.
• 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?
• Note that your new net does not have to conform to the given requirements.
• (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 do not for`get have an answer to all the questions posed here.

In the example TAPAAL Petri net, is a description of a simple queueing system as shown below:

Figure 4: Example queueing system to demonstrate clock. As you browse the different models/components, the annotations will guide you through the reasoning used to make the clock for this net. You can even simulate the net to verify that the clock satisfies the requirements.

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