LODA: From Assembler to Ackermann

We use computational models like Turing machines and λ-calculus to understand the nature of computation. Every undergraduate computer scientist (hopefully) knows that all Turing-complete models and programming languages are essentially equivalent and that any "effectively computable" function can be computed by these models. On the other hand, the halting problem tells us that termination of a Turing machine with a given input is not decidable. In an imperative programming language, this undecidability of termination stems from while-loops. So-called primitive recursive functions on the other hand essentially describe for-loops and are therefore guaranteed to halt. But is there also something in the middle, something between a for-loop and a while-loop?

LODA stands for Lexicographical Order Descent Assembly and is both a minimalistic programming language and a computational model. It consists of only four types of instructions (five if we count syntactic sugar). LODA programs operate on an unbounded sequence of memory registers $0, $1, $2, ... where each of them stores a natural number. The operands of instructions are either constants, direct memory accesses or indirect memory access. There are only two types of arithmetic operations: "add" and "sub". The latter is maybe not exactly what you would expect: since we allow only natural numbers, subtracting a larger value from a smaller value yields 0. Using these two operations, we can also define the assignment instruction "mov X,Y" which overrides the register X with the value of Y. It can be defined simply as "sub X,X" and "add X,Y".

The most interesting part is of course the model of loops in LODA. The language supports so-called "lexicographical order descent loops," which we write using the instructions "lpb X,Y" and "lpe". The interesting thing about these loops is that they are guaranteed to stop for every input and yet that they are more powerful than primitive recursion. This can be shown by implementing the Ackermann function with it.

A somewhat easier example of a LODA program for computing the Fibonacci numbers is shown below. If you are curious how this works and why the expressive power of LODA is "between" for-loops and while-loops, check out the documentation and cool C++ implementation at GitHub.

A Quick View on Compositionality in Graph Pattern Matching

Graph pattern matching is the task of finding all matches (occurrences) of a pattern graph P in a host graph G. Formally, the goal is to compute the set of matches given by {m: P → G | m is a graph homomorphism}. In categorical terms, this is the set Hom(P,G). If we fix the host graph G, we get the functor Hom(_,G): Graph → Set. For any pattern P, Hom(_,G) sends P to the set of matches of P in G. The functor Hom(_,G) is contravariant. Thus, embedding a pattern P in Q means the match set of Q is included in P (modulo a translation of P into Q). In other words, every match of Q in G can be translated into a match of P in G. 

One view of compositionality for graph pattern matching is to decompose a pattern P into a span P₂ ← P₁ → P₃ such that P is the pushout over this span. What does this mean for the corresponding match sets? Well, that's easy to answer now since we know we are dealing with Hom(_,G). If we look at the properties of this functor, we see that it sends colimits to limits. This means also that it maps a pushout of pattern graphs to a pullback of their corresponding match sets. Therefore, we can decompose the pattern matching task by finding the respective match sets of P₁, P₂ and P₃ individually and composing them to the final match set Hom(P₂,G) ×_Hom(P1,G) Hom(P₃,G). With some basic notions from category theory we achieved a quick compositionality result for graph pattern matching, neat.

What is this useful for? It can be used as a basis for operationalization and optimization of graph pattern matching. This has applications in graph databases and model transformations. For scalability of graph pattern matching w.r.t. the size of the host graph, the covariant functor Hom(P,_) is also very interesting.

The observation that a structural model (in this case pattern graphs) is related to its corresponding semantical model (in this case match sets) by a contravariant functor is not at all uncommon. Structure and semantics of behavioral models like Petri nets or Reo connectors are related in a similar way, as they form pairs of adjoint functors. This is not surprising because, as Saunders Mac Lane put it: ‘adjoint functors arise everywhere’.

Aggregations in Henshin

The language concepts of Henshin are based on graph transformations. As such, aggregations have not been in the scope of Henshin so far. Aggregations are well known from relational database systems and are a powerful tool for counting entities, calculating minima / maxima or average values etc.

How do aggregations and graph transformations fit together? Well, in Henshin we know the concept of nested multi-rules. In graph transformation terminology this is often referred to as amalgamation. In essence, a transformation rule is extended with parts that are applied with a for-all semantics. These for-all parts are referred to as the multi-rule, whereas the core part is referred to as the kernel rule. In the graphical editor of Henshin, the multi-rule parts are indicated using *-actions.

Now, the trick for supporting amalgamations in Henshin is to allow to use the values of parameters of multi-rules in the kernel rule. What happens is that for one match of the kernel rule, the multi-rule is matched with for-all semantics, and that its parameter values are exposed to the kernel rule as a collection. This enables the use of aggregations functions in the kernel rule, which combine the values of parameters of the multi-rules.

Consider the two example rules below. Both match one :Family object (kernel rule) and all :Person objects in that family (multi-rule). Now, the set of persons can be used as basis for aggregations. In our two example rules, we use as aggregation functions COUNT and AVG to resp. count the number of family members and calculate the average age of the family members.

Note that the expressions Aggregations.COUNT(x) and Aggregations.AVG(a) are not some special syntax for aggregations. They are just calls to ordinary Java methods. The special thing about these methods is that they take a collection of values as parameters (not single values). The Henshin interpreter just calls the (possibly user-defined) functions to calculate the aggregated values. For the interpreter to know which class to use, it must be defined as part of the Java imports of the rule, as shown in the screenshot below. Additionally, you need to ensure that this class is in the Java classpath when executing the Henshin transformation.

The aggregation support is currently available in the development branch of Henshin. You can find the above rules with accompanying Java code in the examples plugins.

Towards Modeling of Distributed Graph Algorithms

The most prominent approach for distributed processing of very large graphs today is probably the Bulk Synchronous Parallel (BSP) model. BSP is a bridging model for implementing graph algorithms in such a way that they can be massively parallelized and distributed. One application can be found in the Henshin graph transformation tool, where graph transformation systems can be modeled, and code generated for the BSP framework Apache Giraph.

Although the BSP model is widely accepted and used today, there is no standard implementation framework for BSP algorithms. Frameworks that do provide BSP include Google's Pregel, Apache Giraph and GraphX in Apache Spark. For application developers it is not easy to find out which platform is the most suited one for her problem. An implementation of a graph algorithm in, say, Apache Giraph cannot be reused in other frameworks, even though the underlying concepts of BSP are the same. This is unfortunate, particularly because the overhead of developing, deploying and testing these algorithms is rather high due to the complexity of the distributed frameworks.

This problem can be solved by introducing a modeling layer for BSP algorithms. Instead of directly implementing graph algorithms in Pregel, Giraph or GraphX, the idea is to use a modeling language that supports the concepts of BSP. One possible approach is to use UML 2 state machines for the modeling. The figure below shows a state machine for a BSP-model of the shortest path algorithm.

Using such a model, one could generate code for different platforms, e.g. Pregel, Giraph or GraphX. The code generators need to be implemented only once and are straight-forward to build since the BSP concepts are more or less directly used. Using different code generators, algorithm engineers can automatically derive implementations for different platforms and benchmark them against each other without implementing a single line of code.

In Henshin, the code generation for Apache Giraph is quite complex because the concepts of graph transformations are rather different than BSP. One opportunity to simplify it would be to use BSP models as intermediate target language. Specifically, model transformations can be employed to translate a Henshin model into a BSP model. From that point on, platform-specific code generators could be used to generate the final implementation.

Using a modeling approach would enable the reuse of the many many graph algorithms already implemented in the existing BSP-frameworks. Maybe UML state machines are not the best approach for the modeling -- for instance, one could also come up with a (textual) DSL for BSP. The important point is that an abstraction from the actual implementation platforms is made.  

Henshin 1.2

We are happy to announce the release of Henshin 1.2! Henshin is a model / graph transformation tool for EMF models. The new release comes with new features for the graphical editor and a better integration with Apache Giraph.

The graphical editor now supports attribute conditions, which are used to restrict the applicability of transformation rules. In addition, the editor now supports live validation which gives you an immediate warning if you are trying to add an object to two containers or you are using an invalid JavaScript expression etc.

For me the most important new feature of the new version is the improved code generation facilities for Giraph. The new wizard will generate a full-fledged Java-project with all needed libraries, set up a Maven build and even automatically install a local Hadoop test environment if you like. This means that you can model a graph transformation in Henshin and fully automatically generate executable Giraph code that you can directly run in Eclipse. The video below shows you a demo of this new code generator.

Henshin 1.2 is available at our release update site.

Building the Collatz Graph in Henshin

The other day I saw an online video about a number-theoretical problem called the Collatz conjecture. The video included some visualizations of the problem which were based on force-directed graph drawing. It was immediately clear to me that such visualizations could be also easily done in Henshin. So I built a minimalistic EMF model and sketched two simple rules:

The first one multiplies x by 2, the second one is the inverse of the 3x+1 rule. Technically, it is not exactly the inverse of the Collatz function, but the conjecture is still true if and only if these two rules can generate every natural number (if we ignore the upper bound in the first rule).

Finally I created an instance model for the initial state and set up a state space. In the following video you can see how to use Henshin's state space explorer to generate the Collatz graph. Have fun. 

Why Model Transformations != Graph Transformations

Model transformations are probably the most important application of (the formal theory of) graph transformations. This includes classical source-to-target model transformations, bidirectional transformations and synchronizations, as well as in-place rewriting, e.g., for refactoring. All these applications have in common that the underlying graphs to be transformed are actually EMF- or MOF-based structural data models.

These models have of course a graph structure, but when taking a closer look, they are actually more than just that. The higher expressive power of metamodeling languages like EMF or MOF in comparison to simple graphs has some severe implications when trying to apply formal (mathematical) methods known from the graph transformation research community.

Let's take a look at a concrete example of a Henshin transformation. The following rule is a variation of the Bank Accounts example:

This rule collects all accounts which do not belong to any client and adds them to a designated bank for "orphaned" accounts. The graph transformation semantics of this rule does exactly what is shown: it creates zero or more edges between a bank and a number of account objects. In contrast, the EMF-semantics actually has a twist which is not directly visible here: any of the orphaned accounts which before belonged to a different bank object are removed from their original bank. Thus, this rule can actually also delete edges.

This is because in EMF, adding an object to a container also means that it is removed from its old container. Implicit deletion of edges can also occur for edges with multiplicity 1. Another semantical difference to graph transformations exists for the handling of bidirectional references (eOpposite-references). In this case, EMF automatically maintains the opposite references in a consistent state which can have the effect that EMF removes or creates edges. It can actually get more complicated when you have a combination of containment and multiplicity constraints, and opposite edges.

These phenomena can be considered as side effects of rules -- they are actions performed by EMF even if they are not explicitly specified in the transformation rules. Henshin does not prevent these side effects (that is actually not possible), but it will print warning messages when such side effects occur during the execution.

From the EMF / MOF perspective, the described effects are intended and desirable. What is problematic though is to assume that model transformations per se have graph transformation semantics and (what is more dangerous) to apply formal verification methods from the graph transformation domain without taking into account these possible side effects of rules.

There are also other related, partly surprising, phenomena when dealing with EMF models. For example, copying an object does not necessarily yield an identical object, i.e., the expression:

EcoreUtil.equals(eObject, EcoreUtil.copy(eObject))

does not always return true. This is because the copy mechanism in EMF won't make any changes which would alter the original model (e.g. bend an opposite reference).

The lesson learned is that models are more than graphs, and model transformations are more complicated than graph transformations.

Henshin 1.0 (Update)

8 years after the first PoC and 4 years after its official launch, we are proud to announce the release of Henshin 1.0 -- a model transformation language and framework for EMF. Henshin 1.0 is ready for Eclipse Luna and Java 8 (including its new JavaScript engine Nashorn). The primary domain of Henshin is model-driven development and formal verification methods. With its new multi-threaded pattern matching engine and its code generator for Apache Giraph, big data is a new third main domain of Henshin.

The new version of Henshin comes with an extended transformation language with support for specifying Java imports and annotations, and a couple of new utility APIs. Besides the changes under the hood, the 1.0 release also comes with a number of visible new features, including a reworked interpreter wizard and new preferences for the diagram editor. As an eye candy, we also added a new color mode for the diagram editor which goes well together with Luna's Dark theme.

You can obtain Henshin 1.0 from the release update site or clone our Git repo to try it out!

Update from 30-07-2014

And of course we've build a critical bug into the release! Anyway, the fixed version is available at the release update site.

ISA: An Integer Sequence Analyzer

ISA is a proof of concept of an integer sequence analyzer. It consists of a very simple web interface for entering the beginning of an integer sequence. When clicking on Analyze, ISA tries to compute a formula for an infinite sequence that starts with the entered numbers.

Under the hood, ISA uses a term generator to compute (recursive) formulas. These formulas are evaluated and the result is compared with the sequence entered by the user. If no matching formula was found after 30 seconds ISA gives up and times out. To get a feeling what is currently possible, try out the following sequences:

• 0 0 1 1 4 4 9 9
• 2 3 6 18 108
• 1 2 2 3 3 3

The interface and the idea of ISA resembles OEIS which was created by Neil Sloane (former researcher at AT&T Labs). The main difference is that OEIS is a database, whereas ISA is a formula generator.

Since I am using a Raspberry Pi to host and run ISA, some heuristics might be useful to find common sequences more directly. But of course, in general only a tiny class of sequences can be automatically found in this way.

Transformation Tool Contest 2014 -- Call for Solutions

The 2014 Transformation Tool Contest (TTC) seeks your solutions to two challenging transformation problems, involving transforming financial XML models into object-oriented code, and transforming the very large model that underpins the IMDb movie database.

Select your favorite transformation tool and join the contest! The deadline for solution descriptions is 23 April 2014. More information, including links to the problem descriptions, at: http://www.transformation-tool-contest.eu/cfs.html

Just-In-Time Java Compilation in Eclipse

Just-in-time (JIT) compilation is usually applied to get a better execution performance compared to interpreter-based approaches. There are also other scenarios where JIT compilation is useful, e.g., when programming-level code needs to be generated at run-time. Either way, this technique is usually considered to be the domain of experts since it requires a combination of code generation, compilation and dynamic loading and linking. In this post, I show you a simple pipeline based on EMF, JET, JDK and Java core that allows you to do this with minimal effort.

Our starting point is the EMF model (class diagram) shown below. It is a model for simple arithmetic expressions. It consists of an abstract class Term and three concrete implementations of it: Operation, Constant and Parameter.

Below you see an example instance model in the reflective EMF editor. It is basically just a model representation of the expression (3.7 + (p0 * (p1 / 2.0))) where p0 and p1 are parameters. We use here the actual arithmetic operators as enum literals.

The easiest way to evaluate an expression like this one is to write an interpreter which can be as simple as a tree visitor in this case. But today, we want to use a JIT compilation approach to evaluate these expressions. Specifically, given an expression like the one above, we want to generate a Java object that implements this interface:

It contains only one method which evaluates the expression for specific parameter values. The first thing we do is write a pretty-printer that generates a string representation of a term in Java syntax. We extend the EMF-generated Switch class for this:

We get "(3.7 + (params[0] * (params[1] / 2.0)))" if we feed the above Term model into this pretty-printer. Now that we are able to generate the Java expression from Term objects, we just need to generate the rest of the class that will implement the Calculator interface. We use a simple JET template for this, as shown below. There are much more sophisticated template languages, but JET will do just fine in our case.

What is left to do is the actual JIT compilation consisting of three steps:

1. Generate the Java code from a given Term model using JET,
2. Compile the generated Java code using the BatchCompiler of JDK,
3. Dynamically load the compiled calculator class and instantiate it.

The code below does all the three steps. So, again: it takes a Term model and generates an executable calculator instance. Voila, our JIT-compilation.

 
If you would like to try it out yourself, you can check out the complete source code from GitHub.

Parallel Graph Pattern Matching in Henshin (Update)

In my last post, I reported on an improvement of the graph pattern matching algorithm in Henshin that showed a major performance boost for rules where the nodes in the left-hand sides are connected only by <<require>> nodes and edges. As a concrete example, we used the transformation rule below to find couples of actors / actresses in the IMDB movie database which starred together in at least three movies.

Thanks to the tweak in the pattern matching engine we were able to apply this rule to much larger input graphs. Unfortunately, the synthetic test data that we used for our last benchmark does not have the same complexity as the real data from IMDB. In our test data, every person played in not more than 10 movies and every movie had a similarly low number of actors / actresses. In reality, the IMDB data contains movies with more than 1000 actors and obviously also persons that played in a large number of movies.

So I executed our find-couples example on the real IMDB data (thanks for the data import, Tassilo!). Not surprisingly, the results were much worse than for the synthetic data. The reason for this is that the real IMDB data is much more interconnected. So I started tweaking the pattern matcher of Henshin again. Eventually, I realized that I need something more to crack this nut.

SAP Coding Masters 2013

A possible way to improve the performance is to parallelize the graph pattern matching algorithm. In the current development version of Henshin, this is actually implemented! Here is how you can enable it:

int partitions = 10;
EGraph graph = new PartitionedEGraphImpl(model,partitions);
Engine engine = new EngineImpl();
engine.getOptines.put(Engine.OPTION_WORKER_THREADS,
   partitions);

// Execute transformation

engine.shutdown();

You need to use the new implementation of EGraph called PartitionedEGraphImpl. It basically splits up the graph to be transformed into N disjoint partitions. The second change you need to do is to set the number of worker threads in the transformation engine. In theory, this number can be different to the number of partitions, but the easiest setup is to just use the same amount of threads as there are partitions. The third point you need to ensure is that your rule uses *-stereotypes for nodes and edges (essentially it transforms all matches at once). Finally, you should shutdown the engine when your done to get rid of the worker threads.

For the example of finding couples in the IMDB database, this parallel graph pattern matching approach works actually quite well. Below you can see the performance gains achieved on an ordinary desktop computer.

With this new parallel graph pattern matcher in the interpreter, and the recently introduced Giraph code generator, Henshin really is becoming a big-data tool, which I find very exciting.

Update (07 February 2014)

I realized that the performance in absolute number is still quite bad. As I wrote in my earlier post, the optimized match finder uses path constraints to check the existence of the movies which connect the actors. The problem was though that the match finder still made an additional check whether the <<require>> elements exist, i.e., it performed a complete matching of the PAC (positive application condition). This is actually not necessary here because the path constraint is sufficient already.

To fix this problem, I added a static analysis which finds out once in the beginning whether path constraints are enough to check the PAC. This significantly reduces the run-times as you can see below. Using 12 worker threads, the processing of 2 million nodes takes 173 seconds. But to be honest, I have my doubts whether these engine optimizations will be helpful also in other cases.

Nodes	Couples	Time (ms)
499,995	79,470	6,582
1,004,463	244,627	27,239
1,505,143	585,689	87,721
2,000,900	1,017,752	173,142

Path Constraints in Henshin

In our recent paper on the Giraph code generator in Henshin, we conducted some benchmarks using a real-data example. For this we used the publicly available data sets from the IMDB movie database. We parsed the movie, actor and actress records into an EMF model as shown below. Note that I omitted the attributes here for simplicity.

The goal of our transformation on the IMDB data set was to find all pairs of persons (actors or actresses) which starred together in at least three movies. For every such pair we want to create an instance of the Couple class. We used the Henshin rule below to do this. First, note that all nodes / edges have *-actions and thus the rule is applied to all found matches at once. Second, we used <<require*>>-actions for the movies, and not <<preserve*>>. This is important because we want to ensure the existence of these movies, but be don't want to generate separate matches for every combination of movies. There is only one small subtlety in this rule: due to the symmetry of person nodes, we will actually create two couple nodes for every pair. But this could be easily fixed by enforcing an alphabetical order of the persons' names using an attribute condition.

To compare the performance of the Giraph-based engine, we also tried to execute this example with the normal Henshin interpreter. To our surprise, even for a small part of the IMDB data set, the Henshin interpreter was not able to compute a match. To study the problem in a more controlled setting, we defined a small transformation that generates a synthetic test data set of variable size. We then ran the interpreter again and got the following numbers.

Nodes	Couples	Time (ms)
1,700	200	1,625
3,400	400	3,753
5,100	600	7,828
6,800	800	14,386
8,500	1,000	23,301

This looks pretty bad. The input graphs are very small (< 10,000 nodes) and it already takes more than 20 seconds. The main problem is that the execution time grows non-linearly (should be O(n²)) with the size of the input graph. What is the reason for this? Well, the Henshin interpreter first fixes a match for the LHS (<<preserve>> and <<delete>> elements), and after that it tries to match the application conditions (<<require>> and <<forbid>> elements). In our example, this means that it first picks to arbitrary persons, and then checks whether they starred together in 3 movies. Thus. it is basically a brute-force approach that the interpreter runs here.

The pattern matching is implemented in Henshin as a constraint-solving problem. To fix the bad performance of the movies example (and similar problems), we added a new type of constraint to the pattern matching algorithm: path constraints. Path constraints are internally used to check whether there exists a path between two EObjects along a given list of EReferences. The neat thing about these paths is that they can also go via <<require>> nodes. In our example, this indeed works because the movies-reference has an opposite reference: persons. If we now fix one of the two persons, the path constraint via the references [movies, persons] allows the match finder to restrict the solution set for the second person to only those persons who played together with the first one in at least one movie. This drastically prunes the search space which gives us a much better performance.

Nodes	Couples	Time (ms)
1,700	200	133
3,400	400	89
5,100	600	35
6,800	800	36
8,500	1,000	49
...	...	...
170,000	20,000	1,419
850,000	100,000	6,183
1,700,000	200,000	9,836

This looks much better: now we can process 1.7 million nodes in less than 10 seconds. This should be also enough to run the example on the original IMDB data set. The example including the benchmark is part of the examples plug-in of the development version of Henshin.

Henshin + Giraph: Enforced Parallelism

I recently announced the availability of a Giraph code generator for Henshin, which allows you to execute graph transformations in a parallel and distributed manner. It is important to know that there is a fundamental difference in the execution semantics of graph transformations in this approach. Concretely, the application of rules is always maximum parallel, i.e., every rule is always applied to all found matches in parallel. The idea behind this is that we want to enforce the use of parallelism already at the modeling level and to make it hard for developers to use conventional sequential algorithms that cannot be parallelized automatically. For example, the rule AddTriangles below would be applied to all found triangles in parallel. Executing the iterated unit BuildSierpinski to a 3-node triangle therefore generates the full Sierpinski triangle of depth N.

Due to the change in the execution semantics of rules, other existing and also some new modeling concepts specifically tailored for parallel graph transformations become important. For example, vertices and edges with <<require>> and <<forbid>> stereotypes are particularly useful to avoid overlapping matches which could result in inconsistent parallel rule applications. We also introduced concepts that allow you to aggregate over attribute values of all found matches. I will discuss this in more detail in another post.

Henshin + Giraph = Big Data Graph Transformations

Henshin is a graph and model transformation tool for Eclipse that lets you define rules and workflows for transformation in a graphical editor. By default, these transformations are executed using an interpreter on an in-memory EMF model.

Apache Giraph is a distributed and parallel graph processing framework built for high scalability. Giraph is for instance used at Facebook to analyze the underlying graphs of social networks.

So how do Henshin and Giraph fit together? Easy: Henshin provides an expressive graph transformation language with an intuitive graphical syntax. Giraph provides an infrastructure for highly parallel and distributed graph processing. The sort of obvious way of combining the two is to use Henshin as modeling tool and Giraph as execution engine. And that is what we are currently working on.

We implemented a code generator that produces Java code for Giraph from Henshin models. This generated code contains pattern matching code and graph manipulations for rules, and the required coordination to execute transformation units (workflows). The code generation is still an experimental feature but we plan to stabilize it and ship it with the next release of Henshin. We have already a small test suite and conducted some promising benchmarks. More details later.

The Giraph code generator is available in the development version of Henshin (for Eclipse Kepler). You can get it from our nightly build update site or by getting the source code directly.

Parallel State Space Exploration in Henshin

Back from the summer break, I read an interesting article on combining OCL expressions with CTL formulas. Apart from the modeling approach itself, it was interesting to me that the authors used Henshin to generate their state spaces and also compared their modeling and the performance of Henshin's state space generator with GROOVE.

While the GROOVE tool does not really provide an API for its simulator and state space generator, it is fairly easy to do this programmatically in Henshin:

// Set-up:
StateSpace stateSpace = new StateSpaceImpl();
stateSpace.getRules().addAll(rules);
StateSpaceManager manager = 
   new ParallelStateSpaceManager(stateSpace, 4);
manager.createInitialState(new ModelImpl(resource));

// Exploration:
StateSpaceExplorationHelper helper = 
   new StateSpaceExplorationHelper(manager);
helper.doExploration(-1, monitor);

That's it. After you have generated the state space, you can either save it or use a validator to check invariants or to do model checking etc.

The authors of the OCL-meets-CTL paper mention that there is room for improving the performance of Henshin's state space generator, which I fully agree to. Nevertheless, I want to show here that we have put a lot of effort to make Henshin's state space generator as fast as possible. A key difference to GROOVE is that state space generation in Henshin can be parallelized. Let me show you some numbers.

The chart shows the time needed to generate the state space of the dining philosophers example for 10 philosophers. What you can see is that by using multi-threaded state space generation, we obtain a speed-up of factor 3. In absolute numbers, the generator explores around 2000 states per second. That is just half a millisecond to find all rule matches for a state graph, make a copy and transform it for every match, and look up states and update the state space. If you compare it with the performance of the Henshin interpreter itself (see e.g. here), these numbers are top notch. Note also that the speed can be greatly improved simply by increasing the cache sizes of the state space generator (which requires more main memory though).

That being said, there is still of course room for improvement. For example, the scale-up for a high number of processors and threads is not as good as we have hoped. The required locking of the state space seems to be the main bottleneck. The performance can be probably tweaked but it will of course never be as fast as model checkers that work on vector-based data (as opposed to graphs).

Henshin 0.9.10 on its way. We are working on the new version of Henshin which we hope to release in November 2013. It will target and require Eclipse Kepler. The most exciting new feature will be a new execution platform for Henshin transformations. More on this later.

Henshin 0.9.8: Working with Lists

We are happy to announce the release of Henshin 0.9.8! Henshin is a graph-based model transformation language for EMF. Besides a number of bugfixes and performance improvements for the UI, the new version brings support for edge indices, which allow you to work with lists.

Since Henshin is based on graph transformations, it did not allow you to access and manipulate the order of elements in multi-valued references -- until now. This was in fact a design choice, because in most cases we do not care about the order of elements. There are models and applications though were the order matters and is in fact crucial for the semantics of the models. The standard example that comes to my mind is if you build a model from a textual language. There it is natural to represent the order of statements or commands in a list. For example, JaMoPP constructs models from Java source code and in these models, the order of, say, statements is crucial. And of course, we want to be able to apply Henshin to such models as well, e.g., to implement program transformations like refactorings, translations to other languages, or to define an operational semantics (essentially building an interpreter).

Henshin 0.9.8 comes with a new feature called edge indices, which allow you to access and manipulate the order of elements in multi-valued references. We added a new string attribute called index to the Edge class which you can use to specify an expression that evaluates to an integer. In the graphical editor, we use an array notation to specify the indices. For example, if you have an edge of type ref, you could write ref[0] to access the first element in the reference list. We adopted a notation from Python where negative indices can be used to access elements starting from the end of the list, e.g., ref[-1] matches the last element of any list.

If your rule has a parameter i, you can write ref[i] to match the i-th element. Note that if no value for i is passed as a parameter, the match finder will try to find a valid value for you such that a match of the graph pattern can be found. You can also define a change in the index, i.e., you can move elements in a list. For example, if you have parameters i and j, you can write ref[i->j] to move the element at position i to the position j. The rule swap in the screenshot shows an example for this. It matches two EClasses with names x and y in a package and swaps their positions in the eClassifiers reference list if (and only if) the condition (i<j) && (x>y) holds where (x>y) refers to the lexicographical order of strings (JavaScript syntax). Thus, if we apply this rule in a loop, we achieve a sorting of the EClasses in the package by their names. Note that the engine will match all parameters automatically.

Let me say that it is not our intent to implement sorting algorithms (or any other algorithms for that matter) in Henshin. Henshin rules are declarative in nature and not designed for doing such things. Nevertheless, it is important that we can deal with lists in Henshin in order to apply it to order-sensitive models like program models.

Henshin 0.9.8 is available at our release update site and the above sorting example can be found in the examples plugin shipped with the release (or as available in our source code repository).

Copying EMF models with Henshin

Copying arbitrary EMF models is an easy task using the EMF utils class: a simple EcoreUtil.copy(obj) does the job. This method uses the reflective API of EMF to copy EObjects including their type information and all their features. In Henshin, model transformations are statically typed. Therefore, it is not obvious how to realize such a generic copy functionality that works for any EObject. One way to do it anyway is using the recently introduced wrapper model. The idea is that every EObject is wrapped by a WObject which contains metadata information as normal structural features. This allows us to set and modify the type of a WObject without the need to know its type at design time. In a similar way, we can access and change the types and values of structural features. We can use the wrappers to specify a copy-transformation as follows.

We first create for every WObject another WObject of the same type. We then copy all WValues of the WObjects, and then all the WLinks between the WObject. The wrapper objects automatically reflect these changes in the wrapped EObjects. In this way, we realized a generic copy function in Henshin. Note that the goal was not to implement a better copy method than provided in EcoreUtil (I don't think that's actually possible). We just want to show how dynamic typing in Henshin truely increases the expressiveness and the flexibility of the language. The copy transformation can be found in Henshin's examples plug-in.

Dynamic Adaptation in Ant Colonies and Robot Swarms

A particular interesting engineering discipline is the area of materials and technologies that are inspired by nature, e.g. the surface of a Lotus flower or robots which look and behave like animals. For example, last X-mas I got this cute little robot bug which reacts on noises and tries to walk around obstacles on its path.

Interestingly, nature is an inspiration not only in technological areas, but also in theoretical computer science, specifically in the designing of algorithms. The first thing that comes to mind are of course evolutionary algorithms. Another area where ideas from nature are borrowed is swarm intelligence. One specific example of swarm intelligence are so-called ant colony optimization algorithms. The problem solved by such algorithms is that a colony of ants needs to find the shortest path from their nest (N) to a food place (F), as shown below.

Initially, all ants walk around randomly until some of them stumble on the food place, get some food and walk back to the nest. When moving around, the ants leave a pheromone trail. Other ants that pass such trails tend to give up there random exploration and follow the pheromone trail instead, thereby intensifying the trail. On the other hand the pheromones evaporate. That means the longer the path to the food place, the more time there is for the pheromones to evaporate. Thus, the percentage of ants taking the shorter path increases until eventually almost all ants use the shorter path. Using this simple trick, the ants manage to find the shortest path from the nest to the food place without any further coordination.

Such randomized optimization algorithms are also appealing for coordinating robots. But the immediate problem is that there is no equivalent notion for the pheromone trails produced by ants. One possible solution that works without pheromones is the so-called majority rule. The idea is that the robots travel around in teams of size 3. These teams are formed randomly in the nest. Every time a team is formed, they make a majority vote which path they should choose. All team members change their opinion to the elected path and travel to the food place and back. Since the teams are formed randomly, the system will reach a steady state where all robots agreed on one path. Similarly to the ant optimization algorithm, the shortest path has the highest probability to be chosen by the robot swarm. 

While this is a neat algorithm for finding an optimal path without any orchestration, there is one problem to it: it is not adaptable. That means, if due to some change in the environment suddenly the longer path becomes the shorter one, then the robot swarm will stick to its chosen path and not change to the new shorter one. This is because there is no robot left that could seed a drift to the new path.

We investigated two possibilities to make the majority rule adaptive. The first one is called the Switch scheme: if there is a team where all members already believe that the same path is the right one, they switch with a small probability to the other path. The second approach is the so-called MinPop scheme: a small population of the agents is stubborn, i.e. they take part in the voting, but they do not change their opinion. We modeled both approaches as discrete-time Markov chains (DTMCs) and fed the models into PRISM to analyze them. Below you can see the result.

One the top, you can see the efficiency of both schemes, i.e., what is the probability of an agent going down the right path. On the bottom, you can see the adaption times of both schemes, i.e., how much time it takes two turn a complete A-path population into a B-path population. The main thing to observe is that there is a trade-off between efficiency and adaptivity. The more adaptive a protocol is, the less efficient it is. We also compared Swtich and MinPop regarding this trade-off and it looks like the MinPop scheme performs better than the Switch scheme.

The details are described in a short paper by Erik and Pim de Vink and myself, which appeared in the pre-proceedings of QAPL 2013. I want to use the chance to thank Erik for pointing me to this very interesting research area.

Dynamic Types for Henshin

One of the great strengths of EMF is its reflective API and the fact that you can dynamically create models and instances of it without generating any code. Dynamic EMF is really powerful but there are some limitations and common pitfalls. For one, you should be careful when mixing dynamic and static models. Another thing to be careful about is that once you've defined a dynamic EMF model and you have created instances of it, you should beware of making any (structural) changes to the model because there is a good chance that it will invalidate your instances and maybe even cause run-time exceptions. Changing the model while working with instances of it seems to be something that you would not really do in practice, but there are actually applications where this is useful and desirable, e.g. metamodel evolution and instance model migration.

In Henshin, the metamodels are usually fixed and actually required to be known at design-time. That basically means that rules and transformations in Henshin are statically typed. To overcome this limitation, we recently came up with a new way to support dynamic types and metamodel changes. The idea is to use wrappers for instance models which allow us to connect the instance model and the metamodel levels using ordinary structural features. You should not be surprised that we defined these wrappers as yet another EMF model:

A WObject wraps an EObject, WLinks represent instances of EReferences, and WValues specific data values. The default implementation of the wrappers propagates all consistent changes to the wrappers or the metamodel down to the EObjects. Using this model in Henshin allows us to define dynamically typed transformation rules. Let's have a look at the following two example rules.

The first one is an ordinary (statically typed) rule which matches an object a of type A such that the name attribute of a is x and creates an object b of type B and a link of type ref from a to b. The second rule is semantically equivalent, but here we use wrappers. The top row matches the metamodel elements, i.e. two EClasses named "A" and "B", an EReference named "ref" and an EAttribute named "att". The lower part represents the instances of these metamodel elements (modeled using wrappers).

There are important differences in the expressive power between the two approaches: for statically typed rules, the metamodel is fixed and must be known at design-time. In the dynamic approach, the metamodel elements are matched at run-time. This allows us to dynamically create and modify instances, and even to make changes to the metamodel while there are instances of it, as done in the following rule:

This rule deletes the ref-EReference from the metamodel. In addition, all links of this type are removed from all instance models. The deletion of all links is realized using the *-operator (multi-rules in Henshin). Note that we did not connect the wrapper objects with the EClasses using type-references because we also want to handle instances of subclasses of A and B.

This is only a small example, but I think it already shows the potential of the approach. We have described this approach and its use for defining coupled metamodel and instance model evolution in a paper accepted for ICMT 2013. The wrapper model is shipped with the current release of Henshin (0.9.6) together with two examples: one for copying arbitrary EMF models and one on coupled evolution.