Liveness == \A id \in Ids : MyProperty(id) ~> SomeOtherProperty(id)
HenceforthStuttering == [] UNCHANGED AllVars \* all future steps don't change any variables
Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id)
\/ HenceforthStuttering)
HenceforthStuttering == [][UNCHANGED AllVars]_AllVars \* all future steps don't change any variables
Temporal formulas containing actions must be of forms <>[]A or []<>A.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@googlegroups.com.
To unsubscribe from this group, send email to tlaplus+u...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
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)
Spec /\ []<><<TRUE>>_AllVars
Liveness
The error occurred when TLC was checking liveness.The exception was a java.io.IOException: Negative seekoffsetjava.io.IOException: Negative seek offsetat 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 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
>> 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, trySpec /\ []<><TRUE>_vars => Liveness
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 consequentLiveness... 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.
Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id)
\/ LegitimateTermination)
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 seekoffsetjava.io.IOException: Negative seek offsetat 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)
Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id)
\/ LegitimateTermination)
I can't share my spec, but I here are some comments I wrote that helped me analyze the ways in which I needed to weaken my LegitimateTermination condition to account for my liveness assumption. For my spec, the legitimate termination condition required to address these principles turned out to be quite complicated.
This probably reveals how fuzzy my thinking still is about liveness, but so far I haven't found anything wrong with the approach.
(* Our 'legitimate termination' condition. *)\* Legitimate termination is subtle because it is strongly related to the\* particular LivenessAssumption that we have chosen for the specification,\*\* We call a state a 'termination state' of some behavior if it is\* the 'last' state of that behavior, at which 'infinite stuttering' occurs,\* More precisely, there is some natural number n such that for all m >= n,\* the m'th suffix of the behavior begins with the 'termination state'.\*\* N.B.: in the most general sense (i.e. considering _any_ possible system),\* 'termination state' is only defined for a subset of possible behaviors.\* Some behaviors might end in repeating cycles, and other behaviors might\* have an infinite state space and behaviors that never end in infinite stuttering\* e.g. the spec that just increments a natural number without bound:\* x = 0 /\ [][x' = x + 1]_<<x>> /\ WF_<<x>>(x' = x + 1)\*\* There are several interesting kinds of 'termination state':\*\* - Deadlock.\* The Next-state action is disabled in circumstances in which we would want it to be enabled,\* We choose define our specs so that if Next is disabled, that means deadlock --\* -- i.e. a bug in the TLA+ code or the system design. TLC checks for deadlock by default.\*\* - 'lifetime termination' due to reaching the legtimate finite bounds of the model.\* e.g. In this spec, we exhaust the space of identifiers, and all possible internal\* actions have run to completion. Such a state represents the assumption\* that the system cannot be used (or even perhaps experience any more failures)\* after its natural lifetime is exhausted.\* Next is disabled, but in circumstances that we accept as legal.\* We want to allow behaviors to end in such a state, because we don't\* want false-positives.\*\* - 'constrained termination' due to a TLC state constraint or action constraint.\* We clearly don't want to forbid behaviors just because they violate such a constraint\* (or there would be no point in ever using the constraints).\* However, Next is still enabled in such a state.\* The constraint simply stops TLC examining future states (although TLC does\* check invariants for the 'first' such state it finds in each behavior).\* This is the most subtle case of all because the constraint can be entirely\* arbitrary, and it interacts with the liveness assumption in complex ways.\* See section 14.3.4 of Specifying Systems and this discussion:\*\* - 'optional termination due to waiting for voluntary stimulus' in which any\* future progress depends on actions that do not have liveness assumptions.\* Examples of such actions are voluntary actions by an application using\* the system (e.g. to start new operations), and actions by the 'environment'\* such as partial failure. We don't have liveness assumptions on those actions because\* we don't want to _require_ them to happen in every behavior.\* In such a state, Next is *enabled*, but the only sub-actions that are enabled\* are those that don't have liveness assumptions.\* Important: the behavior _may_ continue past such a state (if Next happens to be enabled\* in the state). Indeed, later states may or may not be legitimate termination states.\* For this reason, many system states (perhaps most) may be legitimate termination states.\* e.g. For the current spec, even the initial state is a legitimate termination state\* because any progress requires the application to perform a voluntary action\* which does not have a liveness assumption.\*\* We currently choose to not use state constraints or action constraints with this specification\* because of the subtle interaction with liveness assumptions.
\* So our definition of a legitimate termination state is:\*\* lifetime termination\* or optional termination due to waiting for stimulus\*\* We only assume fairness of 'internal' actions that drive existing in-progress operations forward.\* We don't require that the application ever do anything. Similarly we don't require failure to happen.\*\* In summary, we consider a state to be a legitimate terminating state iff\*\* - internal operations are all in their 'terminal' states, and the only enabled actions\* are voluntary actions by the application that we don't want to 'require'\* (i.e. to start new operations), or are actions by the environment (failure)\* that we also don't want to require.\* or\* - any internal operations that are not yet in one of their 'terminal' states\* are currently blocked, because they (the in-progress internal actions)\* currently depend on the application performing some voluntary action\* which is currently disabled, e.g. due to exhaustion of identifiers.\* i.e. The design of the system assumes certain finite bounds on usage and\* failure-rate and those bounds have now been reached.\* or\* - any internal operations that are not yet in one of their 'terminal' states\* but are currently blocked, because they (the in-progress internal actions)\* currently depend on the application performing some voluntary action for which\* we don't have a fairness assumption (as we don't want to require the application to\* keep using the system). i.e. It's not the system's fault that the system may be stuck\* in the current state indefinitely.