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

Re: [tlaplus] Alternatives to for loops in PlusCal


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]


[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 <ba2...@xxxxxx> wrote:


I am trying to perform the following operation in PlusCal

\* list = {o1, o2}
' = [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.