TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
The Ulpian release is based on the 1.7.3 branch and fixes the issue below.
| sha1sum | file |
|---|---|
| 756b878250f2f2a1a2f6ede3382a8e4398c1540e | tla2tools.jar |
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.
TLC!TLCGet("generated") that equals the number of states generated. fa766305094b698eab3338ed917bd1c8b4542039TLC!TLCSet("exit", TRUE). d62b289af42edb2026cda423cc56bb0fe8477b52TLC!Assert, ... (regression in 1.7.0). 19757bdd6aadf7c0e371c40bf591f0d84f12a592TLC!RandomElement breaks error trace re-construction in simulation mode. e0d64f686dae1aec22728b1acfa40b1a554a7267ALIAS and POSTCONDITION in Toolbox's model editor. e8054e8eb913bc87c336882c7c6e1f8565ada1e9 d3cfde5a37d943b95a354d40ad60b8bef07411b2Spec as next-state relation when restarting model-checking from a state in the error-trace. 7f50021048155a3d085d5d482eede37f09fbf9e5We are grateful for contributions to this release from: William Schultz, Paulo Rafael Feodrippe, and zmatti.
| sha1sum | file |
|---|---|
| 9416f74257aa50f250776db34964db7ec99e9883 | tla2tools.jar |
| 85a0519fa7197bbad694079a93fba6254bd7267a | TLAToolbox-1.7.1-linux.gtk.x86_64.zip |
| 749e30b68418f7f206ff46fc61e7cc10ec24d9cf | TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip |
| c004561e404743fbb83608229380223a1207a8ec | TLAToolbox-1.7.1-win32.win32.x86_64.zip |
| 2bd88a866a8374b44cdc2c3e62260e388316552f | TLAToolbox-1.7.1-linux.gtk.amd64.deb |
The Theano release is based on the 1.7.1 branch and fixes the following two issues:
We are grateful for contributions from Calvin Loncaric and Dmitry Kulagin.
| sha1sum | file |
|---|---|
| 7f21faa2cdae3189e7d5fadb4488f0dfcc658407 | tla2tools.jar |
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.
TLC!TLCGet("generated") that equals the number of states generated. fa766305094b698eab3338ed917bd1c8b4542039TLC!TLCSet("exit", TRUE). d62b289af42edb2026cda423cc56bb0fe8477b52TLC!Assert, ... (regression in 1.7.0). 19757bdd6aadf7c0e371c40bf591f0d84f12a592TLC!RandomElement breaks error trace re-construction in simulation mode. e0d64f686dae1aec22728b1acfa40b1a554a7267ALIAS and POSTCONDITION in Toolbox's model editor. e8054e8eb913bc87c336882c7c6e1f8565ada1e9 d3cfde5a37d943b95a354d40ad60b8bef07411b2Spec as next-state relation when restarting model-checking from a state in the error-trace. 7f50021048155a3d085d5d482eede37f09fbf9e5We are grateful for contributions to this release from: William Schultz, Paulo Rafael Feodrippe, and zmatti.
| sha1sum | file |
|---|---|
| 05b26d1ea827e29201db8af10ff752c76cf4b199 | tla2tools.jar |
| 44ef5267f491c56b1493b5f382075f42503097ee | TLAToolbox-1.8.0-win32.win32.x86_64.zip |
| 338c12bbe06f7816a773984030b2dacaeb60bd0f | TLAToolbox-1.8.0-linux.gtk.x86_64.zip |
| TBD | macOS |
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.
TLCGet("level") in simulation mode. 9652a452d7c27590afdb6f8fd8f9431a01d6a71d-continue mode is combined with -workers >1. d5b5a7fa9f5ccdb78edbe2b286ca08ea9b42dc73-h now displays a usage/help page (Screenshot)
-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.
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.
nomonolith after the -generateSpecTE
SpecTE.tla and SpecTE.cfg file pair - this will not be a monolithic version.SpecTE.tla and SpecTE.cfg file pair if one doesn't existTE.tla and TE.cfg file pair which extends SpecTE and contains appropriate conjunctions featuring the expressionsTE.out and dumping the tool-mode output to stdouttlc2.TraceExplorer with no arguments, or -h will display helpful usage verbiageGeneral → Appearance.TLA+ Preferences → TLC Model Checker to TLA+ Preferences → Model Editor.TLA+ Preferences → TLAPS preference subtree has been altered:
TLA+ Preferences → TLAPS is now at TLA+ Preferences → TLAPS → Color Predicates.TLA+ Preferences → TLAPS → Additional Preferences is now renamed to TLA+ Preferences → TLAPS → Other Preferences.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.TLA+ Preferences → PDF Viewer.dot executable, prior to letting GraphViz attempt to find it.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.')\*)\** END TRANSLATION TLA-9b285153d0358878d62b88c9d4a6a047 → \** END TRANSLATION.) You will still be warned if the PlusCal code content is found to have changed without re-translating.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.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
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.We are grateful for contributions to this release from: Loki der Quaeler, Denys Dushyn, Calvin Loncaric, William Schultz, Jay Lee, and Andrew Helwer.
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.
| 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 |
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.
A /\ B /\ C in given order instead of A /\ C /\ B eb5d554d405d891fdc98cc448184df50ee7e2e242^15 states on-disk or 2^31 in-memory 28a0117c5038bf0470841498fe8987275bc790bbfp parameter)RandomElement operator from TLC's standard module(diameter, states, distinct states, runtime, level, exit) through named registers for TLCGet and TLCSet 592056f265db02ba47c51ec30191b15c0203cd01 43e2b745537726bb0b4f8ad75d52cec6edd5f1d0
java [-Dtla2sany.explorer.DotExplorerVisitor.includeLineNumbers=true] -cp /path/to/tla2tools.jar tla2sany.SANY -d Spec.tla dot Screenshot
java -cp /path/to/tla2tools.jar tlc2.tool.management.StateMonitor [interval] 9ddffad5f5e1adb44195010560d85f20c4f40532 b4834400e0af29f384af1ce06da2f2a58c221492 (Screencast)
1E-10 f12b10e796f775c10b764b3c0afdde0bcc328620-Dtlc2.tool.ModelChecker.BAQueue=true Java system propertytla2tools.jar to simplify command-line on Linux: /path/to/tla2tools.jar /path/to/spec
-XX:+UseParallelGC Java 11 flag to not suffer performance penalty
power_off to speed-up subsequent restart 22a7385453497e19828642287e0b1c1d929db2ac
TLA+ Preferences → TLC Model Checker.
TLC Model Checker → Clone Model → Foreign Model... menu item.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.
| 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) |
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.
BagUnion({b,b}) produces incorrect b (+) b as result bc0f7dbf89a703a5899689b98232f1fe0224191832 bit (x86) variants of the TLA Toolbox have been discontinued with this release. fb680446557e92229a059ef9f93fd48a29c5bb2f
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.
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')
/\ ...
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 bit (x86) variants of the TLA Toolbox can be downloaded from our alternative download site.
| 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 |
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
/\ ...
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 bit (x86) variants of the TLA Toolbox can be downloaded from our alternative download site.
| 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 |
Version 1.4.8 of 25 February 2014