3 ms·
> Model checking with 2 acceptors worked, but I gave up on model checking with 3 acceptors since it took more than an hour. Does anyone know how the TLA model
by jules 11y ago
> Model checking with 2 acceptors worked, but I gave up on model checking with 3 acceptors since it took more than an hour.
Does anyone know how the TLA model checker works? I wasn't able to find this information. Does it use a SAT/SMT solver? Or brute force search?
- ahelwer 11y agoExhaustive search across all states and state transitions. There's a distributed version which helps with especially large state spaces. Combinatorial explosion is an issue. In some cases the best/only option is to formally prove correctness with the built-in proof language; the model checker works well in tandem, for quickly checking assertions before putting effort into a proof. Generally the model checker alone works just fine, though.
- pja 11y agoYeah, it’s exhaustive search. Fortunately storage costs have dropped like a rock over the last few decades, so problems that were hilariously impractical only a few years ago are now checkable on commodity hardware. A fully interlinked (ie guaranteed symmetric inter-node bandwidth) cluster on Amazon EC2 with aggregate memory (even before you start touching secondary storage) in the Terabytes can be rented for a few 10s of $ an hour at spot prices. It may be that Formal Methods time has finally come!