werkzeug_smallAs mentioned in the previous post on Fowlers DSL example,there are some tools available for the TLA+ specification language. In the following a short overview of currently available tools for TLA+ is given. The described tools are and are part of the TLA+ toolset available from the website.

  • SANY – Syntax Analyser for TLA+ specifications
  • TLC – A modelchecker / simulator for TLA+ specifications
  • TLATeX – LaTeX typesetter for TLA+

The PCal Translator is not covered in this post and will be introduced in a separate post, together with PCal language.

SANY

SANY is a syntax analyser for the TLA+ language. The purpose of it is to check the syntax of the specifications (including some static semantics) and provide the errors to the user. As all of the TLA+ Tools currently available, SANY is a command line tool and reports the errors back to the console. In fact SANY is a front-end of the compiler (lexer, parser, semantic analyser). In order to invoke it call:

java -cp %TLA_CLASSPATH% tla2sany.SANY fowler.tla

SANY is currently the only official way to find out, if the specification complies to the rules of the TLA+ language. It is absolutely a non-trivial program, basically because of the complexity of the TLA+ grammar. Especially, the parts responsible for precedence-checking and level-checking are use complex algorithms.

TLATeX

As noticed by Peter, the language has a special notation, which could appear cryptic to someone who see them for the first time. The reason for this is pretty simple: TLA+ is a mathematical language and the ASCII version TLA+ is very close to LaTeX notation of the corresponding mathematical symbols. Everyone, who is aware of LaTeX can read and write TLA+ easily. For others, the ASCII specification can be translated into a TeX file and rendered to a DVI, PS or PDF. A piece of specification of the secret compartment ( download full TLA file), looks as follows rendered as PDF ( download as PDF).
rendered_tla
The question of WYSIWYG editor support involves not only rendering of the symbols (that is the easiest part), but the input of these symbols by the user. Therefor, the ASCII version of TLA (we could also speak about ASCII encoding), which uses at least in certain areas know LaTeX-like encoding is a convenient way for editing specs. There are attempts to create WYSIWYG formula editors, which work pretty good, but the these have to be used with a mouse and the input speed is not comparable with the typing plain LaTeX.

The usage of TLATeX is simple. After the installation of TLA Tools, the TLATeX is invoked from the command line:

java -cp %TLA_CLASSPATH% tla2tex.TLA -shade fowler.tla

The tool produces a .tex file which can be included in the existing document. It also can be rendered directly if LaTeX is installed on machine.

TLC

TLC is a model checker for TLA+ specifications. It’s main purpose is to find bugs in specifications. For this purpose it creates the state-space described in the specification and checks the properties (safety and liveness). In contrast to SANY which is responsible for syntax and static semantics check TLC is checking the dynamic semantics of the specification. At this point I only want to mention, how TLC is invoked. I’ll cover some advanced TLC topics in the later posts:

java -cp %TLA_CLASSPATH% tlc2.TLC fowler.tla

In addition to the TLA file, containing the specification itself, TLC requires a CFG file, which describes the model, that has to be checked. This fact appears unusual to the TLA beginners, but is easy to clarify. The specification of the system is a description of systems behavior. To a given behavior, several models can be constructed. In addition, specifications can be combined resulting in bigger specifications. In the specification, there are no real differencies between actions: (Init, TypeInv, CloseDoor or Spec). Thus, the user has to specify which of these actions are actulally the parts to check.

Tags: , , , , , , , ,