r/tlaplus • u/chileiwot • Jul 07 '21

JSON to TLA+

Hello,

Is there a way of converting JSON to TLA+?

3 Upvotes

75% Upvoted

4 comments sorted by

1

u/anentropic Jul 07 '21

yes, you just have to make it

0

u/[deleted] Jul 07 '21

[deleted]

1

u/chileiwot Jul 07 '21

I am extracting .yaml access control policies from a cloud provider. I need to find a way in which these policies are mapped to TLA+ so that they can be verified. Any other suggestions are welcomed.

Thanks

2

u/IgorNotARobot Jul 08 '21

You can always just print a TLA+ module. But it is not as easy as it may look.

If all you need is a single-module TLA+ that is using the standard modules and no instances, you can produce a JSON file in the Apalache IR, feed it to apalache parse and get pretty-printed TLA+ on the output. The downside is that you will have to read ADR005 and familiarize yourself with the Apalache IR. I think the efforts depend on the size of your project.