Re: [tlaplus] State-constraints and liveness

>> checking liveness properties in the presence of state constraints can be really tricky because the specification may not assert what you think it does. In particular, see section 14.3.5 of the TLA+ book.

Thanks for pointing this out. I believe that I've dodged the issue described in that section of the book, by ensuring that my fairness assumption cannot not be made false by the state-constraint. My fairness assumption is weak-fairness on just the 'internal' actions of the system -- i.e. the actions that drive any 'currently in-progress' operation forward to completion. But my state-constraint only constrains the number of 'calls' by a user of the system that may start new operations. The state-constraint does also constrain the number of actions by the 'physical environment', such as process failure.

But as this is a subtle issue, I could easily have made an error. I plan to test liveness checking as Leslie suggests, by ensuring that it can find violations of intentionally incorrect liveness properties. (See below for how doing so found an apparent problem).

>>I'd suggest that you rewrite your property so that TLC will accept it. For example, try

Spec /\ []<><TRUE>_vars => Liveness

Thankyou. I have now tried this. (I had to change "<TRUE>_vars" to "<<TRUE>>_vars".)

First I tried entering the whole formula as the property to check.

But TLC failed with this error:

Temporal formulas containing actions must be of forms <>[]A or []<>A.

at util.Assert.fail(Assert.java:64)

at tlc2.tool.liveness.Liveness.classifyExpr(Liveness.java:727)

at tlc2.tool.liveness.Liveness.processLiveness(Liveness.java:566)

at tlc2.tool.liveness.LiveCheck.init(LiveCheck.java:36)

So then I tried entering just the antecedent

Spec /\ []<><<TRUE>>_AllVars

... as the "Temporal formula" in the "What is the behavior spec?" section. i.e. Instead of just Spec.

And I entered the consequent

... as the property to check.

TLC accepts this. However, I first tested this configuration by checking several leads-to properties that I know to be invalid, and it failed to find any of them.

So either I'm using your suggestion incorrectly, or I'm still running into the kind of subtle interaction between liveness and state-constraints that you pointed out.

At this point I decide to change my specification to remove the need for a state-constraint. I changed the definition of several sets from Nat to become CONSTANTS that are (small) finite sets, and added enabling conditions to the 'public API' and 'environment' actions to only enable them if they stay in these limits. This change isn't really polluting the conceptual purity of the specification, as in the real system these sets would be finite -- just very, very large. So this change can be interpreted as an assumption that the system will no longer be used if the sets are exhausted.

And I went back to using "Spec" as the 'Temporal formula' in the 'What is the behavior spec?' section.

Again I checked the several known-to-be-incorrect liveness properties.

This time I ran into a new TLC bug, which I think is real -- i.e. not just a user-error entering unacceptable temporal formulas into the wrong part of the toolbox.

The error occurred when TLC was checking liveness.

The exception was a java.io.IOException: Negative seek

offsetjava.io.IOException: Negative seek offset

    at java.io.RandomAccessFile.seek(Native Method)

    at tlc2.util.BufferedRandomAccessFile.seek(BufferedRandomAccessFile.java:212)

    at tlc2.tool.liveness.DiskGraph.getNode(DiskGraph.java:145)

    at tlc2.tool.liveness.DiskGraph.getPath(DiskGraph.java:309)

    at tlc2.tool.liveness.LiveWorker.printTrace(LiveWorker.java:521)

    at tlc2.tool.liveness.LiveWorker.checkComponent(LiveWorker.java:290)

    at tlc2.tool.liveness.LiveWorker.checkSccs(LiveWorker.java:119)

    at tlc2.tool.liveness.LiveWorker.run(LiveWorker.java:613)

I've filed a bug-report here:

http://bugzilla.tlaplus.net/show_bug.cgi?id=293

I tried one further thing. I defined a 'legitimate termination' condition for the system, in which no progress could be made. This is true if no 'public APIs' are enabled (i.e. no new operations can be started), and all existing operations have been driven as far as they can be without new operations being started. i.e. It's legitimate deadlock. I did verify that my legitimate-termination condition is possible, by checking that the invariant ~ LegitimateTermination is violated in the expected case.

I then changed my liveness property to:

Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id)
\/ LegitimateTermination)

i.e. This is the moral equivalent of my '\/ HenceforthStuttering' approach earlier.
I then tried checking my known-to-be-incorrect liveness properties. But TLC again failed to find any violations on models that I believe should exhibit those violations.

Finally, I tried intentionally 'breaking' my specification by injecting bugs to prevent some operations from making progress. In that case TLC did correctly report deadlock. It didn't report that my liveness property was violated -- it just hit states in which the Next action was not enabled.

I don't really know what to try next. Perhaps the problem is with my spec or liveness property; I'll try Leslie's examples from the hyperbook and Specifying Systems.

thanks,

Chris

On Saturday, October 13, 2012 10:50:18 AM UTC-7, Stephan Merz wrote:

Hi Chris,

unfortunately, TLC doesn't check arbitrary temporal properties. "Implied temporal formulas" are restricted to "simple temporal formulas", which may only contain action sub formulas of the form WF_v(A), SF_v(A), []<><A>_v or <>[][A]_v (cf. Section 14.2.4, AFAIK this is still true of current versions of TLC). Your subformula HenceforthStuttering is even simpler, but not a "simple temporal formula" in that sense.

I'd suggest that you rewrite your property so that TLC will accept it. For example, try

Spec /\ []<><TRUE>_vars => Liveness

(for your original definition of liveness). In this way, the liveness property will only be evaluated over behaviors that do not end in infinite stuttering.

However, checking liveness properties in the presence of state constraints can be really tricky because the specification may not assert what you think it does. In particular, see section 14.3.5 of the TLA+ book.

Hope this helps,

Stephan

On Oct 12, 2012, at 11:09 PM, Chris Newcombe <chris...@xxxxxxxxx> wrote:

I'm trying to use TLC to check liveness properties for the first time.

I'm using a state-constraint with TLC, as I described in a previous message: https://groups.google.com/d/msg/tlaplus/nfd1H-tZbe8/eCV3DNKZOicJ

My liveness property is a simple leads-to formula:

Liveness == \A id \in Ids : MyProperty(id) ~> SomeOtherProperty(id)

TLC finds counter-examples in which the (temporal) antecedent is satisfied (for some id in some state), but the consequent is never satisfied because the behavior generated by TLC is artificially truncated -- i.e. ends with infinite stuttering -- because of the state-constraint.

As the counter-example ends in infinite stuttering, I tried weakening the liveness property to allow that:

HenceforthStuttering == [] UNCHANGED AllVars \* all future steps don't change any variables
Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id)
\/ HenceforthStuttering)

But that's not valid TLA+ because the definition of HenceforthStuttering is not a legal TLA+ formula. The toolbox says:

Parse error: [] followed by action not of the form [A]_v

So I tried:

HenceforthStuttering == [][UNCHANGED AllVars]_AllVars \* all future steps don't change any variables

That parses, but TLC now fails immediately with:

Temporal formulas containing actions must be of forms <>[]A or []<>A.

What am I missing? I did wonder if, rather than weakening the liveness property, there might be a way to change the state-constraint such that it wouldn't cause the liveness property to be artificially violated. But I don't currently see how to do that.

many thanks,

Chris

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
To unsubscribe from this group, send email to tlaplus+u...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.