|
|
|
News
Leslie Lamport
Last modified on 18 March 2022
|
|
Apalache Model Checker
[17 Mar 2022]
The new Apalache model checker for TLA+ is now available. Click
here for information.
Survey
[16 Mar 2022]
To help us get a better picture of our community, we have begun
an ongoing survey of the TLA+ community.
If you have not already done so, please fill it out
here.
TLA+ Conference
[16 Mar 2022]
This year's conferences will be held on 22 September 2022 in St.
Louis, Missouri.
PlusCal
Tutorial [2 Dec 2021]
A new tutorial that teaches PlusCal to beginners is now
avaiable here.
TLA+ Community
Events [28 Nov 2021]
The 2021 TLA+ Conference was held on 30 September in St. Louis, USA,
in association with the Strange Loop conference.
A TLA+ Tutorial was given on 8 October in Freiburg, Germany, in
conjunction with DISC 2021.
The programs of both events, with links to the videos and slides
of most of the presentations, can be found on
this web page.
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.
|