Re: Can't check a file

[lxhwy...@xxxxxxxxx]

在 2014年7月11日星期五 UTC+8上午2:14:17，Konstantin Solomatov写道：
> 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

Hello,

I met the same problem as you. I have installed the TLA toolbox and the TLA+ Proof System, but when I checked it, I have the following error:
The following error occurred while running the PM : 
Cannot run program "tlapm" (in directory "D:\0ICT\cygwin\usr\local\lib\tlaps\examples"): CreateProcess error=2, No such file or directory
Cannot run program "tlapm" (in directory "D:\0ICT\cygwin\usr\local\lib\tlaps\examples"): CreateProcess error=2, No such file or directory
I think the problem is similar with you, so I want to know how you deal with it later.

English is not my mother language, but I hope I describe the whole problem well.

Thanks,
LiXiaohui