Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?

No.

Let me defend Markus's response though, which I think actually adds much more value than mine.

PlusCal's print statement is much less useful and much more confusing than you are probably imagining. I believe PlusCal should never have been given a print statement in the first place! Did you know that "TLC may print the value even if the step containing the print statement is not executed" [PlusCal Manual, section 3.2.8]? Did you know that consecutive printed lines are probably not from consecutive states of execution? It is quite reasonable for the first answer to be one that discourages you from such a bizarre language primitive. :)

The good news: TLA+ has much better mechanisms than "printf()-debugging" to learn about a system's behavior. Markus is not suggesting that you have failed to write good correctness properties; he is suggesting that the same TLA+ mechanisms that let you check correctness properties can also be used to explore other properties as well! So let's pop up a level... what properties are you interested in?

Calvin

On Mon, Nov 16, 2020 at 1:57 PM recepient recepient <netsmaza@xxxxxxxxx> wrote:

Programmers unlike other engineers tend to comment on questions not asked ... then not answer the question as asked ... thereby adding no value. The rule is: answer the question as-is, then of course, continue on to other thoughts.

In this case this comment,
>TLC check suitable properties
is fully implied to using a model checker in the first place.

I asked the question I did because I still continue to find TLA+'s interpretation of PlusCal code (see the issue elsewhere in this group) weird. Print helps me understand how TLA thinks in small corner cases.

On Monday, November 16, 2020 at 3:13:16 PM UTC-5 Markus Alexander Kuppe wrote:
On 16.11.20 09:28, recepient recepient wrote:
> ... to do something like,
>
> print << __state_num__, msgQueue >>; (* perhaps state_num is hash on
> current state *)
>
> to help disambiguate msgQueue in different states which have the same valu?

You don't give much detail or context, but you appear to be relying on
TLC's print operator to understand your spec. Don't do this! Instead,
have TLC check suitable properties for which it produces useful
error-traces.

Markus

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/999ac752-32a6-4195-b94f-9c03917927b5n%40googlegroups.com.