On Thursday, December 3, 2015 at 5:05:30 PM UTC+2, Leslie Lamport wrote:
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.
That's perfectly fine, but it should also be significantly less (in practice) than the time to compute (by next-step), or the optimization might not pay off.
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 believe mine is symmetric in both sets.
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}.
Ah, no, that's not what I meant. It allows any initial state, but no matter the mapping between values in the initial state, it is always preserved, so states with different mappings will never be reached. I think I have an effective clarification: consider a model with a single variable `foo` that can obtain the symmetric values `{a, b, c}`. Now introduce a constant, Map, which maps the set to {x, y, z} in any arbitrary way. Then, introduce another variable, `bar` and the following conjunction to the next state formula:
/\ bar' = Map(foo')
I think this model is semantically symmetrical in both sets, but from any given initial condition, only 3 permutations out of 9 are reachable for each state. TLC, however (I think) will construct all 9. Am I wrong (on one count? both counts? :))
Ron