On 08.01.2018 16:26, Markus Alexander Kuppe wrote: Hi, a new TLA+ Toolbox 1.5.5 release has been made available [1][2]. This release primarily 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 /\ ... We advise all users to update as soon as possible. Thanks Markus [1] https://github.com/tlaplus/tlaplus/releases/tag/v1.5.5 [2] https://tla.msr-inria.inria.fr/tlatoolbox/products/  Hi, we since learned that the 1.5.5 release does not fully fix the bug where TLC fails to generate the correct set of initial states. Please make sure that you rewrite your specifications as described above until we are able to provide a proper fix in an upcoming 1.5.6 release. Thanks Markus