Using PTL back-end in Toolbox

[Raúl Pardo]

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

[Markus Kuppe]

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

[Raúl Pardo]

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