<!-- # TLA⁺ Web Explorer -->

Spectacle

<!-- <img src="assets/glassestall3.png" height=31 alt="Spectacle logo" style="vertical-align: middle"> --> <!-- <img src="assets/glasses-svgrepo-com.svg" width="50" height="20" alt="Spectacle logo" style="vertical-align: middle"> -->

Spectacle is an interactive, web-based tool for exploring, visualizing, and sharing formal specifications written in the TLA⁺ specification language. The motivation is to have a better way to quickly interact with a formal specification and easily share results. For example, it provides a way to share protocol behaviors and counterexample traces in a convenient, portable, and repeatable manner.

The tool implements a full TLA+ interpreter in Javascript, building on top of the TLA+ tree-sitter grammar for parsing specifications. This allows for interactive exploration of specs natively in the browser, without reliance on an external language server. A live version is hosted here, and below are some example specifications to try out:

• Lock server
• Cabbage Goat Wolf Puzzle (animated)
• Distributed termination detection (EWD998) (animated)
• Two phase commit (animated)
• Paxos
• FlexiblePaxos
• Raft (animated)
• Snapshot Isolation
• CASPaxos

You can also explore some interesting (and infamous) traces of different protocols:

• Solution to the cabbage goat wolf puzzle (Cabbage Goat Wolf Puzzle)
• Raft log entry is written and later rolled back (Raft)
• Write skew anomaly under snapshot isolation (Snapshot Isolation)
• Read-only anomaly under snapshot isolation (Snapshot Isolation)

<!-- The Javascript interpreter is likely slower than TLC, but highly efficient model checking isn't currently a goal of the tool. --> <!-- Note also that you can basically use the existing web interface as a simple TLA+ expression evaluator, since making changes to definitions in the spec should automatically update the set of generated initial states. --> <!-- This project Utilizes the [TLA+ tree-sitter grammar](https://github.com/tlaplus-community/tree-sitter-tlaplus) to provide a web based TLA+ interface for exploring and sharing specifications. --> <!-- There are still some TLA+ language features that [may not be implemented](https://github.com/will62794/spectacle/issues), but a reasonable number of specs should be handled correctly. For example, see this [Paxos spec](https://will62794.github.io/spectacle/#!/home?specpath=./specs/Paxos.tla). Additional testing is needed to verify the correctness of this interpreter on more complex specs. --> <!-- A basic, preliminary test suite can be found [here](https://will62794.github.io/spectacle/test.html). -->

You can also see a live demo of the tool and its features in this presentation, which also gives a very high level overview of the tool architecture and implementation details.

Running Locally

If you would like to run Spectacle locally and offline, you can do so by cloning the repo and running

python3 serve.py [--local_dir /path/to/local/specs/dir]

from the root directory. This will start up a local server for the app at 127.0.0.1:8000.

The local_dir argument is optional and allows you to use Spectacle to explore a local specification that you may be editing (e.g. in a local IDE). Any *.tla files located in the directory specified by the argument will automatically be detected. You can then load one of these specs from within the "Load" tab under the "From local server" section, where they should be automatically listed. This allows Spectacle to load the specification from your local system and have it be updated as you edit your spec file locally.

Animations

Spectacle provides an easy way to create animated visualizations of your specifications by defining them in an SVG-based format right in a specification. See here for more details on how to define these animations.

Testing

Currently, nearly all testing of the tool is done via conformance testing against TLC. That is, for a given specification, we generate its reachable state graph using TLC and compare this for equivalence against the reachable state graph generated by the Javascript interpreter. You can see the result of all current tests that are run on this page, and the underlying test specs here.