I am trying to understand why this specification is not a safety property.
Every behavior that violates it has some finite prefix that contains some step that violates either the initial condition `x = 0` or the action `x' = x + 1`.
If a safety property is one for which every violating behavior has a finite prefix that cannot be extended to a satisfying behavior,
then this raw TLA formula seems to describe a safety property. Is this wrong, or another definition of safety used?
I do see the element of liveness originating from the semantics, in the comparison that
we are able to require a liveness property, even though (I think) no TLA formula of the form `Init /\ [][A]_v` implies any liveness property of the form `[]<><< B >>_v`. On the other hand, it could imply a liveness property
that doesn't mention steps (of the form `[]<> P` for `P` a state predicate).