Re: [tlaplus] Curious oddity

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

On 03 Sep 2016, at 14:40, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

what do you think of that:

  x = y => [] x = y

Excuse-me Stephan Merz had already answered:

> A => next A  if A is rigid (i.e., does not contain any state variable)

> [We can replace next by []) 

What does a "state variable" mean?

In TLA jargon, it's a "variable". In contrast to a "constant", whose value is fixed by the model, independently of the state, variables may be assigned different values in different states.

Thus, your formula is valid if x and y are declared as CONSTANTS, but not if at least one of them is a VARIABLE.

Stephan