Current Status

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.

Project Goal

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.

Supported Features

  • 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)

Known Bugs

  • 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

Prerequirements

The plugin has been tested under Eclipse 3.1, Eclipse 3.2, Eclipse 3.3

Licensing

Please note, that the TLA+ Plugin is free for non-commercial use, because it uses parts of code which underlies Microsoft Shared Research License.

Installation

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….
eTLA Plugin options
The default TLA+ library modules can be found at [ECLIPSE-INSTALL-DIRECTORY]/plugins/de.techjava.tla.modules_0.0.1/modules/

Further Questions

Please visit the eTLA Sourceforge Project site