Timing
So far, the tutorial has only used discrete event models as examples, which are all untimed. This lesson introduces the concept of timing.
In CIF, time starts at zero (0.0
). Time can progress continuously. That is, after one unit of time has passed, the model time is 1.0
. After an additional one and a half time units have passed, the model time is 2.5
, etc. By default, one time unit corresponds to one second. However, you can decide to use another unit, and tools such as the simulator can be configured to speed up or slow down the simulation accordingly.
Variable time
A variable named time
is always available in every specification. The variable holds the current absolute model time as its value, and can be used throughout the model. Initially, time and thus the value of variable time
start at zero (0.0
). As time progresses, the value of variable time
is automatically updated to ensure it properly represents the current time of the system.
In this lesson, absolute time will be used. In most models, it is easier to use relative time. This can be achieved with continuous variables, discussed in the next lesson.
Timed guards
Consider the following CIF specification:
event push, release;
automaton user:
location start1:
initial;
edge push when time >= 1.5 goto stop1;
location stop1:
edge release when time >= 2.3 goto start2;
location start2:
edge push when time >= 2.4 goto stop2;
location stop2:
edge release when time >= 7.6 goto done;
location done;
end
The push
and release
events represent pushing and releasing of a button respectively. The actual behavior of the button itself is omitted. The specification does model the behavior of a user
. Initially, the user
is in location start1
, and no time has passed. The edge with the push
event is not yet enabled, as the guard is not satisfied. As soon as one and a half time units have passed, the guard condition becomes satisfied, and the push
event becomes enabled. This edge models that the user starts to push the button after 1.5
time units. The user then waits for another 0.8
(2.3
- 1.5
) time units, before releasing the button (stop pushing it). After waiting another 0.1
(2.4
- 2.3
) time unit, the user pushes the button again. Finally, after waiting 5.2
(7.6
- 2.4
) time units, the user releases the button one last time. In the done
location, the push
and release
events are never enabled (no edges for those events), and thus the user never pushes or releases the button again. No other events are enabled, so time keeps progressing forever, without any events happening.
Time transitions
The state space of the above specification is:
The states are labeled with the names of the current locations of automaton user
and the current values of variable time
. The transitions labeled with event names are event transitions. The other transitions are time transitions, which are labeled with the duration of the time transitions, i.e. the number of time units that passes. At the end of the state space, a time transition of infinite duration is shown, to indicate that time can progress forever.
The current locations of automata can not change as time passes as the result of taking a time transition. The only way for the current locations to change, is as the result of taking an edge as part of an event transition.
Urgency
By default, all events in CIF are urgent. Events being urgent means that edges are taken as soon as possible. In other words, event transitions take priority over time transitions. Time can only progress if no event transitions are possible. For further details on urgency, see the future urgency lesson.
Numeric time
In the above example, guard time >= 1.5
is used. You might wonder why the guard is not time = 1.5
, as the intention is that user pushes the button after exactly 1.5
time units, and not after 1.6
or 1.7
time units. The main reason is that the simulator uses finite precision in its numeric calculations to find the moment in time that the edge becomes enabled. The answer also has finite precision. It is often not exactly at 1.5
time units, but is slightly after it, say at time 1.50000000000001
. If you use time = 1.5
as guard instead of time >= 1.5
, the simulator will most likely miss the change in enabledness of the edge, and will never enable the event.