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.

## Time Intervals

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 probability distribution functions:

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.

## Time Reduction

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.

## Conclusion

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:

- 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. [↩]

Hi Micheal,

I am wondering why declare constraints are not supported with state space tools in version 4.0. As I remeber, it was supported in version 3.9.0.

Best Regards,

Carina Hu

Hi Carina,

It was never supported, the tool just didn’t correctly check for it. Basically, you could create a model with constraints and then compute the state-space, and the state-space wouldn’t honor the constraints. Now the tool ensures you get the correct results instead.

Hi Michael,

I have a doubt regarding timed state spaces.

So here’s a scenario:

Say the Initial marking for the model is @ Time = 0.

A token is generated at a particular place at say Time = 100 (under certain circumstances) which I would like to see in the bounded-ness properties of this place using the SS report.

When I fast forward to Time=100 in the simulation, I can see this token. After fast forwarding, if I generate a state space I can see this token in the bounded-ness properties of this place.

But at time = 0, if i directly generate the state space (with or without creationtime SET) and associated report, I CANT see this token in the bounded-ness properties of the place of interest.

Is there something I’m missing? Is there some parameter I need to set for timed state spaces? Or will time not progress along with the state space?..

You should definitely see your token if your model doesn’t make use of probability functions or the like. The state-space tool does not work with and of the random distribution functions. If you don’t use those, try mailing me your model and I can have a look.

Hi Michael,

I have a similar doubt about the calculation of State Space on TIMED petri net.

In my Timed Colored Petri Net (TCPN), when I Calculate State Space and save the State Space report, I find that there are total 6 nodes and 5 arcs in both State Space and Scc Graph.

I display the SS nodes one by one from initial state (1) to get the Occurrence Graph.

The followings are my doubts:

(1) the time stamp(if existence) after each place will be DECREASED by 1 from state, say n, to state n+1. Eg., in state “3 @ 1”, there are four tokens with time stamps: “1`a@1”, “1’b@1”, “1`c@6”, “1`d@7”, after a transition firing, we get state “4 @ 1”, but the corresponding four tokens above will become: “1`a@0”, “1`b@0”, “1`c@5”, “1`d@6”.

(2) after applying the State Space To Sim, the marking in simulator is inconsistent with the marking shown next to the state space node.

Can you help me? Thanks a lot.

I guess you are using CPN Tools 4 with time reduction. Then the behavior is completely according to expectation. The time is reset to the lowest occurring time stamp and the actual offset can be computed based on the transition. This can result in time decreases as you observe (check the paper on time reduction for details on how it works). Switch off time reduction to avoid this.

As for question 2, do you have a simple example showing this behavior?

Thanks, but the creationtime is UNSET, how can I totally switch off the time reduction (or check which paper…) ? 🙂

Hi Micheal,

I hope to know how to put the value of a time stamp into a variable.

Best Regards

Check this tutorial: http://cpntools.org/documentation/concepts/time/time_attributes_in_tokens

Hi Micheal,

Thanks a lot for helping me last time.

I have another question now. I hope to set a time delay on a transition which obey normal distribution. I found that the normal distribution function returns “real”, so I write the inscription as follow: @+RealToIntInf(normal(100.0,150.0)), but it shows a mistake there.

So, how to write the inscripition correctly?

Ps: I don’t quite understand the explanation for the function “RealToIntInf” on the help page.

Hi James,

Your inscription has two problems. First, RealToIntInf takes two parameters, the value to convert, and the precision (e.g., “RealToIntInf 3.52 1” returns 35, preserving one digit after the decimal point).

Second, @+ takes an integer as argument, not an intinf. In your case it is much easier to instead use the Real.round function, which returns the correct type.

Finally, note that “normal” can return a negative value (especially with those parameters), which is truncated to 0, making the distribution not really normal.

Hi Micheal,

Thanks a lot. The Real.round function is quite better. Also, I checked the link you gave and found a lot of help there.

Unfortunately, another problem arises. I hope to make a exponent operation so that I can transform dB to the ratio of numbers. I found the function “pow()” in “The Standard ML Basis Library” which would finish this work, but the CPN Tools recognise it as an unbound variable.

So, is there any way to make CPN Tools carry out mathematical calculations such as exponent, logarithm and so on ?

Most functions need a namespace; the pow function is in Math. For such questions, you should familiarize yourself with the SML basis library, where all general-purpose functions are documented.

Hi Michael

I want to ask if two different tokens use same transition and each has its own time process, how to do it as transition allows for one time definition ( such as @+8)

Regards

It is also possible to have time stamps on output arcs. This gets added to the time stamp of the transition (so if the transition has @+8, the arc ()@+5 and the transition is fired at time 17, the resulting time stamp is 8+5+17=30. It is allowed to leave the transition time empty for a default of 0.

the thing is i have one output arc

lets say i have part 1 and part 2 both enter same transition

part 1 done in 5 seconds and part 2 in 9

on same arc u can’t write expression with time for each part

You say the arc “enter” the transition? Time stamps should always be on arcs that leave the transition (output arcs). Timestamps on input arcs have a different meaning (it is used for pre-emption and should very rarely be used).

If you are really doing two different things, it is often a good idea to use two arcs, but it is possible to have a timed multiset on arcs, and write, e.g., “1`1@+5 +++ 1`2@+9”

Hello,

I need to compare the time of two tokens. A token is in one place P1 and the other in place P2, are under the transition t1. If both have equal times the transition will be enabled otherwise it will not. How do I do this in CPN tools?

You should very rarely compare time stamps. Time stamps are not values but conceptually model that a token is not produced yet.

If you really, really need to compare time stamps, make them part of the token values using the guide “embedding time stamps in tokens” from the CPN Tools homepage.

Where do I find this state space menu with the option “creation time”?

The menu is not identical to the screen-shots on my homepage. On my homepage, I often feature preliminary versions of CPN Tools, with options that have later been hidden (if they are not considered sufficiently stable or the like). Be especially wary if the second number of the version is odd – that indicates a test version.

You get the current version of the menu by dragging out the state-space tools, and right-clicking on the Calculate State-space icon to open the marking menu. Then select Set options. You can close the menu again using the marking menu. A good portion of tools have such options.

Hi Michael

I just want to know is there any method to convert the model time of a Timed CPN model either into minutes or seconds.

Thank You so much.

Hi Micheal,

Thanks a lot for helping me last week.

I have another question now. I’m using CPN tools 4.0.1 and I attached to the transition an interval time delay, as in your example: @[2,7].

I have this error:

Error in time region!

:1.103-1.114 Error: operator and operand don’t agree [tycon mismatch]

operator domain: [int ty] ms* [int ty list]

in expression:

(1 ‘1) @ (2 :: 7 :: nil)

Elaborate failure

Best regards,

Stefano

Hi Stefano,

Make sure you have the time range simulator loaded. It should be installed by default, but you can check by opening the extension server (the CPN icon in your task bar).

Regards,

Michael

Hi Michael,

I have a question about CPN tools I would like to ask you.

After I generate the space state for a time petri net, is there a query that allows me to find all nodes with a specific marking?

Cheers,

Marcello

Hi Marcello,

You can use the SearchNodes or similar functions. Refer to the state-space manual for the details of how the function works and variants of it.

Regards,

Michael