| Hello again,
I'll try to be clearer this time.
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?
First of all, an action formula is not a temporal formula, so TLA does not really define the semantics of s |= [x' = x+1]_x. But for the sake of the argument, let's pretend it was and let's take s |= A (for an action A) to mean that A is true of the first two states of s, just as the meaning of s |= P for a state predicate P is that P is true of the first state of s. So, indeed, we look at states s0 and s1 in order to find out if the formula holds. 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.
Exactly.
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
Again, we look at states s0 and s1, and since the variable x has the same value in both states, the formula again evaluates to true for this behavior. However the formula is false for the behavior
s1 --> s2 --> s3 --> ...
which results from s by removing a stuttering transition, and this shows that the formula [x' = x+1]_x is not invariant under (addition or removal of) stuttering. If the answer is yes, my question is: how does state s0 transit to s1?
I think here is the root of your misunderstanding. When we evaluate the semantics s |= F for a behavior s and a formula F, both are given to us and we don't ask how the behavior or the formula are produced. Your sequence s above is a behavior, so it makes sense to ask if some formula, such as [x' = x+1]_x, is true or false of it. 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.
The action formula [x' = x+1]_x only considers states s0 and s1, therefore it does not restrict in any way the value of x in state s2. On the contrary, the temporal formula [][x' = x+1]_x considers all states of s, and that formula is false of the behavior s, and of the suffix starting at s1.
Hope this helps, Stephan You said "Any formula [A]_f is true for a stuttering transition (two identical states), independently of the actual formula A.". As in this example, the value of x in state s1 is 0, if [x'=x+1]_x is TRUE, either (x'=x+1) or (x'=x) should be executed which leads to the value of x in state s2 equals 1 or UNCHANGED (i.e., 0). x'=x should be executes if we do not consider x'=x+1, so, the value of x should be 0 in state s2 in this example. I'm confused how does the value of x become 2 in state s2 while it is 0 in state s1. If the answer is no, could you please list the transition of state under action [ x' = x + 1]_x satisfies that x is left unchanged in the first step and incremented by 2 in the second step? Or, is there any misunderstanding? Kind regards, Yong 在 2018年1月16日星期二 UTC+8下午10:13:32，Stephan Merz写道： 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...@gmail.com> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.
-- 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.
|