What Is A Spec?
In TLA+, the term specification (or spec) is used to mean one of two
We take the word specification by itself to have the first meaning. We use the term
behavior specification when we mean the second.
- The collection of modules consisting of the root module and and all modules that are imported by the
root module, either directly or indirectly, with
In the context of the Toolbox, we exclude from this collection the standard TLA+ modules such as the
Naturals module. All the specification's module files must be in the same directory
as the root module file.
- The TLA formula that specifies the set of allowed behaviors of the system or algorithm being specified.
↑ Managing Your Specifications