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

[tlaplus] Simple Question - Safety and Liveness

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,


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/befc81a6-d74d-4c08-ae5d-2fc6a18d53cbn%40googlegroups.com.