• Due Date: Sunday 10 December 2023, 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 accompagnied 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 a roundabout. 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 roadways 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.

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.

The figure below shows the roundabout that we want to model.

Figure 3: Roundabout case study. In the image, the roundabout is completely occupied. Notice also that there are multiple vehicles waiting at the East/West inputs.

The precise textual description of the roundabout is as follows:

• There are two ways to enter the roundabout (East and West).
• There are two ways to exit the roundabout (North and South).
• There can be at most one vehicle at an output, but the number of vehicles at an input is unbounded. 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.
• The 'core' of the roundabout is made of four road segments, and each road-segment can hold upto one vehicle.
• Vehicles are free to exit the roundabout in the South or North direction (non-deterministic). For example, a vehicle that enters from the West may exit the roundabout in the North or South directions or continue looping through the roundabout core.
• If there is a vehicle on an output, no other vehicle can leave on that output i.e that output is blocked.
• 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 roundabout during a single (macro-)"step" is defined by the following set of "micro-steps" (in no particular order).
  • On every input, a new vehicle may appear or not (non-deterministically).
  • On every output that contains a vehicle, the vehicle present can disappear or not (non-deterministically).
  • The 4 road-segments that form a cycle in the centre of the roundabout are collectively called the 'core' of the roundabout.
  • The four road segments that are a buffer between the producers/consumers and the core road segments are called the North/South outroads and East/West inroads.
  • If there is a vehicle on either of the North or South road segments of the core, it may either move to the corresponding outroad (if empty) or to the next East-West road segment of the core, if empty (non-deterministic).
  • If there is a vehicle on either of the East or West road segments of the core, it has to move (deterministically) to the North or South road-segment of the core respectively, of-course only if the North/South road segment does not already contain a vehicle.
  • A vehicle on a West/East inroad should enter the core, if the corresponding core road segment is empty. However, preference should be given to a vehicle that is on the corresponding North/South core road segment if that vehicle wants to move to that East/West core segment. (You will only be able to implement this by choosing the correct sequence of events in your clock!)
  • 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.

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 roundabout. Clearly identify all the aspects of the system and all used components.
• (5%) Describe and validly construct the inputs and outputs for the roundabout.
• (5%) Describe and validly construct the core unit of the roundabout.
• (10%) Construct the full roundabout 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 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 may assume that a vehicle will always exit the system when it is able to.
• Two vehicle (one East and West) arrive at the roundabout in the same step. The simulation ends as soon as both vehicle have fully exited the roundabout.
• Three vehicle arrive on the East input, enter the roundabout and try to exit through the North output. However, there is a vehicle which blocks the North output. The execution ends after the third vehicle has arrived.
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.
   • (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 roundabout'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 roundabout:
• (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 roundabout?
• 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 vehicle to move through the entire roundabout 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 vehicle crash?
• This happens if there are more vehicle in the roundabout than its capacity allows.
• Why (not)? Your argument may consist of examples, queries, logical statements...
• Provide a trace in which the vehicle 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.