Markus Alexander Kuppe

@mattmccormick Thanks for opening this pull request. Given that the spec is small, readers will probably wonder what insights writing this spec provided.

Quick question re 1) Were you aware of the [CommunityModules](https://github.com/tlaplus/CommunityModules) and the [`Range`](https://github.com/tlaplus/CommunityModules/blob/be80f411eb3b79972016fc73832f8f42ff1ac7de/modules/Functions.tla#L16-L21) operator specifically? We've been considering graduating some operators/modules from the CommunityModules into TLC, and `Functions.tla` seems like...

This issue is primarily about the content and less about the front-end (IDE). That said, why do you think that a Jupyter notebook is a good first-user front-end? My concern...

Is there an example that shows how to add a benchmark that comes as a self-contained jar file?

That could be done but the jar would be tailored to the benchmark. Not sure we want to "pollute" maven central with such a jar. By the way, the jar...

It is probably best to ditch the idea of a self-contained jar and instead use the [vanilla jar](https://oss.sonatype.org/content/repositories/snapshots/org/lamport/tla2tools/) from maven central and check the specs (input) into this repository. Is...

Two questions: - How do you make sbt consume maven snapshot dependencies? - What the meaning of *optional* JMH-compliant build? TLC fails if we check two different specs with a...

@axel22 If that's a strict requirement, I don't see a way to move forward. I don't have the bandwidth to change TLC to support warmup runs (I once hacked something...

https://github.com/tlaplus/tlaplus/tree/master/general/performance/Grid5k would be the spec that easily simulates two workloads: scalability and computation.

The extension's nightly build supports turning coverage off (see #172).