How to capture a change in an element of an array in TLA+

Question

I am specifying a system whose state consists of a sequence:

VARIABLE Seq

The sequence is constrained to be of a certain type:

TypeInvariant == Seq \in [Nat -> [v1: {0,1}, v2: {0,1}]]

I want to allow, in the state machine, a transition of this type:

The system can move from a certain state to another where any of its elements gets its named property v2 changed from 0 to 1.

So, basically, in the sequence Seq, any element is allowed to cause a transition where the new sequence Seq' remains "the same" (same number of elements), but one element only changes:

[v1 |-> 0, v2 |-> 0]   ====>   [v1 |-> 0, v2 |-> 1]

How to write it in TLA+?

How do you specify such an action in TLA+? I have tried thinking about something like this:

\E s \in Seq : (s' = [s EXCEPT !.v2 = 1] /\ s.v2 = 0)

But I am really not sure if this is the way because I am priming something which is not a declared variable. Is it correct?

Answer 1

You can prime something that's not a declared variable, as long as A) it's part of a declared variable, and B) the variable was primed in a previous clause. In this case it acts as a constraint (the action won't happen if the clause is false.)

For your case, what you want to do is change the whole sequence at once:

\E i \in 1..Len(S):
   /\ S[i].v2 = 0
   /\ S' = [S EXCEPT ![i].v2 = 1]

Note that Len is from EXTENDS Sequences, if you don't want to import that, you can use DOMAIN S instead of 1..Len(S). Sequences also imports the Seq operator, which is why I suggest renaming your variable to something else, like S.