Go backward to Rewriting the Fairness Requirement
Go up to Top
Go forward to Syntax of Simple TLA
Examining Formula Phi
- Each TLA formula representing program:
- Init and always [A] and F
- Init specifies initial variable values.
- A is the program's next-state relation that represents
the execution of the inidividual atomic operations.
- is the tuple of all flexible variables.
- is a conjunciton of formulas of the form WF(A) and/or
SF(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!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine