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

*From*: Ari Sweedler <ari@xxxxxxxxxxxx>*Date*: Sun, 13 Dec 2020 01:44:53 -0700*References*: <CABqWXWH1RNnxrKtAJJuvF-JyB4QLZQYRdgCUpZa-HVYdQWJnqA.ref@mail.gmail.com>

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?

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.

**Follow-Ups**:**[tlaplus] Re: 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?***From:*Leslie Lamport

**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?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] dumping to JSON and not dot files** - Next by Date:
**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?** - Previous by thread:
**Re: [tlaplus] Approaching repeated assignment in PlusCal** - Next by thread:
**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?** - Index(es):