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

Re: [tlaplus] Using PTL back-end in Toolbox

Hi Markus,

Thanks for the answer, it works now. I had set up the path but somehow
the IDE didn't load the module. I tried creating the same project again
and now every works.

-- raul

On 21/06/2019 19:30, Markus Kuppe wrote:
> On 21.06.19 06:35, Raúl Pardo wrote:
>> Hi,
>> I'm following Leslie Lamport's notes on Proving Safety Properties (http://lamport.azurewebsites.net/tla/proving-safety.pdf) to get started using TLAPS. At some point in this document it is required to use the back-end PTL. The document indicates that instructions to use this back-end should be provided in the TLAPS page. However, I haven't been able to find them... 
>> Concretely, in the snippet below, the Toolbox reports that PTL is an undefined symbol.
>> THEOREM Spec => []Mutex
>>     <1>1. Init => Inv
>>     <1>2. Inv /\ [Next]_vars => Inv'
>>     <1>3. Inv => Mutex
>>     <1>4. QED
>>         BY <1>1, <1>2, <1>3 PTL DEF Spec
>> Could you point me to the instructions to make it possible to use TLAPS library modules in the Toolbox?
>> Thanks,
>> -- raul
> Hi Raul,
> did you set the Toolbox's library path to include TLAPS [1]?
> 3. Set the toolbox's library path
> We strongly recommend that you install the Toolbox (version 1.4.8 or
> later). You will need to add the location of the TLAPS.tla file to the
> list of libraries used by the Toolbox. To do this, open the Toolbox and
> go to "File > Preferences > TLA+ Preferences". Add the directory where
> TLAPS.tla is located to the list of library path locations. If you have
> the default installation, this directory is /usr/local/lib/tlaps/.
> Hope this helps,
> Markus

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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/73e57eed-def2-abae-cb41-5a7324a0992d%40gmail.com.
For more options, visit https://groups.google.com/d/optout.