All you need is a simulator? Nope | Protocols Made Fun

[giscus[bot]]

All you need is a simulator? Nope | Protocols Made Fun

Author: Igor Konnov

https://protocols-made-fun.com/testing/model-checking/2026/03/09/random-walks.html

[lemmy]

There are a few advantages to TLC’s approach here.

One is that enumerating all successors is useful for more than just choosing the next step: TLC can also check invariants on all generated successor states, not only on the one that ends up being sampled. That is a meaningful benefit when the goal is to catch bugs, not just drive a walk.

Also, for specs that explicitly model faults, it’s not too hard to correct for “faulty transitions dominate the search” by adjusting the probabilities of the fault actions themselves. That’s the approach we’ve used in practice; SIMccfraft.tla is one example (https://github.com/microsoft/CCF/blob/main/tla/consensus/SIMccfraft.tla). Recent TLC versions also have extended simulator coverage statistics (-Dtlc2.tool.Simulator.extendedStatistics=true), which make this kind of tuning easier to reason about.

It’s also worth mentioning that TLC supports reinforcement learning / Q-learning in addition to random walk. In our experience, though, getting Q-learning to work well is not especially straightforward, because picking the right variables for the hash/input space is non-trivial. Compared to that, manually adjusting action probabilities is much easier to understand and explain. We’ve also found Q-learning’s wall-clock performance to be significantly worse than random simulation with hand-tuned action probabilities.

[ericsson49]

Random walks are not sufficient to achieve complete coverage except for very small state spaces.
...
Another issue with state coverage by random walks is that you would not even know that you achieved complete coverage.

Great two points why safety properties should be validated via exhaustive search.
Nowadays, it's much more accessible.