Formal specifications have become a core part of rigorous distributed systems design and verification, but existing tools have still been lacking in providing good interfaces for interacting with, exploring, visualizing and sharing these specifications and models in a portable and effective manner.

Visualization of dynamic reconfiguration behavior in Raft.

Spectacle aims to address this shortcoming by providing a browser-based tool for exploring and visualizing formal specifications written in the TLA+ specification language. It takes inspiration from past attempts at building similar tools, like Diego Ongaro’s Runway, but it builds on top of TLA+, taking advantage of an existing, well-defined formal specification language, rather than trying to build a new language alongside the tool.

The JavaScript Interpreter

At the core of the tool is a native Javascript interpreter for TLA+. TLC is the primary, existing interpreter and model checker for TLA+ specifications, and it is mature, well-maintained, and has been optimized for performance over many years. It is, however, a somewhat complex and intricate codebase, written in Java, and so it was not a great candidate for integration into a browser-based tool that would allow for dynamic interaction with specifications.

One could build a language server into TLC that allows for remote interaction, but this would provide a less than ideal dynamic browser experience, and would rely on maintenance of an external server. The now defunct Rise4Fun site from Microsoft Research is one example of the downsides of relying on a remote service for running these types of tools.

The development of a Javascript interpreter for TLA+ was enabled by earlier work on building a tree-sitter parser for TLA+, which can be compiled to WebAssembly and run in the browser. Parsing TLA+ itself is a non-trivial task, so the development of this browser-based parser was a big step forward in terms of enabling the development of the interpreter. The interpreter itself is written entirely in vanilla Javascript, and currently consists of around 5000 lines of code. The goal is for the interpreter semantics to conform as closely as possible with TLC semantics, which we try to achieve via a conformance testing approach that compares the results of the Javascript interpreter and TLC on a large corpus of TLA+ specifications.

A benefit of this interpreter implementation is its ability to dynamically evaluate TLA+ specifications and expressions in the browser. For example, the demo below shows the dynamic evaluation of initial states for a single variable declaration (e.g VARIABLE x):

Initial state expression

Initial states generated

Interactive Trace Exploration

A core feature of the tool is the ability to load a TLA+ specification and interactively explore its behaviors. It provides the capability for a user to, from any current state, select an enabled action to transition to a next state, and also allows for back-tracking in the current trace. It also allows for the definition of trace expressions, which allow arbitrary TLA+ expressions to be evaluated at each state of the current trace.

For example, below shows a partial trace of the two-phase commit protocol specification in the tool:

The tool also provides with the ability to easily share traces via static links, which can be reloaded in a new browser window while retaining the generated trace and its existing parameters/settings. This provides a universal, portable way to share system traces, something that was quite awkward with existing tools. For example, here is a link showing two-phase commit driving all the way to commit, and another link showing it driving through to abort. It is also easy to link to system traces/counterexamples that illustrate interesting behaviors and/or edge cases of different protocols e.g. here is a link to a case of a Raft leader being elected, writing a log entry and then committing it across all nodes.

In addition to the trace exploration and expression features, the tool also provides a basic REPL interface, which allows arbitrary expressions to be evaluated in the context of the currently loaded specification. This feature mostly subsumes previous attempts at providing a REPL-like interface for TLA+ specifications.

Visualization

The above features are effective for exploring and understanding a specification, but in some cases it can be helpful to have a more polished and visual way to understand a system and its states/behaviors. Currently, the tool provides a very simple, SVG-based DSL for defining visualizations directly in a TLA+ specification itself, rather than requiring a separate interface/language for defining visualizations.

For example, here is a simple visualization of the final state of the Wolf, Goat, and Cabbage puzzle solution:

and here is a visualization of an abstract Raft specification with an elected leader and some log entries replicated across nodes:

The visualization DSL can currently be defined directly in the TLA+ specification itself, as seen here, and provides a set of basic SVG primitives that can be arranged and positioned in hierarchical groups, following standard SVG conventions. In future, these visualization primitives could be expanded with a variety of richer strucutres (e.g. graphs, lists, charts, constraint-based approaches etc.), but for now even this simple set of primitives allows for a variety of helpful system visualizations.

Conclusion

Overall, the vision is for Spectacle to be complementary to existing TLA+ tooling. For example, it is expected that TLC will remain the primary tool for model checking of non-trivial TLA+ specifications, since it is still the most performant tool for doing so. The goal is for Spectacle to be a tool for prototyping, exploring, and understanding specs, and sharing the results of these explorations in a convenient and portable manner, aspects that few existing tools in the ecosystem excel at.