I'm getting started

[Gisela Rossi]

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

[shaolintl .]

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

--
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...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Gisela Rossi]

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

[shaolintl .]

Hi Gise,
 

Is there also an additional information after "An internal error occured during: 'OpenSpecHandler is parsing spec...'"?

Best regards,
Tomer

[Gisela Rossi]

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

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

[shaolintl .]

Hi Gise,

I have no idea why this exception is raised but I found out it is not that uncommon in Eclipse (the Toolbox is based on Eclipse).

The solution suggested at:
http://stackoverflow.com/questions/1250505/junit4-eclipse-an-internal-error-occured-during-launching

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

[Gisela Rossi]

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