[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Nondeterminism and equivalence
On Sunday, November 20, 2016 at 2:38:23 PM UTC+2, Ioannis Filippidis wrote:
On the other hand, it could imply a liveness property
that doesn't mention steps (of the form `<> P` for `P` a state predicate).
Do you have an example of `Init /\ [A]_v` implying `<> P` but not `P`?