Tutorial-style talk "Weeks of debugging can save you hours of TLA+". The inspiration for this tutorial and definitive background reading material (with spoilers) is "An Example of Debugging Java with a Model Checker " by Michel Charpentier. I believe it all goes back to Challenge 14 of the c2 wiki.
Each git commit introduces a new TLA+ concept. Go back to the very first commit to follow along! Please note - especially when you create PRs -that the git history will be rewritten frequently to stay linear.
Click either one of the buttons to launch a zero-install IDE to give the TLA+ specification language a try:
This tutorial is work in progress. More chapters will be added in the future. In the meantime, feel free to open issues with questions, clarifications, and recommendations. You can also reach out to me on twitter. Basic TLA+ learning material can be found over at Lamport's TLA+ page.
In the previous step, we looked at the graphical representation of the state graph. With the help of TLCExt!PickSuccessor we build us a debugger with which we study the state graph interactively. We learn that with configuration p2c1b1 there are two deadlock states:
The CommunityModules release has to be added to TLC's command-line:
java -cp tla2tools.jar:CommunityModules.jar tlc2.TLC -deadlock BlockingQueue
Note that TLC's -continue flag would have also worked to find both
deadlock states.
Slightly larger configuration with which we can visually spot the
deadlock: 
.
BlockingQueueDebug.tla/.cfg shows how to interactively explore a state graph for configuration p2c1b1 with TLC in combination with GraphViz (xdot):
java -jar tla2tools.jar -deadlock -dump dot,snapshot p2c1b1.dot BlockingQueueDebug
Initial TLA+ spec that models the existing (Java) code with all its bugs and shortcomings.
The model uses the minimal parameters (1 producer, 1 consumer, and
a buffer of size one) possible. When TLC generates the state graph with
java -jar tla2tools.jar -deadlock -dump dot p1c1b1.dot BlockingQueue,
we can visually verify that no deadlock is possible with this
configuration: 
.
Legacy Java code with all its bugs and shortcomings. At this point in the tutorial, we only know that the code can exhibit a deadlock, but we don't know why.
What we will do is play a game with the universe (non-determinism).
Launch the Java app with java -cp impl/src/ org.kuppe.App in
the background and follow along with the tutorial. If the Java app
deadlocks before you finish the tutorial, the universe wins.
(For the c-affine among us, impl/producer_consumer.c is a C implementation of the blocking buffer sans most of the logging).
Add IDE setup for VSCode online and gitpod.io.