[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Initialization of local variables in PlusCal

in PlusCal, I would like to initialize a local variable using the form "variable x \in expr" and use the variable self in expr.

From what I see, that is currently not supported by the translation to TLA+ in version 1.5.2 of the toolbox:
"variable x \in expr" creates a variable x initialized with "x \in [P -> expr]".
Why not change the translation and instead initialize
x with 
"x \in {f \in [P -> UNION {expr : self \in P}] : \A self \in P : f[self] \in expr}"?
Has this _expression_ a meaning in TLA+ if the variable
self does not appear in expr?