What is the meaning of "Extra number of tokens" in the query dialog?

Created by Kenneth Yrke Jørgensen on on 2009-05-09
Keywords:

Timed-Arc Petri net model allows for creation of new tokens and as the result, the net can become unbounded (there is not necessarily any a priori given bound on the maximal number of tokens in the net). In order to enable a translation to UPPAAL, the user has to specify the number of extra tokens that can be used in the net for the newly created tokens. In case that the net is bounded and the user provides a sufficient number of extra tokens (this can be in fact automatically verified in TAPAAL by the "Boundedness Check" in the query dialog), the verification results are exact. In case that the net is unbounded, the implemented reduction provides an underapproximation of the behaviour (hence all found counter-examples are still valid).