[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.
>>
>> INSTANCE TLAPS
>>
>> 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.