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

• Toolbox selfupdate breaks TLC with bogus error OffHeapDiskFPSet.isSupported()Z
• Fixed integer overflow causing an exception after long running model checking

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