Skip to content
Compare
Choose a tag to compare

The Clarke release

Pre-release
Pre-release

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.

Checksums

sha1sum file
f7e707ffe3b68b339b3002a57053c9688d965b6a tla2tools.jar
184015cf66b1005915b65d761398dda725f976e6 TLAToolbox-1.8.0-win32.win32.x86_64.zip
892a9fdb1455ceab32155bfb33010be0f88ccf13 TLAToolbox-1.8.0-linux.gtk.x86_64.zip
TBD macOS
Compare
Choose a tag to compare

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:

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

Checksums

sha1sum file
9416f74257aa50f250776db34964db7ec99e9883 tla2tools.jar
c004561e404743fbb83608229380223a1207a8ec TLAToolbox-1.7.1-win32.win32.x86_64.zip
85a0519fa7197bbad694079a93fba6254bd7267a TLAToolbox-1.7.1-linux.gtk.x86_64.zip
749e30b68418f7f206ff46fc61e7cc10ec24d9cf TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
Compare
Choose a tag to compare

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

Changelog 04/26/2020

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

Additional noteworthy changes

TLC

Bugfix
  • Errors that occurred during liveness checking did not terminate TLC which could lead to a user incorrectly assuming that the specification had satisfied the liveness properties. db26953
  • A race condition in parallel TLC could potentially result in bogus counterexamples or incomplete state space explorations.
  • Absolute file paths on Windows were not working correctly when specifying file locations.
  • Fixed TLCGet("level") in simulation mode. 9652a45
  • Fix crash when -continue mode is combined with -workers >1. d5b5a7f
Feature
  • Running TLC with -h now displays a usage/help page (Screenshot)
  • Setting "-workers auto" automatically detects available parallelism. 4111431
  • Define deadlock checking in model config file. 6b4ed51
  • Evaluate trace expressions on the command-line (Screencast).
    • Running TLC with both the -generateSpecTE flag will enable 'tool mode' output and, in the event that the model check encounters errors, generate a SpecTE.tla and SpecTE.cfg file pair that captures
      the state trace reconstruction in an Init-Next relation spec.
      • This SpecTE.tla will, by default, be a monolithic file, prefaced by the tool output, followed a the SpecTE MODULE definition which includes all extended non-StandardModule TLA code as well.
        • To prevent the monolith inclusion of dependent TLA code, specify nomonolith after the -generateSpecTE
    • TraceExplorer exposes four capabilities:
      • running the TraceExplorer with no spec name puts the TraceExplorer into a mode to receive input via stdin (e.g in order to pipe tool-mode output from TLC)
      • pretty-printing: given an existing tool-mode output from a previous model check run (or piping in such output), pretty-printing will display an output stack to the terminal in basically the same format as one would see in the Toolbox's Error Viewer
      • SpecTE generation: given an existing tool-mode output from a previous model check run (or piping in such output), create a SpecTE.tla and SpecTE.cfg file pair - this will not be a monolithic version.
      • Expression exploration: given an existing tool-mode output from a previous model check run (or piping in such output), and file of expressions, one per line:
        • create a SpecTE.tla and SpecTE.cfg file pair if one doesn't exist
        • then create a TE.tla and TE.cfg file pair which extends SpecTE and contains appropriate conjunctions featuring the expressions
        • then run model checking on this TE spec, both creating a TE.out and dumping the tool-mode output to stdout
        • then do a courtesy pretty-print of the output. Pretty-printing in this scenario will ANSI-bold the expressions and their evaluated values
      • Single expression exploration: as a sort of REPL-adjacent, any single TLA+ expression can be evaluated.
      • running tlc2.TraceExplorer with no arguments, or -h will display helpful usage verbiage
  • CloudTLC may now be run in simulation mode. ab64adf
  • Error messages have been improved for bogus symmetry sets.
  • Error messages have been improved when temporal existential and/or temporal universal quantification is used in a specification.
  • Annotation-based loading of TLC module overrides (Java) for TLA+ operators. eb42f9e
  • More powerful TLC module overrides to programmatically (Java) manipulate successor states. bb64cfd
  • Write snapshots of state graph in dot/gv format after every new state. 305f38b (Screencast)
  • Action names are now printed in error traces emitted in simulation mode. c0180ea
  • Performance has been improved when creating a profiler tree with large specs. b7f9282

Toolbox

  • The Toolbox now ships with AdoptOpenJDK version 14. e7ca63b
Preferences
  • The Toolbox comes with a Dark theme via General → Appearance.
  • The "Show Evaluate Constant Expression in its own tab" preference has been moved from TLA+ Preferences → TLC Model Checker to TLA+ Preferences → Model Editor.
  • The TLA+ Preferences → TLAPS preference subtree has been altered:
    • the previous page at TLA+ Preferences → TLAPS is now at TLA+ Preferences → TLAPS → Color Predicates.
    • The page previously at TLA+ Preferences → TLAPS → Additional Preferences is now renamed to TLA+ Preferences → TLAPS → Other Preferences.
    • Non-color-predicate-related preferences from TLA+ Preferences → TLAPS → Additional Preferences have been moved into TLA+ Preferences → TLAPS.
    • TLA+ Preferences → TLAPS now also features the ability to set a file system location for the tlapm executable should the Toolbox not be able to find it.
  • On macOS, you can now set the preference to have the operating system open PDFs with your default PDF viewer via TLA+ Preferences → PDF Viewer.
  • We attempt to locate the dot executable, prior to letting GraphViz attempt to find it.
Spec Editor
  • The spec editor now allows the collapsing of block comments, PlusCal code, and the TLA+ translation of PlusCal code. The first line of each of these types of runs should feature a minus icon in the line number gutter. Clicking on this icon will collapse the run; while in a collapsed state, holding the mouse over the, now: plus, icon will show the collapsed text as a tooltip.
    • Please review the help page for the PlusCal translator in the Toolbox for guidance
      as to how the comment block surround the PlusCal algorithm should be written.
    • The preferences pane found at TLA+ Preferences → Module Editor allows for the setting of the default folding preferences (e.g 'always fold block comments when opening a specification in the editor.')
  • The spec editor also allows the collapsing of a contiguous run of two or more single line comments (where a single line comment is defined as a line starting with 0 or more spaces and or tabs, followed by a \*)
  • The translation of PlusCal code now generates a checksum of this code and the resulting TLA+ code; this checksum is calculated again when a model is executed and if it has changed, either a warning dialog will be displayed (if executed via the Toolbox) or a log warning will be emitted (if TLC is executed on the command line.)
    • If you make a change to the generated TLA+ code, but do not want to be warned by the Toolbox of the divergence, you can delete only the TLA checksum (e.g \** END TRANSLATION TLA-9b285153d0358878d62b88c9d4a6a047\** END TRANSLATION.) You will still be warned if the PlusCal code content is found to have changed without re-translating.
  • If attempting to generate a PDF of a spec fails because the pdflatex executable could not be found, a more informative warning dialog is now displayed for the user, including a way to directly open the Toolbox preference page specifying executable location.
  • The ability to use the prover against a spec will now be disabled while the spec fails to be successfully parsed.
Model Editor
  • The style of the display of definitions in the "Definition Override" section in the Spec Options tab can be defined in the TLA+ Preferences → Model Editor preferences. There are two styles currently; given a Definition from a Module Name referenced in the primary spec like InstanceName == INSTANCE ModuleName WITH ..., then the two available styles are:
    • Definition [Module Name]
    • InstanceName!Definition
  • The Initial predicate / Next-state text areas were no longer interpreting a TAB as 'advance focus' due to a regression introduced when we moved to multi-line support for these text areas in 1.6.0. Both text areas now interpret a TAB as a focus advance; a TAB in the 'Init:' text area moves focus to the 'Next:' text area and a TAB in that text area advances the focus to the 'What is the model?' section.
  • New models now open a Model Editor instance with only a single tab - the Model Overview page. Running the model will open the Results tab, or should the user want to work immediately with evaluating constant expressions, there is a link at the bottom of the Model Overview page which will open the Results tab (as well as the Constant Expressions tab should the user have configured their preferences to show this in its own tab.)
  • Warn when checking liveness under action or state constraints (see Specifying Systems section 14.3.5 on page 247 for details).
  • Console output from model checking now has the TLC tool marker markup removed.
Spec Explorer
  • Right-clicking on model snapshots was incorrectly presenting the choice to rename the snapshot; this has been corrected.
  • Renaming specifications now correctly cleans up after itself and should no longer prevent models from being opened.
  • Previously, opening a spec while the current spec had a dirty editor open, and to which the user chose to Cancel the offer to save the dirtied editor, resulted in the Toolbox continuing to open the new spec. This has been fixed - the opening process is halted and the original spec remains open.
  • Deleting a spec which has a currently dirty editor open for it, in which the user Cancel-s out of the dialog warning that the user is closing a dirty editor and asking whether they want to Don't Save, or Cancel, or Save, was continuing with the deletion of the spec. It now stops the deletion process.
Trace Explorer
  • The Error-Trace can now be filtered to omit one or more variables and/or expressions. Clicking on the filter icon, when filtering is not on, will display a dialog allowing the user to select from the set of variables and expressions found in the trace; alternatively, the user may ALT-click on a variable or expression in the Error-Trace tree view which will then omit that variable or expression. (Screencast)
    • Also provided in the Error-Trace filtering dialog is the ability to hide variables whose values have not changed. For a variable that has changed at sometime during the trace, it may be displayed in either only the frames in which its value has changed, or in every frame of the trace. (Screencast)
    • While filtering is enabled, a checkbox will be displayed above the variable value viewing text area allowing this area to display all the variables, or only the filtered variables, when a state is selected in the Error-Trace tree.
  • Allow Trace-Explorer to extend additional TLA+ modules (Screencast)
  • Export Error-Trace to system's clipboard (Screencast)
  • Model checking can now be started using any given frame shown in the Error-Trace. Right-clicking on any location row will display a context menu giving the user the opportunity to run the model checking starting at that state. (Screencast)

Running checking in Ad Hoc mode

  • We have ended support for launching workers via JNLP; more information can be found on the master server's web page when running in this mode (e.g http://localhost:10996)

Contributors

We are grateful for contributions to this release from: Loki der Quaeler, Denys Dushyn, Calvin Loncaric, William Schultz, Jay Lee, and Andrew Helwer.

A note to macOS users

Startup on macOS version 10.14 (Mojave) onward might fail with "TLA+ Toolbox can't be opened because Apple cannot check it for malicious software.". Please make sure to follow the instructions outlined in GitHub issue #320 to address this problem.

Checksums

sha1sum file
0c78a97204c376cef3051816aa4125785b973b47 tla2tools.jar
fadc7dbc3e8c679a3ab600038654262c0cc69aa0 TLAToolbox-1.7.0-win32.win32.x86_64.zip
46a46c7035551efaba2f7872b43b59f526343095 TLAToolbox-1.7.0-linux.gtk.x86_64.zip
b44ae6b693147db58f0e13d0d4ec8371f60c3ea4 TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip
Compare
Choose a tag to compare

Changelog

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

Additional noteworthy changes

TLC Profiler

TLC

Performance & Scalability
  • Multi-Threaded Simulation Mode 8355920 Contributor: will62794
  • More efficiently generate the set of subsets for the TLA+ expression (SUBSET S) 4a62e5b
  • Reduce worker contention by separating the trace file into N partial trace files where N is the number of workers 548ce71
  • Speed-up TLC shutdown by calculating 'actual fingerprint collision probability' only if 'calculated probability' exceeds 1E-10 f12b10e
  • Increase TLC throughput by ~10% by refactoring hot code-paths e6c8f6c 1bc2ab1
  • Show active fingerprint set and state queue implementation in startup banner e974533 ea3feb5
  • ByteArrayQueue prototype to increases throughput by reducing the critical section of the queue of unseen states 01b0e98
    • Activate with -Dtlc2.tool.ModelChecker.BAQueue=true Java system property
Command-line
CloudTLC
  • Switch to Azure service principal authentication
    • Automatically handle Azure resource deletion as part of instance termination 5be0e77
  • Gracefully terminate cloud resources when a CloudTLC run is terminated prematurely d593d0e
  • Power-off instead of terminate CloudTLC instances tagged power_off to speed-up subsequent restart 22a7385
  • Adds support for packet.net's t1.small.x86 budget baremetal instances 71a2530

Toolbox

Model Editor
  • Better visualize coverage by coloring the editor 881f2e6
  • Usability improvements to the model editor including:
    • What was previously the "Advanced Options" page has been split into two pages with the Advanced TLC Options occupying its own page now.
      • Neither of these pages are visible by default, and are accessed by hyperlink on the main model page; their open-or-closed state are saved with the model so that subsequent model openings will restore the view to the configuration last seen by the user.
    • The selection of the behavior spec is now performed via pulldown, as seen in this accompanying screencast..
    • The "How to run?" section of the main page has been simplified, as can be seen in the same screencast as above. Checkpoint related TLC options have been moved to the Advanced TLC Options page. A given worker, memory, and disk storage file count configuration can be saved as the default configuration to be used with new models.
    • Init and Next fields of the "What is the Behavior Spec" accept multi-line expressions
    • The "How to run" and the "What to check?" sections on the main page have been given full width of the page.
    • Similarly, the "State Constraint" section on the "Advance Options" page have been given full width.
    • The tables in the "Statistics" section of the "Model Checking Results" page now expand to fill the width of the page, and resize their columns to consume the available width when those tables resize.
    • The "General" section of the "Model Checking Results" page has been condensed to two lines. The top line, always visible, will show:
      • an "Awaiting..." text for an un-executed model.
      • once running, or ran, a Start time, an End time, a status, and potentially a last checkpoint time, and a mode denotation for Depth-first or Simulation runs.
    • ... and the second line will be visible should their be errors in execution, information about fingerprint collision, and/or zero counts on coverage.
    • The Evaluate Constant Expression section in the Results page can be moved to its own tab in the model editor via a preference checkbox in TLA+ Preferences → TLC Model Checker.
    • The Evaluate Constant Expression now features a toggle button to more easily jump in and out of Evaluate Constant model check mode (No behavior spec selected.)
TLA+ editor
Spec Explorer
Trace Explorer
  • TETrace operator to support self-referential error trace expression
  • Supporting naming to compose trace expressions a34ef2c (Screencast)
  • Map SANY errors back to Toolbox expression locations 9ae65ab (Screenshot)
  • Add syntax highlighting and redo/undo in input boxes
  • Allow customizable fonts for the Toolbox's Error Trace viewer
  • Add header button to error trace to toggle tree expansion between collapse and expand all. Shift+Click returns to default two-level expansion 8640936 (Screencast)
  • The edit button is enabled if the table contains one formula, regardless of whether that formula is selected; formulas are able to be drag reordered; changes (addition, editing, removal, and reordering) are now saved automatically. (All covered by Issue #9)
  • There is a button in the Error-Trace section header which allows the 'linking' of the trace viewer with the spec editor; in the same way that one could previously double-click on a trace location to reveal the section of the specification in the spec editor, while the editor is linked this action can be done by a single click, as well as by navigating with the keyboard arrow keys. (Issue #289)
Misc

A note to macOS users

Startup on macOS version 10.14 (Mojave) will fail with "TLA+ Toolbox can't be opened because Apple cannot check it for malicious software.". Please make sure to follow the instructions outlined in GitHub issue #320 to address this problem.

Checksums

sha1sum file
b0fca8d26568c5304b5e4d5ab40f3ffe1ed48ba1 TLAToolbox-1.6.0-linux.gtk.x86_64.zip
836c91cddf98088f7e2c8c2f711e95217d5530da TLAToolbox-1.6.0-macosx.cocoa.x86_64.zip
ae09753744f462957709d94d735ef292e775a05b TLAToolbox-1.6.0-win32.win32.x86_64.zip
aa4876bb4ae1275eb157fe67322fa69fd7452b7a tla2tools.jar
d54307de60caf42e586b06d84994ec9cfcee0675 repository.zip (most of you don't want this)
Compare
Choose a tag to compare

Changelog

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

Additional noteworthy changes

TLC

  • Reword and complete comments of TLA+ standard modules d2f54a1
  • IsABag inconsistent with Bags.tla when parameter is not a bag 5d15bde
  • BagsUnion operator of TLA+ standard module for BagUnion({b,b}) produces incorrect b (+) b as result bc0f7db
  • Correctly handle sequences as input to Bags operators
  • Provisional Randomization standard module
  • tlc2.Generator refactored into tlc2.TLC 6141aed
  • Correctly recreate error trace in BFS mode with RandomElement 3a618d7
  • Minimize the number of duplicate states that are generated as part of the initial predicate f3a98ce
  • Minimize the number of duplicate states that are generated as part of the next-state predicate fba4319
  • Indicate name of action which does not completely specified the successor state fddcdd4
  • Speed-up Cloud TLC by skipping instance provisioning 2bc2488
  • Colorize and label actions (arcs) in state graph visualization 7e80f1d (Screenshot) Contributor: will62794
  • Fix broken error traces with views 5a62945

PlusCal

  • Allow no intervening label between call and goto in PlusCal 188e1fd

Specification Editor

  • Show errors in PlusCal algorithm for assignments to undeclared variables 1e3f8fa
  • Editor command "Goto declaration" now also goes to declarations of TLA+ standard modules 103204a (Screencast)
  • Mouse hover help shows BNF and help for PlusCal statements dbeafb6
  • Show operation definition and comment in mouse hover help ad36f39
  • Code completion for PlusCal statements triggered by Ctrl+Space 13c772f (Screencast)
  • Code completion for operator definitions and declarations triggered by Ctrl+Space c31c2bd (Screencast)
  • Automatically transpile PlusCal to TLA+ on editor save 642b540 (Screencast)

Model Editor

  • Collapse, disable and annotate "Generals" and "Statistics" sections with "No behavior spec" 43d207d
  • Add undo and redo support to constant expression source viewer ff03c66
  • Add TLA+ syntax highlighting to constant expression source viewer fd93b56
  • Report the number of initial states as first item reported in the ResultPage's statistic table (with diameter of 0) 076f0c7
  • Show output/progress of remotely running Cloud TLC in Toolbox 593fc82

Misc

32 bits

32 bit (x86) variants of the TLA Toolbox have been discontinued with this release. fb68044

A note to Java 11 users (mostly macOS)

Please consider downloading a recent Toolbox nightly build (1.6.0) instead of the Toolbox 1.5.7 release below. The nightly builds do not suffer from a startup crash when the system Java VM is newer than Java10.

Compare
Choose a tag to compare

Important bugfix

An uncommon but serious bug in TLC has been found that has existed since its initial implementation. The bug can cause TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either can cause TLC not to examine all reachable states. The error can occur in the following two cases:

The possible initial values of some variable var are specified by a subformula F(..., var, ...) in the initial predicate, for some operator F such that expanding the definition of F results in a formula containing more than one occurrence of var, not all occurring in separate disjuncts of that formula.

The possible next values of some variable var are specified by a subformula F(..., var', ...) in the next-state relation, for some operator F such that expanding the definition of F results in a formula containing more than one occurrence of var' , not all occurring in separate disjuncts of that formula.

An example of the first case is an initial predicate Init defined as follows:

VARIABLES x, ...
  
F(var) == \/ var \in 0..99 /\ var % 2 = 0
          \/ var = -1
   
Init == /\ F(x)
        /\ ...

The error would not appear if F were defined by:

F(var) == \/ var \in {i \in 0..99 : i % 2 = 0}
          \/ var = -1

or if the definition of F(x) were expanded in Init :

Init == /\ \/ x \in 0..99 /\ x % 2 = 0
           \/ x = -1
        /\ ...

A similar example holds for case 2 with the same operator F and the next-state formula

Next == /\ F(x')
        /\ ...

Additional noteworthy changes

Changelog

The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The 1.5.6 milestone lists all completed issues. Github has a more technical changelog listing all commits.

32 bits

32 bit (x86) variants of the TLA Toolbox can be downloaded from our alternative download site.

Checksums

sha1sum file
11272c4874866447fc1da9729ce700322e086c9a TLAToolbox-1.5.6-linux.gtk.x86_64.zip
91ed75dc1df01dd668a97a9aa614f2173e927f51 TLAToolbox-1.5.6-macosx.cocoa.x86_64.zip
5b0b955a832bdf0a334a3ca2e9104dd7a52d9aad TLAToolbox-1.5.6-win32.win32.x86_64.zip
aca06efe0d766b8d43b0288d083995fdc150c3e4 tla.zip
Compare
Choose a tag to compare

This release does not completely address the important bug discussed below

Important bugfix

This release fixes a rare but serious bug that has been in TLC since its initial implementation. TLC could generate an incorrect set of initial states, and hence not examine all reachable states, in the following situation:

The possible initial values of some variable var are specified by a subformula: F(..., var , ...) in the initial predicate, for some operator F such that expanding the definition of F results in a formula containing more than one occurrence of var, not all occurring in separate disjuncts of that formula. An example is an initial predicate Init defined as follows:

VARIABLES x, ...

F(var) == \/ var \in 0..99 /\ var % 2 = 0
          \/ var = -1

Init == /\ F(x)
        /\ ...

The error would not appear if F were defined by

F(var) == \/ var \in {i \in 0..99 : i % 2 = 0}
          \/ var = -1

or if the definition of F(x) were expanded in Init:

Init == /\ \/ var \in 0..99 /\ var % 2 = 0
           \/ var = -1
        /\ ...

Additional noteworthy changes

Changelog

The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The 1.5.5 milestone lists all completed issues. Github has a more technical changelog listing all commits..

32 bits

32 bit (x86) variants of the TLA Toolbox can be downloaded from our alternative download site.

Checksums

sha1sum file
81c2981a0e22fe05e0eac0082625ab863acb9412 TLAToolbox-1.5.5-linux.gtk.x86_64.zip
5ad052e969fc1fbf1e1df964b4aed6c7a2c0c470 TLAToolbox-1.5.5-macosx.cocoa.x86_64.zip
4ace976a1f579b8f9e4c60e516e1142016d2352e TLAToolbox-1.5.5-win32.win32.x86_64.zip
11d7be0ad0b51fe7fbbfe8d4ac78c22cd01d1b68 tla.zip
Compare
Choose a tag to compare

http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release or click here for a more technical changelog

32 bit (x86) variants of the TLA Toolbox can be downloaded from our alternative download site.

sha1sum/shasum:
1ba8ddff282e0d1f31edaf57221a0da1f0e54d32 tla.zip
8c04794d897bf1d1f1c7d5a72db2216aabbca47c TLAToolbox-1.5.4-linux.gtk.x86_64.zip
1510d0d63e93b2436b301facd7f62b58853c8b80 TLAToolbox-1.5.4-macosx.cocoa.x86_64.zip
f75905000593269a94a9b3b0aa2d3570c95ddba2 TLAToolbox-1.5.4-win32.win32.x86_64.zip

Compare
Choose a tag to compare

Version 1.5.2 of 21 December 2015

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