What do you mean by "run"? Check in the TLC model checker? You need to first write a configuration that you want to check. Lamport's Specifying Systems has full documentation for using the model checker from the command line. But if you're a beginner, you might be better off using the IDE, at least at first, as it helps you write a configuration very easily. Also, I would recommend starting with a simpler specification (there are lots of examples available). Otherwise, the checker would just work for a while and spit out "OK", and won't mean much to you.
