## The ProblemAn 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 subformulaF(..., 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 subformulaF(..., 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
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 = -1or 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 ProblemTLC 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. |
||