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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 3 Dec 2015 07:16:56 -0800 (PST)*References*: <feb1173e-380c-4cb1-80ac-a5d8edf1c108@googlegroups.com> <0d9ae6b0-f5f1-4159-a933-32921111ab3d@googlegroups.com> <c7f7df3e-118a-42e1-aca4-e7a47dced84c@googlegroups.com> <82111398-b195-40c1-8926-59e179145fa6@googlegroups.com> <f283857c-31a1-4d9b-b22a-c39fd47f0c44@googlegroups.com>

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

**Follow-Ups**:**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**References**:**The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Leslie Lamport

**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Leslie Lamport

- Prev by Date:
**Re: The effect of symmetry sets on TLC performance** - Next by Date:
**Re: The effect of symmetry sets on TLC performance** - Previous by thread:
**Re: The effect of symmetry sets on TLC performance** - Next by thread:
**Re: The effect of symmetry sets on TLC performance** - Index(es):