Dear Vitaliy,
In chapter 14 you said "TLC usually evaluates an _expression_ many
times, so inserting a Print _expression_ in the specification can
produce a lot of output." This exactly means that structure of
output reflects parsing procedure, but not structure of the model
or its behaviour.
TLC prints the value when it evaluates the Print statement.
Evaluation is not a mathematical concept; it is something that TLC
does when checking a specification. It makes no sense to implement
output in a language for writing formulas. Since printing is
something that's done by TLC, you need to understand TLC to try to
make sense of what gets printed. Section 14.2 explains in detail how
TLC works; in particular, it explains when TLC evaluates an
_expression_. It should explain the output TLC produces for Print
expressions.
How TLC evaluates expressions depends on the syntactic structure of
the _expression_ (its "parsing") not just on the semantics of the
_expression_. I don't know how any program can evaluate an _expression_
independently of the syntax in which the _expression_ is written.
Another point that seems to be the output depends on the TLC
version as well.
I find that surprising, and I would appreciate any example in which
different versions of TLC produce different output from evaluating
Print statements.
Leslie