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

*From*: Ioannis Filippidis <jfili...@xxxxxxxxx>*Date*: Sun, 20 Nov 2016 04:38:21 -0800*References*: <cde0ef35-c0a5-4180-b65b-7a3604d97380@googlegroups.com> <41f9f74f-ab57-4f87-872b-2069de5e6b60@googlegroups.com> <245bd8e2-a9e6-4696-8f39-fcb100b8940d@googlegroups.com> <c86a9fd3-3918-4403-a93a-7446de1cea59@googlegroups.com> <F2D6CCBF-BAD8-49F5-AE21-B138233AE4A8@gmail.com>

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

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

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).

ioannis

**Follow-Ups**:**Re: [tlaplus] Nondeterminism and equivalence***From:*Ron Pressler

**Re: [tlaplus] Nondeterminism and equivalence***From:*Stephan Merz

**References**:**Nondeterminism and equivalence***From:*Ron Pressler

**Re: Nondeterminism and equivalence***From:*Leslie Lamport

**Re: Nondeterminism and equivalence***From:*Ron Pressler

**Re: Nondeterminism and equivalence***From:*Ron Pressler

**Re: [tlaplus] Nondeterminism and equivalence***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Nondeterminism and equivalence** - Next by Date:
**Re: [tlaplus] Nondeterminism and equivalence** - Previous by thread:
**Re: [tlaplus] Nondeterminism and equivalence** - Next by thread:
**Re: [tlaplus] Nondeterminism and equivalence** - Index(es):