Wrote a picture review on the digitalexperiment.de about a good picture taken by a friend. As usual for that site, it is written in German and discusses the issues of a macro shots. I try to provide some hints about this kinds of pictures. Especially, the usage of too wide-opened aperture leads not only the background to become smooth, but alos parts of the main subject. The composition is a very subjective thing, but I suggest to make the subject bigger. Regarding the iso-speed used, it is always a goal to keep it as low as possible. I also provide some subjective impressions about the color and framing…Read more
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.
[source lang=”bash”]
(* ************************************ *)
(* 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”
==========================================
[/source]
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.
[source lang=”bash”]
SPECIFICATION Spec
INVARIANT Inv
[/source]
Running TLC on this specification, with configuration file provided above produced the following output:
[source lang=”bash”]
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.
[/source]
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.
Badges
