Breaking the limits of TLA+ model checking

https://www.hillelwayne.com/post/graphing-tla/

by todsacerdoti • 3 years ago

122 4 3 years ago

Nezteb• 3 years ago

The repo: https://github.com/hwayne/tla-graphing-demo

dwohnitmok• 3 years ago

RE the OP's work to add probability-weighted state transitions, more generally TLA+ doesn't have the ability to talk about state transitions (i.e. actions in TLA+) themselves in a first class way, which makes certain invariants very annoying or impossible to state (e.g. we will converge after no more than 5 steps). I wonder if there's a clean way to extend TLA+ to cover these cases. Admittedly they don't come up that frequently.

nano_o• 3 years ago

In your example, you can just add a variable that is incremented at every step and then use it to state your invariant that convergence must happen within 5 steps.

Sometimes you can encode properties that might initially seem hard to state in TLA+ in a similar way. Lamport has a recent paper explaining how to do that for hyperproperties such as information-flow security: http://lamport.azurewebsites.net/pubs/pubs.html?from=https:/...

raphlinus• 3 years ago

Here's my version of the example translated into safe Rust: https://play.rust-lang.org/?version=stable&mode=debug&editio...

This being safe Rust, it fixes the undefined behavior in the C++ version. You can of course implement that in unsafe Rust, but I can't quite bring myself to post that.

Breaking the limits of TLA+ model checking

Related Stories