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

*From*: 杨永 <stephen...@xxxxxxxxx>*Date*: Thu, 18 Jan 2018 15:37:52 -0800 (PST)*References*: <1b505099-eddd-4365-8655-8a9b2a6e4f8c@googlegroups.com> <9CA40300-AA6F-4B2D-A67D-55E9E27784C7@gmail.com> <d31c3416-10f4-4ecf-8444-d1cc03f145bb@googlegroups.com> <E574A767-4407-43BC-98F7-EC14857680A1@gmail.com>

Hi, Stephan

在 2018年1月18日星期四 UTC+8下午3:48:40，Stephan Merz写道：

Thanks a lot for your patient explanation. I think I seemed to understand a little bit. Can I understand from s^(+n) |= F that we just consider the state at time n for temporal formula F without considering the state of other states at any other time? and, as for []s^(+n) |= F we should consider all states of the behavior s?

Thanks again for your help!

best regards,

Yong

在 2018年1月18日星期四 UTC+8下午3:48:40，Stephan Merz写道：

Hello again,I'll try to be clearer this time.On 17 Jan 2018, at 03:13, 杨永 <steph...@xxxxxxxxx> 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?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=3Again, 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 behaviors1 --> 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,StephanYou 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...@googlegroups.com .

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**:**Re: [tlaplus] Confusion on "invariant under stuttering"***From:*Stephan Merz

**References**:**Confusion on "invariant under stuttering"***From:*杨永

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

**Re: [tlaplus] Confusion on "invariant under stuttering"***From:*杨永

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

- Prev by Date:
**Re: [tlaplus] Run TLC model checker in Azure** - Next by Date:
**Re: [tlaplus] Reusing PlusCal processes in multiple models/modules** - Previous by thread:
**Re: [tlaplus] Confusion on "invariant under stuttering"** - Next by thread:
**Re: [tlaplus] Confusion on "invariant under stuttering"** - Index(es):