[tlaplus] About Action

["hua...@xxxxxxxxx" <huailin@xxxxxxxxx>]

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