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.
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.
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
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
1.5) time units, before releasing the button (stop pushing it). After waiting another
2.3) time unit, the user pushes the button again. Finally, after waiting
2.4) time units, the user releases the button one last time. In the
done location, the
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.
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.
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.
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.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.