[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] I'm getting started
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?
On Sunday, May 11, 2014 6:08:15 PM UTC-3, shaolintl wrote:
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
where $(DIR) is the installation directory (/usr/local normally).