This is an example net to introduce the modelling, verification and simulation features of TAPAAL.
The circles are called places and rectangles transitions. They are connected either by standard arcs between places and transitions, or they can be connected by transport arcs (these arcs always come in pairs) like the ones from P1 to T3 and T3 to P6.
Behaviour of the net is given by tokens. Each place can store a number of tokens and each token has its own real-time age. In our example, there is initially one token of age 0 in the place Start.
A transition can fire if in every of its input places there is at least one token of an age that fits into the interval assigned to the corresponding arc. When transition fires a new token of age 0 is produced to any of its output places for the normal arcs. In case of trasport arc, the age of the token remains the same as the age of the consumed token. Also note that arcs can be weigthed, like the one from T2 to P5 with weight 3 (producing three fresh tokens) and the one from P5 to T4 (consuming two tokens).
The place P2 contains the so-called invariant <=5. This means that tokens in that place cannot be older than 5 time units. A net can perform the so-called time-delays. This means that all tokens in the net grow older by some amount of time, as long as none of the invariants are violated.
Finally, the transition T4 (with a white dot) is an urgent transition, meaning that once it becomes enabled (the tokens arrive to the places P6 and P5), no time delay can happen and some of the currently enabled transitions have to fire. In our example only T4 will be enabled but in general there can be more enabled transitions and none of them has a priority over the other ones. Enabled urgent transition simply implies that time cannot delay.
-----------------------------
In our example we might want to know if it is possible, by doing some time delays and transition firings, to put a token into the place Target.
The query "Target Reachable" expresses this property. It moreover asks for fastest such trace. By clicking on "Verify" the verification will begin and ouput the trace allowing us to place a token into the place Target. By clicking on the symbols > and < one can move back and force in the trace and investigate the intermediate markings.
One may observe that 3 extra tokens are needed in the intermediate markings in order to reach the place Target. Indeed, this number of extra tokens is specified in the query dialog and by clicking on "Check Boundedness", one can verify that 3 extra tokens are indeed enough for an exact analysis.
This net is a workflow net and by going to menu Tools/Workflow analysis, one can see that it is not sound as there is a deadlock in the net.