TAPAAL User Manual
TAPAAL User Manual
Buy on Leanpub

Introduction

In this page we shall informally introduce the model used in TAPAAL, called timed-arc Petri nets with inhibitor arcs, transport arcs and invariants. To do so we shall use a model of a rollercoaster which is illustrated in the following figure. The TAPAAL model can be found here.

A simple TAPN model of a rollercoaster
A simple TAPN model of a rollercoaster

The model of the rollercoaster contains a number of places (drawn as circles), transitions (drawn as black squares) and arcs from places to transitions or transitions to places. Time intervals are associated with arcs from places to transitions. Further, the places in the model may contain tokens, each of which is associated with a real number signifying the age of the token. In the example, there are two tokens in the place called station, both with age 0.0. Invariants may be assigned to places which restrict the ages of the tokens in that place. In our example, the place first_half has an associated invariant of [0,4] (written inv: \leq 4).

There are different types of arcs: normal arcs (normal arrow tip), transport arcs (diamond arrow tip) and inhibitor arcs (circle arrow tip). Intuitively, the normal arcs from places to transitions will consume tokens of appropriate ages and normal arcs from transitions to places will produce tokens of age zero. A transport arc works in a similar fashion except that any token produced will have the same age as the one consumed. Inhibitor arcs are used to test for the absence of tokens of certain ages in places.

The idea of the model is that we have two trains for the rollercoaster represented by the two tokens in station. The rollercoaster must ensure the safety of the passengers which means that the two trains cannot be in the same part of the track at once. Further, since a train may experience some sort of failure at any given time during its trip around the rollercoaster, the system must ensure that the other train is stopped when there is an emergency. Thus, a train can only leave the station and enter the first half of the track if there is no emergency and no other train in the first half of the track (inhibitor arcs are used to check for the absence of tokens in these places) and similarly for entering the second half of the track.

As a concrete example, say the first train fails in the second half of the track while the second train is in the first half. In this case, the second train will be stopped before it enters the second half of the track so there can be no crash between the two.

It takes 4 time units for a train to run through the first half of the track and 3 time units to run through the second part. Thus, a full trip around the track takes 7 time units. Once the first train enters the second half of the track, the other train may leave the station. In the event that a train fails, it takes at least 5 time units to repair it and return it to the station.

Once we have a model of a system, we want to verify if certain properties are satisfied. For instance, we might want to verify if it is possible for the two trains to be in the same part of the track of the rollercoaster at once (except for the station). This property is a safety property because the proof of the property is a finite sequence of steps describing how to reach the situation where both trains are in the same part of the track. Naturally, if we can find such a sequence, we can conclude that there is an error in the mode,l as it should not be possible for the two trains to be in the same part of the track at once. As another example of a property consider one that checks if it is possible for the two trains to run forever without any emergency. This is a liveness property because the proof is an infinite sequence of steps describing how the trains can run forever without an emergency.

Modelling

In this section we will explain the basics of Timed-Arc Petri Nets (TAPN) as used in TAPAAL by illustrating the behaviour of the various features of the model. Following this we will explain how TAPAAL can be used to draw these models.

Modelling Features

In order to provide some intuition for the Timed-Arc Petri Net (TAPN) model, we will now give an example which introduces the various features of the model in a step-by-step manner. We will start with a basic timed-arc Petri net and then gradually decorate that example with transport arcs, invariants and finally inhibitor arcs while explaining the intuition behind the change in behaviour of the net, induced by these additions.

Basic TAPN

The basic timed-arc Petri net is presented in the following figure. The TAPAAL model can be found Here

A basic TAPN model
A basic TAPN model

It includes two transitions t0 and t1 and five places p0, p1, p2, p3 and p4. There are tokens of age 0.0 in the places p0, p1 and p2. Initially, only t0 is enabled because its input place p0 contains a token of an age which satisfies the constraint on the arc from p0 to t0 (the constraint signifies that a token with an age between zero and infinity is required, i.e. a token of any age). Transition t1 requires a token of any age in p1 but also a token of an age in the interval [4,5] in p2 which is why t1 is not enabled initially. Since t0 is enabled, we can fire it whereby we remove a token of an appropriate age from p0 and produce a token of age 0.0 in each of the places p3 and p4. However, we could also choose to do a time delay of, say, 4.5 time units, whereby all tokens in the net would grow 4.5 time units older. Since all tokens are now of age 4.5 both t0 and t1 are enabled since both would have tokens of appropriate ages in all their input places.

Transport Arcs

Let us now introduce transport arcs into our example net. Specifically, we will replace the normal arcs from p0 to t0 and from t0 to p4 with a transport arc from p0 through t0 to p4 as illustrated in the following figure. The TAPAAL model can be found Here.

Adding transport arcs to the model
Adding transport arcs to the model

Note that the :1 on the transport arc is there to help distinguish where each token goes in case we have more than one transport arc through the transition.

For the sake of illustration, assume that we have initially made a time delay of 2.5 time units such that all tokens are now of age 2.5. Transition t0 is still the only enabled transition in net at this point, however there is a difference when we choose to fire t0. By firing t0 we will still remove a token of appropriate age from p0 and produce a token of age 0.0 in the place p3 as before. However, due to the transport arc we will produce a token at p4 of the same age as the token we removed from p0, i.e. of age 2.5 in this case. In this way, the transport arcs allow us to preserve the age of tokens as we transport them around the net.

Invariants

Let us now add invariants to our example net. Specifically, we will add invariants to the places p2 and p4 that disallow tokens older than 5, as illustrated in the following figure. The TAPAAL model can be found Here.

Adding Invariants to the model
Adding Invariants to the model

Note that by convention, if no invariant is given for a place then this implicitly means that the invariant for this place is [0, \infty). Assume that we have done a time delay such that all tokens are of age 5.0. At this point we cannot do any further time delays because that would violate the invariant at p2. We are forced to fire either t0 or t1, both of which are enabled. Thus, invariants facilitate urgency in the model. One of the particularities of the use of invariants and transport arcs is demonstrated by the invariant of the place p4, which has implications for the transition t0 because of the transport arc from p0 through t0 to p4. Since transport arcs preserve the ages of tokens we can only fire t0 when there is a token of age smaller than or equal to 5 in p0, otherwise the token produced at p4 would violate the invariant on that place.

Inhibitor Arcs

Finally, let us introduce inhibitor arcs into our example. Specifically, we will replace the arc from p2 to t1 with an inhibitor arc as illustrated in the following figure. The TAPAAL model can be found Here.

Adding inhibitor arcs to the model
Adding inhibitor arcs to the model

Intuitively, an inhibitor arc is the opposite of a normal arc. For instance, t1 will now be enabled whenever there is a token of any age in p1 and no token in p2. Thus, initially both t0 and t1 are enabled since there are tokens in p0 and p1 with appropriate ages, and there is no token in p2. In this way, inhibitor arcs allow us to test for the absence of tokens in an input place.

Modelling in TAPAAL

The main window of TAPAAL contains all the tools needed to draw Timed-Arc Petri Nets (TAPN).

The main window in TAPAAL.
The main window in TAPAAL.

TAPAAL supports drawing/modelling of all the features explained in the section modelling features. It is possible to have multiple models open, and each model has its own drawing surface contained within a tab. Note that models in different tabs can not communicate or synchronize in any way. The left-hand pane contains the query list and the integer constant list. Integer constants will be covered later.

The query list allows you to create and save any number of queries for your model. For more information regarding the construction of queries please refer to the section verification section.

Modelling Tools

The modelling toolbar contains all the tools needed to draw TAPN models.

The modelling toolbar of TAPAAL
The modelling toolbar of TAPAAL

The modelling tools are (from left to right in the toolbar):

  • Select components
  • Add a place
  • Add a transition
  • Add a normal arc
  • Add a transport arc
  • Add an inhibitor arc
  • Add an annotation (like the textbox in the main window screenshot above)
  • Add a token
  • Delete a token

Tokens can also be added or deleted by placing the cursor over a place and scrolling up or down on the scrollwheel on your mouse.

Editing Models

When you draw your models you often want to edit certain aspects, such as renaming a place or transition, adding invariants, changing an interval, etc. This can be done by double clicking the thing you want to edit.

Editing Places

Double clicking on a place brings up the place dialog where you can edit the attributes of the place.

The dialog for editing places.
The dialog for editing places.

This dialog allows you to rename the place, add or remove tokens. Further, you can also specify invariants of the place. Note that in invariants it is possible to make use of integer constants which we will cover later in this section.

Editing Transitions

Double clicking a transition brings up the transition dialog where you can edit the attributes of the transition.

The dialog for editing transitions.
The dialog for editing transitions.

This dialog allows you to rename the transition as well as specify the rotation of the transition. Note that you can also rotate a transition by placing the cursor over it and using the scrollwheel on your mouse.

Editing Arcs

Double clicking an input arc (of any type) brings up the arc dialog where you can edit the attributes of the arc.

The dialog for editing arcs.
The dialog for editing arcs.

The main purpose of this dialog is to allow you to change the time interval on the arc. It is possible to use both strict and non-strict bounds on the interval. Note that as for place invariants, it is possible to use integer constants in these intervals.

Integer Constants

As mentioned in the beginning of this section the left-hand pane of the main window contains the integer constant list. In TAPAAL it is possible to define integer constants which can then be used in invariants and time intervals. This is useful if you are using the same constant over and over and want an easy way to change the value if needed.

To demonstrate the usefulness of these constants consider the model in the screenshot of the main window in the beginning of this section which contains 4 integer constants: deadline, min, periodA and periodB. This model is the webserver example which is one of the examples include in TAPAAL. To open it go to File -> Example nets -> webserver.

It models two users A and B who are continuously making requests to a webserver with a specified period and the webserver must then try to handle all the requests from the users. However, if a request is not handled before a specified deadline (in this example the deadline is the same for all requests), it will be dropped.

In this example, the deadline constant represents the deadline for the requests and periodA and periodB are the periods with which user A and B produce new requests. Notice how these constants are used in multiple places. If we want to see what happens if we increase the deadline for handling requests, we can easily do this by only changing the value of the deadline constant from e.g. 5 to 6. Thus, we only need to change it in one place instead of every place where the constant is used.

The dialog for editing constants
The dialog for editing constants

Changing the value of a constant is done by double clicking it in the constant list which will bring up the constant dialog where you can change the name of the constant as well as the value.

Note that integer constants are only syntactic sugar, meaning that whenever you leave the modelling mode of TAPAAL (be it for simulation or verification), TAPAAL will substitute the values of constants in guards and invariants.

Simulation

In this section, we will look at how TAPAAL can be used for simulation of TAPN models. We will do this in terms of an example using the simple rollercoaster model presented in the introduction. The TAPAAL model can be found Here

Clicking the green flag in the toolbar will put TAPAAL into simulation mode as illustrated in the following screenshot.

TAPAAL in simulation mode
TAPAAL in simulation mode

In simulation mode it is possible to simulate the behaviour of the model by firing transitions and doing time delays. This feature can be very helpful to discover simple errors in your model by allowing you to examine if your model behaves as intended.

Enabled transitions are marked with a red color as the depart transition in the above screenshot. Firing an enabled transition is done by clicking it. When firing a transition there might be multiple tokens of appropriate age in each input place. By default, TAPAAL will select a random token of appropriate age from each input place, however, it is possible to change how this token selection is done using the token selection method dropdown box in the left-hand pane. The possibilities are: random, youngest (youngest token of appropriate age selected), oldest (oldest token of appropriate age selected), and manual (manually select which token to consume from each input place).

Time delays are performed using the Time delay button in the left-hand pane. The text field to the left of this button specifies the duration of the time delay (default value is 1.0). Thus, to do a time delay of 2.4 time units (assuming this is possible in your model) you write 2.4 in this text field and press the button.

The lower part of the left-hand pane contains the simulation history. During simulation of your model TAPAAL will remember the history of time delays and transition firings, allowing you to step back and forth through this history. Stepping back and forth through the simulation history is done using the blue arrows above. This feature is useful if you for instance encounter a point at which you have two transitions enabled and want to examine what happens if you choose one or the other. You can just pick one of them and continue the simulation and then later step back through your history to that point and try the other transition instead of having to start over from the beginning.

In order to illustrate some of these points consider the following example. Assume that we want to simulate that both trains of the rollercoaster goes around the track once with no failures. This can be done by following this simulation:

  • Fire the depart transition (first train leaves the station)
  • Do a time delay of 4.0
  • Fire the halfway transition (first train enters the second half of the track)
  • Fire the depart transition (second train can now leave the station)
  • Do a time delay of 3.0
  • Fire the return transition (first train is now done going around the track)
  • Do a time delay of 1.0
  • Fire the halfway transition (second train enters the second half of the track)
  • Do a time delay of 3.0
  • Fire the return transition (second train returns to station)

In order to simulate that the second train experiences a failure in the second half of the track we can step back once and fire the fail_2 transition instead of the return transition and continue the simulation from there.

Verification

In this section we will explain the verification part of TAPAAL.

Query Dialog

TAPAAL has capabilities to verify queries about your model. A query is created by pressing the New Query button in the query secion of the left-hand pane. This will open the query dialog which is displayed in the following screenshot.

The query dialog
The query dialog

The query dialog contains a wealth of options. First of all you can specify a name of your query in the very top of the dialog. To perform the actual verification TAPAAL will translate your model to a Network of Timed Automata (NTA) and then use the UPPAAL verification engine on the produced NTA. In case you are interested in seeing the NTA produced by TAPAAL you can click the Save UPPAAL XML button which will export the NTA TAPAAL creates during the verification.

k-Boundedness Checking

The boundedness checking part of the query dialog.
The boundedness checking part of the query dialog.

The query dialog allows you to specify the extra number of tokens that TAPAAL is allowed to use during the verification. Because TAPN models can produce additional tokens by firing transitions (e.g. a transition that has a single input place and two output places) the verifier may need to use additional tokens compared to those that are currently in the net. By specifying some extra number of tokens you can ask TAPAAL to check if your net is k-bounded for this number of tokens (i.e. k = number of tokens currently in model + number of additional tokens allowed).

Simply put if your model is k-bounded then k is an upper bound on the number of tokens that your model can contain in any given marking. For instance, assume that your model currently contains 3 tokens and you ask TAPAAL if the model is bounded if you allow it to use 7 additional tokens. If the answer is yes then you know that in any given marking your model will not contain more than 10 tokens, thus the model is 10-bounded. In fact, it is not possible in this case to reach a marking where the model contains 11 or more tokens. On the other hand, if the answer is no the only thing you know is that it is possible to reach a marking with 11 or more tokens, but this tells you nothing about whether an upper bound actually exist.

If you get confirmation from TAPAAL that your model is indeed bounded for some number of tokens, then you can ask TAPAAL to find the least amount of additional tokens needed to make the net bounded. Generally, the more additional tokens you allow TAPAAL to use the longer the verification of your queries will take. Thus, you may have allowed TAPAAL to use 100 additional tokens but in reality only 10 additional tokens are needed. By letting TAPAAL find the least amount of additional tokens needed you may experience slightly faster verification time.

Query Construction

The query construction part of the query dialog
The query construction part of the query dialog

Constructing the query is done using the query construction buttons seen in the figure above. This is done by clicking on something in the text field that you want to change and then pressing one of the buttons below the text field to change the selection. Queries in TAPAAL are created by first specifying which type of query you want to verify. The options here are:

  • (EF) There exists some reachable marking that satisfies
  • (EG) There exists a trace on which every marking satisfies
  • (AF) On all traces there is eventually a marking that satisfies
  • (AG) All reachable markings satisfy

Following this, you specify the predicate to check. This is given as a boolean predicate consisting of some combination of conjunction, disjunction, negation and atomic propositions. Atomic propositions are of the form

<place_name> <operator> n

where <place_name> is the name of a place, <operator> is one of the operators <, <=, =, ⇒, > and n is an integer. Thus, in the proposition we can only talk about the number of tokens in a place and not their ages.

For instance, in the figure above a proposition Garbage = 0 is specified which means that the place Garbage must contain zero tokens.

Since, the query type is EG, the full query specified simply means: There exists a trace on which every marking satisfies that the Garbage place contains zero tokens. In other words, it is possible to avoid placing any tokens in the Garbage place.

Constructing queries

The above discussion used a query that was already constructed. We will now look at how to construct such queries. If you create a new query in TAPAAL, the query construction part of the query dialog will look as in the following figure.

The query construction part of the query dialog for a new query.
The query construction part of the query dialog for a new query.

Specifically, we will demonstrate how to construct the query EG (P0 = 0 and P1 > 0) (for this discussion we assume you have two places named P0 and P1 in your TAPN model). The expression <*> in the query text field is a placeholder which is the starting point for creating a query. Clicking on the placeholder selects it and enables the quantification buttons beneath the query text field. Selecting the EG quantifier puts the EG quantifier in front of the placeholder, so the query now reads EG <*>.

Next, select the placeholder by clicking on it and afterwards click the And button, the query now reads EG (<*> and <*>). Select the first placeholder, construct the first atomic proposition P0 = 0 using the comboboxes in the predicates section of the query dialog and subsequently press the Add Predicate to Query button. This replaces the currently selected placeholder with the chosen atomic proposition and the query now reads EG (P0=0 and <*>). Select the placeholder and repeat the process for the atomic proposition P1 > 0.

Note that you are not limited to replacing placeholders. For instance, if you wanted to say change the conjunction to a disjunction, you simply click on the and in the query text field to select the conjunction and then press the Or button. Similarly, if you want to add and additional conjunct to the conjunction, you simply click it (or one of the conjuncts) and press the And button, which adds a new conjunct to the query. Changing an atomic proposition is also as easy as clicking it and changing the propositions using the comboboxes in the predicates section.

Note that should you make a mistake the query construction has undo/redo support using the buttons in the Editing section. Likewise you can also delete the current selection (i.e. replace it with a placeholder) or reset the entire query (again, replace the entire query with a placeholder) in case you want to start over. Finally, expert users have the option of manually entering the query by clicking the Edit Query button, which makes the query text field editable. However, if you make a mistake when manually entering the query TAPAAL will inform you that it could not parse the query you entered. You will then have the option to edit the query again or revert back to whatever query was present before you pressed the Edit Query button.

Verification Options

The query dialog allows you to fine tune your verification by setting various verification options.

The verification options of the query dialog.
The verification options of the query dialog.

Analysis Options

The first options is the Analysis Options where you can specify the search strategy to use. The possible search strategies are:

  • Breadth First Search
  • Depth First Search
  • Random Depth First Search
  • Search by Closest to Target First

The chosen search strategy determine how the UPPAAL verification engine performs the search.

Trace Options

The Trace Options allow you to instruct TAPAAL to find a trace for your query. For instance, if you are trying to verify that it is always the case that there is at most 1 token in some specified place and you get a negative answer then you might want to see a trace that tells you how it is possible to put more than 1 token in the place. In the event that you do get a trace, TAPAAL will open the trace in simulation mode allowing you to step through it. Note that a current limitation of UPPAAL is that it is not always possible to obtain a trace.

Reduction Options

Finally there is the Reduction Options, which allows you to choose which reduction method to use and whether or not to use symmetry reduction. The possible reduction methods are:

  • Standard
  • Optimised Standard
  • Broadcast Reduction
  • Broadcast Degree 2 Reduction

The difference between these reductions are rather technical and thus left out here. The interested reader is referred to the list of published paper involving TAPAAL which can be found Here. Note, that the Standard and Optimised Standard reduction methods does not in general support queries of the type EG and AF.

The use of symmetry reduction can greatly reduce the verification time of your models. Note however that currently it is not possible to obtain a trace if symmetry reduction is used.