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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sat, 13 Oct 2012 19:50:22 +0200*References*: <914c0d7a-c10e-4bf0-8347-699201b91841@googlegroups.com>

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.n...@xxxxxxxxx> wrote: I'm trying to use TLC to check liveness properties for the first time. |

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

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

- Prev by Date:
**A workaround to make the Toolbox usable on recent versions of Ubuntu 12** - Next by Date:
**Re: [tlaplus] State-constraints and liveness** - Previous by thread:
**State-constraints and liveness** - Next by thread:
**Re: [tlaplus] State-constraints and liveness** - Index(es):