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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 3 Oct 2023 09:24:23 +0200*References*: <81a73f7d-ab60-4d68-8dd1-dbe1620816fcn@googlegroups.com>

Hi Jones, the effect of a state-machine specification I /\ [][N]_v becoming inconsistent after conjoining it with a liveness property L is an extreme case of violation of machine closure [1]. When the liveness property is defined as a conjunction of (countably many) weak or strong fairness conditions WF(A) or SF(A) where A is a sub-action (in first approximation, a disjunct) of the next-state relation, you can be sure that every finite behavior satisfying the state machine specification can be extended to a behavior that satisfies the complete specification. Hope this helps, Stephan [1] https://lamport.azurewebsites.net/pubs/pubs.html#lamport-old-fashioned
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/89CE3139-C47F-4421-BF15-4D078251545E%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Fairness conditions and <<A>>_v***From:*Jones Martins

**References**:**[tlaplus] Fairness conditions and <<A>>_v***From:*Jones Martins

- Prev by Date:
**[tlaplus] Fairness conditions and <<A>>_v** - Next by Date:
**Re: [tlaplus] Fairness conditions and <<A>>_v** - Previous by thread:
**[tlaplus] Fairness conditions and <<A>>_v** - Next by thread:
**Re: [tlaplus] Fairness conditions and <<A>>_v** - Index(es):