Re: [tlaplus] I'm getting started

Hi Tomer,

Thanks for your help! I have everything installed now (I think), I've modified the $PATH and I've found the examples directory.

I still can't make it work though. I've tried to load the Euclid.tla example within the toolbox and an error message appears saying: " 'OpenSpecHandler is parsing spec...' has encountered a problem. An internal error occured during: 'OpenSpecHandler is parsing spec...' ".

What am I doing wrong?

Thanks,

Gise

On Sunday, May 11, 2014 6:08:15 PM UTC-3, shaolintl wrote:

Hello Gise,

The link you have specified is for the installation of the TLA Toolbox, which contains also a link for installing the Proof system (TLAPS) and its examples.

The Toolbox is the graphical IDE for TLA+ and contains most of the TLA tools (parsers, compilers and TLC). The Proof system should be installed separately.

The link for installing the proof system is:
http://tla.msr-inria.inria.fr/tlaps/content/Home.html

If you have installed the Proof system, then the examples can be found in

$(DIR)/lib/tlaps/examples
where $(DIR) is the installation directory (/usr/local normally).

Best regards,
Tomer

On 11 May 2014 22:28, Gisela Rossi <gise.r...@xxxxxxxxx> wrote:
Hello everyone,

I'm getting started with TLAPS. I've read the paper "Verifying Safety Properties With the TLA+ Proof System" and there it mentions "We have written a number of proofs, mainly to ﬁnd bugs and see how well the prover works. Most of them are in the examples sub-directory of the TLAPS distribution."

But I downloaded the lastest distribution of LTAPS (from http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#installing) and there is no sub-directory named examples.

Where can I find that subdirectory with examples?

Thanks for the help,
Gise

--
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...@googlegroups.com.
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.