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

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

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,


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/1c553ac6-e534-355a-799b-d684dcf81fb5%40lemmster.de.
For more options, visit https://groups.google.com/d/optout.

Attachment: ToolboxLibraryPath.png
Description: PNG image