Hello,
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?