Proposal: design robust export format for TLC state graph

The TLA+ tooling ecosystem is expanding, and that means there is demand for the Java-based tla2tools.jar to function not only as a standalone artifact, but also a reliable base for the parsing, interpretation, and model-checking of TLA+ specifications so other tools do not need to re-implement that functionality (related: #1048). Exporting the state graph explored by TLC is a common desire; TLC already implements the -dump format for multiple output formats (JSON and DOT graph description language), but this proposal is for design work to examine whether these formats are sufficient & should simply be improved upon with additional features & bugfixes, or a full custom format is necessary.

The TLC state graph output is consumed by several projects that I know of:

• Scimitar - a tool for inductive proof composition written by @will62794 - consumes the state output as JSON
• This talk by @defo10 et. al at the 2024 TLA+ conference about deriving useful visualizations of large state graphs using the DOT output format
• Various trace validation & test-case generation projects seem to use this, as described in the MongoDB eXtreme Modelling in Practice paper

So the questions are:

1. Do the existing DOT and JSON export formats meet the needs of users?
2. Could the existing DOT and JSON export formats be made to meet the needs of users with additional features & bugfixes (for example fixing #816)?
3. Would designing a custom binary state graph output format be worth the drawback of consumers having to implement a parser for it?

@lemmy mentioned state graph export was primarily intended for debugging the tools themselves, although people have found alternative uses for it.

CC @fwhdzh. As discussed in November community meeting.