Calvin, thank you taking time to respond. Was not aware of PlusCal Manual, section 3.2.8; noted. Just like printf can never replace a symbolic debugger, static analysis, and so on in regular programming languages, print can't be any bottom line in model checking. Agreed.
Still to write LTL expressions right one has to have a sense of what states are reachable, when, and in what format. In my earlier work I was stymied by the fact TLA was not reaching every legal next state I thought possible. `print` helped me see what went wrong because I could at least get a hint of what TLA was up to - what it was running - and places it never seemed to get to. Sometimes variables will have same values but in different states ... making print tough to interpret right ... motivating my earlier question.
Anyway, ... engaging question on better mechanisms than printf()-debugging" to learn about a system's behavior generalizing away from print,
* How/can we ask TLA to tell us legal next states from a specified label? Partial answer? the DOT diagram generator or error trace might be helpful here. The former eats memory on large state but otherwise spot on and the latter I do not understand.
* How/can we ask TLA to tell us about non-reachable labels? Periodically I see TLA pointing out unreachable code, however, not consistently. In my earlier case there was indeed code that was never hit, therefore my loop never continued, and therefore state I wanted to make never happened. Having TLA point out "hey, your label is never hit" would be a plus.
* A more operational question: I run TLA with a single LTL expression entered in Property section. The expression reads "LogSizeConsistent == <>([](LogSize=MessageIndex))". Only it is enabled. When TLA stops it reports "1 Error" under model checking results tab. The console shows,
---------
Checking temporal properties for the complete state space with 132 total distinct states at (2020-11-18 20:28:27)
Temporal properties were violated.
The following behavior constitutes a counter-example:
<39 states elided>
----------
Now as LogSizeConsistent is the only one enabled, I know which property failed.
TLA doesn't bother to name it. Why? Finally, no where in the counter example does TLA tell me the value of LogSize, which is a defined function. Nor does it refer to or name LogSizeConsistent in the counter example. Clicking on the hyperlink "1 Error" shows nothing new. TLA is probably right; but I am a lot perplexed about why.
Regards