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.

After Microsoft joined OMG the move towards model-driven software development became obvious. Microsoft already put some effort on the development of DSL technologies. But OSLO is something much bigger, so let’s try to predict what it could be….I’m not employed by Microsoft. I’m not working on OSLO. Still, I’m interesting in MDSD and the technology bunch around it. It was difficult to oversee, that Microsoft left the “very confidential” stage and allowed several people to tell a little bit about the OSLO project. The official statement says that OSLO is: a language, a tool, a repository… For me, the questions about these terms have the following priority: language, repository, tool. I think the latter two are the way, how Microsoft will earn money. The language is the most interesting part for me.The advertising machine is running and the Microsoft celebrities are inviting everyone to the Professional Developer Conferences (PDCs):

Don Box

Don Box (here) intoduces an intersting list:

• COM Type libraries
• .NET metadata attributes
• XAML
• OSLO

This means to me, that we speak about a declarative language, with own type system, that allows to develop own types in order to describe entities from my domain. I have no clue, why the link to XAML is present. Maybe, if we speak about a language for data modeling, the representation can be created using XAML.Then Don says, that Microsoft develops a textual internal DSL for modeling. In the same time, he speaks about “visual design” that is applicable to the same model. This seems a little wierd for Microsoft, but is well adopted in Eclipse Ecosystem (e.g with a combination of Xtext and GMF used as two representations linked to the same metamodel). The model repository emerges as a database, which can be compared with Teneo Approach.The next paragraph seems very confusing to me, I’ll try to remove buzzwords out of it: I can write an application by populating the repositry with the definition of my app. Our goal is to make it possible to build apps purely out of data. If not possible, the goal is to make the transition to traditional code easy.

Douglas Purdy

Douglas Purdy is another one who is allowed to natter about OSLO. It seems that the tool chain is pretty ready, because of his wish to use community feedback in order to improve it. Apart of this, he does not reveal any details.

David Chappell

So, I searched a little in the Internet and finally found the following interview with David Chappell. He reveals much more details:

• The language is a designed to create so-called schemas. (or metamodels, how I understood this)
• A schema is something, to that models (schema instances) are conform.
• Both schemas and models (schema instances) are stored in repository.
• There is a way to use the tool (the editor) with both: schemas and schema instances.
• There are some predefined schemas (DSLs, metamodels), which can be used to describe: activities, workslows, systems, etc..
• There are some additional tools that are built upon the DSLs (e.g. process server)

From this point, the OSLO stuff begins to make sense for me. The basic language seems to be a kind of a meta language (meta-meta-model) for definition of DSLs for different purposes. The produced DSLs seems to be defined in a way, that the instances have the same form as the schemas – because of uniform repository and bindings of visual and textual editor. Still, I have no clue how dynamics can be realized.

Darryl K. Tafft

Darryl K. Taft writes on eWeek. Here things gets names, and technical details beging ta make sence. The language is in fact declarative and is called D (has nothing to do with another language called D). Now, after the words of David Chappell, the following text makes more sense: “We’re trying to make it simple to get an idea out of your brain and onto a hard disk” – he is not speaking about a DSL, but about D, which is designed to develop DSLs. Finally, another very important sentence: An Oslo user need not learn the D language to use Oslo, however. “The language is a technical detail for a certain audience,” Lovering said. – this is something clear to me, because you don’t have to understand the DSL definition in order to be able to use a DSL. In addition, if the DSL is both, graphical and textual, you possibly only need to understand the pictures (I argue if the productivity can really be boosted in that way, but this is another story).Then, after I thought that I got the idea, a very strange sentence apears: The Oslo language also is partially based on TLA+, a language developed by Microsoft researcher Leslie Lamport, Lovering said. In fact, I know what TLA+ is, because I used to work with it. TLA+ is untyped formal language for description of dynamics of concurrent systems. It uses actions (arbitary mathematical statements) to describe the change of system behaviour. Leslie Lamport and his team developed a model checker, that can verify temporal and logical properties of the modeled system. The only link I know is tha fact, that Leslie Lamport worked together with David Langworthy, who is working in “Connected Systems Division” and seems to be involved in the development of the D language (he is one of the speaker on PDC).Maybe there is a kind of a action dynamics defined on top of schemas stored in repository. In fact I hope that D is not a behaviour description language.

Mary Jo Foley

Finally, the last source I reviewed for information were several posts ( 1, 2, 3) of Mary Jo Foley.Microsoft is planning to ship a set of predefined schemas within the repository, but customers and software vendors will be able to add their own. – this seems to be the idea of multiple predefined DSLs, because otherwise we will just speak about simple structure of a database.

Summaries

I think in this point of time it does not make sense to gather more sources of OSLO. OSLO seems definitly interesting, and will be published in the end of October. Microsoft entered the modeling arena – this will create a new army of people who understand the words model, DSL and generator. I’m still interesting in the D language: it seams to be declarative, text-based schema definition language with a graphical representation. The defined schemas can somehow be stored in a repository, based on a RDBMS. There are still many open questions like: How to handle dynamics? How to create applications from data? What is the relationship between D and TLA+, I’m familiar with? The best thing is to wait, they will answer the questions soon.