Go to the previous, next section.

Error Messages

The indentation of spec code depends to a large extent on a correct usage of TLA+ constructs. If some conditions are violated or not respected, there are generally two ways to proceed: make a good guess about the proper indentation relying on other contextual information or inform the user that there is an error-prone condition violating syntactic rules. The TLA mode pursues the strategy of signalling error messages to the user that clearly indicate a wrong structure. A TLA error message generally consists of the string `TLA Error:' and a short message explaining the failure of the current operation.

message

explanation

Missing LHS of formula or definition

The current line includes a semicolon supposed to conclude a structure which is obligatory begun with an identifier followed by `=='. That identifier--making up the left-hand side of the current structure--is missing.

No corresponding LET found

The current line contains an `IN' statement that requires a preceding `LET' in the same formula or symbol definition. That `LET' statement is missing.

Not within symbol definition

A command has been issued that involves a whole symbol definition such as commenting it, but point is not inside a symbol definition.

Corresponding opener of grouping missing

The current line contains a `}', `)' or `]' that has no preceding opening counterpart.

Missing THEN branch

The current line contains the `ELSE' branch but there is no preceding `THEN' branch.

INCLUDE keyword missing

The current line contains the `WITH' keyword but there is no preceding `INCLUDE' keyword.

Template not allowed in CONSTANT module

An attempt has been made to insert a keyword reserved for `TEMPORAL' modules into a `CONSTANT' module.

Additionally, this warning can be issued:

message

explanation

Template Template already used

A keyword has been inserted that was already present in the current buffer.

Go to the previous, next section.