If you need to model check a very large state space, then it is a good idea to watch this video from TLA+ conf from 2018 where Markus Kuppe shares some tricks on how to improve TLC model checker performances: