Simon Zambrovski

As 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).

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.

It seems to be popular to write Fowler’s DSL in all languages. I follow this idea and start a series of posts on TLA+ with Fowlers state-machine example coded in TLA+. TLA+ is a specification language developed by Leslie Lamport.  TLA+ is based on Temporal Logic of Actions, which combines logic of actions (denoting the state change of the system) with temporal operators. This specification language allows reasoning on dicrete systems and is quite powerful. It is even more intersting, that the language is equiped with a set of tools. The TLA+ Tools include a Syntax Analyzer (SANY), a Simulator with Model Checker (TLC) and a pretty printer, for creating LaTeX-style representation of the source. The tools are implemented in Java and are published under MS-Research license. The source code of the tools is also available. Since TLA+ is developed by the father of LaTeX, its ASCII representation looks very similar to LaTeX, and is convenient for the input.

(* ************************************ *)
(* Controller of the secret compartment *)
(* of Mrs. H, who loves secrets!        *)
(* Following the example of M. Fowler,  *)
(* which can be found at:               *)
(* http://martinfowler.com/             *)
(* ************************************ *)
------------- MODULE fowler --------------
(* ************************************ *)
(* Variables                            *)
(* ************************************ *)
VARIABLE
  state, \* the state for display, only
         \* to be compliant with  Fowler
  light, \* state of the light
  draw,  \* state of the draw
  panel, \* state of the secret panel
  door   \* state of the entry door

TypeInv ==
(* ************************************ *)
(* Type invariance                      *)
(* ************************************ *)
  /\ state \in { "idle",
                 "active",
                 "waitingForDraw",
                 "waitingForLight",
                 "unlockedPanel" }
  /\ light \in { "on", "off" }
  /\ draw \in { "opened", "closed" }
  /\ door \in { "locked", "unlocked"}
  /\ panel \in { "locked", "unlocked" }

Init ==
(* ************************************ *)
(* Initial state                        *)
(* ************************************ *)
  /\ state = "idle"
  /\ light = "off"
  /\ draw  = "closed"
  /\ door  = "unlocked"
  /\ panel = "locked"
------------------------------------------
(* ************************************ *)
(* Actions                              *)
(* Note that the state variable is not  *)
(* used for the determination of the    *)
(* actual state, but only for display.  *)
(* This shows that this variable        *)
(* is not required in TLA+              *)
(* ************************************ *)

CloseDoor ==
(* ************************************ *)
(* Closes the door, to activate         *)
(* ************************************ *)
  /\ door = "unlocked"
  /\ door' = "locked"
  /\ state' = "active"
  /\ UNCHANGED << panel, light, draw >>

LightOn ==
(* ************************************ *)
(* Switch on the light, if the draw is  *)
(* opened, this opens the secret panel  *)
(* ************************************ *)
  /\ light = "off"
  /\ light' = "on"
  /\ IF draw = "opened" THEN
       /\ state' = "unlockedPanel"
	   /\ panel' = "unlocked"
	   /\ door' = "locked"
	 ELSE
	   /\ state' = "waitingForDraw"
	   /\ UNCHANGED << panel, door >>
  /\ UNCHANGED << draw >>

OpenDraw ==
(* ************************************ *)
(* Open the draw, if the light is on,   *)
(* this opens the secret panel          *)
(* ************************************ *)
  /\ draw = "closed"
  /\ draw' = "opened"
  /\ IF light = "on" THEN
       /\ state' = "unlockedPanel"
	   /\ panel' = "unlocked"
	   /\ door' = "locked"
	 ELSE
	   /\ state' = "waitingForLight"
	   /\ UNCHANGED << panel, door >>
  /\ UNCHANGED << light >>

ClosePanel ==
(* ************************************ *)
(* Closes the secret panel and move the *)
(* system to initial state              *)
(* ************************************ *)
  /\ panel = "unlocked"
  /\ panel' = "locked"
  /\ light' = "off"
  /\ draw' = "closed"
  /\ door' = "unlocked"
  /\ state' = "idle"
------------------------------------------
Next ==
(* ************************************ *)
(* All possible actions                 *)
(* ***********************************  *)
  \/ CloseDoor
  \/ LightOn
  \/ OpenDraw
  \/ ClosePanel

Spec == Init /\ [][Next]_<< panel, light,
  draw, door, state >>

THEOREM Spec => []TypeInv

Inv ==
(* ************************************ *)
(* The panel is never unlocked          *)
(* by opened door                       *)
(* ************************************ *)
  \/ panel = "unlocked" => door = "locked"
  \/ door = "unlocked" => panel = "locked"
==========================================

In order to run a model checker, the configuration file fowler.cfg needs to be created. It says which part of the model is the specification, and what should be checked. In the example above, the specification action is called Spec and states, that if the Init action is executed, the Next action can always be executed by allowing stuttering steps by changing values of the variables panel, light, draw, door and state. The actual property we want to check is the fact, that the compartment is really safe, which means that the secret panel can be unlocked if and only if the door is closed. This is stated in the property Inv which has to be an invariant property of the system.

SPECIFICATION   Spec
INVARIANT       Inv

Running TLC on this specification, with configuration file provided above produced the following output:

TLC2 Version 2.01 of February 23, 2008
Model-checking
Parsing file fowler.tla
Semantic processing of module fowler
Finished computing initial states: 1 distinct state generated.
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic):  2.927345865710862E-18
based on the actual fingerprints:  1.2569902552401487E-14
15 states generated, 9 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.

This means, that it reached all states with very high probability and checked in every state the required property.
The compartment of Martin is safe! Modelchecked by TLC.