tlc essentially uses brute-forcing, apalache uses SMT solvers. tlc still has some advantages over apalache in some conditions, but actually I've never even use

tlc 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).