Initializing local variables in PlusCal

[Ugur Yavuz]

In PlusCal, one can initialize local variables under a process statement through declarations of the form variable z = exp or variable z \in exp. Under procedure statements, however, this is limited to the first form only, and there is no non-deterministic initialization.

Is there a particular reason for this restriction?

[Andrew Helwer]

Hi Ugur,

When I read this I thought to myself "it must be because the variables are translated to a LET/IN or something" but after testing it I see that is not the case, they are (secretly global) variables like everything else. Whatever pluscal manuals I can find online also do not shed light on this question; for example, The PlusCal P-Syntax Manual only says:

The procedure statement is optionally followed by declarations of vari-
ables local to the procedure. These have the same form as the declara-
tions of global variables, except that initializations may only have the form
“variable = expression”. The procedure’s local variables are initialized on
each entry to the procedure.

So this is a good question! My only speculation is that nondeterministic procedure calls were thought to be unintuitive, or capable of generating TLA+ code that TLC could not easily handle. But it would be nice for someone with more knowledge of PlusCal to chime in.

Andrew

On Thu, Oct 30, 2025 at 4:49 PM 'Ugur Yavuz' via tlaplus <tla...@googlegroups.com> wrote:

In PlusCal, one can initialize local variables under a process statement through declarations of the form variable z = exp or variable z \in exp. Under procedure statements, however, this is limited to the first form only, and there is no non-deterministic initialization.

Is there a particular reason for this restriction?

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/1d422e3b-2c78-42ed-bc84-71ab200e76bfn%40googlegroups.com.

[Ugur Y. Yavuz]

Yes, that's what I saw in the manual as well, but I was a bit surprised there wasn't any further explanation. In principle, one could just initialize those variables non-deterministically as part of a process declaration instead, and the procedures would effectively inherit them. But it's nice to be able to declare variables alongside the parts of code they belong to, rather than elsewhere.

In my particular case, I didn't actually need non-determinism, but it still felt odd to have to hand-pick a value from the intended domain. Fortunately, initializing with something like CHOOSE v : v \in Domain did the trick for me: picking a fixed, yet arbitrary value, keeping the initial value abstract enough for my purposes.