3 ms·

> TLC could, in some situations, check whether an uncountably infinite number of program executions I'd love to see an example of an uncountably infinite numbe

> TLC could, in some situations, check whether an uncountably infinite number of program executions I'd love to see an example of an uncountably infinite number of program executions checked. The set of all computable values as countable, after all.

jlokier 6y ago
Ah, I think I see it. The set of infinite, non-deterministic execution traces is uncountable (same reason real numbers composed of infinite sequences of digits from a finite set are uncountable). On the other hand, the set of infinite execution traces which can result from any deterministic, finite-size program is countable (because the set of programs is). But programs take inputs. And the set of possible inputs to an infinite execution trace is uncountable (same reason as reals, above). The prover needs to show that a program behaves correctly when given any sequence of inputs, even if the program never terminates and keeps taking new inputs forever. That requires proofs over an uncountable set of infinite execution traces.
pron 6y ago
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)
- jlokier 6y ago
  Thanks!

jlokier 6y ago

Ah, I think I see it. The set of infinite, non-deterministic execution traces is uncountable (same reason real numbers composed of infinite sequences of digits from a finite set are uncountable). On the other hand, the set of infinite execution traces which can result from any deterministic, finite-size program is countable (because the set of programs is). But programs take inputs. And the set of possible inputs to an infinite execution trace is uncountable (same reason as reals, above). The prover needs to show that a program behaves correctly when given any sequence of inputs, even if the program never terminates and keeps taking new inputs forever. That requires proofs over an uncountable set of infinite execution traces.

pron 6y ago

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)

jlokier 6y ago
Thanks!