I am looking to use TLA+ to generate test cases for another programming language, Julia.
I have read the following:
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.