Syntax of Simple TLA
TLA logic without quantification.
- <formula><=><predicate>
| always [<action>]state function | not <formula>
| <formula> and <formula> | always <formula> - <action><=> boolean-valued expression
of constant symbols,
variables, and primed variables
- <predicate><=> action with no primed
variables
| Enabled <action> - <state function><=> non-boolean expression
containing constant symobls and variables
Author: Wolfgang Schreiner
Last Modification: May 14, 1998