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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 16 Jul 2022 09:35:09 +0200*References*: <befc81a6-d74d-4c08-ae5d-2fc6a18d53cbn@googlegroups.com>

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

**References**:**[tlaplus] Simple Question - Safety and Liveness***From:*Victor Clayton Barnett

- Prev by Date:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Next by Date:
**Re: [tlaplus] Video Tutorial Series Lecture 4** - Previous by thread:
**Re: [tlaplus] Re: Simple Question - Safety and Liveness** - Next by thread:
**[tlaplus] EOL/EOVS dates of v1.7.2** - Index(es):