Re: [tlaplus] Yet more code conformance checking

[Igor Konnov <igor.konnov@xxxxxxxxx>]

I forgot to mention that there is also a simple way to produce TLA+
specs without going via the whole AST/IR route. In a recent project
for Stellar, we experimented with template engines such as EJS, which
are normally used to produce static web sites. It is relatively easy
to write a TLA+ template that generates a TLA+ spec tuned for fixed
inputs. Here is an example [1]. This does not solve the issue of
parsing TLA+ and doing preprocessing each time, but this approach is
quite convenient from the engineer's p.o.v., as one can load
blockchain transactions using the standard SDKs.

[1] https://github.com/freespek/solarkraft/blob/main/doc/case-studies/xycloans/MCxycloans_monitor.ejs.tla

Best,
Igor

On Mon, Jul 7, 2025 at 10:32 AM Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
>
> Hi Ognjen,
>
> On Sun, Jul 6, 2025 at 3:48 PM Ognjen Maric <ognjen.maric@xxxxxxxxx> wrote:
> >
> > On 7/5/25 8:00 PM, Igor Konnov wrote:
> > > Apalache has the server mode [...]
> > Thanks - I wasn't aware of this at all. I'll have a look at how I could
> > go about integrating this when I find some time. Python may already be
> > enough for my purposes, though a Rust client would likely make my life
> > easier.
>
> Back then, writing GRPC clients was a bit tedious, but I guess, an LLM
> could produce a GRPC client in Rust.
>
> > And since you're here :) I take it extending Apalache to just check the
> > conformance of a state pair with a formula isn't really trivial?
>
> Currently, Apalache emits traces in JSON [1]. What you are asking for
> is whether it would be possible to load two states,
> e.g., in the same format as [1], and evaluate them against a predicate
> of a preloaded model. This is definitely doable
> and it's not really hard to implement for someone who knows the codebase.
>
> We also had a more ambitious RFC-10 [2]. With this RFC, you would be
> able to introduce a feedback loop between
> the system under test and the model. Basically, evaluating the outputs
> of the system against the model and producing
> next inputs to the SUT. This was never implemented, though, again,
> it's a very feasible task.
>
> [1] https://apalache-mc.org/docs/adr/015adr-trace.html
> [2] https://apalache-mc.org/docs/adr/010rfc-transition-explorer.html
>
> Best,
> Igor

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/CACooHMBbn6T4n6vbA-kpsgdgZm%2BMhjT2Zkk1UM%2BsdWoXsSfoBw%40mail.gmail.com.