Re: [tlaplus] Yet more code conformance checking

Re: the TLC streaming idea, I can clarify. It's in the context of using the Antithesis implementation fuzzer. The base idea is to expose the trace as an async lazy-filled sequence value, which populates with elements as the system makes progress (still for one execution, it just means we can check things earlier). On its own, streaming data to TLC might only find a counterexample sooner, since it can stop system execution early. If you have a hypervisor that's constantly cloning and branching your system execution (Antithesis), however, running TLC in parallel with the system means potential work deduplication, since you're exploring branches in both the system's state and TLC's in progress model check (so no rechecking path prefixes at the end). Likely less useful outside Antithesis, but that was the idea.

Best,

-Finn

On Sun, Jul 6, 2025 at 6:44 AM Ognjen Maric <ognjen.maric@xxxxxxxxx> wrote:

Hi Jesse,

thank you for the comments, appreciated!

On 7/5/25 7:35 PM, A. Jesse Jiryu Davis wrote:
> Regarding the JVM startup cost, I can imagine it's painful. Would it
> help if Apalache permitted a streaming API so you could interact with it
> without restarting? Unfortunately Apalache isn't maintained now, I think

It would definitely shave off a non-negligible part of the overhead.
Unfortunately since I generate one model per state pair, this still
incurs the overhead of Apalache pre-processing for each state pair,
which wouldn't go away with a streaming version. I guess the ideal
solution would be to really directly add the functionality to check the
compliance of a state pair with a formula, but I haven't looked at the
Apalache codebase so I have no idea how difficult this would be.

> My intern Finn Hackett is also working on trace-checking, using TLC.
> He'd considered adding a streaming API to TLC so it could a) handle very
> long traces but only keep a couple states in memory, and b) run trace-
> checking concurrently with the implementation test, and abort the test
> soon after the implementation's behavior diverges from the spec, instead
> of running after the test completes.
I don't really get how the streaming API allows you to lower the memory
footprint, or indeed how to check a trace interactively (if I understand
you correctly) - could you explain?

As for the second point, this wouldn't be a big win for my current use
cases. There, the setup for an implementation test may indeed take a
while, but once the state pairs start being produced the test usually
ends quickly. So starting the checks in parallel wouldn't give me much.
Of course this could be quite different in other cases.

Cheers,
Ognjen

--
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/929bd577-37d7-495e-bd45-1255de164776%40gmail.com.