As Andrew said, the algorithm is breadth-first search. Today, the main components of the search are:
- tlc2.tool.impl.Tool (enumerates initial and successor states)
- tlc2.tool.queue.IStateQueue and its subclasses (stores the queue of not-yet-visited states)
- tlc2.tool.fp.FPSet and its subclasses (stores the set of already-visited states; or rather, the 64-bit hashes of already-visited states)
- tlc2.tool.Worker (in a loop: dequeues a state, checks properties, enumerates successors, and enqueues not-yet-visited successors)
Andrew wrote that "there really isn't much to optimize". This is only half true. There are many different ways to optimize state exploration: make successor-state enumeration faster, make the queue have lower thread contention, make the visited-state-set use less (or more) memory, etc.
However, many people much smarter than me have spent enormous effort making TLC as fast as possible. The truth in Andrew's statement is that "there really isn't much left to optimize, and what's left is very difficult to implement correctly". I don't want to discourage you---many people would be very grateful if you improved TLC's performance---but I don't know of any low-hanging fruit you can pick.
> Is there a good solution to the state space explosion problem in TLC?
It depends. Andrew alluded to my favorite solution: symmetry reduction. Symmetry reduction can exponentially decrease the number of states that TLC has to explore. You can check invariants and action properties under symmetry reduction, but unfortunately you cannot use it to check liveness properties faster.
If you are able to use symmetry reduction, I highly recommend it as the first line of defense against state space explosion. You can find information about it in Specifying Systems, section 14.3.4: