[FEATURE] Change the JSON encoding for a seamless integration with JsonPath expressions

[andrey-kuprianov]

The current TLA+ JSON encoding works fine on itlself, but while trying to apply JsonPath expressions used in Jsonatr, e.g. in this spec, it turned out that JsonPath expression do not work when special symbols ('+', '=', etc.) are used as object keys -- and exactly this we do in our current JSON encoding, to shorten it a bit.

As the JSON encoding is anyway used for automated processing, we need to change it slightly, to have a more straightforward structure without using special symbols as keys, albeit a bit inflated in size. The proposed encoding should look like this file.