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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Mon, 25 Mar 2019 14:51:43 -0700 (PDT)*References*: <864f5ffb-f895-467f-8de1-0fa26d2ca8d4@googlegroups.com>

Dear Philippe,

In your first example, the real problem is not that TLC reports that

<>FALSE is satisfied, but that it reports that FALSE is not satisfied.

<>FALSE is satisfied, but that it reports that FALSE is not satisfied.

You have written a spec that is not machine closed. I will explain

what that means. Recall that a safety property is one that is not

satisfied by a behavior if it is not satisfied by a finite prefix of

the behavior, meaning that the finite prefix cannot be continued to an

infinite behavior satisfying the property. A liveness property is one

such that any finite behavior can be continued to an infinite behavior

satisfying the property. A machine closed spec is one that is the

conjunction of a safety property and a liveness property such that any

finite behavior satisfying the safety property can be continued to an

infinite behavior satisfying both the safety and liveness properties.

In short, machine closure means that conjoining the liveness property

to the safety property doesn't disallow any finite behaviors allowed

by the safety property.

what that means. Recall that a safety property is one that is not

satisfied by a behavior if it is not satisfied by a finite prefix of

the behavior, meaning that the finite prefix cannot be continued to an

infinite behavior satisfying the property. A liveness property is one

such that any finite behavior can be continued to an infinite behavior

satisfying the property. A machine closed spec is one that is the

conjunction of a safety property and a liveness property such that any

finite behavior satisfying the safety property can be continued to an

infinite behavior satisfying both the safety and liveness properties.

In short, machine closure means that conjoining the liveness property

to the safety property doesn't disallow any finite behaviors allowed

by the safety property.

Specs that are not machine closed are weird and are usually

wrong--that is, they don't mean what the writer intended. TLA is the

only temporal logic I know of that has a simple way to write a spec

that is easily seen to be machine closed. That way is to make the

liveness part the conjunction of weak and/or strong fairness

conditions on actions that imply the next-state action. Your spec

does not satisfy that condition, since x'=3 doesn't imply the

next-state action x'=1. Your spec is "extremely" non-machine closed:

conjoining the liveness property rules out all finite behaviors.

wrong--that is, they don't mean what the writer intended. TLA is the

only temporal logic I know of that has a simple way to write a spec

that is easily seen to be machine closed. That way is to make the

liveness part the conjunction of weak and/or strong fairness

conditions on actions that imply the next-state action. Your spec

does not satisfy that condition, since x'=3 doesn't imply the

next-state action x'=1. Your spec is "extremely" non-machine closed:

conjoining the liveness property rules out all finite behaviors.

If you were "bitten" by this, it means you wrote a spec that is not

machine closed. If that is the spec you intended to write, then I and

perhaps others members of the group would like to see that spec and

find out why you wrote it that way. If the spec was incorrect and you

expected TLC to catch the error, this will point out this obvious

fact: if a spec is incorrect because it disallows behaviors it should

allow, then the only way to find the error is by checking that the

spec satisfies a property that it shouldn't. Now that you know adding

fairness of actions that don't imply the next-state action can lead to

weird specs, you will probably not do it again. If you want to add a

fairness condition on an action A that you're not sure implies the

next-state action, you can have TLC check that the safety part of the

spec satisfies the property [][A]_vars.

machine closed. If that is the spec you intended to write, then I and

perhaps others members of the group would like to see that spec and

find out why you wrote it that way. If the spec was incorrect and you

expected TLC to catch the error, this will point out this obvious

fact: if a spec is incorrect because it disallows behaviors it should

allow, then the only way to find the error is by checking that the

spec satisfies a property that it shouldn't. Now that you know adding

fairness of actions that don't imply the next-state action can lead to

weird specs, you will probably not do it again. If you want to add a

fairness condition on an action A that you're not sure implies the

next-state action, you can have TLC check that the safety part of the

spec satisfies the property [][A]_vars.

The reason that TLC does not find the property FALSE is true is that

any state predicate is a safety property, and TLC checks a simple

safety property by checking that it is satisfied by the safety part of

the spec (the Init /\ [][Next]_vars). A simple safety property is any

conjunction of an initial predicate, an invariance property, and/or a

property of the form [][Action]_predicate. Thus, if you intentionally

wrote a non-machine closed spec, TLC can incorrectly warn you that a

behavior satisfying your spec doesn't satisfy a simple safety property

because the property is not satisfied by Init /\ [][Next]_vars.

any state predicate is a safety property, and TLC checks a simple

safety property by checking that it is satisfied by the safety part of

the spec (the Init /\ [][Next]_vars). A simple safety property is any

conjunction of an initial predicate, an invariance property, and/or a

property of the form [][Action]_predicate. Thus, if you intentionally

wrote a non-machine closed spec, TLC can incorrectly warn you that a

behavior satisfying your spec doesn't satisfy a simple safety property

because the property is not satisfied by Init /\ [][Next]_vars.

Machine closure is not discussed in the documentation because no

engineer is likely to want to write a spec that isn't machine closed.

Instead, I simply tell users to express liveness by fairness

conditions of subactions of the next-state action, which imply the

next-state action. Please inform me if that advice is missing from

someplace where it should appear.

engineer is likely to want to write a spec that isn't machine closed.

Instead, I simply tell users to express liveness by fairness

conditions of subactions of the next-state action, which imply the

next-state action. Please inform me if that advice is missing from

someplace where it should appear.

----------

As for your second example, I've assumed it was obvious that adding a

constraint can cause TLC to fail to find an error because it can rule

out all the behaviors that reveal the error. This is perhaps more

obvious for violations of an invariance property because it can rule

out all states that don't satisfy the invariant. If it is not obvious

that it can also cause violations of liveness properties to be missed,

then please let me know where that should be documented.

constraint can cause TLC to fail to find an error because it can rule

out all the behaviors that reveal the error. This is perhaps more

obvious for violations of an invariance property because it can rule

out all states that don't satisfy the invariant. If it is not obvious

that it can also cause violations of liveness properties to be missed,

then please let me know where that should be documented.

Thanks,

Leslie

On Monday, March 25, 2019 at 4:42:44 AM UTC-7, philippe.queinnec.pro wrote:

Two silly cases where TLC finds that <>FALSE is a valid property of the models. The first case is correct but unexpected. The second case uses CONSTRAINT which changes the meaning of the spec w.r.t liveness.

Would it be possible for TLC to warn that the situation is dangereous?

I have been bitten by both cases in a larger model (500 lines of TLA+) and lost a lot of time because of a typo (first case) and trusting "constraint" too much (second case).

---------------- MODULE foo ----------------

VARIABLE x

Fairness == WF_x(x' = 3)

Spec == x = 0 /\ [][x' = 1]_x /\ Fairness

Ouch == <>FALSE

============================================

TLC (and TLA+ logic) correctly proves <>FALSE:

Init /\ [][Next] has a unique execution (modulo stuttering) : x=0 -> x=1

This execution does not satisfy fairness.

Thus Spec = FALSE and Spec => anything.

------------------------------------------------------------ ----

---------------- MODULE bar ----------------

EXTENDS Naturals

VARIABLE x

Next == x' = x + 1

Spec == x = 0 /\ [][Next]_x /\ WF_x(Next)

Constraint == x <= 2

Ouch == <>FALSE

============================================================ ====

With CONSTRAINT Constraint, TLC proves <>FALSE:

Init /\ [][Next] and the constraint has a unique execution (modulo stuttering):

x=0 -> x=1 -> x=2 -> x=3

It does not satisfy fairness, and Spec = FALSE.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**[tlaplus] Re: Proving false with fairness***From:*Leslie Lamport

**References**:**[tlaplus] Proving false with fairness***From:*philippe . queinnec . pro

- Prev by Date:
**Re: [tlaplus] Re: Why is this temporal property violated?** - Next by Date:
**[tlaplus] Re: Proving false with fairness** - Previous by thread:
**[tlaplus] Proving false with fairness** - Next by thread:
**[tlaplus] Re: Proving false with fairness** - Index(es):