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

[tlaplus] Using PTL back-end in Toolbox


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?

-- 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.