TLA+ Graph Explorer

This is a static web application to explore and visualize a TLA+ state graph or a TLA+ trace.

The application works by parsing a dot file generated by a TLA+ specification and then having visual representations to more easily understand and go through the reachable states.

The application is written to support big dot files and not load the whole file into memory. This is achieved by reading the file in chunks and storing only the location of the node in the file. The structure to save the nodes location, in my experiments, takes around 1/10th of the dot file size.

Examples

For more examples: examples.

Example 1 - Default Configuration

Spec: https://github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals.

Example 2 - Personalized state

Spec: https://github.com/afonsonf/ceph-consensus-spec.

Usage

Overview

The application is in the folder src. To run it, open the index.html file in a browser (tested in Chrome and Firefox).

The default way to represent a state is showing the pretty printed version, as shown previously in example 1.

The representation of a state can be personalized by changing the function drawState in the file tla-state.js. An example of a personalized state representation is shown in the example 2 and the source code is in examples/ceph-consensus. There are other examples in the folder examples.

To help create a personalized representation of a state, the application comes with a parser that parses a tla+ state into JavaScript structures. The parser definition is in folder expr-parser and example usage of the parser (function parseVars) can be found in the examples.

Obtain a dot file for state exploration

Using cli:

export TLA_PATH=path/to/tla
alias tlc="java -cp $TLA_PATH/tla2tools.jar tlc2.TLC"

tlc -dump dot spec.dot spec.tla
# Open the .dot file in the application in graph explorer mode (index.html)

Using the toolbox:

• Create a model
• Enable graph feature at:
  • Model Overview > Additional TLC Options > Features > Visualize state graph
• Run the model
• Open the folder of the spec in your file explorer
  • There should be a .toolbox folder with a folder for each model run
• Open the .dot file in the application in graph explorer mode (index.html)

Obtain a trace output for trace exploration

Using the cli:

export TLA_PATH=path/to/tla
alias tlc="java -cp $TLA_PATH/tla2tools.jar tlc2.TLC"

tlc -tool spec.tla > spec.out
# Open the .out file in the application in trace mode (trace-explorer.html) 

Using the toolbox:

• Create and run a model
• Open the folder of the spec in your file explorer
  • There should be a .toolbox folder with a folder for each model run
• Open the .out file in the application in trace explorer mode (trace-explorer.html)

Related tools

The ideas behind this tool were inspired by TLA+ Animation Module and Runway.