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

Re: [tlaplus] Curious oddity




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