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
]
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!
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998