[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] TLA+ major mode for Emacs
- From: Christian Barthel <bch@xxxxxxxxx>
- Date: Thu, 27 Aug 2020 17:40:31 +0200
- User-agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (berkeley-unix)
I am currently in the process of learning TLA+ and how to specify
software. To do that, I created a Major-Mode to edit TLA+
specifications within the Emacs ecosystem(*). If someone is also
interested in writing specifications with Emacs, the elisp code
can be downloaded here .
This is one of my first emacs major-modes. Any hints, tips or
further additions are welcome. The implemented functionality:
- Syntax Highlighting for TLA+ Specification Files
- Running `SANY Syntactic Analyzer' on TLA+ files,
default keybinding: `C-c C-t c'.
- Exporting TLA+ Specification files with TLATeX to
DVI, PS or PDF files (Export it with `C-c C-t e'
and open the viewer `C-c C-t o')
- Inserting TLA+ Operators with an easy to use menu
or typical Emacs keystrokes.
- Use templates to generate Modules
- An Emacs widget to create TLC configuration files
- Options to run the TLC model checker on TLA+
specifications (`C-c C-t m').
- Translate PlusCal code to TLA+ specification
with `C-c C-t p'.
To install and configure:
(setq tla+-tlatools-path </path/to/tla2tools.jar>)
See more details with `describe-mode'.
I will try to further extend the elisp code while I am reading
the `Specifying Systems' book. The current version seems to
support most of what I am currently using: write a spec, do some
syntax highlighting, check the spec (c-c c-t c), run the TLaTeX
pretty printer (c-c c-t e) or try to model check with TLC
(c-c c-t m).
Any additional improvements are welcome,
(*) I am using BSD operating systems and it seems that the
eclipse TLA+ Toolbox is not running on that operating system.
However, the tla2tools.jar can be used with a Java runtime.
 Emacs tla+-mode.el:
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87sgc83xn4.fsf%40barthel.ch.