Best regards,Hi Gise,Is there also an additional information after "An internal error occured during: 'OpenSpecHandler is parsing spec...'"?
On 13 May 2014 16:17, Gisela Rossi <gise.ross...@xxxxxxxxx> wrote:
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.htmlIf you have installed the Proof system, then the examples can be found in
where $(DIR) is the installation directory (/usr/local normally).Best regards,
TomerOn 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,
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.--
You received this message because you are subscribed to the Google Groups "tlaplus" group.--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/WQ5JK3tEtBw/unsubscribe.
To unsubscribe from this group and all its topics, 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.