Re: [tlaplus] Temporal property

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

I believe that you want to write

  Prop == [][x=1 => y'=2]_<<x,y>>

and check this as a temporal logic property. It asserts that whenever x or y change their values during a transition and x equals 1 in the first state, then y equals 2 in the second state.

Regards,

Stephan

On 2 Nov 2016, at 05:59, vit...@xxxxxxxxxx wrote:

Hi, is it possible in TLA to specify and check the property linking values of current and next states, like Prop == (x = 1) => (y` = 2). Seems to be the operation "=" for primed variables (as e.g. y') will be considered as assignement, but not comparison? Tq.