Ron Pressler

Where are the sources to the runtime?

2

I see only prebuilt JARs. Thanks!

See: - https://bugs.openjdk.java.net/browse/JDK-8027634 - https://bugs.openjdk.java.net/browse/JDK-8061999

Make instrumentation fully automatic

7

Determine potentially blocking methods by analyzing the call graph. Don't require manual designation of methods as blocking.

TLC evaluates boolean operators incorrectly when the first argument is non-boolean

5

According to *Specifying Systems* §16.1.3, the value of `2 \/ TRUE` is `TRUE`, and of `2 /\ FALSE` is `FALSE`. Indeed, TLAPS successfully checks both: ``` THEOREM (2 \/ TRUE)...

Pretty Print to HTML

11

I'd like to propose a new tool, which may make for a nice project for GSoC **Pretty Print to HTML (difficulty: easy) (skills: Java, HTML)** TLA+ has a great pretty-printer...

Try using jedis, though no async there

Allow more control in the API over Messenger message ACKS

1

This will enable us to control backpressure for remote Quasar channels.

...so that, in the future, we'll be able to pass in a lock factory that makes Fiber-blocking locks.