Re: Can't check a file

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

it looks like you are trying to launch TLAPS, the TLA+ Proof System. It doesn't come with the default Toolbox installation but must be installed separately. Please see the instructions at http://tla.msr-inria.inria.fr/tlaps/content/Home.html.

Stephan

> 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