Can't check a file

[konstantin...@xxxxxxxxx]

Hello,

I installed TLA Toolbox, and wrote a simple program from the book. Unfortunately, I can't check it. I am having the following error:

The following error occurred while running the PM : 
Cannot run program "tlapm" (in directory "/Users/kostik/Documents"): error=2, No such file or directory
Cannot run program "tlapm" (in directory "/Users/kostik/Documents"): error=2, No such file or directory

What can I do about it? 

P.S. I am using OSX