\EE is the ASCII representation of the TLA temporal
operator that is printed as a bold \exists (existential
quantification) symbol. For any
temporal formula
F
and
flexible variable
x,
the formula
\EE x : Frepresents formula
F
with
x
"hidden".
To a first approximation, formula
\EE x : Fis true for a behavior
s1, s2, ...iff there exists a behavior
t1, t2, ...that satisfies
F
such that, for all N > 0,
states
sN and tN
are the same except for the values that they assign to
the
variable
x.
In the precise definition, one can add
stuttering steps
to the
behavior
s1, s2, ...before choosing the behavior
t1, t2, ....