Uncorrected TLC Bug

Last modified 11 January 2018

The Problem

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:
  1. 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.

  2. 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 Workaround

The workaround is to rewrite the initial predicate or next-state relation so it is not in the form that can cause the bug.  The simplest way to do that is to expand (in-line) the definition of  F  in the definition of the initial predicate or next-state relation.