TLA+ Language
  • Implements the Temporal Logics of Actions (Lamport, 1994)
  • Used for the specification of real-time, discreet, but also hybrid, continuous systems
  • liveness, fairness, deadlock...
  • Intuitive notation

TLA+ Tools
  • TLC - Temporal Logic Model Checker
  • TLATex - generates formatted text
They are both written in Java by Lamport and his team (Compaq, Microsoft Research).

TLA# Objectives
  • Mission:
    • Integration of TLA+ language with Visual Studio IDE.
  • Objectives:
    • Code editing
    • Integration of TLA+ tools
    • Grammer adjustment

What has been done
  • Open source (version 0.1)
  • Installer package
  • TLA language package:
    • TLA+ grammar adjustment for Visual Studio IDE - LALR(1)
    • Syntax highlighting
    • Error detection in real time
  • TLA integration package:
    • A top level menu
    • Contextual menu
    • Option Page (Tools -> Options : Tla Sharp
    • Verify command which calls the TLC modal checker and
      shows the result in the Output window of the VS IDE
    • Make DVI, PDF and HTML commands which transforms the
      tla file in the specified format (TLA Tools).
    • Autocompletion

Download page:  TLA #

The team:
  • Coordinating teacher:
    • Vasile V. Alaiba
  • Langyage package:
    • Amalia Elena Goldan
    • Andrei George Dobjenschi
  • Integration package and Installer:
    • Daniela Benea
    • Bogdan - Mihai Pirau (team leader)
Screenshots Logo

First image
Sercond image
Third image
Fourth image
Fifth image
Sixth image
Seventh image
Eighth image
Nineth image
Tenth image
Eleventh image
Last update: 07 November 2007, 13:39 GMT