Skip to content

The Brontinus release

Choose a tag to compare
@lemmy lemmy released this 23 Feb 00:16
· 575 commits to master since this release

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


The high level changelog is available at The 1.7.1 milestone lists all completed issues.

Additional noteworthy changes


  • 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
  • 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


  • 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
  • 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


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


sha1sum file
9416f74257aa50f250776db34964db7ec99e9883 tla2tools.jar
2bd88a866a8374b44cdc2c3e62260e388316552f TLAToolbox-1.7.1-linux.gtk.amd64.deb