Module 5.2: Variable 'time'

In CIF, the variable time is always present; you don't have to declare it. In this variable, the time that has passed is tracked. So, it for instance indicates the time since a simulation of the model started.

Officially, the unit of time is not defined by the CIF language. However, CIF tools interpret time by default as being represented in seconds. Some tools allow it to be configured, essentially making time run faster or slower.

Variable time is of type real. While type int only allows whole numbers, type real also allows for instance values 0.0004, 1.5 and 3015.4673519. Variable time initially has value 0.0, and it gradually increases as time goes on. For instance, one simulated second later it is 1.0, yet again a simulated second later it is 2.0, and another simulated half a second later it is 2.5. Keep in mind that simulated time may run faster or slower than wall-clock time.

The value of variable time can be used in the model like that of any other variable. It can thus for instance be used in guards. However, variable time is read-only. You thus can't assign it new values, similar to how algebraic variables can't be assigned a value.

Example

As an example of using variable time, consider the following CIF model:

                        
                            automaton Stopwatch:
                                event time_passed;

                                location Zero:
                                    initial;
                                    marked;
                                    edge time_passed when time >= 60  goto One;

                                location One:
                                    edge time_passed when time >= 120 goto Two;

                                location Two:
                                    edge time_passed when time >= 180 goto Three;

                                location Three;
                            end
                        
                    

The Stopwatch automaton models a stopwatch. It counts the number of full minutes of time that have passed, up to three minutes. Initially, Zero full minutes have passed. Once variable time reaches 60, the first minute has passed, and the automaton goes to its One location. That is, the automaton stays in the Zero location for the first minute, and only when the guard holds does it transition to the One location. Then, once 120 seconds have passed, it goes to its Two location, and similarly it goes to its Three location once 180 seconds have passed. The automaton only tracks passage of up to three minutes, and thus in location Three it stops tracking time. Note the ; after Three, which indicates that this location has no elements, such as initial, marked or edges. Time will still pass, and thus variable time still increases in value, but event time_passes is not enabled, and thus no more transitions can occur for it. Time may then progress indefinitely, while the automaton stays in its Three location.

By using time in the guards, the behavior of the model becomes time-dependent. For instance, the occurrence of transitions for the time_passed event in the example above depend on the passage of time.

You may have noticed that we used guard time >= 60. You could have expected time = 60, since the event should be enabled after 60 seconds, and not after 60.1 or 63 seconds. And theoretically, you'd be correct. However, practically, variable time has value 60 only for an infinitely small duration. When for instance a simulator measures time, it will likely not evaluate the guard exactly when time is 60. If it regularly checks whether the guard has becomes enabled, it could also determine that the guard holds just after a minute has passed, for instance when variable time is 60.0000000000001 or so. Guard time >= 60 thus indicates that the event becomes enabled after a minute has passed. The simulator will try to enable the event as soon as possible after a minute of time has passed. Using time = 60 as guard means that in most cases the event will not get enabled, as the simulator will not check at exactly the right moment.

We can visualize the state space of the stopwatch as follows:

Initially, the automaton is in its Zero location, and no time has passed, so the model starts in the (Zero, 0.0) state. Then 60 seconds pass (or a little bit more), by means of a time transition. The model is then in the (Zero, 60.0) state. There are in fact infinitely many states between the (Zero, 0.0) and (Zero, 60.0) state, such as (Zero, 0.0000000000001), (Zero, 0.00000034) and (Zero, 0.71). And between them are infinitely many time transitions. We can however combine consecutive time transitions to form longer time transitions. And since we can't depict infinitely many states and transitions, we represent them by an arrow labeled with the time that passes between the states, namely 60.0 seconds, representing the full combined time transition between the states. The time_passed event then becomes enabled in state (Zero, 60.0), and by an event transition for this event we get to the (One, 60.0) state. Time then passes again, taking the model to the (One, 120.0) state, and so on. Once the model reaches the (Three, 180.0) state, time can progress infinitely, as indicated by the infinity symbol (∞). The state space of a hybrid model thus has two types of transitions: event transitions and time transitions.

Event urgency

In CIF, events are urgent. This means that if an event is enabled, it takes priority over passage of time. As long as at least one event is enabled, time will not progress. This also means that in the example above, event time_passed will not happen after 63 seconds, but really as soon as possible after a minute has passed. We will look at the concept of urgency in more detail later in this module.

Quiz