[tlaplus] Re: Simple Question - Safety and Liveness

On Wednesday, July 13, 2022 at 3:14:51 PM UTC-4 Andrew Helwer wrote:

Any logical formula over a step will have primed and unprimed variables. The primed variables refer to the values in the second state in the step, and the unprimed variables refer to the values in the first state in the step. We say this step formula is possible or enabled in a state if the subformulas containing only unprimed variables are true of that state (and I guess if the formula's primed variables don't have a logical contradiction like P' /\ ~P' or something? but maybe it will still be enabled even then). Basically if the precondition is satisfied. In your case, <<x’=x+2>>_x does not actually have any such preconditions (except maybe a variable x existing but maybe not even that) because it doesn't have a subformula containing only unprimed variables. So it will always be possible/enabled, but WF_v(A) and SF_v(A) can't be fairness properties because although A is always enabled, an A step is never taken.

An example of a formula which wouldn't always be possible/enabled is <<x % 2 == 0 /\ x' = x + 2>>_x, which will only be enabled when x is in a state where its value is even.

Andrew

On Wednesday, July 13, 2022 at 10:40:11 AM UTC-4 vcbar...@xxxxxxxxx wrote:
Hi,
I am trying to learn TLA+ as a Computer Engineering undergrad. I am reading the safety and liveness document from the TLA+ website and am trying to understand the definition of:

<<A>>_v = A /\ (v' \= v)

and when it is enabled. When I first read the definition, it seems this would be ENABLED in a behaviour specified by a formula S when there is a step allowed by S that satisfies:
A /\ (v' \= v).

But then this example is provided:

However, WF_v(A) and SF_v(A) need not be fairness properties. For example, let S equal (x=0) /\ [][x’=x+1]_x,
let A equal x’=x+2
and let v equal x.
An <<x’=x+2>>_x step is possible in any reachable state of S , but no such step satisfies x’=x+1. (A reachable state of S is one that occurs in some behavior that satisfies S .) Hence, no finite sequence of states satisfying S can be extended to satisfy S as well as WF_v(A) or SF_v(A).

So in this case, he's saying that <<x’=x+2>>_x is enabled in any state of a behavior satisfying S because a <<x’=x+2>>_x step is 'possible' in any state of S, but it is not a fairness property essentially because it's not actually allowed within the confines of S. What does possible mean in this case?

Thank you,

Victor