August 31, 2014

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.