Symbolic Model Checking for TLA+ Made Faster