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