Learning
TLA+
This is the section to go to if you are new to TLA+ and want to find out what it’s all about–particularly its How to Start section.
PlusCal
PlusCal is a language for writing algorithms that is based on TLA+; but it’s possible to start with PlusCal and learn the TLA+ that you need to use it as you go along.
Examples
This section has examples of how TLA+ and PlusCal are used. It contains the examples from the TLA+ book and others, created both by Leslie Lamport and other people.
Leave a Reply
57220 views, 78 so far
today
September 26th, 2011 at 12:15 pm
Hi,I’m happy to find out this website and I ask my question to know exactly which one of the formal specification and tool should I use to verify correctness of C-DEVS protocol?
Thanks to reply to me as soon as possible.
July 3rd, 2012 at 12:22 am
Sorry for the delay–somehow, I didn’t see this. I don’t know what the C-DEVS protocol is or what kind of correctness properties you want to verify. Things that are called “protocols” are usually best specified in TLA+ rather than in PlusCal. Any TLA+ spec should be checked with the model checker before doing anything with it. I don’t know if you have the time, energy, or expertise to try using the TLAPS proof system. I don’t know about anything about non-TLA+ tools.