| Hello, unless you want to explore the impact on non-atomic updates in concurrent contexts (in which case you'd also need to break up your action into multiple updates in a TLA+ specification), there is no need to program this update as an explicit loop in PlusCal. The power of PlusCal comes from its use of TLA+ expressions in algorithms. You can simply write ballots := [obj \in Objects |-> IF obj \in list THEN obal ELSE ballots[obj]] in your PlusCal algorithm. [1] Regards, Stephan [1] Note that I'm replacing the subexpression "[ballots[o] EXCEPT ![a] = obal]" by "obal" since I am assuming that this is what you actually intend in the TLA+ excerpt: why would you replace an array element with an entire array, also "o" is not defined. I am assuming that "obal" is defined in the context of the TLA+ excerpt that you are showing here.
|