TLA+/PlusCal generators from source code

Deividas Bražėnas

unread,

Mar 31, 2022, 2:39:43 PM3/31/22

to tlaplus

Hello,
I'm writing a master's thesis about generating TLA+ specifications from Elixir source code. I'm currently doing a literature analysis but having trouble finding any information about existing tools that would convert the source code to the TLA+ specification - I only find the tools that generate the source code from specs.

Maybe you know any tools with this functionality?

Thanks!

Deividas Bražėnas

unread,

Mar 31, 2022, 2:41:31 PM3/31/22

to tlaplus

Or maybe you have some other information that may be helpful for me :) In the current approach, I'm generating simple TLA+ specs from the AST of Elixir code.

A. Jesse Jiryu Davis

unread,

Mar 31, 2022, 3:54:22 PM3/31/22

to tla...@googlegroups.com

My coauthors and I did a big literature review for "eXtreme Modelling in Practice" a couple years ago, and I don't recall seeing any code-to-TLA+ research.

The content of this email, including all attachments, is confidential. If you are not the intended recipient, please notify us immediately and delete this email. Any disclosure, copying, distribution or any other use of its content is strictly prohibited.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/157baf7c-4fb6-4cd4-93ed-87410d1576cbn%40googlegroups.com.

Nam Nguyen

unread,

Mar 31, 2022, 5:30:29 PM3/31/22

to tla...@googlegroups.com

https://www.youtube.com/watch?v=trm9Lp0yt6Y

First result for "elixir tla" on YouTube.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFRUCtbt9xme-KpQnd0VdqMfcnVk5iceAqi7vUz4cw9-52Qz9w%40mail.gmail.com.

Deividas Bražėnas

unread,

Apr 1, 2022, 1:32:41 AM4/1/22

to tlaplus

Thank you! Will definitely take a look!

Deividas Bražėnas

unread,

Apr 1, 2022, 1:33:35 AM4/1/22

to tlaplus

I knew this TLA transmutator for a while, but sadly it works in an opposite direction - spec to code.

Felipe Oliveira Carvalho

unread,

Apr 13, 2022, 11:59:10 PM4/13/22

to tla...@googlegroups.com

What you are trying to do is similar to the existing PlusCal to TLA+ translation, but with a much more complicated source language — Elixir. Getting familiar with how PlusCal works will elucidate a lot of things.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/42259d7f-e9b8-4a3e-a5ee-d648ae6ce0e9n%40googlegroups.com.

Reply all

Reply to author

Forward