[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Tools enhancements in "Smart Casual Verification of the Confidential Consortium Framework"

A screencast demonstrating the feature is linked from the commit that introduced unsatisfied breakpoints [1]. Additionally, breakpoints now generally support TLA+ breakpoint expressions [2].  Looking ahead, a forthcoming journal version of "Validating Traces of Distributed Programs Against TLA+ Specifications" [3] dedicates additional space to debugging trace validation.

On the technical side, the TLA+ Debugger integrates with TLC’s interpreter, intercepting execution when all variables are defined and a subsequent subformula of the next-state relation Next causes the Next to evaluate to false. For example, in the context of trace validation, the unsatisfied breakpoint will fire if x = 1 and x' = 3 after reading the (current) value from the log/trace file.

----- MODULE Spec -----
VARIABLE x

SomeSubAction ==
    /\ x \in Nat
    /\ x’ = x + 1   

Next ==
    \/ SomeSubAction

=====

---- MODULE Trace ——
EXTENDS Spec

TraceNext ==
   /\ x’ = ReadValueFromTheLog
   /\ SomeSubAction

=====


Relatedly, the newer `constrained` sub-command of TLC’s Dot state-graph “dumper" will cause it to also dump and annotate states that are excluded from the model due to State or Action Constraints.

Markus

[1] https://github.com/tlaplus/tlaplus/commit/f849bf1b8f85960c0c0ca2cae1034a1feeb20b52
[2] https://github.com/tlaplus/tlaplus/pull/1099
[3] https://arxiv.org/abs/2404.16075
[4] https://github.com/tlaplus/tlaplus/commit/24479f74c8a02fbe2f83981ca6210e2f7fa7799f


> On May 19, 2025, at 9:45 PM, Finn Hackett <fhackett.py@xxxxxxxxx> wrote:
> 
> I was actually surprised to see (4) in this list - somehow I missed that when reading around, looking up video tutorials, etc. It also may be that the button is right there and I didn't realize how to trigger the behavior... (tl;dr yes docs good)
> 
> Is there a PR I can look up (for the vscode plugin I assume)? I ended up building something in the same vein, but using a special TLC VIEW directive instead. Curious to see how the debugger version behaves.
> Note: I tried the obvious search on Github and got nothing, so I'm resorting to "does anyone remember what / when".


-- 
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/581D1F04-BE1F-4D52-A09D-6AA25BF609D0%40lemmster.de.