| "State" is a semantic notion. A state assigns a value to each variable (there are infinitely many variables in TLA, although a TLA+ module declares only finitely many variables and only the values assigned to these variables are relevant for evaluating the formulas that appear in the module).
State functions, state predicates, actions, and temporal formulas are syntactic notions. For example, a state function is an _expression_ that does not contain (free) primed variables or temporal operators etc. If x and y are variables than x, x+2, x \union y, { << x, s >> : s \in y }, x = y, x \in y, ~(x > y+42) are state functions.
And as you say, state predicates are state functions that evaluate to TRUE or FALSE. The three last examples above are state predicates.
State functions (and in particular state predicates) are evaluated over (single) states, actions are evaluated over two states, temporal formulas are evaluated over behaviors.
If you want to see a more formal definition, perhaps [1] can be helpful.
Regards, Stephan
Hi, Stephan The notation "[]s^(+n) |= F" is misspelled by I. It should be the right one you have given (s^(+n) |= []F).
I think I should make clear sense of all the concepts, such as temporal formula, state function, state predicate, state, action, and step, etc., includes their definitions and the purpose of using these concepts.
(page 15)
(1) ...state consists of the values of variables... (2) ...a state is an assignment of values to variables...
as (1) said state consists of the values of variables. Does it mean a state represents instantaneous values of variables? (2) says it is a assignment of values, does this mean a state is an operation in (2)? If it is not an operation, does a state just represent the current values of all variables in the system? My understanding is a state just represents the current values of all variables in the system.
Then,
(3) A state function is an ordinary _expression_ (one with no prime or 2 ) that can contain variables and constants. (page 25)
Does a state function mean an _expression_ that represents the current values of some or all variables in the system?
so,
(4) A state predicate is a Boolean-valued state function. (page 25)
Based on (3) definition of state function, it means a state predicate can evaluate the state function whether TRUE or FALSE.
For example, can I assume (val \in Data ) /\ (rdy = 0) /\ (ack = 1) a possible state function? and then, a state predicate evaluate this state function through judging current value of val, rdy, and ack?
Maybe, I make misunderstanding again.
I appreciate your kind help，
Yong
在 2018年1月19日星期五 UTC+8下午4:42:15，Stephan Merz写道： Temporal formulas need to be evaluated over behaviors (infinite sequences of states), not states, and s^(+n) denotes the suffix of the behavior s starting at the n-th state (so that s^(+0) is just s). Of course, if F is a state predicate, evaluation of s |= F actually only considers the first state of s.
I don't know what you mean by the notation "[]s^(+n) |= F", it does not appear in the book. In order to evaluate
s^(+n) |= []F
you consider all suffixes, i.e. you check whether
(s^(+n))^(+m) |= F i.e. s^(n+m) |= F
holds for all non-negative integers m.
Stephan
Hi, Stephan
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.
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...@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.
-- 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.
-- 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.
|