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

Conditionally modify array elements


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?


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.