Re: [tlaplus] Yet more code conformance checking

[Igor Konnov <igor.konnov@xxxxxxxxx>]

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/CACooHMAuky0dvk1NBPHMRidviuTN%2BrWKaAYm_1LDG9-dJPqQJw%40mail.gmail.com.