• Due Date: 24 November before 23:55.
• 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. The report must be called index.html. Make sure to mention the names and student IDs of all the team members. The other team member must submit a single HTML file containing only the coordinates of both team members. This will allow us to put in grades for both team members in BlackBoard.
• Submission Medium: BlackBoard. 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 to do safety analysis. You will learn how they can be built, as well as how state-space exploration can be done by means of a CTL query language. This solution is to be made with TAPAAL. Make sure to clearly indicate which files implement which models in your report. This assignment expands on the PRT case from previous assignments. Carefully read and understand the full assignment before starting your solution!

The figure below gives an example of a small PRT map with 6 stations (circles) and 3 lights (squares with the letter "L"). The arrows represent the direction in which the rail should be followed. Note that each station is reachable from every other station (i.e., you can drive in an "8"-shape). An "X" identifies that there is currently a trolley in that station. We would like to analyze the safety of this railroad, for which we will use Petri-Nets.

For simplicity reasons, the notion of a "track" is introduced. A track is a simple railway segment over which a single trolly can ride. If two trolleys find themselves on a single track, we will assume they have collided. This allows us to simplify the above figure in terms of tracks: each station and light will be represented by a simple track. In total you should get 9 tracks.

• A light is a special kind of track. If the light is "red", no trolleys may pass. If the light is "green", all trolleys can pass. The top and bottom lights start at "red" in the model's initial state, whereas the middle light starts at "green". Each "iteration" of the system, a light should change its color.
• The trajectory has one "merge" and one "split". Keep this in mind when creating your model. The trolleys are free to choose which branch of the split they take (i.e., they can travel in an "8"-shape).

We can simulate this system by defining a "clock". Every time this clock "ticks", the following events occur:

1. All trolleys must move to the next track, unless prevented by a red light.
2. The lights change from "red" to "green" or from "green" to "red".

To construct a Petri-Net of the given rail network, you will use TAPAAL and its 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.

You can (and should) make use of Global Constants for arc weights. Additionally, you are required to 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 track). This allows you to maintain an overview, whilst also creating much cleaner nets. Use Shared Places to define interactions between multiple components.
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.

1. Create and describe a Petri-Net for the railroad system. Clearly identify all the aspects of the system and all used components.
   • (10%) Describe and validly construct a single rail track/segment. What happens when this is a light?
   • (10%) Construct the full railroad.
   • (15%) Introduce the clock into your model. Make sure the required events (see above) only happen exactly once for each "tick". Clearly describe what is used to accomodate for the introduction of the clock.
2. (20%) Provide a trace for the following scenarios. You are free to choose another initial position for the trolley(s).
   • A trolley traveling for at least 2 tracks before passing through a light that is red when the trolley arrives there.
   • A trolley that travels in a single "8"-shape over the network, without ever seeing a red light.
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.
   • (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 subset of your model instead.
     • Can you add/remove a place/transition 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 for the model and explain what they mean in terms of the railroad.
     • Which invariants did you expect? Which ones are surprising? Why?
     • Can you add a single place or transition to the model that changes these invariants (for the better or the worse)? Your new model does not have to conform to the requirements.
4. Use queries in TAPAAL to analyze the following aspects of the PRT:
   • (5%) Boundedness:
     • Do not use the "Check Boundedness" to analyze the model's boundedness. There is currently a bug in TAPAAL that breaks this feature.
     • 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. Is the result what you expected? Why (not)?
   • (5%) Deadlock:
     • Note that (due to a bug/feature in TAPAAL) the "deadlock" predicate is meant to check deadlocks in timed nets, which should not be used in this assignment. When enabling "Some Trace" in the "Trace Options", a simulation trace is opened/shown after verification if it found a sequence of fireings that caused the query to happen. If no such trace was opened, the query failed, even if the popup menu says it didn't.
     • Use a query to find whether or not there is a deadlock in your net. What fireings cause this to happen? What does this mean for the railroad?
     • 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 isn't a deadlock, describe why there is no deadlock. What would a deadlock look like in the Reachability/Coverability graph?
   • (5%) Liveness:
     • Pick an interesting transitions in your net and determine the their liveness using queries.
     • Can you add a single place/transition to alter this result?
   • (5%) Fairness:
     • Prove 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 trolley to move two tracks in a single clock tick.
     • Your proof 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.
   • (5%) Safety:
     • Can two trolleys crash? Why (not)?
     • Provide a trace in which the trolley 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 trolley collision?
     • Can you find a way to add a single transition/place such that there is a possibility for crashes?
5. (10%) 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.

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.