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