Table of Contents
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.
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.
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.
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.
The basic timed-arc Petri net is presented in the following figure. The TAPAAL model can be found Here
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.
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.
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.
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.
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.
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.
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.
The main window of TAPAAL contains all the tools needed to draw Timed-Arc Petri Nets (TAPN).
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.
The modelling toolbar contains all the tools needed to draw TAPN models.
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.
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.
Double clicking on a place brings up the place dialog where you can edit the attributes of the place.
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.
Double clicking a transition brings up the transition dialog where you can edit the attributes of the transition.
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.
Double clicking an input arc (of any type) brings up the arc dialog where you can edit the attributes of the arc.
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.
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:
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
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
periodB are the periods with which user
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.
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.
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.
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:
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
departtransition (first train leaves the station)
- Do a time delay of 4.0
- Fire the
halfwaytransition (first train enters the second half of the track)
- Fire the
departtransition (second train can now leave the station)
- Do a time delay of 3.0
- Fire the
returntransition (first train is now done going around the track)
- Do a time delay of 1.0
- Fire the
halfwaytransition (second train enters the second half of the track)
- Do a time delay of 3.0
- Fire the
returntransition (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.
In this section we will explain the verification part of TAPAAL.
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 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.
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 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.
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
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
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.
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
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
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.
The query dialog allows you to fine tune your verification by setting various verification 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 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.
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:
- 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.