Hi Ioannis,you are of course right – I don't know what I was thinking.Sorry,StephanOn 20 Nov 2016, at 13:38, Ioannis Filippidis wrote:On Sun, Nov 20, 2016 at 12:37 AM, Stephan Merz wrote:For example, the specification    x = 0 /\ [](x' = x+1) implies the liveness property   \A n \in Nat : <>(x > n) so the specification is not a safety property.Hi Stephan,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 thatwe are able to require a liveness property, even though (I think) no TLA formula of the form Init /\ [][A]_v impliesany liveness property of the form []<><< B >>_v. On the other hand, it could imply a liveness propertythat doesn't mention steps (of the form []<> P for P a state predicate).ioannis