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