Corrected TLC Bug

Leslie Lamport

Last modified on 30 January 2018

The Problem

An uncommon but serious bug in TLC has been corrected in Toolbox release 1.5.6.. The bug was in the initial implementation of TLC. It could have caused TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either could have caused TLC not to examine all reachable states. The error could have occurred 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 Solution and a Possible Performance Problem

TLC sometimes caches values it has computed in case those values are later re-used. The bug was caused by TLC using cached values when it should not have. The solution involved disabling the incorrect use of cached values. However, it also disabled some correct uses of cached values. We believe that this will have no noticable affect on TLC's performance. Please let us know if you have reason to believe that the fix has significantly slowed TLC down on one of your specs.