You didn't say if the translation succeeded. It probably did, since
you didn't indicate that it produced an error message. You could find
out by looking at the tla file to make sure that it put the
translation there.
TLC's console output makes it pretty clear if there was an error.
Since you don't know if it it found an error, it probably didn't. But
we'd have to see the console output to be sure. But assuming the
translation succeeded and TLC found no error, this means that you have
correctly specified some protocol that has a finite number of
reachable states. What else it means depends on what the
configuration file told it to check. You also didn't say what was in
the configuration file.
But before you go any further, you should stop running TLC from a shell
and run it from the Toolbox. See the TLA+ web page to find out how to
download and install the Toolbox.
Leslie