TLA+ Graph Explorer
This is a static web application to explore and animate a TLA+ state graph.
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.
Example 1 - Missionaries and Cannibals
Example 2 - Ceph consensus algorithm
How to use
The application is in the folder src.
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-3mon.