Re: [tlaplus] Good specs for parser benchmarking

https://github.com/tlaplus/tlaplus/issues/413 has the problem (and solution) related to the "eXtreme Modeling in Practice" paper [1]. In a nutshell, the bottleneck wasn’t parsing but semantic processing of TLA+ records that span some 60k LOC.

The Farsite spec [2] should be a more holistic benchmark.

Markus

[1] https://arxiv.org/abs/2006.00915
[2] https://github.com/bringhurst/tlaplus/tree/master/org.lamport.tla.toolbox.uitest/farsite

On Feb 1, 2022, at 1:07 PM, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

Anyone have good suggestions for really long specs that would be good candidates for TLA+ parser benchmarking? Are the specs in the MongoDB extreme modeling paper available for download externally?

Andrew

--
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/73fa621e-111e-4c69-af4a-9c25a9ad77a3n%40googlegroups.com.