Proposal: standardize allowing multiple sequential modules in a file

[ahelwer]

tlaplus/tlaplus#1104 made me realize that this hasn't gone through the standardization process, although it should. This would expand the TLA+ file standard to allow sequential module definitions, like:

freeform extramodular text

---- MODULE First ----
EXTENDS Second
op == TRUE
=======================

more freeform text

---- MODULE Second ----
EXTENDS Third
op2 == TRUE
=======================

even more freeform text

---- MODULE Third ----
op3 == TRUE
=======================

concluding freeform text

The tree-sitter-tlaplus parser already supports this, as you can see from the highlighting in the above snippet. SANY currently supports this by splitting the file using regexes in MonolithSpecExtractor. This could instead be formalized and moved into the syntax parser, to avoid the general nightmare of long-tail regex context issues. So the new root node of the SANY parse tree would be a list of modules interspersed with extramodular text, instead of a single module node.

This is useful when writing tests for TLA+ tooling and also when whipping up a quick spec where you want an encapsulated utility module without making it a nested module for some reason.

[muenchnerkindl]

What was the motivation for introducing MonolithSpecExtractor in the first place? Sequences of modules are certainly never mentioned in Specifying Systems.

[Calvin-L]

It was introduced in 505e073f as part of a series of changes that allow command-line users to explore error traces outside of the toolbox. It was not designed as a user-facing feature, but users can easily discover that it exists by examining TLC's autogenerated outputs.

From time to time I have found it useful:

• Small utility modules can be separated from a big spec without cluttering a project with more files.
• A multi-module spec can be bundled into a single file that is easier to scp to a big remote machine for model checking.
• A functioning TLC configuration can be bundled in the same file as the spec, as a kind of documentation about which definitions are important invariants/properties to check.

That said, I am still on the fence about whether this feature is something we want to support, and I'm interested to hear what others think.

[lemmy]

What was the motivation for introducing MonolithSpecExtractor in the first place? Sequences of modules are certainly never mentioned in Specifying Systems.

I can't find a statement in Specifying Systems that mandates a strict 1:1 mapping between a (non-nested) module and a file. At any rate, the MonolithSpecExtractor was primarily added (in 2020) to improve trace exploration (TE) on the command line. More concretely, for TE to not pollute the $CWD with many, many generated files. It has also been used to write TLC integration tests. The feature has its limit (e.g. regex) but has proven itself useful within the scope of TLC. I'm not sure if it useful enough to be made "official" (for some definition of "official").

tlaplus/tlaplus#1104 made me realize that this hasn't gone through the standardization process, although it should.

There is the SLC and this RFC repository, but I'm not aware of a "standardization process". Moreover, it is up for debate if TLC's config file, Apalache's configuration and annotations, the number of modules TLC reads from a single file, ... should be covered by the TLA+ specification language.

[lemmy]

Let’s continue this discussion in #1 to avoid expanding the scope of this issue? Could you please recreate your last comment over there?

[ahelwer]

I've been thinking further about this and one big question is whether to only resolve modules from multi-module specs in the root spec; options:

1. Allow resolving all multi-modules in all specs, not just the root; this means the resolver will need to look for a given module in all .tla files in all its search directories, not only .tla files with a filename matching the module name.
2. Restrict resolving multi-modules to the root spec; this means that some modules could parse correctly when parsed as root but not parse correctly when imported (for example if the top-level spec imports other specs in its file for utility functions).
3. (Synthesis) Only allow resolving multi-modules from within the same spec file. So one module cannot import another module unless that module is either defined as a multi-module in the same file or defined as a top-level module in another file. Put another way, only top-level modules are visible outside the file.