[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.