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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Mon, 15 Oct 2012 14:47:49 +0200*References*: <914c0d7a-c10e-4bf0-8347-699201b91841@googlegroups.com> <5E0ED368-14BA-4701-B45B-BAFD42750E2A@gmail.com> <15bbc751-d922-4dc9-9958-46223ab53f83@googlegroups.com>

Hi Chris, […]
Spec /\ []<><<TRUE>>_AllVars
I'm probably asking the obvious, but does your constrained specification allow for any behaviors where variables keep changing eventually? E.g., if you have some counter that can only increase but for which the constraints impose an upper bound then at some point the model can no longer continue and has to stutter. In such a case, augmenting the specification by []<><<TRUE>>_AllVars effectively rules out all behaviors, so any property will hold vacuously. (TLC will still report failures of invariants since these are checked as it generates states.) Perhaps a more appropriate specification of the fairness conditions would be something like WF_AllVars(Constraints /\ InternalActions) where InternalActions is the disjunction of all internal actions of your system and Constraints describes the state constraints. This condition requires that internal actions should eventually occur from states that satisfy your state constraints but requires nothing of states that do not satisfy the state constraints. Thus, the formula is not vacuously satisfied over the constrained runs, unlike WF_AllVars(InternalActions) which is false of the constrained runs in case the internal actions remain enabled in the states that do not satisfy the constraints. (Of course, depending on your spec you may want to impose several constraints of the form WF_AllVars(Constraints /\ A) instead of a single constraint for the disjunction of the internal actions.) Now, you may see counter-examples to your liveness property that are due to some operation that has been started but couldn't finish within the bounds of the constraints. In order to rule out these, you may have to weaken your liveness property to something like Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id) where LegitimateTermination could be just "~Constraints" or a suitable refinement that expresses that the handling of request "id" couldn't finish within the bounds. (Otherwise, if all your runs end up violating the constraints eventually, you haven't really verified anything.) Again, understanding what is actually verified by the model checker in such situations can be really subtle.
Alternatively, you could override Nat in the model that you pass to TLC by specifying something like Nat <- 0 .. 9 in the "Definition Override" tab in the advanced options. (If you use any operations on naturals, you'll probably have to override these as well.) I agree, though, that the change that you made is nicer.
Ouch. Looks like TLC can't find its states anymore on the disk. I'm afraid I can't help you here. Stephan |

**Follow-Ups**:**Re: [tlaplus] State-constraints and liveness***From:*Chris Newcombe

**References**:**State-constraints and liveness***From:*Chris Newcombe

**Re: [tlaplus] State-constraints and liveness***From:*Stephan Merz

**Re: [tlaplus] State-constraints and liveness***From:*Chris Newcombe

- Prev by Date:
**Re: [tlaplus] State-constraints and liveness** - Next by Date:
**RE: [tlaplus] Re: Display bug in TLA+ Toolbox / TLC** - Previous by thread:
**Re: [tlaplus] State-constraints and liveness** - Next by thread:
**Re: [tlaplus] State-constraints and liveness** - Index(es):