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

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

Hello, I'm reading "Smart Casual Verification of the Confidential Consortium Framework". Markus is a co-author. It's great! The authors succeeded where I had failed and they clearly describe how they did it.

The paper mentions new features in the TLA+ tools:
  1. "we manually weighted failure actions to reduce the likelihood of them being chosen"
  2. "we implemented depth-first search (DFS) in TLC"
  3. "TLC had already been enhanced to support trace validation"
  4. In the TLA+ debugger, "we implemented a new unsatisfied breakpoint that activates for each state in T that is found to be unreachable"
  5. "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?

Thanks, I know I'm asking for a lot of info.

--
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/2443fd1a-1c35-419a-95b8-72de361f28bdn%40googlegroups.com.