Re: [tlaplus] Any tool(s) for generating TLA+?

PlusCal is an imperative language that is used as a starting point in TLA+ code generation. The generated code describes the state transitions modeling the program counter and stack as part of the model state.

You could look at that or if your system already produces some kind of state transition specification, generating the code yourself might not be that hard.

Be careful with not generating specs and models with state spaces too big that make model checking impossible.

--

Felipe

On Thu, May 25, 2023 at 5:09 AM Gareth Smith <anythingwithawire@xxxxxxxxx> wrote:

yeah I am looking as well - I have an application that lets you specify state based behaviour for industrial automation and functional safety as an executable specification, and part of this is once the specification is data then formal methods translation looks do-able

So I am already generating functionality in a few different languages of code for export OK, but not TLA+ yet

Currently I end up in negotiations with a prospective buyer, so maybe I won't get there first, but if there was a starting point of a codebase or similar I could leverage off, that would be great.

On Wed, May 24, 2023 at 7:25 PM thomas...@xxxxxxxxx <thomasgebert@xxxxxxxxx> wrote:
I am currently working on a formal system that I have been manually translating over to TLA+ . I was debating writing myself a TLA+ generator doing some dumb string-concat logic, but I was curious if there were any tools that would let me pass things into some kind of tree and output TLA+?

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/65a2da9f-19d4-499d-b233-7377cde1bac1n%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CALDKJw3FTUaafCD4enKWEkaW3VHiinodAsPjmAK%2Btpv0n%2BOR-w%40mail.gmail.com.