Leslie Lamport

Last modified on 7 February 2021

Weeks of debugging can save you hours of TLA+  [7 Feb 2021]

A video by Markus Kuppe described here.

VSCode Alternative to the Toolbox   [2 Jan 2021]

A Visual Studio Code extension for TLA+ is available here.  It lacks many features of the Toolbox, but people who dislike the Toolbox may prefer to use it.

TLA+ Community Event   [3 Nov 2020]

This virtual event was held in October 2020 as a satellite of the DISC 2020 Conference.  The program and videos of the talks can be found on its Web site.

PlusPy   [6 Aug 2020]

This is a system written by Robbert Van Renesse that actually executes a TLA+ specification.  See this post on the TLA+ Google group.

New TLAPS Release   [5 Aug 2020]

After much too long, there has been a new release of the TLAPS proof system.

Community Modules   [5 Aug 2020]

This is an open GitHub repository for TLA+ users to share specifications or parts of specifications, such as operator definitions, that may be useful to others.

TLC Profiler   [5 Aug 2020]

The Toolbox provides profiling of a TLC execution of a model.  It can show you in what parts of a spec TLC is spending a lot of time, as well as helping find problems with the spec.  It's on a help page that can be found here on the web or in the Toolbox by searching help for profiling.

TLC Features   [5 Aug 2020]

The ability to collect and report information with the TLC module's TLCGet and TLCSet operators has been enhanced.  See the document Current Versions of the TLA+ Tools for details.

TLC Liveness Checking Error-Reporting Bug   [21 Apr 2020]

Because of a bug that has existed for many years, if TLC runs out of memory or another resource while checking liveness, then it produces the correct error message but exits normally, without producing an error code.  The Toolbox displays no error warning when this happens, and you have to look carefully at the Model Results page to see that TLC did not complete successfully.  When run from a command line with no options that cause TLC to produce extra output, the error message should be easy to see.  A shell script that runs TLC will probably not report the error.  This bug was fixed in the 20 April 2020 release of TLC.