Not sure I understand your question: TLC *does* model check your spec, it just (correctly) signals a deadlock, since the non-clock variables may stutter according to DoNothing until the clock exceeds its bound, at which point no action is enabled anymore. If you intend to avoid this, DoNothing needs a stronger time bound, see attached module for a possible definition.
Since the modified spec generates an unbounded state space, you'll need to add a state constraint to your model, such as
clock <= MAX_TIME
Hope this helps,