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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

All technical work related to the paper is publicly documented in the CCF and TLA+ GitHub repositories. Good entry points are:

https://github.com/microsoft/CCF/issues?q=label%3A%22tla%22
https://github.com/microsoft/CCF/issues/5057

Below is a non-exhaustive list of more specific pointers:

- "we manually weighted failure actions to reduce the likelihood of them being chosen"

* https://github.com/microsoft/CCF/issues/6537
* https://github.com/microsoft/CCF/pull/6562
* https://github.com/microsoft/CCF/blob/main/tla/consensus/SIMccfraft.tla
* https://github.com/microsoft/CCF/blob/main/tla/consensus/SIMCoverageccfraft.tla
* https://github.com/tlaplus/tlaplus/commit/05d755591382ce1a574142b004e918074807c23f

* Related: RL/QL work stream started with https://github.com/tlaplus/tlaplus/commit/6dfec66b288f5c57296be8630fab9cea0200b2d4


- "we implemented depth-first search (DFS) in TLC”

* https://github.com/tlaplus/tlaplus/pull/867
* https://github.com/tlaplus/tlaplus/commit/62625342a01b96c2839c575b49dce1b8489fae94


- "we implemented a new unsatisfied breakpoint that activates for each state in T that is found to be unreachable”

* https://groups.google.com/g/tlaplus/c/wuJbBRqZdTQ/m/v6mCu99_AQAJ


- "T can be visualized as a graph that not only includes all unreachable states but also references the subformula responsible for the state being unreachable"

* https://github.com/microsoft/CCF/pull/5989#issuecomment-1928816893
* https://github.com/tlaplus/tlaplus/commit/24479f74c8a02fbe2f83981ca6210e2f7fa7799f
* https://github.com/tlaplus/tlaplus/commit/312518885c0f4688fceb1b30d27c2aed61a6628f


- Action composition

* https://github.com/tlaplus/tlaplus/pull/805



I'm also happy to answer specific questions at the next TLA+ Community call on June 3rd.

Markus

> On May 19, 2025, at 4:45 PM, A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:
> 
> The paper mentions new features in the TLA+ tools:
>     • 
> "we manually weighted failure actions to reduce the likelihood of them being chosen"
>     • "we implemented depth-first search (DFS) in TLC"
>     • "TLC had already been enhanced to support trace validation"
>     • In the TLA+ debugger, "we implemented a new unsatisfied breakpoint that activates for each state in T that is found to be unreachable"
>     • "T can be visualized as a graph that not only includes all unreachable states but also references the subformula responsible for the state being unreachable"
> The paper summarizes this effort as "enhancing the TLC model checker to support trace validation, which involved implementing support for action composition, DFS, improved debugging support, and visualizing the state graph." So I think the enhancements are in both TLC and the VS Code TLA+ debugger.
> 
> Question: Am I right that the paper mentions 6 new features, and where can I learn more about them?

-- 
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/0A74A7BB-29C0-41F6-BD73-E56F4F7F23E8%40lemmster.de.