Guide on Spec Structuring

[Pierre-Louis Suckrow]

Hey,

I’m looking for resources or examples that explain how to structure a system specification in a clear and intuitive way.

I’m currently working on a prototype application, and even with just a few modules things are already starting to feel messy, especially when it comes to handling generated TeX files and PDFs. I’d like to find a way to organize the spec so it stays readable and scalable as the project grows.

If you have recommendations for guides, frameworks, or even personal approaches that have worked well for you, I’d really appreciate hearing about them.

Thanks in advance,
Pierre

[Andrew Helwer]

Some random tips as they come to mind:

• Really consider whether a given feature needs to be modeled. Remember you aren't building a system that has to actually work, you're just trying to capture the essence of the system in a way that can find important bugs in the design. Abstraction is difficult! People consult your spec to look at the core business logic, not the logic of how to send a network message. If most of your TLC runs are just catching runtime errors in your data model that's a sign you could be adding too much detail.
• Coming from programming we've learned it is good to make things modular and reusable with good encapsulation. Avoid thinking of modules as classes to be instantiated. It is preferable to inline everything in one module if at all possible.
• Split out functionality that exists only to make a module model-checkable by putting it in a MCModuleName.tla file that extends or instances the ModuleName.tla file you actually want to model-check. This will make your ModuleName.tla file easier to understand for the purpose of specification. Similarly, split out proofs into a separate ModuleName_proofs.tla module.
• Simplicity is difficult and often becomes possible only after you have made something complicated. A spec isn't done when it accurately models the system, it is done when it models the system in a simple way that captures only the important parts.
• Refinement is a more advanced TLA+ skill but it can be a good exercise to get you to write a simpler version of your spec. Lamport tends to talk about writing abstract specs first and then refining them into more detailed ones, but I've found it is easier to go the other way.

Andrew Helwer

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/2ee7999e-426a-4cfe-ac81-4d5e8e10e167n%40googlegroups.com.

[fwefew 4t4tg]

Mr. Suckrow,

Consider reading the pdf in https://github.com/gshanemiller/tla-examples. The RPC example to complete the document is in-progress.

To my knowledge this document gives the most complete, self-contained treatment of TLA/PlusCal with examples.