The project is frozen. Parts of it will be contributed in the TLA+ Tools developed on MS-R site. This page is just a placeholder and will be removed/ redirected, as soon as the main TLA+ site provides the more accurate content.
eTLA plugin adds capability of working with TLA+ inside Eclipse IDE. It is a wrapper around the original TLA+ Tools, which makes them more convenient in use and integrates them in a standard IDE. TLA (The Temporal Logic of Actions) is a logic for specifying and reasoning about concurrent and reactive systems. It is the basis for TLA+, a complete specification language. For further information on TLA-related subjects, please visit the page of Leslie Lamport or the official TLA+ web page. The first impression of how the plug-in works can be gathered by viewing a Flash demo.
- TLA+ Project support
- TLA+ Editor with syntax highlighting and auto-completion
- Tight integration of TLA+ Tools, enables syntax and semantic analysis and problem reporting triggered by save of resource.
- Integration of TLC Model Checker (over Run As menu)
- TLC is sticky after several runs, and does not compute correctly
- The editor provides support for TLA+ version 1 (not TLA2+)
Further Development (rejected)
- TLA+ Editor Outline
- Support of TLC simulation mode
- Support of EMF-based TLA+ representation
The plugin has been tested under Eclipse 3.1, Eclipse 3.2, Eclipse 3.3
Please note, that the TLA+ Plugin is free for non-commercial use, because it uses parts of code which underlies Microsoft Shared Research License.
In order to install the plugin, please use techJava Update Site for Eclipse Update Manager. It can be accessed under
http://update.techjava.de/. After installation please set up the TLA+ library modules using Window > Preferences… > TLA+ Preferences > Syntax Analyser > Add….
The default TLA+ library modules can be found at [ECLIPSE-INSTALL-DIRECTORY]/plugins/de.techjava.tla.modules_0.0.1/modules/
Please visit the eTLA Sourceforge Project site