Confusion on "invariant under stuttering"

[杨永 <stephen...@xxxxxxxxx>]

Hi, guys

I am reading "TLA+ Specifying Systems", and I'm confusing on the problem of invariant under stuttering(Page 90). The 3rd paragraph is as follows:

A state predicate (viewed as a temporal formula) is invariant under stuttering, since its truth depends only on the first state of a behavior, and adding a stuttering step doesn't change the first state. An arbitrary action is not invariant under stuttering. For example, the action [ x' = x + 1]_x is satisfied by a behavior $a$ in which x is left unchanged in the first step and incremented by 2 in the second step; it isn't satisfied by the behavior obtained by removing the initial stuttering step from $a$ . However, the formula [][ x' = x + 1]_x is invariant under stuttering, since it is satisfied by a behavior iff every step that changes x is an x' = x + 1 step -- a condition not a affected by adding or deleting stuttering steps.

My question is,

since [A]_f = A \/ (f'=f), I think, in action [ x' = x + 1]_x, x is left unchanged in the first step, the second step should be increased x by 1 after execute the action. How to understand that "x is incremented by 2 in the second step"?


Thanks,

Yong