Dear Leslie,
thank you for your comments.
Yes, my reading includes chapter 14.
TLA+toolbox is a blackbox, if not
provide possibility to explore their internal mechanisms. And this is what users typically expect from Print
operator.
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.
Print becomes useful if we not
only get values, but know points / rules / structure of the output.
And this looks like a problem,
especially if we compare parser of a mathematical language with a parser of a programming
language, where structure of output is strictly defined.
Yes, to implement output in a
language composed from formulas Print also should be a formula.
I use Print only as true
formula, and try to avoid all possible optimisation issues, but not always may predict
/ explain structure of Print output. Another point that seems to be the output depends
on the TLC version as well.
Best regards,
Vitaliy.
I start with your book "Specifying Systems".
How much of that book have you read?
E.g. for the print function - how it can be used for analyses of TLA model if its work significantly depends on internal structure of TLC algorithm?
Print(a, b) is defined to equal b. As far as the meaning of a TLA+ specification goes, you can simply replace every instance of Print(a, b) with b. When you run TLC on a model of a specification, it prints out lots of things. What it prints out can depend on whether you write Print(a, b) rather than the equivalent _expression_ b. If you want to understand the output of TLC, you’ll have to learn about TLC—for example, by reading Chapter 14 of Specifying Systems.
Leslie