TLA #

• 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

• TLC - Temporal Logic Model Checker
• TLATex - generates formatted text

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

• 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

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