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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 24 Apr 2019 13:43:38 +0200*References*: <15ef49ae-c054-4362-929c-a059b59e8ee0@googlegroups.com> <b70775e6-52e8-46d9-bf35-6d98cdb3c4e1@googlegroups.com>

When TLC reports a counter-example to an invariant, it is guaranteed to be of smallest length because the state space is explored using breadth-first search [1]. Checking liveness properties relies on exploring strongly connected components of the state graph and the above guarantee does not hold. The state graph is still the same, independently of the liveness property that you try to verify, but different counter-examples may be reported. Stephan [1] Using default settings, and ignoring effects due to parallel exploration.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**Follow-Ups**:**Re: [tlaplus] Re: When TLC error trace send with stuttering - what does this mean?***From:*david streader

**References**:**[tlaplus] When TLC error trace send with stuttering - what does this mean?***From:*david streader

**[tlaplus] Re: When TLC error trace send with stuttering - what does this mean?***From:*david streader

- Prev by Date:
**[tlaplus] Converting a set into a tuple in one step** - Next by Date:
**[tlaplus] Re: Converting a set into a tuple in one step** - Previous by thread:
**[tlaplus] Re: When TLC error trace send with stuttering - what does this mean?** - Next by thread:
**Re: [tlaplus] Re: When TLC error trace send with stuttering - what does this mean?** - Index(es):