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)

Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine