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

*From*: Huailin <huailin@xxxxxxxxx>*Date*: Thu, 22 Apr 2021 14:05:51 -0700*References*: <6841633b-0f09-4fa9-bedf-1d2345f680dbn@googlegroups.com> <f0c51d43-c594-44af-a30b-ded598c34182n@googlegroups.com>

Thanks a lot, Andrew.

__"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."__

__"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. "__

From Lamport's paper or/and the book,

and

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.

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

On Thu, Apr 22, 2021 at 6:38 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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--On Wednesday, April 21, 2021 at 11:48:27 PM UTC-4 hua...@xxxxxxxxx wrote: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

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f0c51d43-c594-44af-a30b-ded598c34182n%40googlegroups.com.

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAE7Z%3D%2B7X96c9p%3DoKvBMPJe2DUmD2J07VJS775GOQX3qHw%3DY9iw%40mail.gmail.com.

**Follow-Ups**:**Re: [tlaplus] Re: About Action***From:*Andrew Helwer

**Re: [tlaplus] Re: About Action***From:*Isaac DeFrain

**References**:**[tlaplus] About Action***From:*hua...@xxxxxxxxx

**[tlaplus] Re: About Action***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Floating Point operations to check equivalence of algorithms** - Next by Date:
**Re: [tlaplus] Re: About Action** - Previous by thread:
**[tlaplus] Re: About Action** - Next by thread:
**Re: [tlaplus] Re: About Action** - Index(es):