This post has 710 words. Reading it will take approximately 4 minutes.
CPN Tools has supported timed models almost since the first releases. Starting with version 3, we introduced models where we allowed the time stamp to be a real value, making it simpler to make simulation-based analysis. CPN Tools allows choosing time stamps from an interval but in a manner that still allows state-space analysis.
Timed models allow us to specify a duration for each transition, like this:
When we execute the transition, the produced token will have a time-stamp that is 5 time units into the future, indicating we cannot consume the token before time 5:
In CPN Tools 4, we can also specify an interval, indicating that the actual value of the time stamp should be taken at random from the interval:
Now, if we execute the transition (5 times), we get this state:
We see that the tokens have different time stamps; they are chosen at random (uniformly) from the interval specified. We could of course achieve something similar using one of the:
We can still do that, and if we want another distribution than the uniform distribution we have to do that. The difference between then and now is that if we look at the possible bindings of the transition in the initial state, as expected, we get:
The variable has no variables, so trying to manually select them would not work. However, using the new syntax we get:
As we see, we can actually pick the time stamp for the token here1). Time intervals can be used in time regions (as above) and on output arcs:
The values are added, so the token on the middle place would arrive 4 time units later than the top one, and the bottom one another 11 times units later in this case:
No only can manually select the time ranges, we can also use such models for state-space analysis. This would not be possible using random distribution functions as the tool cannot in that case determine how to do exhaustive analysis.
Of course, models with time ranges are also prone to state space explosion. If we have a state-space with a range with 1000 values, we do get 1000 nodes just due to time. Even if we assume that we keep time intervals sane, allowing time may make the state space infinite, even though it does not have to be:
This model has an infinite state-space even though the behavior is very simple: we just have two cycles with t1 and t2, moving tokens between a and b. Executing “a lot” of steps reveals why the state-space is infinite:
We see that while the behavior is finite, the time-stamps grow unbounded. This model, however, never looks at the absolute value of the time-stamp, but only uses it for delay. Therefore, the actual value of the time-stamp is not so important; we only care about the delay. We can use this to do reduction:
With this option switched on, we obtain a state-space with just 5 nodes:
The idea is that we ignore the actual model time only looks at how far into the future each time-stamp is. This effectively resets the model time after executing each transition, subtracting the model time from each time-stamp. We also do not care about any time-stamps that turn negative this way – if the time stamp is less than or equal to the model time, the token is ready, and the actual value has no influence on this.
This reduction works great in together with time ranges to make any model depending on delays only finite and analyzable, even in the presence of time intervals.
We have looked at time intervals in CPN Tools 4 and seen how they make it possible to select the random time-stamp during simulation, but more importantly make is possible to do state-space analysis of models which do not have constant duration. We have introduced the time-condensed state-spaces and seen how they can turn state-spaces that would otherwise be infinite finite if they only rely on delays and not on absolute time.
To see this in action, check out this video demonstration:
Time person of the year 2006, Nobel Peace Prize winner 2012.
- This could in principle be achieved before as well by introducing an unbound variable of a small integer type, but here we do not require that the type is small. [↩]