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

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

Hi Markus and Ron,
our experience using the TLC’s symmetry reduction was also mixed.
The extended version of our iFM’2012 paper contains a few example models where we did try TLC’s symmetry reduction:


On 2 Dec 2015, at 14:12, Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:

On 02.12.2015 13:23, Ron Pressler wrote:
Is there a way to improve the implementation(s) of permute()? A quick
glance at the code showed what may possibly be way too many allocations
(in tuples and record) due to what seems like an overly eager allocation
policy (e.g. arrays are allocated before even a single permuted element
is found). But as all that's required of the permutations is a
fingerprint, perhaps a more substantial optimization may be possible.

Hi Ron,

those are interesting findings. Can you send me a (stripped down)
spec/model that exemplifies the performance problem?


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.