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

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.