Clocked Transition Systems
Clocked transition systems
can be used to model discrete or continuous real-time systems,
and are partially supported in the educational release of STeP.
Clocked transition systems differ from
fair transition systems in the following ways:
-
There are designated clock variables T, the master clock,
(global time)
and tick (time progress measure) which may
not be changed by the standard transitions.
Only T may be used in the standard transitions.
Initially T is set to 0.
These variables are declared automatically when
a clocked transition system is specified.
-
Fairness conditions on transitions are
irrelevant, and therefore only the condition
NoFairness is allowed.
- The user can specify a special progress condition.
It restricts the amount that time is allowed to progress
between the standard transitions.
The progress condition is written as:
Progress expn
where expn is assumed to be
a first-order formula F(clock1,...,clockn,T),
with the auxiliary clocks clock1,...,clockn
and the global clock T as free variables.
The progress condition corresponds to a transition of
the form:
Transition tick:
modvar tick
enable tick > 0
/\ Forall t : rat .
(0 <= t /\ t <= tick --> 1
F(clock1+t,...,clockn+t,T+t))
assign
(clock1,..,clockn,T) := (clock1+tick,...,clockn+tick,T+tick)
which is generated automatically by the parser.
It is helpful to think about this transition as one
that allows time to progress from T to T + tick,
whenever the progress condition F is satisfied
for all intermediary values between T and T + tick.
Clock variables are always of type real.
The (now)
classic railroad crossing real-time system
has been described using
Clocked
Transition Systems.
step-comments@cs.stanford.edu
Last modified: Fri Jul 17 10:42:20 PDT 1998