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

• Make constant types first-class citizen in model editor
• Include step names in error trace
• Add preference page to configure proxy servers
• Remove model locking
• Allows users to specify the number of model snapshots to preserve

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