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