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.
A live version of the tool is currently 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
- Raft (animated)
- Snapshot Isolation
You can also explore some interesting (and infamous) protocol traces:
- (Cabbage Goat Wolf) Solution to the cabbage goat wolf puzzle
- (Raft) Log entry is written and later rolled back
- (Snapshot Isolation) Read-only anomaly under snapshot isolation
- (Snapshot Isolation) Write skew anomaly under snapshot isolation
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.
The current tool expects that a specification has defined its initial state predicate and next state relation as Init and Next definitions, respectively. If your specification has these defined under different names, they will not be recognized and no initial state or next state evaluation will occur. In this case, you can still use the tool in REPL mode, though.
Eventually this will be made configurable, but the current tool looks for these hard-coded definitions. Also, there is incomplete support for user module imports, so specs are largely expected to be written in a single module. The interpreter does, however, support most operators from the TLA+ standard modules by default.
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.
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.