learning_tla/learn_tla/core/12-modules.md

12. Modules

Modules are usually not necessary as most specs are less than 300 lines long, which can be kept in a single file.

The main use is to create abstract libraries, or isolate invariants in separate files.

Modules

Shared TLA+ files should be in the same folder as the spec.

EXTENDS is much like a C #include "somefile.h"

• it brings all symbols defined in the files listed in the EXTENDS line to the current file
• except those defined with LOCAL
• there can only be ONE EXTENDS line in any given file

INSTANCE

INSTANCE does more that EXTENDS:

• There can be multiple INSTANCE lines in a given file
• LOCAL INSTANCE imports the instance's symbols as LOCAL, locking the imported symbols if the file gets imported later
• Instance operators can be namespaced using Foo == INSTANCE Sequences,
  • use as Foo!Append(seq, 1) instead of Append(seq, 1)
  • this supports multiple namespaces for the same imported instance
• Instance imports can define the CONSTANTS in the imported modules,
  • using: INSTANCE <imported> WITH <const1> <- <val1>, ...
  • Not all constants have to be defined thus, enabling use of the namespaced instead as an operator: XAxis(X) == INSTANCE Point WITH Y <- 0