Go to the previous, next section.
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
Missing LHS of formula or definition
No corresponding LET found
Not within symbol definition
Corresponding opener of grouping missing
Missing THEN branch
INCLUDE keyword missing
Template not allowed in CONSTANT module
Additionally, this warning can be issued:
message
Template Template already used
Go to the previous, next section.