Go to the previous, next section.
This section covers the most commonly used features such as inserting templates for different types of modules, indenting spec code and commenting certain areas of text or code.
Using templates eases the process of inserting defined keywords and structures in a given language and reduces the amount of errors typically caused by typos. This also holds for specification code written in TLA+. All keywords can be easily accessed by using the mode's menu or a keyboard shortcut.
Module headers as they are defined in (Mester 93) not only cover the line that the keyword MODULE is in, but also include IMPORT, EXPORT and PARAMETERS clauses. The concept of header is used differently in that only accounts for the code line containing the keyword MODULE. It is, however, enriched with additional comments. In order to distinguish between these notions we just use header if we refer to the latter and module header in the other case.
Headers should follow conventions determining their information content, such as date and time of creation, information about the author, a one-line description and the template used by revision control systems such as RCS or SCCS. This is a typical example of a header that contains no type information but an already filled RCS ID slot:
MODULE LibraryActions (* LibraryActions.t -- Library transactions *) (* Created: Tue Mar 29 11:10:48 1994 *) (* Author: Frank Wegmann <wegmann@talisker> *) (* $Id: LibraryActions.t,v 1.2 1994/06/25 17:43:33 wegmann Exp wegmann $ *)
Before inserting a new header, the buffer is checked for an existing one. The user then has to confirm whether that header should be deleted. If not, no insertion is made and point remains unchanged. The complete header will be inserted and point is just behind the long dash to let the user provide short information about the module itself. If tla-use-vc is nil, don't insert a comment line for version control systems (default is t).
There are three shortcuts according to the possible type information. An untyped header contains no type information and is therefore considered a TEMPORAL module. However, it is recommended to indicate the module's type for better readability. Furthermore, the END keyword will be inserted at the very end of the buffer if it is not already present.
(C-c C-h) Insert template for header of current buffer.
arg determines the type of header, as specified by tla-header-list.
Delete complete module header. This is normally used from within
tla-header and thus the user is not asked for confirmation.
List of module header types used by tla-header.
Each entry is a list with three elements. The first element is the key indicating the type of header. The second element is the entry appearing on the menu, and the third element is the string to insert just before the keyword MODULE.
If non-nil insert comment with RCS ID as last part of header.
A certain range of keywords may appear in the body of a CONSTANTS module. The upper half of the submenu titled "Insert TLA+ Keyword" contains all allowed keywords. The command prefix C-c C-k is common to all keywords so that their respective templates can be inserted via shortcuts.
Before insertion takes place, the mode checks the current position of point. If point is inside a symbol definition or formula, the template gets inserted just behind that structure. A warning will be issued if the template is already present.
All keywords that are allowed in CONSTANTS modules can also be used in TEMPORAL modules. Furthermore, those keywords located in the lower half of the submenu can be used. The same restrictions that hold for the insertion of CONSTANTS MODULE keywords also hold for TEMPORAL ones. Additionally an error will be signalled when the user wants to insert one of the following keywords in a CONSTANTS module.
List of tTLA+ keywords used by tla-keyword.
Each entry is a list with three elements. The first element is the key inserting the appropriate keyword. The second element is the entry appearing on the menu, and the third element is the string that will be inserted on a line by its own.
It is often necessary to comment out temporarily a region of code. This can be done with the commands C-c ; and C-c % . C-c ; will comment out all lines in the current region, while C-c % will comment out the current symbol definition. To uncomment, simply type C-u - C-c ; to uncomment all lines in the region.
By default, these commands will insert or remove a single `(*' or `*)'. To insert more than one, give an argument. For example, C-u 5 C-c % will add five `%' to each line, while C-u - 5 C-c % will remove up to 5 `%' from each line.
However, commenting commands will work on the whole region or symbol definition, even if there is already a commented line in it. Since nested comments are not allowed in TLA+, this should be avoided. This support for multiple levels of commenting will be removed in a later version.
Command: tla-comment-region count
(C-c ;) Add or remove `(*' from the beginning and `*)' from the end of each line in the current region, as specified by count. Comments will only be added if there is at least one uncommented line in the current region.
Command: tla-comment-formula count
(C-c %) Add or remove `(*' from the beginning and `*)' from the end of each line in the current spec formula, as specified by count. A formula begins at the line containing `==' and ends at the line containing `;'.
Command: tla-comment-paragraph count
Add or remove `(*' from the beginning and `*)' from the end of each line in the current paragraph, as specified by count. Since most paragraphs only comprise one line, this is of minor interest.
At the current stage of implementation, indentation is not complete. One of the shortcomings is that you can only indent single lines.
The characters indented are spaces, since tabs are not feasible for
most existing tools. Therefore the current buffer will normally be
untabified each time you save it. This is controlled by the value of
tla-auto-untabify which is normally non-nil. Instead of
inserting tabs, M-i should be used for inserting space up to the
next tab stop position.
Indentation is controlled by the environment containing point. The keywords
whose templates can be inserted all start at the very beginning of a line and
thus become reindented properly if they don't start a line.
Symbol definitions and formulas start with a uniform left-hand side made up
of an identifier with or without additional type information ("qualified") and
the ASCII representation of "equals by definition" (`=='). These are
generally indented by the value of tla-indent (default 2). The first
continuing line is indented by the value of tla-inner-indent (default 4),
if there are no structures on the first line that request a different indentation.
This is a typical example of indented code taken from the BankAction module (1).
ReceiveRequest(A : ATM) ==
:E: r :in: ATMMessage
::
/\ pending[A].req = "None"
/\ AtoB.Rcv(r,A)
/\ Unchanged( bToA )
/\ pending' = [CHG pending ; A :mapsto: r]
;
TLA mode looks for a number of character sequences that determine the indentation of the next line. Here three different indentations have been used: the first body line of the action gets the standard tla-inner-indent, while the indentation of the second line is controlled by the position of the existential quantifier `:E:'. The characters indicating the end of the scope description (`::') demand the indentation of the "bulleted" list of conjunctions below. Finally, the semicolon concludes the code of the action and is therefore indented the same number of spaces as the beginning line.
One type of indentation deserves a special treatment: if conjunctions and disjunctions are to be bulleted as in the example above, operators of the same kind are stacked upon each other. This holds when tla-bullet-lorand is non-nil (default). But structures can be nested, as can be seen in the following lines from ATMAction:
N == :E: A :in: ATM
::
\/ /\ :E: am :in: ATMMessage :: AtoB.Send(am, A)
/\ Unchanged( bToA )
\/ /\ :E: bm :in: BankMessage :: BtoA.Rcv(bm, A)
/\ Unchanged( aToB )
;
The second and fourth conjunctions are properly indented since TLA mode knows that only operators of the same kind can be stacked upon each other. If tla-bullet-lorand were nil that line would have been indented according to the position of the double colon above. This behavior forces the user to pursue a common style of writing specification code. A last example shows that bulleting works even across other conjunctions or disjunctions that are enclosed in a separate structure:
Elevator == :EE: Light, Location, Direction
::
/\ Ser(Light,Location,Direction).Init
/\ [] ([
\/ :E: f :in: Floor
:: Ser(Light,Location,Direction).PressButton(f)
\/ Lif(Light,Location,Direction).MoveUp
\/ Lif(Light,Location,Direction).MoveDown
] _ (Light,Location,Direction)
)
/\ :A: f :in: Floor
:: Light[f] = "on" :leadsto: Light[f] = "off"
;
tla-indent-line will indent the current line.
reindent-then-newline-and-indent indents the current line, and
then inserts a new line (much like ret) and move the cursor to an
appropriate position at the left margin.
Number of spaces that make up the indentation of an unnested line.
Number of spaces to add to the indentation of tla-indent.
If non-nil, current buffer will be untabified upon saving.
If non-nil, lists of conjunctions and disjunctions will be "bulleted" wrt to nested structures.
All GNU Emacs versions prior to version 19.19 come with an outline mode with only limited functionality. A port of the current outline mode to Emacs 18 and Lucid Emacs is available from `ftp.iesd.auc.dk:/pub/emacs-lisp/outln-18.el'.
TLA+ mode supports the standard outline minor mode for outlining symbol
definitions. (See section `Outline Mode' in GNU Emacs Manual.) Normally, outline-minor-mode will use the prefix key
C-c, which is also used by TLA mode, so it might be better to
choose another prefix key by inserting
(setq outline-minor-mode-prefix "\C-c\C-o") ; Or whatever...
in your `~/.emacs' file. There is a menu item "Toggle Outlining" turning the minor mode on or off.
Outlining a document means to impose a hierarchical order on it. Since there is no apparent hierarchical structure in specification code, the current version defines just two levels: the first one matching keywords and the second one matching symbol definitions. This suffices to get an overview of the current code and the regular expressions needed are not too complex to be noticeably slow.
For instance, when point is on a first-level heading (i.e. a keyword) you could hide the entire structure up to the next heading by hiding the subtree (C-c C-o C-d). If you then show branches by typing C-c C-o C-k, all headings of the next, i.e. second level are visible again but their contents is hidden:
ACTIONS
N == :E: A :in: ATM...
ReceiveRequest(A: ATM) == ...
DoRequest(A: ATM) ==...
r == pending[A].req;
a == pending[A].amt;...
Next == \/ CheckOut...
However, as can be seen in this example, there is a problem with nested, multiline symbol definitions introduced by LET. The second and following lines of a LET definition look absolutely perfect to the outline mode in the sense that they are matched as a second level heading (since the symbol definitions in LET are regular symbol definitions). There seems to be no apparent solution for this problem if one sticks to the regular outline mode.
In Emacs 19 it is possible to use different fonts and colors in order to
highlight certain regions of a document. While TLA+ mode doesn't support
color it makes use of different fonts, also called faces. This is invoked
automatically when the value of tla-use-font-lock is non-nil.
The use of different faces is controlled by the font lock minor mode. If you
want to toggle this mode, simply type M-x font-lock-mode.
In the current version the use of faces is restricted to comments and strings. Comments will be italicized and strings will be underlined. There is no need to emphasize keywords since they are already uppercase. There is no reason to fontify more than that (e.g. by fontifying symbol definitions) since fontifying large documents gets quite slow.
If non-nil then buffer will be automatically fontified when entering TLA mode.
Go to the previous, next section.