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

[Paul Eipper <lkra...@xxxxxxxxx>]

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.