[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`?