Conditionally modify array elements

[fai...@xxxxxxxxx]

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.