[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Temporal property

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,


On Thursday, November 3, 2016 at 12:50:33 PM UTC+8, Leslie Lamport wrote:

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.