Go backward to Semantics of Simple TLA Go up to Top Go forward to The Rules of Simple Temporal Logic

Additional Notation

• p' <=> p(forall 'v': v'/v)
• [A]_f <=> A or (f' = f)
• <A>_f <=> A and (f' notequal f)
• Unchanged f <=> f' = f
• eventually F <=> not always not F
• F |-> G <=> always (F => eventually G)
• WF_f(A) <=>(always eventually <A >_f) or (always eventually not Enabled <A>_f)
• SF_f(A) <=>(always eventually <A >_f) or (eventually always not Enabled <A>_f)