Re: [tlaplus] dumping to JSON and not dot files

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 09.12.20 07:49, migu...@xxxxxxxxxxxxxxxx wrote:
> 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.


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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/346e5bfa-b540-be40-27eb-0557c5a3616a%40lemmster.de.