search

tlaplus / tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
https://lamport.azurewebsites.net/tla/tla.html
MIT License
2.33k stars 197 forks source link

Proposal: design robust export format for TLC state graph #1073

Open ahelwer opened 1 week ago

ahelwer commented 1 week ago

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:

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.

lemmy commented 1 week ago
  1. Provide hooks/callbacks for downstream consumers to hook into TLC's state-space exploration.

Also related: https://github.com/tlaplus/tlaplus/issues/639

fwhdzh commented 1 week ago

This proposal looks excellent, and I look forward to seeing it completed.