Simple Question - Safety and Liveness

[Victor Clayton Barnett]

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

[Andrew Helwer]

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

[Andrew Helwer]

Correction on formula above (only one equals sign for equality, not two): <<x % 2 = 0 /\ x' = x + 2>>_x

[Victor Clayton Barnett]

Great, that makes sense. 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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/712d17b1-5e5b-4746-9c08-f0eb096c1781n%40googlegroups.com.

[Stephan Merz]

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

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/befc81a6-d74d-4c08-ae5d-2fc6a18d53cbn%40googlegroups.com.