A <EM>temporal formula</EM> is a Boolean-valued expression that can
contain 
 <A HREF = "variables.html">flexible and rigid variables</A>
and temporal operators.  Semantically, it is true or false
of a 
  <A HREF = "behavior.html">behavior</A>.
The temporal operators of TLA can be defined in terms of the primitive
operators 
    <A HREF = "box.html"><CODE>[]</CODE></A>
(&quot;always&quot;)
and
  <A HREF = "EE.html">\EE</A>
(hiding).