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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sat, 19 Nov 2016 10:00:26 +0100*References*: <cde0ef35-c0a5-4180-b65b-7a3604d97380@googlegroups.com> <B1B0F433-F2EF-4987-8468-F0693CF4B338@gmail.com> <e0b40cdd-6d92-4ef0-a534-9ed086e2b081@googlegroups.com>

Not sure I understand your question but allow me to reformulate. The liveness requirement filters out behaviors that would be perfectly acceptable for the safety part of the specification. The idea of machine closure is that the state machine executing the safety part of the specification does not need "prescience" in order to make those choices that will be compatible with the liveness condition: any choice allowed by the next-state relation can be completed to an infinite behavior satisfying the overall specification, using a fair scheduler. A machine-closed specification does not place any constraints on internal non-determinism, whereas non machine-closed specifications may have such constraints.
Morally, yes, assuming that the different choices are actually possible based on the safety part (think invariants). For example, the following (trivially machine-closed) variation of your example x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((x < 0 ∧ x'=x-1) ∨ x’ = x + 1)]_<<t,x>> allows for an apparent choice of decrementing x that cannot be realized due to the invariant ☐(x > 0). Stephan |

**Follow-Ups**:**Re: [tlaplus] Nondeterminism and equivalence***From:*Ron Pressler

**References**:**Nondeterminism and equivalence***From:*Ron Pressler

**Re: [tlaplus] Nondeterminism and equivalence***From:*Stephan Merz

**Re: [tlaplus] Nondeterminism and equivalence***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] Nondeterminism and equivalence** - Next by Date:
**Re: [tlaplus] Nondeterminism and equivalence** - Previous by thread:
**Re: [tlaplus] Nondeterminism and equivalence** - Next by thread:
**Re: [tlaplus] Nondeterminism and equivalence** - Index(es):