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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Tue, 16 Jan 2018 15:13:27 +0100*References*: <1b505099-eddd-4365-8655-8a9b2a6e4f8c@googlegroups.com>

Hello, action formulas are evaluated over two states. The action formula [x'=x+1]_x is true for two states s and t if either the two states assign the same value to x or if the value of x in t is the value of x in s plus one. Any formula [A]_f is true for a stuttering transition (two identical states), independently of the actual formula A. As an extreme example, [FALSE]_f is true for a stuttering transition, but false for any non-stuttering transition. These examples show that [A]_f is in general not invariant under stuttering: assume for a moment that [A]_f were a temporal formula (similarly as state predicates are lifted to temporal formulas) and suppose that you evaluate that formula over a behavior that starts with a stuttering transition, then that behavior satisfies [A]_f. If you remove the initial stuttering transition, there is no reason why the resulting behavior should still satisfy [A]_f. This is exactly the point of the example given in the book. In contrast, it is not hard to convince yourself that the temporal formula [][A]_f is invariant under addition or removal of (finitely many) stuttering transitions. Hope this helps, Stephan > On 16 Jan 2018, at 08:27, 杨永 <stephen...@xxxxxxxxx> wrote: > > 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 > > -- > You received this message because you are subscribed to the Google Groups "tlaplus" group. > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > Visit this group at https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:

**References**:

- Prev by Date:
**Confusion on "invariant under stuttering"** - Next by Date:
**How to define a partial function and add an element to a set of functions in TLA+?** - Previous by thread:
**Confusion on "invariant under stuttering"** - Next by thread:
**Re: [tlaplus] Confusion on "invariant under stuttering"** - Index(es):