Hacker News Reader

>don't only not run all possible executions of a program, they don't even run it once.

Can you please clarify? A tla+ spec (or pluscal to tla+) is supposed to verify against all possible interleavings of reachable states like spin. You seem to be saying something different

View on HN

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.

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.

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.

Reply on news.ycombinator.com