Re: [tlaplus] The effect of symmetry sets on TLC performance

[Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>]

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
Description: Binary data

Attachment: BijectionCst.tla
Description: Binary data

Attachment: Functions.tla
Description: Binary data

Attachment: BijectionCst_Statespace.pdf
Description: Adobe PDF document

Attachment: BijectionCst_PermFlood.pdf
Description: Adobe PDF document

Attachment: BijectionCst_Nauty.pdf
Description: Adobe PDF document