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

*From*: Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>*Date*: Thu, 03 Dec 2015 16:52:44 +0100*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> <4c9e536c-f18f-4b99-adad-7ffa3a4b38aa@googlegroups.com> <9a1e660e-f417-4413-814a-f1f127afcaf4@googlegroups.com>

Hi Ron, Does the following capture your example ? I include the Dot rendering of the full state space (as computed by ProB when loading the TLA file) : BijectionCst_Statespace.pdf I also include the state space obtained using a technique called "permutation flooding", which I think to be quite close to what TLC does. Only one state is checked; the others are marked as permutations. [Permutation flooding is typically not the approach of choice in ProB; but if one stores just fingerprints as in TLC then it should be fine.] Finally, I also include the state space obtained using the nauty package to compute a canonical forms for every reached state; just one canonical form exists here. Greetings, Michael

**Attachment:
BijectionCst.cfg**

**Attachment:
BijectionCst.tla**

**Attachment:
Functions.tla**

**Attachment:
BijectionCst_Statespace.pdf**

**Attachment:
BijectionCst_PermFlood.pdf**

**Attachment:
BijectionCst_Nauty.pdf**

**Follow-Ups**:**Re: [tlaplus] 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

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

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

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