Hi Marc,
TLC was written to evaluate TLA+ specifications.
It uses various optimizations that take advantage
of mathematical properties--for example, that
no matter how many times an _expression_ is
evaluated, it always returns the same result. For
various reasons, certain hacks have been added to
make TLC act as if it were not evaluating
mathematics and were instead executing a
programming language. These interact in strange
ways with TLC's optimizations. While there were
good reasons to add these hacks, they are not good
enough to subvert TLC's main purpose: to evaluate
TLA+ specifications as efficiently as possible.
When using those hacks, you will just have to
learn to live with their strange behavior.
Dominik Hansen has explained one of TLC's
optimizations: trying to compute constant
expressions only once. It therefore (usually)
precomputes definitions of the form
identifier == constant _expression_
I'm not sure if it does the same thing for LET
definitions, or only computes the value with the
first use of the definition. You can experiment
to find out what it does for LETs. As Dominik
pointed out, you can prevent this once-only
computation by giving the defined operator an
argument.
Another thing that TLC often does is lazy
evaluation, not evaluating an _expression_ until it
needs the _expression_'s value. For recursive
definitions, this can be a pessimization. It
could also lead to problems when trying to use
RandomElement. The operator TLCEval has been
added to the TLC module to cause eager evaluation.
See its description in the document "Current
Versions of the TLA+ Tools".
Leslie