Go to the previous, next section.
Having several different variants of TLA+ means having to deal with several classes of tools and the varying language scope of each of them. The concept of a variant tries to cope with the difficulties resulting from this situation. A variant determines which specific features of the language is defined. For instance, eTLA+ does not allow typed identifiers in contrast to tTLA+. This yields a different behavior of the mode.
However, support for different variants is not completed yet. For now,
the predominant variant is "tTLA+" and most routines still expect
the code to behave like tTLA+ code, i.e. according to the rules in
(Mester 93).
List containing the different variants of TLA+ that are supported. Each element is a list whose first element is the name of the variant that will also be the entry in the menu bar.
The following elements will each indicate presence or absence of a particular language features: The second element denotes typing. If non-nil, typing is mandatory and thus identifiers followed by bracketed expressions will signal an error. If nil, typing is optional and untyped identifiers are allowed. The third element denotes the use of the END keyword. If non-nil, insertion of a header automatically takes care of a final END keyword. The fourth element denotes mixfix operators. If non-nil, mixfix operators are allowed. The fifth element denotes postfix operators. If non-nil, postfix operators are allowed.
Indicates current variant of TLA+. Must be an element of tla-variant-list.
User Option: tla-variant-default "tTLA+"
Indicates default variant of TLA+. Must be an element of tla-variant-list.
Go to the previous, next section.