Thanks! This is exactly my problem, and I see that you have a good definition of the property I'm looking for:
"We will then establish a reduction theorem that shows that for every fine-grained run there exists an equivalent round-based (“coarse-grained”) run in the sense that the two runs exhibit the same sequences of local states of all processes, modulo stuttering"
The question is, then, suppose I have a set of such local state variables, how do I specify in TLA+ "this variable always obtains the same sequence of values modulo stuttering"?
Ron