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

[konstantin...@xxxxxxxxx]

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.