Next: The assert declaration
Up: Assertions
Previous: Assertions
Contents
Temporal formulas may contain all of the usual expression operator of SMV,
plus the temporal operators G, F, X and U. The meanings of these operators
are as follows:
- X p is true at time
if p is true at time
.
- G p is true at time
if p is true at all times
.
- F p is true at time
if p is true at some time
.
- p U q is true at time
if q is true at some time
,
and for all times
but
, p is true.
A temporal formula is true for a given execution of the program if
it is true at the initial time (
).
2002-10-28