TLA logic without quantification.
| always [<action>] | not <formula>
| <formula> and <formula> | always <formula>
of constant symbols,
variables, and primed variables
| Enabled <action>
containing constant symobls and variables