I have observed that many new users want to write TLA+ specs so they
can be reused. I have one word of advice for those users: Don't.
The way to reuse a TLA+ spec is copy, paste, and modify.
This flies in the face of everything you've learned about writing
programs. It does so for the same reason that TLA+ does not look like
any programming language: specifications are very different from
programs.
The most obvious difference between them is size. I have the
impression that the specs written by engineers at Amazon and Microsoft
working on cloud systems are a few hundred lines long. Other than one
outlier, the longest specs I know of were written by engineers at
Intel. They were about 2000 lines long. I was told that this was
because that was the largest spec a single person could understand.
If a spec started becoming longer than that, they would remove details
by abstraction to make it smaller. Programming languages could be a
lot simpler if no one ever wrote a program longer than 2000 lines.
A more important difference appears when you consider what one reuses
when programming. If you're writing a sorting program, you don't make
it reusable in the sense that you could write the program so that, by
changing the parameters, you could change it from executing quick sort
to executing heap sort. Reusing means being able to write another
program that uses sorting as a primitive, without caring about how
it's implemented. In a TLA+ spec of an algorithm that uses sorting,
that use might appear as a subformula like A' = Sort(A), where Sort
has a 3-line definition. You hardly need a separate module for a 3-line
definition. A reusable sorting program needs to pass in arguments
specifying where to find the sorting key and what the ordering
relation is. In TLA+, you just copy a Sort definition used in one
spec and make some trivial modification to those three lines to
reflect the difference in the location of the sorting key and the
ordering relation. This is easy enough, and it makes the spec a lot
simpler than if you imported a single definition that could be reused
without modification.
A Sort operator is actually one of the most complicated parts of a
TLA+ spec you're likely to reuse. Consider message passing in a
distributed algorithm. If you wrote a distributed program and had to
write your own code for sending and receiving messages, you would
certainly not want to have to rewrite it for your next distributed
program. Now look at the spec of the Paxos consensus algorithm in the
TLA+ GitHub examples repository. Here is the "procedure" that's used
to send an arbitrary message m:
Send(m) == msg' = msg \cup {m}
It was hardly worth writing that definition just to be able to write
"Send(m)" instead of "msg' = msg \cup {m}" throughout the spec. But I
thought it made the spec a little easier to read. There isn't even
any explicit receive action. The presence of a message to be received
is simply an enabling condition of an action. What can be reused from
the spec is the idea of representing message passing with a variable
containing the set of all messages that have been sent. Simple ideas
are expressed simply in TLA+; you don't need to reuse the "code" that
embodies them.
If you want to learn to write specs, write a spec of a particular
system or algorithm you're interested in. Worry about getting that
system or algorithm right. Don't think about what else you might want
to do with your spec. That's what I do. That's what engineers who use
TLA+ to build real systems do.
Leslie