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

# Re: The effect of symmetry sets on TLC performance

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