[tlaplus] Using PTL back-end in Toolbox

[Raúl Pardo <raul.pardo.jimenez@xxxxxxxxx>]

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

-- 
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/9ecf8bcd-1403-4b49-88bb-36eb99d8e93b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.