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 writeballots := [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.On 27 Sep 2018, at 14:29, Balaji Arun wrote:Hi,I am trying to perform the following operation in PlusCal\* list = {o1, o2}ballots' = [obj \in Objects |->                     IF obj \in list                    THEN [ballots[o] EXCEPT ![a] = obal]                    ELSE ballots[obj]]ballots is a function, and I only want to modify part of the function indicated by the list set.In programming, I can accomplish with a for loop, but PlusCal doesn't have one.Any ideas? -- 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+u...@xxxxxxxxxxxxxxxx. To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.