TLA+ Graph Explorer

This page summarizes the projects mentioned and recommended in the original post on

Our great sponsors
  • Onboard AI - Learn any GitHub repo in 59 seconds
  • InfluxDB - Collect and Analyze Billions of Data Points in Real Time
  • SaaSHub - Software Alternatives and Reviews
  • tlaplus-graph-explorer

    A static web application to explore and animate a TLA+ state graph.


    > wonder whether there will be an update to map those children to the names of the actions taken in the spec

    This can be done by, for example, adding a variable to the spec with the label of the transition, lets say a variable named label. Then in the tool you can parse the state string (variable value in function updateChilds,, and then use the label when creating the radio button.

    The label can be obtained from the variable value in updateChilds with something like: label = parseVars(value).get("label").

    > You write the visualizations in D3 I guess?

    The visualization I think can be written with any javascript library, at least I tried to make it able to do so. In the second example I wrote the visualization with svg.js.

  • coyote

    Coyote is a library and tool for testing concurrent C# code and deterministically reproducing bugs.

    Visualizations do help a lot when model checkers and concurrency schedule exploration tools like Coyote find bugs. Coyote include the ability to visualize the traces if you express your concurrency using actors (see

    It also allows you to implement your own "logger" through which you can emit enough information to construct some cool visualizations. I had a lot of fun working on visualizing an implementation of Paxos using Coyote (then P#) (screenshot at

  • Onboard AI

    Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts