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

[tlaplus] About Action


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,


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/6841633b-0f09-4fa9-bedf-1d2345f680dbn%40googlegroups.com.