4 ms·
Does TLA+ system prove the model or does it verify the model by essentially brute-forceing it? AlLoy seem to do the brute force verification using SAT solvers.
by billfruit 4y ago
Does TLA+ system prove the model or does it verify the model by essentially brute-forceing it? AlLoy seem to do the brute force verification using SAT solvers.
- thamer 4y agoYes it is essentially brute-forcing it. Note that TLA+ is the language that the model is written in. The program validating is called TLC, it's a model checker.
- _flux 4y agotlc essentially uses brute-forcing, apalache uses SMT solvers. tlc still has some advantages over apalache in some conditions, but actually I've never even used apalache with my models (I'm still in the practice phase, though).