Here are the steps to take in order to run TLA from the command line:

1) Update your .cshrc file with the following line

setenv CLASSPATH /eecs/local/pkg/tla

2) cd to the directory where you have your spec files

3) create an accompanying config file (.cfg) for each .tla file. More information on the config files syntax may be found in “Specifying Systems” https://lamport.azurewebsites.net/tla/book-02-08-08.pdf\book – pg. 251 and up

4) assuming that you have created a config file, run the following command

java tlc2.TLC  <your_file>.tla