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
On 17 Jan 2018, at 03:13, 杨永 <stephen...@gmail.com> wrote:
Hello, Stephan
Thanks for your help, but, I'm still confused with the problem.
You said that action formulas are evaluated over two states, that is, I should consider two states if I want to evaluate the Boolean value of an action.
For example, there is a behavior "s" with the state sequence as
s0 --> s1 --> s2 --> s3 --> ... --> sn
x=0 x=0 x=1 x=2
and an action [x'=x+1]_x.
Does it mean I should judge s0 and s1 in "s" if I want to determine the value of s |= [x'=x+1]_x?
As in this example, s0 --> s1 is a stuttering step, because this step satisfies [x'=x+1]_x that the value of "x" is UNCHANGED. So, s |= [x'=x+1]_x equals TRUE in this example.
However, the example in the book (Page 90) says "the action [ x' = x + 1]_x is satisfied by a behavior "s" in which x is left unchanged in the first step and incremented by 2 in the second step". Does the example means action [x'=x+1]_x also satisfies a behavior "s" as
s0 --> s1 --> s2 --> s3 --> ... --> sn
x=0 x=0 x=2 x=3
If the answer is yes, my question is: how does state s0 transit to s1?
I think the value of x in state s2 should be 0 or 1 if the step is a [ x' = x + 1]_x step while x=0 in state s1, because [x'=x+1]_x == (x'=x+1) \/ (x'=x), that is, the value of x should be UNCHANGED or increased by 1 in each step of the behavior.