tTLA+ Browser
'Tools for TLA based specifications' project
Computer Networks and Distributed Systems Group
Department of Computer Science, University of Dortmund, Germany
Features
Reading and analyzing formal specifications should be supported by
tools. For specifications based on Leslie Lamport's specification language TLA+
(with concrete syntax named tTLA+) this browser facilitates
- module based source text display / browsing,
- contents listings,
- module hierarchy graph construction and display,
- hypertext-like navigation within and between modules,
including display of definitions and usages of symbols within this
hierarchy, symbol explanations on demand and bookmarks,
- graphical parsetree display for the structure of each specification
module,
- static semantic checks by separate preprocessor, e.g.
- sort analysis,
- type checker for catching some typical type errors,
- support for interactive construction of a semantic concept, i.e.
system structure, allowing the user to build his own individual
process/interface view of a system described by the specification;
mainly of use in process-oriented developments,
- optional integration of the TEM
emacs-mode allows incremental positioning on the errors detected by the
preprocessor for correction.
The typical screenshot above shows a module hierarchy graph of a specification
(here: Lamport's Distributed Bank example), an error log window, a module o
display window and a navigation window.
Distribution
TBR-ed20.tar is release 2 of the external distribution
of the tTLA+ browser prototype. The tarfile contains a subset
(without tex sources and precanned binaries; but including a (german language)
postscript file of the thesis) of the thesis work.
It is electronically available from our
FTP repository, and
from our WWW repository,
maybe you intend to read the tarfile's README
first.
TBR-ed20-bin-dec.tar contains precanned binaries for
Ultrix 4.2a DECstations 5000/2xx with X11.
It is electronically available from our
FTP repository, and
from our WWW repository.
Authors
Michael Geikowski, Olaf Meier
Arnulf Mester, last updated: Mar 16, 1995
Informatik IV, Uni Dortmund