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