Re: [tlaplus] Alternatives to for loops in PlusCal

I forgot to remove the element from the set todo, the correct PlusCal snippet should be

todo := list;

w: while (todo # {}) {

with (o \in todo) {

todo := todo \ {o};

ballots := [ballots EXCEPT ![o] = ...]

}

Stephan

On Friday, October 5, 2018 at 9:09:19 AM UTC+2, Stephan Merz wrote:

Hi,

sorry for the late reply. If you want to modify your array non-atomically, you can write something like the following:

variable todo = {}; \* add an auxiliary variable to your variable declarations

todo := list;
w: while (todo # {}) {
with (o \in todo) {
ballots := [ballots EXCEPT ![o] = ...]
}
}

Hope this helps,
Stephan

On 29 Sep 2018, at 15:04, Balaji Arun <ba2...@xxxxxx> wrote:

I see. I want the change to be an atomic action, so I will keep what I have. Thank you!

But, just to understand, how could I split this up in PlusCal and keep it non-atomic?

btw, the ballots is a function of a function. I am trying to update an array element within an array.

On Thursday, September 27, 2018 at 8:29:03 AM UTC-4, 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+unsubscribe@googlegroups.com.
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.