Re: [tlaplus] Simple Question - Safety and Liveness

In order to add to Andrew's reply: the ENABLED operator does not refer to any specification S, but considers an action in isolation, and the same is true for the fairness formulas WF_v(A) and SF_v(A). For any action formula B,

ENABLED B == \E x' : B

where x' is the tuple of all state variables that have (free) occurrences in B. In particular, assuming that v is the tuple of all state variables that occur in A,

(ENABLED <<A>>_v) <=> \E v' : A /\ (v' # v)

So, concretely,

ENABLED << x \in Nat /\ x' = x-1 /\ y' = y >>_<<x,y>>

is equivalent to x \in Nat, since for any such x, x-1 # x and therefore << x-1, y >> # << x, y >>, and

ENABLED << x \in Nat /\ x % 2 = 0 /\ x' = x+2 /\ x' % 2 # 0 >>_x

is equivalent to FALSE.

It can be shown that for any action A, WF_v(A) and SF_v(A) are liveness properties because any finite sequence of states can be extended to an infinite sequence satisfying the fairness formula. In particular, this is trivial for the second example above because both fairness formulas are equivalent to TRUE since the action is never enabled. Moreover, even (countable) conjunctions of fairness formulas are guaranteed to be liveness properties.

However, this doesn't mean that such an extension to an infinite sequence of states is compatible with a given safety property, such as a formula Init /\ [][Next]_v. In the first example above, the fairness formulas are incompatible with the safety property

S == x = 0 /\ y = 0 /\ [][x' = x-1 /\ y' = y+1]_<<x,y>>

It is desirable that a fairness property [note that I wrote "fairness formula" for WF_v(A) or SF_v(A) above] for an underlying (safety) specification S guarantees compatibility with S in the sense that the system cannot "paint itself into a corner" by reaching a state from which it becomes impossible to respect the fairness property while still satisfying S. This concept is called "machine closure" [1,2] and is the one that you allude to when you consider enabledness of an action with respect to S.

Stephan

[1] http://lamport.azurewebsites.net/pubs/pubs.html#lamport-fairness

[2] https://will62794.github.io/tlaplus/formal-methods/2020/08/05/machine-closure.html

On 13 Jul 2022, at 16:40, Victor Clayton Barnett <vcbarnett93@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

--
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.

--
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/8BC9791A-9ED7-4107-B0EA-8A5EC496991E%40gmail.com.