lemmster

Direct link to Github repo: https://github.com/tlaplus/PlusPy

Lamport lists various learning resources on his page: http://lamport.azurewebsites.net/tla/learning.html

I am the engineer who translated https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/... into Java (https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...). The translation took me about half a day. Later, while running scalability experiments, a correctness bug intermittently showed up, on which I spent approximately two weeks to find the root cause. The two weeks included fixing around a dozen bugs in code that was not specified in TLA+. However, none of these bugs were correctness bugs and unrelated to the correctness bug. Eventually, I translated the TLA+ spec into input for Java Pathfinder, which found the cause of the correctness bug immediately: The Java translation contained an off-by-one bug in a for loops (TLA+ is one-indexed while Java is zero-indexed). I am still convinced that a code review would have found the bug and that JPF was a very heavyweight substitute for a fresh pair of eyes. In other words, the bugs that get introduced during the translation phase are shallow and easily corrected.

Note that no other bugs have been reported for the code since.

Below are a few specs related to refactoring/rewriting the TLA+ model checker to scale to more cores:

* https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...

* https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...

* https://github.com/lemmy/PageQueue

Did you also wire up trace expression evaluation in Emacs?

To what kernel release(s) do the flags apply?

An review of the post is at https://lemmster.de/tla-liveness-review.html