I don't quite follow what you're saying, but I think you understand.
There are lots of ways to write sensible specs in TLA+, and TLC can handle
only a tiny fraction of them. Fortunately, our experience writing programs
almost always leads us to write sensible specs that TLC handles. For
example we naturally write x' = x+1 rather than x+1 = x', and
(y # << >>) /\ (y' = Tail(y))
rather than
(y' = Tail(y)) /\ (y # << >>)
However, there are things that programming languages allow that lead to
non-sensible specs if naively translated into TLA+. These include
an assignment statement such as y[1] := ... and putting an assignment
statement in an `if' test. That's why you need to understand what
a TLA+ spec means.
On rare occasions, we (including me) write a sensible spec in a way
that seems reasonable but that TLC can't handle. That's why there's a
description of how TLC works. But they are rare--I think it's
happened to me only a couple of times. A much more difficult problem
is teaching people to go outside the limits of what programming
languages allow them to do and take advantage of the power of math
that TLA+ provides and that TLC can handle.
Leslie