[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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:

If you have installed the Proof system, then the examples can be found in
where $(DIR) is the installation directory (/usr/local normally).

Best regards,

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 find 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,

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.