Symmetry and Liveness

[Y2i]

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

[Leslie Lamport]

I deleted my previous post on this topic.  It contained much that was wrong.  If you received it by email, please ignore it.  I should by now know better than to post anything I write late in the evening. 

Yuan Yu and I did a fair amount of thinking about the interaction of symmetry reduction and property checking.  Unfortunately,  none of what we deduced was written down and I remember little of it.  I intend to think and then write about this, and to check what I write with others before posting it.

Leslie

[Y2i]

Thank you for taking your time to respond, Leslie.  I did not realize it would be a question on an advanced topic while asking it late at night.  If you think it is worth your time, I'll be looking forward to your next post here.

Yuri

[Leslie Lamport]

TLC can check the following kinds of properties.

   1. A state predicate I (an initial predicate)
  
   2. []I for a state predicate I (an invariant)
  
   3. [][A]_vars for an action A, vars the tuple of all variables.
  
   4. Any TLA temporal formula that is the conjunction of disjunctions
      of the following kinds of formulas:
     - One containing only temporal operators and state predicates. 
       (Those predicates can be of the form ENABLED A for an arbitrary
       action A.)
     - A formula of the form []<><<A>>_vars or <>[][A]_vars for some
       action A.

Symmetry sets define a group of permutations Sym on the model values
in those sets.  For any permutation P in Sym and any state s, let P(s)
be the state obtained from s by replacing each model value m in M that
appears in s by P(m).  For example, if there are two variables x and y
and two model values m1 and m2, and P is the permutation that
exchanges m1 and m2, then P([x <- {m1, 1}, y <- <<m1, m2>>]) equals
[x <- {m2, 1}, y <- <<m2, m1>>].  A state predicate I is symmetric iff
for every state s and every P in Sym, I is satisfied by s iff it is
satisfied by P(s).  An action A is symmetric iff for every pair of
states s and t and every P in Sym, A is satisfied by s -> t iff it is
satisfied by P(s) -> P(t).  A spec is symmetric iff its initial
predicate, next-state action, and all actions in its fairness
conditions are symmetric.

For properties of types 1-3, if TLC catches an error, then it produces
an error trace that is a counterexample to that property.  If the spec
and the predicate or action of the property are symmetric, then TLC
will catch any error if it runs long enough (for example, if it
terminates).  If the spec and property are not symmetric, then TLC
might not find an error even though the property doesn't hold.

For a property of type 4, if the spec and all actions and predicates
in the property are symmetric, then if TLC terminates, then

 - If TLC reports an error, I BELIEVE that the property does not
   hold.  However, the error trace may not be a correct
   counterexample.  In fact, the counterexample might not even
   satisfy the spec's next-state relation.  A simple modification
   to the way TLC computes error traces will ensure that it doesn't
   report an incorrect counterexample.

 - TLC may fail to report an error even though the property does
   not hold.  This can be corrected, but requires TLC to gather
   additional information when it builds its graph of fingerprints
   of reachable states.

We expect that, in the fullness of time, these problems will be
corrected.

For a property of type 4, if the spec or the property is not
symmetric, then:

  - IF TLC reports an error, I BELIEVE that the property does
    not hold.  However, TLC may produce an incorrect error trace.
    It may even fail to find an error trace, reporting an error
    saying something like "Cannot construct state from its
    fingerprint."

  - TLC may fail to report an error even though the property does
    not hold.

There is no way to get TLC to do any better in this case.

Note: A fingerprint collision acts like an additional symmetry reduction
for which the spec and the properties being checked are not symmetric.

[Y2i]

Thank you so much Leslie!  In addition to answering my question, this also gives a great summary of the TLC capabilities.  Really appreciate the extra details!

Yuri