Python serialization standalone

[lemmy]

Would it be possible to make the Python serialization available as a first-class TLA+ operator similar to the Json and the Java serialization? This way, users could serialize large numbers of traces generated by TLC simulation mode.

[tangruize]

Thanks for opening the issue! My first feeling is that Json may be powerful and portable enough. And it may not be so necessary to do a python serialization since Json can be easily loaded. Later I will try Json.tla and IOUtils.tla out and consider how to implement this function.

It seems that using Json.tla requires modifications of the TLA+ specification. Maybe it is more useful to dump Json formatted trace in TLC? I found a JsonStateWriter.java that might do this job. If there is a need, I‘d be very delighted to contribute to tlaplus.

[lemmy]

Thanks for opening the issue! My first feeling is that Json may be powerful and portable enough. And it may not be so necessary to do a python serialization since Json can be easily loaded. Later I will try Json.tla and IOUtils.tla out and consider how to implement this function.

Json doesn't have support to handle sets and sequences--one has to come up with hacks. Also, it could prove useful in the scope of PlusPy.

It seems that using Json.tla requires modifications of the TLA+ specification. Maybe it is more useful to dump Json formatted trace in TLC? I found a JsonStateWriter.java that might do this job. If there is a need, I‘d be very delighted to contribute to tlaplus.

Indeed, one could amend the spec to convert a trace to json. However, it is generally advised to use MC.tla files anyway to not clutter the original specification with model-checking concerns. The upside of Json.tla is that a) it works in other scenarios such as Alias, and b) users can replace it with other serialization formats such as EDN.

[tangruize]

I also find that Json supports only key-value pairs and arrays. It seems that the Python serialization will be useful and I will investigate more later. Thank you for your helpful comment.