[tlaplus] Initializing local variables in PlusCal

["'Ugur Yavuz' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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