[Next] [Up] [Previous] [Contents]
Next: The assert declaration
Up: Assertions
Previous: Assertions
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 t if p is true at time t + 1.
- G p is true at time t if p is true at all times .
- F p is true at time t if p is true at some time .
- p U q is true at time t if q is true at some time ,
and for all times < t' but , p is true.
A temporal formula is true for a given exectution of the program if
it is true at the initial time (t = 0).
Ken McMillan
Sat Jun 6 21:41:59 PDT 1998