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

Symmetry and Liveness

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,