Go backward to
Describing Programs with RTLA
Go up to
Top
Go forward to
Adding Liveness
TLA
Formula
Phi
is too simple.
Should allow
stuttering steps
Leave both
x
and
y
unchanged.
Example: clock specification.
Clock
C
1
with hours
h
and minutes
m
.
Clock
C
2
with hours
h
, minutes
m
, seconds
s
.
C
2
should statisfy specification of
C
1
.
But
C
2
has 59 steps where
h
and
m
do not change!
Such stuttering steps should be ignored.
Modification of
Phi
:
Phi
<=>
Init
Phi
and
always
(
A
or
(
(x'=x)
and
(y'=y)
))
Phi
<=>
Init
Phi
and
always
A
_<
x, y
>
[
A
]
f
:=
A
or
(f'=f)
TLA is subset of RTLA
Elementary formulas of form
always
[
A
]
f
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998
