Given a system where an input can be any int, how can you describe it with TLA+ in a way that TLC can check?
Btw, extreme noob here. Started Hillel Wayne's book. Saw this
https://www.learntla.com/introduction/example/ If we actually wanted to test all possible cases, we could replace money \in 1..20 with money \in Nat, where Nat is the set of natural numbers. This is perfectly valid TLA+. Unfortunately, it’s also something the model checker can’t handle. TLC can only check a subset of TLA+, and infinite sets aren’t part of that.
And this TLA+ started as a notation, and the model checker, TLC, only came out 5 years later. As it was never intended to be run, there’s some assumptions of it being a read document instead of being runnable code.
So I kinda get it, the mathematical proof of "All natural numbers" isn't computable. However, I am first a computer scientist and second,,, well not even second. And thirdly a (wannabe) mathematician. So the fact that Nat is not a finite number. To put it in the language of mathematics, this is the finite set of the values of all valid ints: GF(1)32. (On a 32-bit system, that is).
So should I write something like \in 0..4294967296 or \in -2147483648..2147483647 everywhere in my code? That's not reasonable. Unless TLA+ does something fancy with efficiency (something inductive, to prove that the remaining values follow from prior cases), then I am wrong to want to test all integers.
But then... what's the point of a spec that isn't exhaustive? Can someone help explain?