- Each TLA formula representing program:
`Init`*and*`always`[`A`]$$_{f}*and*F`Init`specifies initial variable values.`A`is the program's next-state relation that represents the execution of the inidividual atomic operations.- $f$ is the $n$ tuple of all flexible variables.
- $F$ is a conjunciton of formulas of the form WF$$
_{f}(`A`) and/or SF$$_{f}(`A`) wher`A`represents a subset of the program's atomic operations.

- Parallel composition:
- Two programs represented by
`Phi`and`Psi`. - No variables in common
`Phi`*and*`Psi`describes parallel composition of both programs!

- Two programs represented by

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

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