[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: 杨永 <stephen...@xxxxxxxxx>*Date*: Mon, 15 Jan 2018 23:27:46 -0800 (PST)

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

**Follow-Ups**:**Re: [tlaplus] Confusion on "invariant under stuttering"***From:*Stephan Merz

- Prev by Date:
**TLA+ REPL** - Next by Date:
**Re: [tlaplus] Confusion on "invariant under stuttering"** - Previous by thread:
**Re: TLA+ REPL** - Next by thread:
**Re: [tlaplus] Confusion on "invariant under stuttering"** - Index(es):