TBR-ed20.tar package / README / 94/10/31-am Universitaet Dortmund, Informatik IV, Computer Networks and Distributed Systems Group D-44221 Dortmund, Germany TLA-project (DEC EERP-GY-037A) README-author: Arnulf Mester This directory contains the result of the continuation of the tTLA+ browser (TBR) development, resulting in release 2 of TBR. Electronic distribution via ftp://ftp.informatik.uni-dortmund.de/pub/ls04-info/ and http://ls4-www.informatik.uni-dortmund.de/RVS/P-TLA/ Authors ------- - Olaf Meier (release 2) Diploma thesis "Ein erweitertes Werkzeug zur rechnergest\"utzten Einarbeitung in TLA-Spezifikationen verteilter Systeme" (in german) - Michael Geikowski (release 1, was available as TBR-ed10.tar) Diploma thesis "Werkzeugunterstuetztes Einarbeiten in Spezifikationen verteilter Systeme in TLA+" (in german) tTLA+ stands for "Tool TLA+" and is a subset of Leslie Lamports TLA+ proposal dated Feb, 92. (Cf. below) Contents -------- Beside of this README this directory contains three subdirectories: src/ preprocessor - the sources for the tTLA+ preprocessor 'tpp' browser - the sources for the main program 'tTLA+Browser' (this constitutes the graphical hypertext-oriented front-end) doc/ - postscript-files for the german! diploma thesis of O. Meier tlasrc/ - contains sample specifications in tool input syntax with the following top-modules: * DistributedBank.t : Lamports example from the 9/91 TLA+ draft adopted to tTLA+ * Elevator.t : Harters example adapted from TA to tTLA+ * Echo.t : Echo-Algorithm * SeqDiscovery.t : Sequential Net-exploration * and some other ... Compilation and Installation of the tTLA+ browser ------------------------------------------------- The tTLA+ browser task integrates two programs: - the preprocessor 'tpp' and - the main program 'tTLA+Browser'. The source of the preprocessor (directory src/preprocessor) is split into the files: Makefile adjlistgnu.C adjlistgnu.h crossref.C crossref.h dbinterface.C dbinterface.h env.C env.h higraphgnu.C higraphgnu.h layout.C layout.h lex.yy.c list.C list.h parsetree.C parsetree.h parser1.y parser2.y pqueuegnu.C pqueuegnu.h scanner.l semconcept.C semconcept.h sort.C sort.h symlist.C symlist.h tlatype.C tlatype.h tppmain.C typecheck.C typecheck.h The source of the main program (directory src/browser) is split into the files: Makefile adjlistcxx.C adjlistcxx.h browser.C dbinterface.C dbinterface.h higraphcxx.C higraphcxx.h link.C link.h list.C list.h modwin.C modwin.h navwin.C navwin.h pilayout.C pilayout.h pqueuecxx.C pqueuecxx.h ptlayout.C ptlayout.h semconhelp.C semconhelp.h semconwin.C semconwin.h topwin.C topwin.h For both programs makefiles exist in their source directories. You have to adapt src/browser/Makefile to your location of X and Motif includes and libraries (in Dortmund: /usr/local/{motif|X11}/...). Run 'make' in both directories. 'make install' installs the binary in ./bin. 'make clean' cleans up after make. Because the browser needs the preprocessor, both binaries should be located in the same directory or in a directory of the current search path. Software requirements: - 'tpp' and 'tTLA+Browser' are using flex/bison and GNU g++. - 'tTLA+Browser' is using DEC C++ (1.0) and X11R5 (not necessarily). Precanned binaries running on Ultrix 4.2a DECstations 5000/200 and /240 with (DEC)Motif installed, are included in a separate available tarfile TBR-ed20-dec-bin.tar resulting in directory 'bin' as convenience if you do not want to compile it from scratch for yourself. This directory also contains an X resources file for xrdb -merge < xresources . (Also available in src/preprocessor of TBR-ed20.tar) Usage ----- Either using the graphical front end 'tTLA+Browser' or 'tpp' directly: A tTLA+ specification is a collection of ASCII-files (nearly as for spec92.sty, but without dashed lines, explicit END and cautious use of tabs, see examples). The file-names all have the suffix ".t" (this suffix will automatically be appended from the tools). With 'tTLA+Browser' one can start anywhere in the module hierarchy, working from there to the bottom. tp parses only one module, not doing any import or inclusion. The prototype uses two environment variables: - TLASRC: denotes the directory where the modules of the interesting tTLA+ specification can be found; (to use the examples, it should point to directory tlasrc). - TLALIB: denotes the directory for tTLA+ module library files (not used in external distribution) [new, not in release 1] - TBRDB: denotes a scratch directory, where automatically generated files could be saved in. [name changed from release 1 TLADB] Is one of the environment variables not defined when the browser starts, it uses the current working directory for it. The preprocessor can be used independently from the main program, to check specifications for syntactical and partly for semantical correctness. Start tpp with the name of the file, which contains the main module of the specification to be analyzed. The main program 'tTLA+Browser' is started without parameters. The interesting specification could be choosed via a file selector box. Diploma Thesis -------------- Directory doc containts a printable postscript version of O. Meiers diploma thesis. It is basically a dvi-file with postscript inclusions. The thesis is in GERMAN language. Feedback -------- Please e-mail feedback, comments, application experiences etc. to mester@ls4.informatik.uni-dortmund.de Thanks in advance. Restrictions in use ------------------- This is a research prototype, provided AS IS for use in the scientific community only.