Re: The effect of symmetry sets on TLC performance

To fingerprint a state, TLC should construct a single new state that
is a permutation of that state and fingerprint the permuted state.
The time to construct that permuted state should be linear in the size
of the state.

A specification is symmetric in a set S iff for every behavior b
allowed by the specification and every permutation p of S, the
behavior obtained by applying p to every state of b is also a behavior
allowed by the specification. (Applying p to a state means replacing
each element s of S by p(s).)

I interpret what you have written to meant that your specification
allows only intial states in which foo = a iff bar = x. Such a
specification is not symmetric in either {a, b, c} or {x, y, z}. I
believe that the only way for a specification not to be symmetric in a
set S of model values is if it contains an _expression_ of the form
"CHOOSE s \in S : ...". A model can also produce an asymmetric
specification by using individual model values in S in instantiating a
constant or overriding a definition.

Leslie

On Wednesday, December 2, 2015 at 9:48:56 PM UTC-8, Ron Pressler wrote:

On Wednesday, December 2, 2015 at 10:43:06 PM UTC+2, Leslie Lamport wrote:
(1) While TLC fingerprints the permuted state, it computes next states based on the actual state. Hence, every state that it examines is reachable.

In order to fingerprint the permuted state, TLC fully constructs it. That's what I meant by "computes" in that context.

(2) If your spec is actually symmetric, then every permutation of a reachable state is reachable. If there are permutations that are not reachable, then your model is incorrect. However, the result of this incorrectness is that TLC may fail to examine a reachable state that it should examine; it will not cause it to examine unreachable states.

Let me try to explain what I mean with a clearer example, and please let me know if I'm wrong. Suppose I have two variables, `foo` and `bar`, `foo` obtaining one of the values {a, b, c} and `bar` the values {x, y, z}. My initial state maps sets `foo and `bar` in such a way that if `foo` is `a` then `bar` is `x`, if `foo` is `b` then `bar` is `y` and if `foo` is `c` then `bar` is `z`. My model is symmetrical in both sets of values, and every possible initial mapping from {a,b,c} to {x,y,z} is valid, but I'm only interested in symmetries that preserve the original mapping. I am only interested in 3 permutations, while TLC will generate 9. I'm interested in the symmetries because in the course of running the model starting from my initial state, the model will reach a state that is symmetrical in the pair (a, x) to a state with (b, y) which may have already visited, and so have no interest in (re-)exploring. TLC, though, will also generate (for the purpose of fingerprinting) states with the pairing (a, y). Those states are indeed reachable if my initial state allowed them. So it is true that if all 9 permutations are applied to the initial condition, then all 9 permutations of all states are indeed reachable, but that is of no interest because it amounts to no more than running the model with different names, rather than not visiting states that are symmetrical to those I've already visited.

Again, if I start with the pairing [a |-> x, b |-> y, c |-> z] I may reach a state that is symmetrical with {<<a, x>>, <<b, y>>, <<c, z>>} but not {<<a, y>>, <<b, x>>, <<c, z>>}. If there was a way to let TLC have symmetrical sets of _pairs_ of model values, I could just specify that set of pairs as a symmetry set and have `foo` and `bar` pick a first and second element of a pair respectively, but I'm not aware of a way to do that.

Ron