About Action

[hua...@gmail.com]

Folks,

For an TLA's action, which is essentially a boolean expression, does it ONLY relate to two variables(primed or non-primed)?

For instance,  x' + 1 =y. (Please refer to Section 2.3 in Lamport's seminal paper "The Temporal Logic of Actions"-ACM 1993).

Can we have an  x' + 1 = y+z  as an action? If yes, how we define the "old state" and the new state with the postfix notation? maybe define a super-state to cover (y, z)?

Thanks huge,

Huailin

[Andrew Helwer]

Hi Huailin,

The formula x' + 1 = y + z is syntactically valid and can be used in an action property, but if you want to use TLC it cannot be used in an action itself. See Specifying Systems p238 for the expressions TLC can handle when computing successor states; they include expressions of the form:

• x' = e
• x' \in S
• UNCHANGED x

Andrew

[Huailin]

Thanks a lot, Andrew. 

From Lamport's paper or/and the book, 

"An action represents a relation between old states and new states, where is unprimed variables refer to the old state and the primed variables refer to the new state."

and 

"Formally, the meaning [[A]] of an action A is a relation between states--a function that assigns a boolean s[[A]]t to a pair of states s, t. "

Hence, if I have an action described as my previous email: x' + 1 = y+z 

then the meaning of s[[x' + 1 = y+z ]] t:

s: (x, y,z) values.

t: (x', y,z) values. /* y and z are not changed after this action

 In other words, in TLA, the state is NOT 1:1 mapped to a variable, but to the whole set of the variables.

Am I correct?

Thanks,

Huailin

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/8tZQbkMScgU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f0c51d43-c594-44af-a30b-ded598c34182n%40googlegroups.com.

[Isaac DeFrain]

Hello Huailin,

Yes, a state in TLA+ is an assignment of values to all variables declared in the spec. For example, if you have variables x, y, and z declared, then to define a state, we must provide values for each variable x, y, and z.

You can try defining an action, say Action, which does not say how the value of z, for example, changes between states. TLC will throw the following error: Successor state is not completely specified by action Action of the next-state relation. The following variable is not assigned: z.

For example, the spec:

---- MODULE Variables ----

EXTENDS Naturals

VARIABLES x, y, z

Action1 ==
    /\ x < 10
    /\ x' = x + 1
    /\ y' = y + 1

Action2 ==
    /\ x < 10
    /\ y + z >= 1
    /\ x' = y + z - 1
    /\ UNCHANGED <<y, z>>

Init ==
    /\ x = 0
    /\ y = 0
    /\ z = 0

Next == Action1 \/ Action2

Spec == Init /\ [][Next]_<<x, y, z>>

====

Action1 does not specify the value of z in a successor state... Maybe you actually do not want the value of z to change so you can add UNCHANGED z to Action1 and TLC will perform a successful model check.

Note: x' = y + z - 1 is equivalent to x' + 1 = y + z, but as Andrew suggested, you must write it in the form x' = y + z - 1 in order for TLC to evaluate it properly.

Best,

Isaac DeFrain

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAE7Z%3D%2B7X96c9p%3DoKvBMPJe2DUmD2J07VJS775GOQX3qHw%3DY9iw%40mail.gmail.com.

[Andrew Helwer]

I can't really speak to how it works with TLA, but in TLA+ you would need more than the formula x' + 1 = y + z to fully specify the successor state. For one, you would need to specify that y and z remain unchanged, since the formula x' + 1 = y + z would be true even if y and z were to have silly values in successor state t, like y = "green eggs" and z = "ham".

In general a state is an assignment of values to all variables. A spec just captures a small number of those variables out of all the variables in the system, and the world. And each action in the spec must fully specify the values of each spec variable.

Andrew

[Huailin]

Thanks, Isaac. 

Your illustration makes much sense to me. 

Just like what Lamport also used in his literature for example purpose: If we wanna define a moving object's position spec. in the universe, we used x, y, z three variables in a spec.  to describe its coordinates. But the STATE for the object's position is ONE, which is  the collection of the 3 variables. We cannot say the object has 3 states, while it does have 3 variables. 

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxFR%3DZmPmNzOp_Tkzhh%2BSDvGCQo9ZM0FFda1wd%2Bf4u7vDQ%40mail.gmail.com.