Go backward to Rewriting the Fairness RequirementGo up to TopGo forward to Syntax of Simple TLA |

- 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

Author: Wolfgang Schreiner

Last Modification: May 14, 1998