Thanks a lot, Andrew.
From Lamport's paper or/and the book,
"An action represents a relation between old states and new states, where is unprimed variables refer to the old state and the primed variables refer to the new state."
"Formally, the meaning [[A]] of an action A is a relation between states--a function that assigns a boolean s[[A]]t to a pair of states s, t. "
Hence, if I have an action described as my previous email: x' + 1 = y+z
then the meaning of s[[x' + 1 = y+z ]] t:
s: (x, y,z) values.
t: (x', y,z) values. /* y and z are not changed after this action
In other words, in TLA, the state is NOT 1:1 mapped to a variable, but to the whole set of the variables.
Am I correct?