search

tangruize / tlc-cmd

Run TLC in cmd
MIT License
14 stars 0 forks source link

Python serialization standalone #1

Open lemmy opened 3 years ago

lemmy commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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.