4 ms·
>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
by doonesbury 6y ago
>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
- pron 6y agoThe 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.
- salawat 6y agoDefine "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.
- doonesbury 6y agoOK, 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.