Download Latest Version tla2tools.jar (2.3 MB)
Email in envelope

Get an email when there's a new version of tlaplus

Home / v1.7.1
Name Modified Size InfoDownloads / Week
Parent folder
TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip 2022-02-23 175.3 MB
0
TLAToolbox-1.7.1-win32.win32.x86_64.zip 2022-02-23 181.5 MB
0
TLAToolbox-1.7.1-linux.gtk.x86_64.zip 2022-02-23 182.0 MB
0
TLAToolbox-1.7.1-linux.gtk.amd64.deb 2022-02-23 178.5 MB
0
tla2tools.jar 2022-02-23 2.3 MB
0
README.md 2020-12-30 3.8 kB
0
The Brontinus release.tar.gz 2020-12-30 88.4 MB
0
The Brontinus release.zip 2020-12-30 91.3 MB
0
Totals: 8 Items   899.4 MB 0

Click here to jump to the downloads at the bottom of this page!

Changelog

The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The 1.7.1 milestone lists all completed issues.

Additional noteworthy changes

Tools

Feature
  • Improve some of TLC's error messages. [e328ae]
  • Add TLC!TLCGet("generated") that equals the number of states generated. [fa7663]
  • Prototype: Support multiple TLA+ modules in a single .tla file. [505e07]
  • Programatically stop simulation with TLC!TLCSet("exit", TRUE). [d62b28]
  • Prototype: Add an interactive TLA+ REPL. [97afa3] (Screencast)
  • Drop intermittent stuttering steps from error trace in simulation mode. [cfcfaf]
  • Return non-zero error codes from SANY on more errors. [10f77c]
  • ALIAS. [f5306c]
  • POSTCONDITION. [ced926] e9be5d0fa41ba38879b2e92307853a3ad9855542 [be394f]
  • Prototype: Visualize action coverage in simulation mode. [3d3259] 3913dd181a5cac755acb1577a6503b6f5d443137
  • Report number of and mean/variance/standard deviation of length of generated traces in simulation mode. [d175e3] 7a3bcb0302edfc5b2f720002a8561bc5a8552c47
  • Let users set the maximum number of traces to generate in simulation mode. [a969d5]
Bugfix
  • TLC shows no error trace for violations of TLC!Assert, ... (regression in 1.7.0). [19757b]
  • State graph visualization in dot format broken for specs with instantiation. [a8fc5b]
  • Simulation mode ignores ASSUMPTIONS. https://github.com/tlaplus/tlaplus/issues/496
  • TLC!RandomElement breaks error trace re-construction in simulation mode. [e0d64f]
  • NoClassDefError when running TLC on Java 1.8. [e6bd13]
  • Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort https://github.com/tlaplus/tlaplus/issues/539 [8b52d2]

Toolbox

Feature
  • Open a Toolbox spec, module, or TLC model in the file manager such as Windows Explorer, Finder, or Nautilus.
  • Proof-of-concept: Remove GraphViz dependency by rendering state graph visualization with embedded browser (macOS & Linux only). [478d85]
  • Bundle CommunityModules as part of the Toolbox. [3beb71]
  • Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. [dc6769]
  • Set ALIAS and POSTCONDITION in Toolbox's model editor. [e8054e] d3cfde5a37d943b95a354d40ad60b8bef07411b2
  • Re-worked PlusCal/TLA+ divergence warning (please manually remove 1.7.0 markers). [f1cf51] e434e139adebf73ed8f9470117031f1ad4b749df [7c61d1]
Bugfix
  • Quickly open spec or model in OS file manager. [06280a]
  • Do not enter Spec as next-state relation when restarting model-checking from a state in the error-trace. [7f5002]
  • Multiline trace expressions fail to parse in Toolbox. [defe0c]

Contributors

We are grateful for contributions to this release from: William Schultz, Paulo Rafael Feodrippe, and zmatti.

Checksums

sha1sum file
[9416f7] tla2tools.jar
[85a051] TLAToolbox-1.7.1-linux.gtk.x86_64.zip
[749e30] TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
[c00456] TLAToolbox-1.7.1-win32.win32.x86_64.zip
[2bd88a] TLAToolbox-1.7.1-linux.gtk.amd64.deb
Source: README.md, updated 2020-12-30