Re: [tlaplus] I'm getting started

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.ross...@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...@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.