CIF 3

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:

../../../_images/user_state_space.png

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.