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