Not all computations produce a value; most don't. Consider this TLA+ specification: VARIABLE x □(x ∈ 0..9) or, written in a form that can be checked b

Not all computations produce a value; most don't. Consider this TLA+ specification: VARIABLE x □(x ∈ 0..9) or, written in a form that can be checked by TLC: VARIABLE x x ∈ 0..9 ∧ □[x' ∈ 0..9]_x It says "x is a variable that is always an integer between 0 and 9, and it describes a system that nondeterministically assigns a number 0-9 to the variable x at each step, forever. It has an uncountable number of executions, each of infinite length, yet because it has a small number of states -- ten to be precise -- TLC can easily and quickly check many propositions about it. It is true that most of the behaviours don't have a corresponding determistic Turing machine and so most of those sequences are not computable, but it is not only a perfectly valid specification, but also a reasonable abstraction of real systems (e.g. a program that forever asks the user to input an integer between 0 and 9). On the other hand, this specification describes a system that picks an arbitrary natural number and then counts down to zero. It has only countably many executions (one for each initial number chosen), and each of them is finite in length -- i.e. they all terminate (I've omitted a liveness condition necessary to state that each computation will actually terminate, as it would mean little to those not familiar with TLA+ [1]): VARIABLE x x ∈ Nat ∧ □[x > 0 ∧ x' = x - 1]_x And yet TLC cannot check it because it has infinitely many states and TLC is an explicit-state model checker. In practice, we let TLC check a derived specification that overrides the value of Nat, the set of all natural numbers, with some finite set. [1]: To those familiar with TLA+, the real specification is: VARIABLE x LET Next ≜ x > 0 ∧ x' = x - 1 IN x ∈ Nat ∧ □[Next]_x ∧ WF_x(Next)