Using `-dump` option to produce state dumps in machine readable format

Recently we touched the topic of model based testing and -simulate configuration of tlc in the TLA+ community.

When using -simulate and -dump options to generate random behaviors of the model with the goal of using them to produce tests for systems written in other languages the question of state dumps parsing arises.

Currently -dump option generates state dumps in TLA+ format. Still, it's quite beneficial to have a machine readable format of such dumps as eventually it will be parsed by the abstract test generator.

Therefore, it's proposed to update the following part of the TLC code so that it generates dumps in JSON format: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java#L735