# Re: [tlaplus] Re: Can't check a file

Hello Paul,

I have the following file:

-------------------------------- MODULE spec --------------------------------
EXTENDS Naturals
VARIABLE hr

HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr # 12 THEN hr + 5 ELSE 1
HC == HCini /\ [][HCnxt]_hr
-----------------------------------------------------------------------------
THEOREM HC => []HCini
=============================================================================

How can I specify constants? If I just use run, it seems that nothing happens.

Thanks,
Konstantin

On Thursday, July 10, 2014 6:55:53 PM UTC-4, Paul Eipper wrote:
> Hello,
>
>
>
> From the toolbox, did you try to create a model in "TLC Model Checker"
>
> -> "New Model"? Then by specifying the values for the declared
>
> constants you should be able to "run" the model to check the program.
>
>
>
> On the console you should get the output for the run, something like
>
> this (omitted some of the verbose output here):
>
>
>
> @!@!@STARTMSG 2262:0 @!@!@
>
> TLC2 Version 2.05 of 23 July 2013
>
> Running in Model-Checking mode.
>
> Starting SANY...
>
> Parsing file MC.tla
>
> ( ... more file parsing ... )
>
> SANY finished.
>
> Starting... (2014-07-10 19:48:34)
>
> Computing initial states...
>
> Finished computing initial states: 1 distinct state generated.
>
> Model checking completed. No error has been found.
>
> ( ... statistics follows ... )
>
> Finished. (2014-07-10 19:48:36)
>
> @!@!@ENDMSG 2186 @!@!@
>
>
>
> hth,
>
> --
>
> Paul Eipper
>
>
>
>
>
> On Thu, Jul 10, 2014 at 6:46 PM,  <konstantin...@xxxxxxxxx> wrote:
>
> > 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
>
> >
>
> > --
>
> > You received this message because you are subscribed to the Google Groups "tlaplus" group.
>
> > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
>
> > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
>
> > Visit this group at http://groups.google.com/group/tlaplus.
>
> > For more options, visit https://groups.google.com/d/optout.