We use TLA+ to find flaws in our designs. But there’s another, subtler benefit: we also find places where the spec is ambiguous. Formally specifying your problem forces you to decide what you actually want out of your system. This is especially important when we model “business logic,” features, and requirements. To work through this, we’ll use TLA+ to spec a simple library system and show how the act of specifying can itself find faults in the spec.
In our system, people should be able to check out books, renew books, and return them. They will also be able to reserve books: a reserved book cannot ...
