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.8.0 milestone lists all completed issues.

Additional noteworthy changes

Tools

Feature

• Improve some of TLC's error messages. e328ae9
• Add TLC!TLCGet("generated") that equals the number of states generated. fa76630
• Prototype: Support multiple TLA+ modules in a single .tla file. 505e073
• Programatically stop simulation with TLC!TLCSet("exit", TRUE). d62b289
• Prototype: Add an interactive TLA+ REPL. 97afa3c (Screencast)
• Drop intermittent stuttering steps from error trace in simulation mode. cfcfafb
• Return non-zero error codes from SANY on more errors. 10f77cf
• ALIAS. f5306c6
• POSTCONDITION. ced9269 e9be5d0 be394f8
• Prototype: Visualize action coverage in simulation mode. 3d3259d 3913dd1
• Report number of and mean/variance/standard deviation of length of generated traces in simulation mode. d175e31 7a3bcb0
• Let users set the maximum number of traces to generate in simulation mode. a969d55

Bugfix

• TLC shows no error trace for violations of TLC!Assert, ... (regression in 1.7.0). 19757bd
• State graph visualization in dot format broken for specs with instantiation. a8fc5b1
• Simulation mode ignores ASSUMPTIONS. #496
• TLC!RandomElement breaks error trace re-construction in simulation mode. e0d64f6
• NoClassDefError when running TLC on Java 1.8. e6bd13e
• Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort #539 8b52d23

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). 478d856
• Bundle CommunityModules as part of the Toolbox. 3beb711
• Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. dc67692
• Set ALIAS and POSTCONDITION in Toolbox's model editor. e8054e8 d3cfde5
• Re-worked PlusCal/TLA+ divergence warning (please manually remove 1.7.0 markers). f1cf514 e434e13 7c61d1a

Bugfix

• Quickly open spec or model in OS file manager. 06280a4
• Do not enter Spec as next-state relation when restarting model-checking from a state in the error-trace. 7f50021
• Multiline trace expressions fail to parse in Toolbox. defe0c7

Contributors

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