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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 13 Dec 2020 09:51:06 +0100*References*: <CABqWXWH1RNnxrKtAJJuvF-JyB4QLZQYRdgCUpZa-HVYdQWJnqA.ref@mail.gmail.com> <CABqWXWH1RNnxrKtAJJuvF-JyB4QLZQYRdgCUpZa-HVYdQWJnqA@mail.gmail.com>

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. Stephan
--
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**:

- Prev by Date:
**[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?** - Next by Date:
**[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?** - Previous by thread:
**[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?** - Next by thread:
**[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?** - Index(es):