Re: [tlaplus] Conditionally modify array elements

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

the main reference for getting started with TLA+ is the Hyperbook, available at http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html. More generally, the documentation available from http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html is very helpful if you take the time to study it.

From your message, it seems that you are talking about PlusCal. The initialization of the variable is syntactically incorrect, a function (array) value is written in TLA+ in the form [p \in S |-> e]. You can use a similar form to assign a new value to the variable in the process body in a single step (hint: the expression may contain references to the existing array). More conventionally, you could use a while loop to assign individual array elements in different steps. Deciding the "grain of atomicity" in the model of a computation is one of the main design choices. Again, the Hyperbook will give you more information.

Hope this helps, and happy exploring.

Stephan


> On 11 Nov 2015, at 20:18, fai...@xxxxxxxxx wrote:
> 
> Hi,
> 
> I'm new to TLA+ and unable to figure out a way to solve the below problem:
> 
> I have a array a, and would like to modify certain elements in the array if they satisfy some condition. How could I achieve this?
> 
> Eg:
> 
> variable a = [\A p \in 1..N |-> p]
> 
> now in the process body, I would like to achieve:
> 
> \A p \in 1..N, if (a[p] < k) then a[p] = k+1
> 
> Please help me with the syntax to achieve the above result.
> 
> -- 
> 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 http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.