The search for strongly connected components (SCC) is the (scalability) bottleneck of TLC's liveness checking. It would be interesting to find out how GPU-based SCC search algorithms such as [1,2] perform on TLA+ liveness graphs. In previous work, we collected statistics about the shape of the average TLA+ liveness graph. One could use these statistics to generate synthetic graphs in addition to the existing real-world graphs.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/FA267897-C49A-45C5-8D22-FCFAB9B1F6F4%40lemmster.de.