[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Nondeterminism and equivalence

Hi Ioannis,

you are of course right – I don't know what I was thinking.


On 20 Nov 2016, at 13:38, Ioannis Filippidis <jfili...@xxxxxxxxx> wrote:

On Sun, Nov 20, 2016 at 12:37 AM, Stephan Merz <stepha...@xxxxxxxxx> 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 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).