dumping to JSON and not dot files

[migu...@ciencias.unam.mx]

I am looking to use TLA+ to generate test cases for another programming language, Julia.

I have read the following:

https://github.com/tlaplus/tlaplus/issues/367

1. Does TLC have to process the entire model for it to generate the dump file of the entire state space?

2. Is there a way to dump TLC  trace into JSON format? It would significantly ease the parsing of the dump file and open up that tooling for many other languages.

[Markus Kuppe]

Hi,

there have been a number of talks [1,2,3,4,5] on this topic at the
recent TLA+ community event [6]. As part of [3], Jordan Halterman
contributed a Json module [7] to the CommunityModules [8] with which it
is possible to re-format traces as Json. TLC has to explore all
reachable states to dump the state graph. Star Dorminey's Kayfabe [1]
imports the state graph from TLC's dot dump.

Markus

[1] https://www.youtube.com/watch?v=lj31oIaYSj4
[2] https://youtu.be/aveoIMphzW8
[3] https://youtu.be/itcj9j2yWQo
[4] https://youtu.be/IIGzXX72weQ
[5] https://youtu.be/TP3SY0EUV2A
[6] http://conf.tlapl.us/2020/
[7] https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla
[8] https://github.com/tlaplus/CommunityModules

[Markus Kuppe]

On 09.12.20 07:49, migu...@ciencias.unam.mx wrote:

> 2. Is there a way to dump TLC  trace into JSON format? It would
> significantly ease the parsing of the dump file and open up that tooling
> for many other languages.

[1,2] shows a simple trick on how to export TLC error traces to JSON.
This is easy thanks to a contribution by Jordan Halterman to the
CommunityModules [3].

Markus

[1] http://tla.msr-inria.inria.fr/kuppe/TLC-Json.gif
[2]
https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840_json.tla
[3] https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla