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

*From*: Y2i <yur...@xxxxxxxxx>*Date*: Thu, 21 May 2015 00:05:04 -0700 (PDT)

TLC really speeds up when we assign a symmetry set to a constant. But then I read the following in section 4.7.3 of p-manual:

**Do not tell TLC both to assume symmetry and to check liveness. The
interaction of a symmetry assumption with TLC’s algorithm for checking liveness is subtle. It’s hard to determine if liveness checking will produce
correct results when symmetry is assumed.**

What does subtle interaction between symmetry assumption and liveness checking mean?

Thank you,

Yuri

**Follow-Ups**:**Re: Symmetry and Liveness***From:*Leslie Lamport

**Re: Symmetry and Liveness***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] TLC footprint value already on disk** - Next by Date:
**Re: [tlaplus] TLC footprint value already on disk** - Previous by thread:
**Re: [tlaplus] TLAPS and string search algorithms** - Next by thread:
**Re: Symmetry and Liveness** - Index(es):