Tool Prototypes
'Tools for TLA based specifications' project
Computer Networks and Distributed Systems Group
Department of Computer Science, University of Dortmund, Germany
This page reflects (in their tool subpages) effort done to
make external distributions available (priorized by external demands).
The acronym tTLA+ below denotes a subsets/variant of TLA+
to facilitate first tool prototypes ("tool TLA+"), the
acronym eTLA+ below a tTLA+ based language definition for executing
specifications ("executable TLA+").
Construction and Design
- TBR - Graphical Browser for tTLA+ specifications
- TEM - An emacs major mode for editing TLA+ specs
- IT - eTLA+ Interpreter (graphical and textual version)
- status: completed, release after rehash
- ASPEC - Audiovisual/graphical animation of eTLA+ specifications
- TCO - Coarsener Tool
- status: completed (prototype), release on demand
- L2TLA - LOTOS to TLA+ Translator
- status: completed (prototype) , release on demand
Analysis and Verification
- RMC - Refinement Mapping Checker
- RMS - Refinement Mapping Searcher
- status: enhanced version (guided search) completed,
external release on demand
- TOAST - (Otter based) tool assisted reduction of proofs
- TOAST1 (safety part), TOAST2 (fairness part)
- status: completed, external release after rehash
- Covered in research report 492/93.
Work done in early phases (based on Transition Axioms theory)
- EST2TA - Estelle to TA translator
- ETA - Syntax-oriented Editor for TA
- GIXTA - Graphical Interpreter for xTA
- TAREFMAP - Refinement Tool
- TASEDI - Emacs-Leif-based editor for TA
- TASEM - Parser for TA in C++
- VIMOS - Graphical Composition of distributed systems specifications
Arnulf Mester,
last updated: Mar 16, 1995
Informatik IV, Uni Dortmund