//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[lang-tut-time-chapter-intro]]
== Timing

indexterm:[timing]
indexterm:[timed system]
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.

indexterm:[time]
indexterm:[variable,time]
indexterm:[time,variable]

[[lang-tut-time-chapter-intro-var-time]]
=== 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 <<lang-tut-time-chapter-continuous-variables,continuous variables>>, discussed in the next lesson.

=== Timed guards

Consider the following CIF specification:

[source, cif]
----
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.

indexterm:[transition,event]
indexterm:[transition,time]

=== Time transitions

The state space of the above specification is:

image::{lang-tut-imgsdir}/time/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 <<lang-tut-time-chapter-urgency,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 <<tools-cifsim-chapter-index,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 <<tools-cifsim-solver-chapter-root-problems,miss the change>> in enabledness of the edge, and will never enable the event.
