[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: [tlaplus] Question: Given a system where an input can be any int, how can you describe it with TLA+ in a way that TLC can check?

 TLC exhaustively checks finite (and typically small) instances. The underlying assumption is that for actual systems, this is an effective way of finding bugs. If you need higher assurance, you can do theorem proving, which can be applied to arbitrary (including infinite-size) instances, at the cost of more human effort.StephanOn 13 Dec 2020, at 09:44, Ari Sweedler wrote:I first asked this question on Reddit, https://www.reddit.com/r/tlaplus/comments/kc75n0/given_a_system_where_an_input_can_be_any_int_how/, but figured this was a better place to ask. I'll copy/paste my post & question here to save y'all from having to click that link: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?Thanks,Ari -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABqWXWH1RNnxrKtAJJuvF-JyB4QLZQYRdgCUpZa-HVYdQWJnqA%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4A977ACC-D56A-4888-97B6-B4D5A548FF67%40gmail.com.

• References: