Softpedia >Windows >Programming >Other Programming Files >TLA Toolbox >  Changelog

TLA Toolbox Changelog

What's new in TLA Toolbox 1.8.0 Pre-release

Oct 24, 2021
  • Tools:
  • Feature:
  • Improve some of TLC's error messages.
  • Add TLC!TLCGet("generated") that equals the number of states generated.
  • Prototype: Support multiple TLA+ modules in a single .tla file.
  • Programatically stop simulation with TLC!TLCSet("exit", TRUE).
  • Prototype: Add an interactive TLA+ REPL. 97afa3c (Screencast)
  • Drop intermittent stuttering steps from error trace in simulation mode.
  • Return non-zero error codes from SANY on more errors.
  • ALIAS.
  • POSTCONDITION.
  • Prototype: Visualize action coverage in simulation mode.
  • Report number of and mean/variance/standard deviation of length of generated traces in simulation mode.
  • Let users set the maximum number of traces to generate in simulation mode.
  • Bugfix:
  • TLC shows no error trace for violations of TLC!Assert, ... (regression in 1.7.0).
  • State graph visualization in dot format broken for specs with instantiation.
  • Simulation mode ignores ASSUMPTIONS.
  • TLC!RandomElement breaks error trace re-construction in simulation mode.
  • NoClassDefError when running TLC on Java 1.8.
  • Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort
  • 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).
  • Bundle CommunityModules as part of the Toolbox.
  • Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support.
  • Set ALIAS and POSTCONDITION in Toolbox's model editor.
  • Re-worked PlusCal/TLA+ divergence warning (please manually remove 1.7.0 markers).
  • Bugfix:
  • Quickly open spec or model in OS file manager.
  • Do not enter Spec as next-state relation when restarting model-checking from a state in the error-trace.
  • Multiline trace expressions fail to parse in Toolbox.

New in TLA Toolbox 1.7.1 (Oct 24, 2021)

  • Re-worked PlusCal/TLA+ divergence warning (please manually remove 1.7.0 markers, i.e. everything on the line following * BEGIN TRANSLATION).
  • TLC shows no error trace for violations of TLC!Assert, ...
  • NoClassDefError when running TLC on Java 1.8.
  • Dot visualization (graphviz) fails due to invalid character ! when spec uses instantiation
  • Simulation mode ignores ASSUMPTIONS.
  • Back to state missing for lasso error trace found by simulation
  • AtNode does not show up in (dot) graph output of semantic explorer
  • Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort
  • End support for liveness checking and multiple workers in DFID mode because both features are unreliable
  • Multiline trace expressions fail to parse in Toolbox.
  • Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support.
  • Toolbox intermittently shows no error trace on an invariant violation

New in TLA Toolbox 1.5.6 (Jan 30, 2018)

  • Corrects TLC bug
  • Fixes a bug in the Toolbox's update mechanism that would cause it to make TLC impossible to run.
  • Fixes a TLC bug that caused it to stop with an integer overflow exception after many hours of model checking.

New in TLA Toolbox 1.5.5 (Jan 9, 2018)

  • Fixes a TLC bug

New in TLA Toolbox 1.5.3 (Apr 20, 2017)

  • Bug fixes include eliminating incorrect error traces in TLC liveness checking.
  • Execution by multiple worker threads in TLC has been speeded up.
  • The Toolbox can now be set as the default program for running .tla files.
  • The built-in PDF viewer is now the default on Windows and Linux.
  • TLC can be run on multiple EC2 or Azure instances by button pushing.
  • An apt repository is provided for Linux installations.

New in TLA Toolbox 1.5.2 (Jul 27, 2016)

  • Added a quick access dialog for showing and selecting models and modules.
  • The toolbox now maintains backups of previous versions of modules.
  • Models now have a field for free-form comments.
  • Only one Toolbox instance can now be run at a time.
  • A -userFile parameter allows redirecting Print/PrintT output to a file.
  • Not all states of very long error traces are displayed initially.
  • Ended support for 32-bit Toolbox releases on Mac OSX.
  • Several optimizations and bug fixes were made.

New in TLA Toolbox 1.5.1 (Jul 27, 2016)

  • Fixes several bugs in TLC and a bug in the Toolbox's trace explorer.

New in TLA Toolbox 1.5.0 (May 13, 2015)

  • Distributed TLC in the Cloud--significantly improves distributed TLC.
  • Significantly speeds ups TLC's liveness checking.
  • Improvements to the Decompose Proof Command.
  • Improvements to the TLC Errors view, including ability to show trace in reverse order.
  • Fixes all known bugs in TLC's liveness checking.
  • Fixes TLC bug of infinite loop if a recursively defined operator is used as an operator argument in its own definition.
  • Numerous bug fixes.

New in TLA Toolbox 1.4.8 (Jan 12, 2015)

  • Added a feature to Renumber Proof command.
  • Disallowed and in names of named proof steps.
  • Minor bug fixes to Toolbox and TLC.
  • Corrected definition of Tail in standard Sequences Module.

New in TLA Toolbox 1.4.7 (Jan 12, 2015)

  • Fixes bugs in the Toolbox's Decompose Proof command

New in TLA Toolbox 1.4.6 (Jan 12, 2015)

  • Fixes bug in PlusCal translation of fairness for algorithms with procedures.
  • Adds handling of strings to TLC's implementation of Tail and SubSeq.
  • Fixes a minor TLATeX bug.

New in TLA Toolbox 1.4.5 (Jan 12, 2015)

  • The Decompose Proof Command has been added to the Toolbox editor.
  • It makes it easy to perform the standard hierarchical decompositions of a proof based on the structure of the formula to be proved.
  • A few minor bugs have been fixed.

New in TLA Toolbox 1.4.4 (Jan 12, 2015)

  • There have been numberous changes to distributed TLC and how to run it.
  • Syntax coloring of PlusCal algorithms was added.
  • TLATeX now formats PlusCal algorithms.
  • Support for library folders required by Version 1.1.1 of TLAPS has been added.
  • Version 1.4.3.c of 24 May 2012
  • Version 1.4.3.b of 24 April 2012
  • Version 1.4.3.a of 17 April 2012
  • These are intermediate versions that contain the current version of TLAPS.tla and fix mostly minor bugs.
  • Version 1.4.3.c fixes a bug that can cause an updated version of the Toolbox to use an earlier version of TLC.
  • The latest version is available only by updating. (Select Check for Updates on the Toolbox's Help menu.)

New in TLA Toolbox 1.4.3 (Jan 12, 2015)

  • Adds a "Cardinality of largest enumerable set" TLC parameter.
  • Fixed the order of definitions and declarations in the MC.tla file.
  • Includes TLC version 2.05 of 7 April 2012, which adds the TLCEval operator to the TLC module.
  • Includes PlusCal Verion 1.8 of 30 March 2012.

New in TLA Toolbox 1.4.2 (Jan 12, 2015)

  • Selecting a location in an error report and control-clicking jumps to its source in PlusCal code.
  • Supports library folders (directories) for modules used in multiple specs.
  • Provides a built-in pdf viewer that can be used for viewing pretty-printed modules.

New in TLA Toolbox 1.4.1 (Jan 12, 2015)

  • Contains a new editor command for jumping from a region in the TLA+ translation of a PlusCal algorithm to the region of PlusCal code that generated it.
  • Introduces some additional editor commands, including one for parenthesis matching.
  • Fixes a number of bugs, including ones that occurred when TLC checked large models.

New in TLA Toolbox 1.4.0 (Jan 12, 2015)

  • Includes a method for obtaining new releases from inside the Toolbox.
  • Includes PlusCal Version 1.6, which:
  • Slightly changes the syntax for specifying fairness.
  • Permits using previously declared macros in a macro definition.
  • Added the Forget Specification command.
  • Includes a first release of the distributed version of TLC.
  • Includes a fix to SANY to support binary, octal, and hex numbers.
  • Added default overriding of definitions like Foo == CHOOSE v : v \notin S.
  • Definition overriding section of advanced model page now opens if there are overrides.
  • Fixed a TLC bug in overriding instantiated definitions.
  • Displays timeout as a reason for prover failure.

New in TLA Toolbox 1.3.1 (Jan 12, 2015)

  • Includes PlusCal Version 1.5, which adds:
  • Fairness specifation in a PlusCal algorithm.
  • Translation simplifications, including omission of the pc variable when not needed.
  • Contains a number of minor bug fixes.