Skip to content

Releases: tlaplus/tlaplus

The Clarke release

06 Dec 22:02
@lemmy lemmy
v1.8.0
72c23c9
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.
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
59476d5172ed6a06588e595090ae4971898e634d tla2tools.jar
5312580ab22b201ec9e4afe029edb09ed60d981a TLAToolbox-1.8.0-win32.win32.x86_64.zip
211e39abc40924d50d6cb20d863b65200aa82f95 TLAToolbox-1.8.0-linux.gtk.x86_64.zip
TBD macOS
Assets 8

The Ulpian release

21 Mar 00:11
@lemmy lemmy
v1.7.3
3ea3222
Compare
Choose a tag to compare
The Ulpian release Latest
Latest

The Ulpian release is based on the 1.7.3 branch and fixes the issue below.

Changelog

Checksums

sha1sum file
756b878250f2f2a1a2f6ede3382a8e4398c1540e tla2tools.jar

Please download the latest TLA+ Toolbox version from https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1#latest-tla-files

Assets 3

The Theano release

02 Feb 22:35
@lemmy lemmy
v1.7.2
3c7caa5
Compare
Choose a tag to compare
The Theano release

The Theano release is based on the 1.7.1 branch and fixes the following two issues:

Changelog

Contributors

We are grateful for contributions from Calvin Loncaric and Dmitry Kulagin.

Checksums

sha1sum file
7f21faa2cdae3189e7d5fadb4488f0dfcc658407 tla2tools.jar

Please download the latest TLA+ Toolbox version from https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1#latest-tla-files

Assets 3

The Brontinus release

23 Feb 00:16
@lemmy lemmy
v1.7.1
be99a7d
Compare
Choose a tag to compare
The Brontinus 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.7.1 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
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
Assets 7

The Aristotle release

01 Apr 00:01
@lemmy lemmy
v1.7.0
eb3ff99
Compare
Choose a tag to compare
The Aristotle release

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 ...
Read more
Assets 8

The Zenobius release

11 Jul 22:44
@lemmy lemmy
v1.6.0
0cae24f
Compare
Choose a tag to compare
The Zenobius release

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
Read more
Assets 7

The Xenophon release

18 Jul 08:00
@lemmy lemmy
v1.5.7
bfdbe00
Compare
Choose a tag to compare
The Xenophon release

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.

Assets 8

The Thucydides release

30 Jan 15:10
@lemmy lemmy
v1.5.6
2cf4197
Compare
Choose a tag to compare
The Thucydides release

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

The Herodotus release

08 Jan 14:50
@lemmy lemmy
v1.5.5
fafcc24
Compare
Choose a tag to compare
The Herodotus release

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
Assets 6

The Diodorus release

07 Oct 17:49
@lemmy lemmy
v1.5.4
14252e9
Compare
Choose a tag to compare
The Diodorus release

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

Assets 6