Go backward to Describing Programs with RTLAGo up to TopGo forward to Adding Liveness |

- Formula
`Phi`is too simple.- Should allow stuttering steps
- Leave both
*x*and*y*unchanged.

- Example: clock specification.
- Clock
*C*with hours_{1}*h*and minutes*m*. - Clock
*C*with hours_{2}*h*, minutes*m*, seconds*s*. *C*should statisfy specification of_{2}*C*._{1}- But
*C*has 59 steps where_{2}*h*and*m*do not change! - Such stuttering steps should be ignored.

- Clock
- 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}

- Elementary formulas of form

Author: Wolfgang Schreiner

Last Modification: May 14, 1998