Hacker News Reader

The model checker TLC, like SPIN, does verify "against all interleavings" but it doesn't "run" all of them; in fact, it runs none of them. Conceptually, it gives you the answer about all of them, but the algorithm doesn't actually run them.

View on HN

OK, that's clearer. Thank you. Certainly not nit-picking, but it's worth pointing out in passing that computing the state to check qll the interleavings --- albeit not actually running each path through the reachable states but looking for safety or livness violations --- requires real work being super exponential in the worst case.

Define "against all interleavings", or is that something I'd understand after reading TLA+'s documentation?

I think I get the drift, I'm just wanting to confirm "read the docs" is the only missing bit.

Reply on news.ycombinator.com