• Due Date: Sunday, 16 November 2025, 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, analyze, and compare roadway intersections and roundabouts. 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.

You are discouraged but allowed to make use of any GenAI tool in solving the assignment or writing the report (for example, to correct grammatical mistakes) as long as you adhere to the UA Guidelines for students on responsible use of GenAI.

You are required to cite any use of GenAI and describe what portions of the assignment you used it for.
You should also mention all other sources, including collaborations.

Note that a significant part of demonstrating that the learning goals have been achieved, includes being able to

1. explain the relevant concepts in the assignment,
2. explain the design choices in your implementation, and
3. critically discuss your solution.

This will be evaluated in a short (~15 minute) oral evaluation, which will be conducted in the week following the deadline of every assignment.

Note: Building Petri nets 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 nets automatically by means of graph transformation.

We want to model and compare 4-way road traffic intersections and roundabouts.

Part 1: Intersection

Figure 1: Simplified intersection

The precise semantics of the intersection are as follows:

1. There are four directions (North, South, East and West) from which cars can enter and exit the system.
2. The number of cars at each of the four inputs is unbounded.
3. Cars do not wait at an output, and disappear immediately. 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).
4. There is a buffer road segment between each input/output and the intersection at each of the 8 entries and exits from intersection, with capacity one.
5. At most one car is allowed to be present at the center of the intersection at any moment.

Clock

We can model the evolution over time of our intersection by modelling a discrete "clock". Every time this clock "ticks", a single "step" is executed. What happens to (each car in) the intersection during a single (macro-)"step" is defined by the following set of "micro-steps" (in no particular order).

• An unbounded number of new cars may appear or not (non-deterministic) at the input.
• If a car was in the input in the previous tick, and if the input buffer is unoccupied, the car will move into the buffer (deterministic).
• If a car was in an input buffer in the previous tick, and if the intersection is unoccupied, the car will move into the intersection. Before a car enters the intersection, the direction in which it will exit is determined randomly.
• If a car was in the intersection in the previous tick, and if there is an empty output buffer segment in the direction the car will exit, the car will move into the output buffer (as shown in the figure, it is not allowed to go back the direction it came from).
• If a car was in an output buffer in the previous tick, then it will move to the corresponding output (deterministic).
• If a car was in an output place in the previous tick, it will leave (deterministic). The counter for number of cars served should be incremented consequently.
• 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 (both should be implemented):

1. Each direction of input traffic is serviced alternately (note that you need to account for the case, for example, if there is a car coming from only one direction - in this case regardless of the current priority, the car moves into the intersection).
2. Cars can only move a maximum of one step in every clock tick. You will implement this by careful design of the clock.

Part 2: Roundabout

Figure 2: Simplified roundabout.

The precise semantics of the roundabout are as follows:

1. There are four directions (North, South, East and West) from which cars can enter and exit the system.
2. The number of cars at each of the four inputs is unbounded.
3. Cars do not wait at an output, and disappear immediately. 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).
4. There is a buffer road segment between each input/output and the roundabout at each of the 8 entries and exits from intersection, with capacity one.
5. The roundabout consists of four road segments connecting each of the four directions, diagonally.

Clock

We can model the evolution over time of our roundabout by modelling a discrete "clock". Every time this clock "ticks", a single "step" is executed. What happens to (each car in) the roundabout during a single (macro-)"step" is defined by the following set of "micro-steps" (in no particular order).

• An unbounded number of new cars may appear or not (non-deterministic) at the input.
• If a car was in the input in the previous tick, and if the input buffer is unoccupied, the car will move into the buffer (deterministic).
• If a car was in an input buffer in the previous tick, and if the next section of the roundabout is unoccupied, the car will move into the roundabout segment (deterministic). For example, a car approaching from the East will move into the North-East segment of the roundabout if it is empty.
• If a car was in the roundabout in the previous tick, the car will randomly make one of three moves:
  1. If the proceeding roundabout segment is empty, the car may move there.
  2. If the corresponding exit buffer segment is empty, the car may move there.
  3. If the proceeding roundabout segment is occupied, the car may choose to wait and not move.
• If a car was in an output buffer in the previous tick, then it will move to the corresponding output (deterministic).
• If a car was in an output in the previous tick, it will leave (deterministic). The counter for number of cars served should be incremented consequently.
• 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 a single notion of fairness (which should be implemented):

1. Cars can only move a maximum of one step in every clock tick. You will implement this by careful design of the clock.

Additional semantics (10%)

With the semantics as described above for the roundabout, note that there is possibility for:

1. looping of a car around the roundabout.
2. a car exiting in the same direction that it entered from

To make it a fair comparison with the intersection implement the semantics of the roundabout such that the above two cases do not occur for 10% of the assignment's grade. Argue why your roundabout does not allow these two cases in your report.

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 each, the intersection and roundabout. Clearly identify all the aspects of each system and all used components in your report.
• (5%) Describe and validly construct the inputs and outputs for the systems.
• (5%) Describe and validly construct the other elements of the systems.
• Give meaningful names to all the places and transitions in your Petri nets for the assignment.
• (10%) Finally, fully construct each system by linking your inputs and outputs to the core (intersection or roundabout + buffers). Make sure to clearly denote (by appropriate naming) which input/output is which.
• (15%) Introduce the clock into each system.
• 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 for each system. Make sure to describe the full clock tick. You will have to simulate this manually in TAPAAL. The simulation ends as soon as all cars have fully exited the system or if there is no possible movement for cars. Is there a livelock or a deadlock? Describe each trace in your report.
• 2 cars arrives from each direction in the first tick. No other cars arrive during the simulation.
• One car arrives alternatingly from each direction until 8 cars have arrived. No other cars arrive during the simulation.
3. Use this Python script to do some preliminary analysis for each 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 each 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 each system and compare them:
• (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)?
• NOTE: It is an observed anti-pattern that students check n-boundedness, for any random n, in their net without any motivation for that number. Have some reasoning for why you chose to test a particular bound.
• (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 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 fairness.
• 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 cars crash?
• This happens if there are more cars in any part of the system than its capacity allows.
• Why (not)? Your argument may consist of examples, queries, logical statements...
• Provide a trace in which the cars 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 assignment.
• 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 3: 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.

You will use TAPAAL to create Petri net models, and to perform some analyses.

To analyze reachability, coverability and P(lace)-invariants, you will use not use TAPAAL, but 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.

Apart from modelling, also simulation and checking for satisfaction of LTL/CTL formulas will be done with TAPAAL.

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 4: 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 5: Menu options to view the advanced workspace for making components in your Petri net.