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