Hi,
I was able to fix the problem and I thought I it might be useful for future users if I comment what was happening.
Apparently what was happening is that I was trying to load the example from /usr/local/.../examples
which is the default installation directory. But in Unix based systems this directory is read-only. When I copied the directory to another location with read-write permissions, it was able to load the example.
I have two suggestions:
1) It might be a good idea to add explicitly this step to the documentation ( the step of copying the directory to another location with more permissions).
2) The error shown should be something more descriptive of the problem itself and not a java null pointer error.
I hope this helps someone :)
Regards,
Gise
On Tuesday, May 13, 2014 11:55:32 AM UTC-3, shaolintl wrote:
is "deleting the workspace and the Eclipse directory and starting over".
Maybe you had/have another version of Eclipse and it interferes with the Toolbox?
I am sorry I could not give you a better advice.
Best regards,
Tomer
On 13 May 2014 16:46, Gisela Rossi
<gise.r...@xxxxxxxxx> wrote:
Hi!
Unfortunately, that is the entire error message. In details it says:
"An internal error occurred during: "OpenSpecHandler is parsing spec...".
java.lang.NullPointerException"
Thanks!
Best regards,
Gise
Hi Gise,
Is there also an additional information after "An internal error occured during: 'OpenSpecHandler is parsing spec...'"?
Best regards,
Tomer
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
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,
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.
--
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.