- 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.

- Clock $C$
- Modification of
`Phi`:`Phi`$<=>$`Init`$$_{Phi}*and*`always`(`A`*or*($(x\text{'}=x)$*and*$(y\text{'}=y)$))`Phi`$<=>$`Init`$$_{Phi}*and*`always``A`_<$x,\; y$>- [
`A`]$$_{f}:=`A`*or*$(f\text{'}=f)$

- TLA is subset of RTLA
- Elementary formulas of form
`always`[`A`]$$_{f}

- Elementary formulas of form

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine $$