Re: Can't check a file

[konstantin...@xxxxxxxxx]

Hello,

Thank you for the quick reply. As far as I understand , TLAPS isn't required for usage of the system. What I wanted to do is just model check a simple clock example, from the book. I entered it, press run and nothing happens. What should I do to run model checking? Do I need to install any other tools?

The error which I mentioned is shown when I do any proof commands.

Thanks,
Konstantin

On Thursday, July 10, 2014 3:20:07 PM UTC-4, Stephan Merz wrote:
> 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