日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

Bidirectionizing Model Transformation
Languages through Partial Translation∗
Soichiro Hidaka

Massimo Tisi

While most model-transformation languages in Model-Driven Engineering are unidirectional, bidirectionality
is a valuable property in a number of applicative contexts where artifacts need two-way synchronization.
Several bidirectional transformation engines have been developed in various research communities, but thebidirectional semantics of a model transformation is generally considered more diﬃcult to express and predictcompared to the unidirectional case.
In this paper we propose a method to partially bidirectionalize existing unidirectional languages bycompilation towards bidirectional languages and coupled execution of the two language engines. Users write
the forward direction of their transformations in the same unidirectional language they are used to, andobtain a system that (besides performing the complete forward transformation) can automatically propagate
in the backward direction a well-defined subset of the target updates. The method does not require any
ad-hoc modification to the two transformation engines, and has clear well-behavedness properties that makethe behavior of the combined system predictable. The approach is exemplified by bidirectionalizing the ATL
model-transformation language on top of the GRoundTram bidirectional graph-transformation system.

1 Introduction
In the field of Model-Driven Engineering (MDE),
model-transformation languages (MTLs) have been
designed to facilitate the expression of relationships
between models, in the form of transformation
rules [5]. Transformation engines apply such rules
to automatically generate new models or update
existing ones, keeping the transformation’s source
and target models consistent. In several applications, synchronization between models needs to be
bidirectional, as modifications can be performed inboth sides of the transformation and global consistency has to be guaranteed. For this reason
several bidirectional transformation languages havebeen developed, both within and outside the MDE
community [17]. However, taking into account the∗ This is an unrefereed paper.

Copyrights belong to
the Authors.
部分翻訳に基づくモデル変換言語の双方向化
日高 宗一郎, 法政大学情報科学部, Faculty of Computerand Information Sciences, Hosei University.
マシモ ティージー, AtlanMod チーム (フランス国立情報学自動制御研究所, 国立高等鉱業学校ナント校, LINA),
AtlanMod team (Inria, Mines Nantes, LINA).

bidirectional semantics during the development of
the model transformation adds a significant layerof complexity to the transformation design: execution properties of a bidirectional system are generally more complex and it is more diﬃcult for thedeveloper to predict the exact system behavior [8].
Because of this, several MTLs are unidirectional,
and focus on providing an eﬃcient solution for theunidirectional scenario. It is still possible to achievebidirectionality in these languages, by separately
writing two opposite transformations. However thisraises other reasons of complexity, since users needto verify case by case the consistency of the two
unidirectional transformations, and keep their evolution coupled.
An alternative approach for the application ofunidirectional transformation languages to bidirectional scenarios is the bidirectionalization of theunidirectional language [25] [31]. In this approach,users write one direction of the transformation byusing the unidirectional transformation language
they are used to. The language is overloaded witha bidirectional semantics so that the resulting system is equivalent to the unidirectional system in theforward direction, but it exhibits the additional ca-

pability of propagating in the backward direction aset of changes to the target models. Full bidirectionalization of the unidirectional model transformation is in general not possible without imposing
restrictions to the model transformation language,
and existing work [27] is mainly focused on extending the part of the unidirectional language that isbidirectionalized.
Instead of focusing on maximizing the extent of
the bidirectionalization, this paper proposes a coupled execution of unidirectional and bidirectionaltransformation engines. The user writes a unidirectional transformation in an existing unidirectional
language, and the unidirectional transformation engine performs the complete forward transformation
with its full expressiveness. A transformation compiler translates part of the unidirectional transformation into an equivalent transformation in an existing bidirectional language. The unidirectionaland bidirectional transformation engines are executed in parallel and the system performs seamless synchronization between the respective models. The semantic gap caused by partial compilation makes the full system alignment challenging.
With respect to related work, our approach: 1)
does not require restrictions to the forward transformation semantics; 2) clearly distinguishes theparts of the target models whose updates are subject to backward-propagation by the underlying
bidirectional transformation engine; 3) does not require modifications to any of the two engines involved; 4) exhibits a easily user-predictable behavior (formally it satisfies a variation of wellbehavedness property from [4]). We define theconditions for the applicability of our approach interms of properties that need to be respected by
the two transformation engines and by the partial translation. We show that a system respecting these properties can support a useful set of
backward-propagable updates.
We exemplify the proposed approach by building
a bidirectionalized version of the ATL model transformation language [19], on top of the GRoundTram [13] [14] bidirectional graph-transformation
system by partially translating ATL to UnQL [2],the graph transformation language bidirectionalized [12] in the GRoundTram system. The resulting
tool is a contribution of its own and its source code

Package+name = String

ownedElements

Attribute

0..*Classifier

type1+name = String+name = String+multivalued = Boolean
attr

Datatype

Class

0..*

owner

Fig. 1: Class diagram metamodelis freely available at the paper page†1 . The page
contains also a technical report [16] that extends
this paper with technical details.
The paper is structured as follows: Section 2 introduces a running case for the paper; Section 3
gives a general description of the approach and Section 4 formalizes its main properties; Section 5 illustrates the integration of ATL and GRoundTram;
Section 6 compares the approach with related work
and Section 7 concludes the paper.

2 Running Case
2. 1 User scenario
Our research eﬀort aims at simplifying the coupled evolution of model artifacts in MDE, hence it
is applicable whenever some models are maintainedand evolve while staying consistent with each other.
To illustrate our approach, we refer in this paper
to a simple example that considers two models: a
UML class diagram and a relational schema. We
can imagine, e.g., that the class diagram is modeling the code of an object-oriented program and therelational schema (that models tables in a relational
database) represents its persistence layer. The user
wants to develop a model-to-model transformation(MMT) to express the relation between the UML
classes of the application’s data model and the relational tables, according to an object-persistence
policy. The transformation computes which tables
and attributes to produce for each UML element.
Figures 1 and 2 show the source and target metamodels of the transformation, while Fig. 3 shows
an instance of each metamodel†2 .
We suppose that both the class model and the re†1 https://github.com/atlanmod/ATLGT.
†2 While in figure we show models in their abstract
object-diagram notation, we can imagine them tobe rendered in their particular graphical concrete
syntax by the editing tools.

Schema+name = String

ownedElements 0..*

Table
+name = String

col
0..*

Columnkey +name = String
0..1

type
0..1

Type
+name = String

Fig. 2: Relational metamodel
lational schema may be manually edited during theapplication development or maintenance, depending on the user background (software architect or
database expert) or the preferred tool (UML diagram editor or database editor). While application
code will have to be manually evolved, an automated system should make sure that classes andtables of the data model are always synchronized.
Hence our scenario requires a MMT system working in two directions.
While bidirectional MMT systems exist thatwould fit this scenario, they require the representation of consistency by a bidirectional transformation language. In this paper we propose an alternative approach that allows the user to specify the transformation using a unidirectional language. Depending on the particular unidirectional
language, the user may prefer it because of higher
expressive power, simpler semantics or just familiarity.
We propose to address the two synchronisation
directions by using diﬀerent tools:
Forward: The user writes the forward transformation using a unidirectional MMT language
and the unidirectional engine performs forward
transformation.
Backward: Part of the forward transformation istransparently compiled into a bidirectionaltransformation language. A bidirectional engine performs backward propagation of target
updates.
In the following we describe the two transformation engines we selected for our experimentation:
the unidirectional ATL model-transformation engine [19] and the bidirectional GRoundTram graphtransformation engine [12] [13] [14].
2. 2 ATLIn our example the user develops in the ATL language the simple MMT transformation in Listing 1

that transforms the left side of Fig. 3 into its rightside†3 .
An ATL transformation (module) is constituted
by a set of rules that describe how elements of thetarget model are generated when patterns in thesource model are matched. The Object Constraint
Language OCL [32] is used as expression languagein the transformation rules. Rules are composedof an input pattern and an output pattern. Input
patterns are associated with OCL guards that impose conditions on the input elements matched by
the input pattern. Output patterns are associatedwith bindings, OCL expressions that define how toinitialize properties of the elements created by theoutput pattern.
E.g., the rule SingleValuedAttribute2Column(lines 28-38) selects input model elements of type
Attribute (line 30) and transforms them into output elements of type Column (line 33). A guard(line 31) imposes to match only attributes thatare not multivalued (multivalued attributes would
have a more complex representation in the relational schema). A first binding (line 34) computes
the column name as the concatenation of class andattribute name; a second one (line 35) imposesthat the owner of the Column corresponds to theowner of the Attribute; a third one (lines 36-37)
states that if the attribute has a primitive type
(DataType) then the type of the column should correspond to the type of the attribute (String otherwise).
Rule Class2Table (lines 20-27) creates a table foreach class, initialises the list of columns with the respectively transformed attributes (line 25), and selects as table key the attribute whose name ends by
the string Id, if any (line 26). Rule DataType2Type(lines 12-19) copies into relational types the class
diagram types, but only if no class exists with thesame name of the type, to avoid conflicts. Finally, rule Package2Schema (lines 3-11) transforms
all non-empty packages into relational schemas and†3 This transformation code is inspired from theClass2Relational case study (http://sosym.dcs.
kcl.ac.uk/events/mtip05), the de-facto standard example for model transformations, but simplified and adapted for illustrative purpose. Notably this version of the transformation does notsupport multivalued attributes in the class diagram.

1

module C l a s s 2 R e l a t i o n a l ;2create O U T

3

rule

:

R e l a t i o n a l from I NClassDiagram ;

from

4

p : ClassDiagram ! Package

5( not p . ownedElements . isEmpty () )

6

to

7

out : Relational ! Schema

8( n a m e <−p . n a m e ,9o w n e d E l e m e n t s <−p . o w n e d E l e m e n t s )

10
11

}

12

rule

DataType2Type {

from

13

d : ClassDiagram ! DataType

14( ClassDiagram ! Class . allInstances ()15−>s e l e c t ( c16|c . n a m e = d . n a m e )−>i s E m p t y ( ) )to17t : Relational ! Type

18
19

}

20

rule

( n a m e <−d . n a m e )Class2Table {

from

21

c : ClassDiagram ! Class

22

to

23

t : Relational ! Table24( n a m e <−c . n a m e ,25

c o l <−c . a t t r ,k e y <−c . a t t r −>s e l e c t ( a

26
27

}

28

rule

|

a . name . e n d s W i t h ( ’ Id ’ ) ) )SingleValuedAttribute2Column {

from

29

a : ClassDiagram ! Attribute30( not a . multivalued )

31

to

32

c : Relational ! Column

33( n a m e <−a . o w n e r . n a m e+’ _ ’+a . n a m e ,3435

o w n e r <−a . o w n e r ,36

t y p e <−i f

a . type . oclIsTypeOf ( ClassDiagram ! DataType )then a . t y p e

37
38

:

Package2Schema{

else

thisModule . stringType

endif )}

Listing 1: Class2Relational in ATL

initializes their list of tables.
Note that ATL rules implicitly interact for generating cross-references among target model elements. E.g., at line 25 the binding col<-c.attr
states that the columns (col) of the table to generate correspond to the attributes (attr) of thematched class (c): in practice, the result of thetransformation of these attributes, by any rule, will
be added as a column of the table.
Listing 1 exemplifies the core subset of the ATL
language, for an illustration of the complete lan-

guage we refer the reader to [19].
2. 3 GRoundTram
GRoundTram is an integrated framework fordeveloping well-behaved bidirectional transformations expressed in the language UnQL [2]. Figure 4
shows the syntax of UnQL. It has templates (T ) at
the top level to produce rooted graphs with labeled(L) branches ({L : T, . . . , L : T }), union of templates (T ∪T ), graph variable reference ($g), conditionals, SQL-like select (select) queries with bind-

: Package: Schemaname = ’Families’

name = ’Families’
ownedElements

ownedElements: Attribute

type: Class

attr: Class: Table: Column

name = ’Person’

name = ’Family’

name = ’Person family’

name = ’family’

name = ’Family’

multivalued = false
attr

type
attr

attr

: AttributeownedElements

ownedElements: Attribute

attr: Tablename = ’Person’

attr

attr

: Column: Column

key: Attributename = ’personId’

name = ’name’

name = ’members’
multivalued = true
type

type

: DataTypename = ’Person personId’

name = ’Family name’
type

multivalued = false

multivalued = false

type

type
: Typename = String

name = String

Fig. 3: Sample ClassDiagram model and corresponding Relational model (shown in object-diagram
syntax). Corresponding elements have the same position in the two models. Updates to elements withdashed lines are not backward-propagable.

(template)T(binding)(condition)

B::=
BC ::=||
L::=
Lp ::=
Gp ::=
Rp ::=|(label)(label pattern)(graph pattern)(regular path pat.)

::=
|
|
|

{L : T, . . . , L : T } | T ∪ T$g | if BC then T else T
select T where B, . . . , B
letrec sfun fname(L : $G)= . . . in fname(T )Gp in T | BC
not BC | BC and BC
BC or BC | L = L
isEmpty(T )$l | a$l | Rp$G | {Lp : Gp, . . . , Lp : Gp}a || Rp.Rp | (Rp|Rp)
Rp? | Rp∗ | Rp+

Fig. 4: Syntax of UnQL
ings (B), and structural recursion (sfun). Bindings include graph pattern matching (Gp in $G)
and Boolean conditions (BC). Conditions include
usual logical connectives, label equality and emptyness check isEmpty(T ) which is true if there is
at least one edge reachable from the root of thegraph generated by T . Label expressions include
label constants and variable ($l ) bound by the label patterns in the graph patterns and the argument of structural recursion. Graph patterns bindthe entire subgraph $G or labels on the branches
and following subgraphs {Lp : Gp, . . . , Lp : Gp}.
Label patterns may include regular expressions of
the labels (Rp) along the path traversing multiple
edges.
Listing 2 shows the UnQL transformation that
corresponds to the bidirectional part of the ATL
transformation in Listing 1. It transforms thegraph encoding of the Class model in the left sideof Fig. 3 to the graph encoding of the Relationalmodel in the right side, without the dotted part.

The transformation consists of structural recursion functions (sfuns). In the listing, the lastdefinition (function Class2Relational at lines 1331) is the main function that corresponds to the
ATL module Class2Relational. Its clauses generate elements according to diﬀerent ATL rules —Package2Schema (lines 14-19), Class2Table (lines
20-22), and SingleValuedAttribute2Column (lines
23-30). As described in Section 3, the clausefor DataType2Type is missing by intention, as todemonstrate the partiality of the translation. References between target elements are represented
by definition and call of sibling mutually-recursivefunctions: ownedElements Package2Schema calledat line 17 for the reference ownedElements in therule package2Schema (lines 2-5), col Class2Table
called at line 22 for col in the rule Class2Table(lines 6-8), and owner SingleAttribute2Column
called at line 30 for owner in the rule SingleAttribute2Column (lines 9-12). Several calls and definitions for other bindings are again missing byintention. The three SQL-like select expressions(lines 18, 21 and 27) perform shallow copy of primitive data type values by capturing the subgraphunder label name and creating the new edge withthe same label and the same subgraph. The conditional expressions if (lines 15-19 and 24-30) withthe graph emptiness predicate isEmpty check theexistence of particular subgraph patterns, and areused to express the ATL guards. The where clauseallows regular expressions on labels like multivalued.Boolean (line 25) for complex pattern matching: we use it to encode traversals of attributes andreferences in OCL expressions.

1 select2
3

letrec sfuno w n e d E l e m e n t s _ P a c k a g e 2 S c h e m a ({ o w n e d E l e m e n t s : $g })= { o w n e d E l e m e n t s : C l a s s 2 R e l a t i o n a l ($g )}| o w n e d E l e m e n t s _ P a c k a g e 2 S c h e m a ({$l : $g }) = {}6 and sfun
7
c o l _ C l a s s 2 T a b l e ({ a t t r : $g }) = { c o l : C l a s s 2 R e l a t i o n a l ($g )}8| c o l _ C l a s s 2 T a b l e ({$l : $g }) = {}9 and sfun
10o w n e r _ S i n g l e A t t r i b u t e 2 C o l u m n ({ o w n e r : $g })11= { o w n e r : C l a s s 2 R e l a t i o n a l ($g )}12| o w n e r _ S i n g l e A t t r i b u t e 2 C o l u m n ({$l : $g }) = {}13 and sfun (* main function *)14
C l a s s 2 R e l a t i o n a l ({ P a c k a g e : $g })=15
i f (not isEmpty(
16
select { d u m m y :{}} where { o w n e d E l e m e n t s : $g} in $g )17
then { S c h e m a : ( o w n e d E l e m e n t s _ P a c k a g e 2 S c h e m a ($g )18∪ (select { n a m e : $g} where { n a m e : $g} in $g ))}19
else {}
20| C l a s s 2 R e l a t i o n a l ({ C l a s s : $g })=21{ T a b l e : ( ( select { n a m e : $g} where { n a m e : $g} in $g )22
∪ c o l _ C l a s s 2 T a b l e ($g ))}23| C l a s s 2 R e l a t i o n a l ({ A t t r i b u t e : $g }) =24
i f isEmpty(select { d u m m y :{}}
25
where { m u l t i v a l u e d . B o o l e a n : $g ′ } in $g ,26
{ t r u e : $d} in $g ′ ) then27
{ C o l u m n : ( ( select { n a m e :{ S t r i n g :{$on ˆ $n}}}28
where { o w n e r . _ n a m e . S t r i n g :{$on : $d}} in $g ,29
{ n a m e . S t r i n g :{$n : $d}} in $g )30
∪ o w n e r _ S i n g l e A t t r i b u t e 2 C o l u m n ($g ))} else {}31 in C l a s s 2 R e l a t i o n a l ($db )4

5

Listing 2: Class2Relational transformation in UnQL

GRoundTram extends UnQL as UnQL+ to support more user-friendly syntactic sugars [15] [14] but
this paper does not depend on the extension.

3 Overview of the Approach
Our strategy for bidirectionalization is to combine a popular and powerful unidirectional modeltransformation language with an existing bidirectional transformation language with well-definedbidirectional properties. The user writes the transformation in the unidirectional language and does
not need any knowledge of the bidirectional language, since the bidirectional system is executedcompletely behind the scenes. The bidirectionaltransformation language may sacrifice expressive
power for the capability of back-propagating updates on the target. We tolerate the expressivity
gap between the two languages by partially trans-

lating the unidirectional transformation language
into the bidirectional transformation language.
Fig. 5 shows a global view on our approach. We
run the unidirectional (UX in figure) and bidirectional (BX in figure) transformation systems
in parallel, maintaining their artifacts in separate
technical spaces. Because of partial translation
the UX and BX transformations are not equivalentand our challenge is providing a generic method
to keep the two transformation systems consistent
with each other. Thanks to such synchronization
the user of our example will be able to generate therelational model in Figure 3, to update it (e.g., byrenaming a table or adding a column) and to see
the change propagated to the class diagram (correspondingly, as a renamed class or an added attribute).
A full system roundtrip starts from a source

UX Transf.
Target Update

TracerUX
Technical
Space

Source ModelUX to BX
Data Model

BX
Technical
Space

Source Model

UX Transf.

Target Model

Updatedw/ Traces

w/ Traces

Model w/ Traces

Partial UX to BX

UX to BX

Transl.

Data Model

TargetBX Fwd Transf.

Target SubModel

Updatedw/ Traces

w/ Traces

Model w/ Traces

Target

BX Bwd Transf.
w/ Traces

Fig. 5: Overview of the approach (models are rectangles, transformations are rounded rectangles andHOTs are double rounded rectangles)
model in one of the two technical spaces. When thetransformation languages have diﬀerent data models, we need a clearly defined bidirectional transformation (UX to BX Data Model ) between thesedata models.
Once the correspondence among the data models
is defined, we need a mechanism to align the execution of the two engines. Our solution is the injection of a stable generation of model element identifiers within the unidirectional transformation (UXTransf.). The generation is loosely-coupled [18] inthe sense that the translation logic remains unchanged while the identifier-generation logic is injected transparently via the Tracer higher-ordertransformation (HOT) [30]. The resulting transformation (UX Transf. w/ Traces) is executed on thesource model to produce a target model with stable traceability information. Stability here means
that, given identical input model and transformation, identical identifiers are produced. In our example the Tracer HOT augments the rules in Listing 1 with bindings computing element identifiers.
Listing 3 shows the result for rule Class2Table as it
would appear in UX Transf. w/ Traces: the binding at line 7 assigns an identifier to the newly created table, computed by concatenating the identifier of the matched Class (c. xmiID ), the name of
the rule (Class2Table) and the name of the output
pattern element (t).
The unidirectional transformation is then translated to the bidirectional language by a translation
HOT (Partial UX to BX Transl.). It is important

to note that the trace generation logic embedded in
the unidirectional transformation is also translated
to the bidirectional transformation language, generating identical model element identifiers (BX Fwd
Transf. w/ Traces). In this way we are able to retrieve corresponding elements in the two technicalspaces by coincident identifiers. In the running example, Listing 4 is translated from Listing 3, andlines 10-11 generate the new id of the model element, being the direct translation of line 7 in Listing 3.
In our example, the correspondence between the
Listings 1 and 2 highlights the partiality of the
UX to BX HOT at both the rule level and thebinding level. We assume that ATL rules withcomplex guards are not translatable in UnQL:
e.g., in Listing 2 we have no corresponding clause
for the rule DataType2Type because the current
ATL to UnQL compiler can not translate the
OCL operation allInstances(). Analogously weassume that complex bindings are not translatable: e.g., the bindings of key and type, respectively in the rules Class2Table and SingleValuedAttribute2Column, are not translated to Listing 2,
since string comprehension and type introspection
is not supported by the current ATL to UnQL compiler.
Given the partiality of the translation, the target
model of the forward bidirectional transformation
is in general diﬀerent from the target model of theoriginal unidirectional one. However we impose astrict property to the partial translation: the tar-get models generated from the bidirectional transformation need to be strictly included in the target
models of the unidirectional system. The property
will be formally discussed in the next section, butintuitively it aims to provide a clear separation of
updatable and not updatable parts in the target
model and make the system user-predictable. In
the running case, the elements depicted with continuous lines in the right side of Fig. 3 are common to the target models of both the systems.
The elements with dashed lines (Type elements,
key references and type references) are exclusively
produced by the unidirectional language, since the
ATL code that produces them is not translated
to UnQL (respectively, DataType2Type rule, typebinding, key binding). Submodel†4 matching is
guided by the identifiers produced in the previous
step. In our current approach the target model editor uses this information to forbid updates to thenon-propagable part.
Finally, the cycle in Fig. 5 closes by receiving
updates to the propagable part of the target model(Target Update), and transforming the updated
target model to the bidirectional system (UX to
BX Data Model ). The bidirectional system willthen be able to apply backward transformation (BX
Bwd Transf. w/ Traces) to update the source,by taking into account the source model, target
submodel and updated version of the target model,
and maintaining the identifier correspondence.

4 Well-Behavedness

under

PartialTranslation
In our approach only a subset of the unidirectional transformation language LU is translated,since not all the language constructs can be bidirectionalized due to the limited expressive powerof the target language. In this section we formally
prove that the global system we described in Fig. 5
is well-behaved [4] if its components respect certain conditions. Intuitively these conditions require
that: 1) LU respects a modularity property that
we call rule additivity, 2) we can build a bijective
transformation between the data models of LU andthe underlying bidirectional language LB , 3) we canbuild a translator of the part of LU to LB such
†4 Definition of submodel is given in Sec. 4.

that the models produced by transformations in LB
coincide with the ones produced by corresponding(partial) transformations in LU , and 4) LB is wellbehaved. The four conditions for applicability are
suﬃcient for coupling any two transformation systems. Thanks to these properties we are able toreflect updates to the target model of the unidirectional system by passing through the bidirectional
system.
In the next section we will present evidence ofthe practical applicability of the approach by showing that these four properties are satisfied by ATL,
GRoundTram and the translation we have built.
However the four conditions are satisfied by severaltransformation systems in model-driven engineering. In particular: 1) Property 1 is satisfied byother popular UX model-transformation languages
besides ATL (e.g., Epsilon ETL [21]), 2) Property 2 is easily satisfiable by encoding models in
low level representations, like well-known encodingof node-labeled graphs by edge-labeled graphs, 3)given Property 2, Property 3 is satisfiable by designof the translator (this requires a significant eﬀort,
in general depending on the chosen languages), 4)
Property 4 (or analogous) is common among BX
languages [4].
We first recap the notion of well-behavedness [4],that intuitively guarantees that a round-trip in abidirectional transformation system does not havesurprising eﬀects for the user.
Definition 1 (Well-bahavedness). Given a transformation expression t, the pair of its forward semantics F[[t]] : S → V which is a total function
from source artifact (e.g., models or graphs) totarget artifact, and its backward semantics B[[t]] :S × V → S which is a partial function from target artifact to source artifact, w.r.t. the original
source artifact is well-behaved if the following two
properties hold.
F[[t]]as = at ⇒ B[[t]](as , at ) = as
(GetPut)
B[[t]](as , a′t ) = a′s ⇒ B[[t]](as , F[[t]]a′s ) = a′s(WPutGet)
Diagrammatically, WPutGetS
is represented as the figue on
the right.
V
Our aim is to achieve thisB[[t]]
property at the level of model
B[[t]]
transformation (in LU ) on top/
S vx
VF [[t]]of bidirectional graph transfor-

We require that LU is rule additive.
Property 1 (Rule additivity of Model Transformation Language). LU is rule additive.

Rules may further contain components like bindings in ATL, in which case the inclusion relation
between these bindings are also considered as we
instantiate in Sec. 5. 2. Even in such a case, we callthis relation rule additivity for simplicity.
Based on the rule additivity, we project themodel transformation to produce transformed submodel using the following model transformation
projection operation.
Definition 5 (Model Transformation Projection(Π)). A function Π : LU → LU is called modeltransformation projection if ΠT ⊆MT T for T ∈LU .
For a transformation T ∈ LU , since ΠT ⊆MT T ,rule additivity of LU implies ΠT m ≺M T m.
Rule additivity can be represented by the commuting diaMM: T
gram on the right.
T
Notice the diﬀerence between/  ′T
MM T and MM ′T (correspond- MM S ΠT MM
ingly GS T and GS ′T ). Since
the models in the latter may lack some model elements or features because of the partiality, the corresponding metamodel should be relaxed to allow
the absence of these elements and properties. We
do this by changing all the mandatory features tooptional (and likewise the lower bound of multiplicity constraints to zero). To avoid clutter we donot make these diﬀerence explicit in the rest of thispaper.
Next we need a bijective mapping beteen models
and graphs, i.e., the pair of model to graph transM
lation M
G ↓ and graph to model translation G ↑ to be
inverse with each other.
Property 2 (Bijection between Models andGraphs).
M
M(M(M
G ↓ ◦ G ↑) g ≡G g
G ↑ ◦ G ↓) m ≡M m
where ≡G denotes graph equivalence (isomorphism) and ≡M denotes equivalence between models as isomorphism of node-attributed graphs. The
graph isomorphism is not easy to decide in general,so we assume a distinguished attribute in the model
element to uniquely identify the element, and thatthe identifier is translated bijectively through M
G↓
and M
↑.
In
the
rest
of
the
paper,
we
simplyuse=Ginstead of ≡M assuming these identifiers.
For the transformation produced by projection,
we require the soundness of the translation of
the transformation: given model transformation≺Mmation (in LB ).
It is worth noting that the original source artifact
as ∈ S is needed to recover the information that
may had been discarded by the forward transformation [4]. WPutGet [14] corresponds to Weak
Invertibility by [6] that is a weaker variant of PutGet [9] that corresponds to Correctness [28].
Under partial translation we first project thetransformation T to the one that is fully translated.
To clearly distinguish the target of the projectedtransformation and that of the original transformation, we make the former embedded in the latter. This embedding is represented by the following
submodel relation between models.
Definition 2 (Submodel Relation (≺M )). m′ ≺Mm denotes m′ is a submodel of m. This notionof submodel is similar to the inclusion morphism
between graphs in general as in [7], extended to
typed attributed graphs, in the sense that m1 is asubmodel of m2 if there is an inclusion morphismfrom m1 to m2 .
Intuitively, bigger models have more model elements and more features for model elements withthe same identifiers. The relation ≺M between
models is instantiated for each data model of LU ,for example by using set inclusion relationship between the set of model elements in the models.
We need the following relationship between thetransformation T ∈ LU and its translatable partT0 .
Definition 3 (Inclusion Relation of Model Transformations (⊆MT )). T0 ⊆MT T denotes that modeltransformation T0 ∈ LU is included in model transformation T ∈ LU .
The relation ⊆MT between transformations is instantiated for each model transformation language,
for example by using set inclusion relationship between the set of rules in the transformations. The
definition of T0 ⊆MT T should reflect the restricted
image produced by T0 relative to T , as below.
Definition 4 (Rule Additivity). A model transformation language LU is rule additive for the inclusion relation ⊆MT between model transformationsof type MM S → MM T in LU , if for all models
ms ∈ MM S , T0 ⊆MT T implies T0 ms ≺M T ms .

T : MM S → MM T , translation ⟨⟨ ⟩⟩ : LU → LB
from model transformation to graph transformation, model to graph translation M
G ↓, graph to modeltranslation M
G ↑, and translated forward graph transformation F [[⟨⟨T ⟩⟩]] : GS S → GS T , where GS S and
GS T represent source and target graph schema,
respectively, we require that if we convert source
model to graph, perform the graph transformation,and convert back to model, that is the same as directly transform the source model by model transformation.
Property 3 (Soundness of Total Translation).
Given T ∈ LU and ⟨⟨T ⟩⟩ ∈ LB , the following equation holds.
M
T =M
G ↑ ◦ F [[⟨⟨T ⟩⟩]] ◦ G ↓It can be represented by
T/MMO T
MM S
the diagram on the right.
M
M
G↑
It is worth noting that G↓/when T is an identity GS S
GS T
F [[⟨⟨T ⟩⟩]]
transformation, it still holds by the second equivM
alence (MG ↓ being the right inverse of G ↑) in Property 2.
Partial translation ⟨⟨T ⟩⟩P (= ⟨⟨T0 ⟩⟩) is implemented
as ⟨⟨ΠT ⟩⟩. Consequently, the range of Π should bewithin the domain of ⟨⟨⟩⟩, i.e.,ran(Π) ⊆ dom(⟨⟨⟩⟩).
Finally, we require that LB is well-behaved(Def. 1).
Property 4 (Well-behavedness of underlying bidirectional graph transformation). Given a graphtransformation expression t ∈ LB , the pair of its
forward semantics F [[t]] : GS S → GS T and its backward semantics B[[t]] : GS S × GS T → GS S is wellbehaved.
We then implement the bidirectional modeltransformation. The forward transformation is
simply T ∈ LU . For backward transformation, we
need the following notion of model restriction.
Definition 6 (Model Restriction). Restriction ofmodel m1 ∈ MM with m2 ∈ MM , denoted by
m1|m2 , is a submodel of m1 induced by the subset
of nodes (model elements) in m1 that have nodes in
m2 with matching identifiers.
Since we have m1|m2 = m′1 ⇒ m1|m′1 = m′1 and≺m2 ≺M m1 ⇔ m1|m2 = m2 , we also denote m2 ←−M−
m1 when we compute a restriction from m1 . The
restriction m1|m2 operator is instantiated for eachdata model of the model transformation language.

1
MM S

1MM T
T

≺M

w
/MM
? T

T0 =ΠT

2
M
G↓

5



6

GS S

UMM T |≺M

/ T
GS

F [[⟨⟨T0 ⟩⟩]]

3

 w

⟨⟨UMM

MM
? S

GS S r

7|T ≺M

9 (14)

⟩⟩ T

4 M↓
G

T0



(13) M 8
G↑

UMM

M
G↑

MM T

B[[⟨⟨T0 ⟩⟩]]( , )(12)F [[⟨⟨T0 ⟩⟩]]

MM T
∼B[[T ]]( , )

≺M


1MM T

MM S

∼B[[T ]]( , )
0 ≺
MM S
M

/MM Tw
M
G↓

GS T
B[[⟨⟨T0 ⟩⟩]]( , )

T

(10)

(11)

∼B[[⟨⟨T ⟩⟩]](GS , )
0
S



/ T
GS

Fig. 6: Commuting diagram for bidirectional transformation based on partial translation of modeltransformation T
Now we define the backward model transformation.
Definition 7 (Backward Model Transformation).
Given source model ms ∈ MM S , updated target
model m′t ∈ MM T , T ∈ LU , its projector Π, model
to graph transformation M
G ↓, graph to model transM
formation G ↑, ⟨⟨ ⟩⟩ : LU → LB and backward graphtransformation B[[ ]]( , ) : GS S × GS T → GS S , thebackward model transformation B[[T ]]( , ) : MM S ×
MM T → MM S is implemented by
B[[T ]](ms , m′t ) =M′
M
M
G ↑(B[[⟨⟨ΠT ⟩⟩]](G ↓(ms ), G ↓(mt|(ΠT )ms )))Given the previous definitions, bidirectionalmodel transformation in the global system can be
performed by the concrete sequence of steps shown
below.
1. Perform forward model transformation T ms to
get mt .
2. Update mt to m′t with m′t = u mt , whereu ∈ UMM is an update function on models that
conform to metamodel MM .
3. Compute the restriction m′t|T0 ms where T0 =
ΠT .
4. Obtain gt′ by converting the restricted model
to graph with M
G ↓.
5. Obtain gs = M
G ↓ ms .
6. Performforwardgraphtransformation
F [[⟨⟨T0 ⟩⟩]]gs to obtain trace information needed
for the next step.
7. Perform backward graph transformation
B[[⟨⟨T0 ⟩⟩]](gs , gt′ ) to obtain gs′ .
′8. Obtain the updated source model m′s as M
G ↑ gs .
9. As post processing, perform forward model

transformation T m′s to get m′′t as the final
updated target model, which may be diﬀerent
from m′t †5 .
The following lemmas hold on the system built
using the backward transformation in Def. 7.
Lemma 1. Given LU and LB with Properties 1,
2, 3 and 4, the pair of T ∈ LU and backward
model transformation B[[T ]]( , ) as defined by Def. 7
satisfies the GetPut property.

Get properties by Lemma 1 and Lemma 2.

Theorem 1 and other related properties can beconcisely illustrated by the commuting diagram in
Fig. 6 by composing the diagrams we have presented so far. We try to render the same kind ofarrows in parallel. In the diagram, the front plane
represents the graph technical space, while the backplane represents the model technical space. Artifacts are converted between the two technicalM
spaces by M
G ↓ and G ↑. WPutGet in the graph
Proof. We show B[[T ]](ms , T ms ) = ms .
technical space (Prop.4) can be represented by thecommuting triangular diagram at the bottom of
the front plane. The dotted arrow from GS S to
LHS
B[[⟨⟨T0 ⟩⟩]]( , ) indicates that the backward trans={ Def. 7, T0 = ΠT }M
MM
formation
is w.r.t. the original source graph in
G ↑(B[[⟨⟨T0 ⟩⟩]](G ↓(ms ), G ↓(T ms|T0 ms )))GS.
Thevertical arrow ∼B[[⟨⟨T0 ⟩⟩]]( , ) is an (inS=
{ T0 ms ≺M T ms (Property 1) }M
MM
duced) equivalence relation between the updated
G ↑(B[[⟨⟨T0 ⟩⟩]](G ↓(ms ), G ↓(T0 ms )))M↓ (Property 3, Property 2) } target graph and that with another forward trans=
{M
↓
◦T
=
F
[[⟨
⟨T
⟩
⟩]]
◦
0
0
G
G
M
M
M
formation, which represents that these two target
G ↑(B[[⟨⟨T0 ⟩⟩]](G ↓(ms ), F [[⟨⟨T0 ⟩⟩]]G ↓(ms )))graphs are equivalent w.r.t. their eﬀect on the={ Property 4(GetPut) }M M
source graphs (they result in the same updated
G ↑(G ↓(ms ))source graph). It corresponds to [6]’s equivalence={ Property 2 }in the context of weak invertibility. The horizontalmsaxis represents the (model and graph) transforma= RHS
tion, while the vertical axis represents updates andrestrictions. Of the model transformation rules T
Lemma 2. Given LU and LB with Properties 1,
only T0 = ΠT (⊆MT T ) can be fully translated,
2, 3 and 4, the pair of T ∈ LU and backward
and the commuting triangles in the back plane repmodel transformation B[[T ]]( , ) as defined by Def. 7
resent rule additivity (Prop. 1). The square on
satisfies the WPutGet property.
the top and the bottom represents the soundness
The proof is in Figure 7. In this proof, we useof translations (Prop. 3). The vertical arrow onMshorthands ↓ and ↑ for M
G ↓ and G ↑, to avoid clutter.
the back bottom labeled ∼B[[T0 ]]( , ) is the equivIt is now obvious that LU on top of LB is wellalence relation on the model technical space thatbehaved.
is induced by ∼B[[⟨⟨T0 ⟩⟩]]( , ) . The update operation
Theorem 1 (Well-behavedness of Model Transfor(UMM T |≺M ) represented by the rightmost verticalmation). Given LU and LB with Properties 1, 2, 3
downward arrow on the back plane assumes thatand 4, the pair of T ∈ LU and backward transforonly the submodel part restricted by the image ofmation B[[T ]]( , ) defined by Def. 7 is well behaved.
T0 is updated, so the square to which the arrow belongs commutes. The square right below also commutes where the equivalence ∼B[[T ]]( , ) is induced
Proof. The pair satisfies the GetPut and WPutby ∼B[[⟨⟨T0 ⟩⟩]]( , ) .
†5 m′t and m′′
Each one of the concrete steps listed before ist may disagree when forward transformation duplicates part of the source model while
depicted in the diagram as a thick arrow with auser updates only one of the duplicates (handledsans-serif number. The parenthesized numbers repas explained in the paragraph following Theorem 1
resent the sequence that corresponds to Lemma 2:
and in footnote 6). We take m′′t as the final upanother backward transformation with respect todated target model in this case. WPutGet en′′′
the same original source model follows the path onsures that mt and mt has the same eﬀect in updating source model.
the bottom plane, so, when finished, it returns toProof. We show B[[T ]](ms , m′t ) = B[[T ]](ms , T (B[[T ]](ms , m′t ))).
RHS=

{ Def. 7, T0 = ΠT }B[[T ]](ms , T (↑(B[[⟨⟨T0 ⟩⟩]](↓(ms ), ↓(m′t|T0 ms )))))={ Def. 7, T0 = ΠT }↑(B[[⟨⟨T0 ⟩⟩]](↓ ms ,↓(T (↑(B[[⟨⟨T0 ⟩⟩]](↓ ms , ↓(m′t|T0 ms ))))|T0 ms )))={ Property 1 }′↑(B[[⟨|T0 ms ))))))){⟨T0 ⟩⟩]](↓(ms ), ↓(T0 (↑(B[[⟨⟨T0 ⟩⟩]](↓(ms ), ↓(mt}
Property 2 and Property 3, i.e.,=
F[[⟨⟨T0 ⟩⟩]]= ↓ ◦T0 ◦ ↑↑(B[[⟨⟨T0 ⟩⟩]](↓(ms ), F [[⟨⟨T0 ⟩⟩]](B[[⟨⟨T0 ⟩⟩]](↓(ms ), ↓(m′t|T0 ms )))))={ Property 4(WPutGet) }↑(B[[⟨⟨T0 ⟩⟩]](↓(ms ), ↓(m′t|T0 ms )))={ Def. 7, T0 = ΠT }LHS
Fig. 7: Proof of Lemma 2

the original position in the diagram.
So far we have focused on achieving wellbehavedness of bidirectionalized LU . However,
the extreme case where Π produces empty transformation for every input still satisfies the wellbehavedness, but the whole system accepts no modification because the target of ⟨⟨ΠT ⟩⟩ is empty. Similarly, ⟨⟨⟩⟩ needs to have as large domain as possible.
If it is undefined in any input, the whole system
would not be bidirectional. So we have the following quantitative requirements, though they are not
the focus of our paper.
• dom(⟨⟨⟩⟩) is maximized• ran(Π) is maximized (within dom(⟨⟨⟩⟩))

5 ATL on GRoundTram
In this section we exemplify our proposal by integrating ATL and GRoundTram: we instantiate
LU as ATL, LB as UnQL, models as EMF models conforming to Ecore metamodels serialized in
XMI format, graphs as edge-labeled graphs [2] conforming to the KM3 [20] metamodel implemented
as graph schema [15], serialized to GraphViz DOT
format [14]. We first describe the integration of thetwo data models (models and edge-labeled graphs)
Mthrough instantiation of M
G ↓ and G ↑ and then proP
vide a partial translation ⟨⟨ ⟩⟩ from ATL to UnQL.
Then we show that the integrated bidirectionalmodel transformation satisfies well-behavedness(Theorem 1). We have shown in Section 4 that the

global well-behavedness as Theorem 1 is implied byRule Additivity (Property 1) of LU , bijection between models and graphs (Property 2), soundnessof ⟨⟨⟩⟩ (Property 3), and well-behavedness (Property 4) of LB . Here we show that these properties hold for this combination of ATL and GRoundTram.
5. 1 Integrating Data Models
The ATL (EMF) and GRoundTram data models
exhibit some significant semantic gaps.
First, since GRoundTram relies on node identities to store trace information and manage updates
to graphs, we can not always freely generate identifiers of graphs in M
G ↓. Therefore, we refine the bijection in Property 2 to a bidirectional transformation,
where MG ↓ takes as input the original graph (i.e.,
the graph before the M
G ↑ conversion), in addition
to the (possibly updated) model. In this bidirectional transformation, MG ↑ corresponds to forward
transformation and M↓
tobackward transformationG
satisfying the following:
M
M(MGGetPut)
G ↓ g (G ↑ g) = g
M M(G ↑(G ↓ m)) ≡M m
(MGCreateGet)
M(M(MGPutGet)
G ↑(G ↓ g m)) ≡M m
MGCreateGet corresponds to the case where theoriginal graph is not available, like in step 5 in theconcrete sequence of steps following Definition 7.
In this case, node identities in the graph are generated by M
G ↓ arbitrarily but MGCreateGet ensures

: Class
attr name = ’Family’: Tablename = ’Family’ colxmi:id = ’IN.1...’r

xmi:id = ’1’
ÀÁ
Class
name

attr

String‘Family’

Table
name
String‘Family’colcol_Class2Table

Fig. 8: Overview of ATL to UnQL translationthat the model m is recovered by M
G ↑ using model
element identifiers also discussed below.
Since Lemmas 1 and 2 assume bijection before
the above refinement, their proofs should be reworked. Fortunately they still hold as follows. In
Lemma 1, the first use of Property 2 is replaced
by MGGetPut where Property 3 feeds the original source graph for M
G ↓, while the second use isreplaced by MGCreateGet. Lemma 2 holds similarly.
The other semantic gap between the two technical spaces is caused by the respective use of isomorphism or bisimulation. Since the GRoundTram
technical space uses bisimulation equivalence [2] instead of isomorphism equivalence, the translated
UnQL can introduce arbitrary duplicates and unfold of cycles in the graphs. Naively convertingthese duplicates back to the ATL technical space
would hamper the synchronization. Since GRoundTram is equipped with a normalization phase [14]where bisimilar nodes are contracted to one node,
this duplication is eliminated. We assumed in Section 3 that all model elements have unique identifiers. Such an identifier is encoded by a primitivetype attribute label within the model-element subgraph. This prevents accidental contraction of subgraphs encoding isomorphic submodels. A graphin the equivalence class [g]∼G where ∼G denotes
bisimilarity, maps to the same model as g does,i.e., we haveM
g 1 ∼G g 2 ⇒ M
G ↑(norm g1 ) ≡M G ↑(norm g2 )where norm is the normalizer.
The third gap is based on set semantics of thegraph model, so that order between edges is notpreserved. Consequently, ordered sequences needadditional encoding of the order or introduction ofordered graph models [11] [33].
5. 1. 1 Encoding Models by UnCAL

GraphsThe graph data model we use is rooted and edgelabeled. This means there is no label on nodes.
Our graph encoding of models [15] [10] [14] is basedon the graph schema KM3 (Kernel MetaMetaModel [20]). An XMI model is converted to graphin the following way.
• Basic data type: Datatypes in KM3 areencoded as
String | Integer

/•
value
/•
•
• Class data type: Attributes in KM3 areencoded as| Float | Boolean

featurename
ClassifierName/•/G•
where G encodes the subgraph that represents
the feature.
Classes in KM3 are encoded as graph union of
the subgraphs encoding the attributes.
• Entire Model: The model encoded in the
XMI file is a sequence of top level XML elements encoding top level model elements.
These are encoded by a graph union ofClassifierName/•
G
where G encodes the subgraph representing
the object of the class. Note that only classinstances appear at the top level.
M
M
Metamodels are used for both M
G ↓ and G ↑. G ↑ reusesand extends the KM3 validator to extract the structure of the graph, while M
G ↓ traverses the tree structure of the XMI file recursively, keeping track ofreferences identified by xmi:id attributes. Pleaserefer to the long version [16] for details on the conversion algorithm.

5. 2 Integrating
Transformation
Languages
The integration of ATL and UnQL is realized bypartial translation from ATL to UnQL and alignment of the results of the two transformations. We
give the translation algorithm in Section 5. 2. 1, anddiscuss its partiality in Section 5. 2. 2. Comparison
with the translation in our previous work [27] isconducted in Section 5. 2. 3.
We first instantiate the relation ≺M in the ATL(EMF) data model by the following partial order,
where a model m is composed of a set of model
elements m.E, and each model element e ∈ m.E
having unique identifier e.id contains the set e.F offeatures. Then,
m1 ≺ M m2 ⇔∀e1 ∈ m1 .E, ∃e2 ∈ e2 .E. e1 .id = e2 .id ∧ e1 .F ⊆ e2 .F.
≻M is instantiated similarly. We consider two features equal if they have the same name and haveequal values (in case of primitive attributes) or ifthey refer to elements having the same identifiers.
Model restriction m1 |m2 is defined if for all model
elements e2 ∈ m2 .E there exists e1 ∈ m1 .E withmatching identifier and for each feature f in suchmodel element e2 there exists a feature in e1 withthe same name.
m1 |m2 = {id = e.id,
F = {f | f ∈ e.F, f2 ∈ e2 .F, f.name = f2 .name}| e ∈ m1 .E, e2 ∈ m2 .E, e.id = e2 .id}
We use this restriction under the scenario wheremodel m1 ≻M m2 is modified and the modified partof m1 corresponding to m2 is extracted. m1 |m2 =m2 is a special case in which m1 is not modified.
Next we instantiate the relation ⊆MT between
ATL transformations defined by the following partial order, where a transformation T is composed of
set of rules T.R, each rule r ∈ T.R having unique
identifier r.id contains the set r.O of output patterns, each pattern p ∈ r.O having unique identifier
p.id contains the set p.B of bindings. Then,
T1 ⊆MT T2 ⇔ ∀r1 ∈ T1 .R, ∃r2 ∈ T2 .R, r1 .id = r2 .id∧∀p1 ∈ r1 .O, ∃p2 ∈ r2 .O, p1 .id = p2 .id∧p1 .B ⊆ p2 .B.
We consider two bindings equal if they have thesame feature name and have syntactically the same
binding expressions. T1 ⊇MT T2 is defined similarly. The definition of T1 ⊆MT T2 reflects the restricted image produced by T1 relative to T2 withrespect to rule, output pattern and binding levels.
5. 2. 1 ATL to UnQL
We then instantiate Π in Def. 5 to generate, fromthe full ATL transformation, a transformation in
the translatable subset of ATL. The sequence ofrules in an ATL module is filtered as follows. An
ATL rule which has a guard that does not matchwith the production rule guard in Listing 5 (suchas a let expression in the production rule xgauard )is discarded. For each ATL rule, its sequence ofbindings is filtered as follows. A binding whose
OCL expression on the right hand side of <- does
not match with the production rule oclExp in
Listing 5 (such as a let expression in the production
rule xOclExp ) is discarded. Since these filterings
discard each rule and binding in its entirety, thisoperation is a model transformation projection Π
defined in Def. 5, i.e., it is easy to show that
ΠT ⊆MT T . A brief discussion on this projection
is given in Section 5. 2. 2. This projection produces
T0 from T in Fig. 6.
We then fully translate the transformation after
projection to UnQL. The range of Π is still a superset of our previous work [27] which did not include
guards. The set of ATL rules are translated into
structural recursions in UnQL as shown in Fig. 10.
The translation rule ⟨⟨ ⟩⟩ρ for an ATL module named
id m with the list rules of rules under type environment ρ that includes source and target metamodel
is defined in Fig. 9a. A module is translated to a
combination of main clauses MainClauses of main
structural recursion and a list of mutually recursivefunction definitions pathfuns to traverse the pathexpressions in the bindings. They are generated byan auxiliary translation ⟨⟨⟩⟩r applied for each rule.
The last “catch-all” clause following MainClauses
corresponds to the semantics of ATL in which nothing is produced for omitted rules. ⟨⟨⟩⟩r (Fig. 9b)
generates a pair of 1) a corresponding clause in themain function and 2) the list of structural recursion function definitions that are called in the clauseas a result of translating OCL expressions in bindings. All the clauses returned by ⟨⟨⟩⟩r constitute theclauses MainClauses of the main function, and all
the function definitions constitute pathfuns. These
aggregations are conducted by standard functions
on lists map, unzip and concat, and this form of collecting the return value is similar in other auxiliarytranslations below, while the translation traverses
from top level rules to bindings.
Given a guard OCL expression g and the environment ρ, ⟨⟨g⟩⟩Gρ (Fig. 9c) generates a boolean expression in UnQL. Logical connectives are translated
directly, and the predicate e.isEmpty that tests
whether e produces an empty collection is translated using UnQL’s isEmpty. Equality test with⟨⟨module id m rules⟩⟩ρ =let ρ = ρ{modname 7→ id m } inlet (MainClauses, pathfuns) =(id × concat) ◦ unzip ◦ map(⟨⟨ ⟩⟩rρ ) rules inletrecpathfunsand sfun
MainClauses| id m ({$l : $g}) = {}in id m ($db)⟨⟨rule id r from id s : oclType s (guard ) to outPats⟩⟩rρ
= let ρ = ρ{id s 7→ oclType s }{rulename 7→ id r } inlet ρ = ρ{id t 7→ Tt | (id t : Tt ) ∈ outPats} in
let id m = ρ(modname) inlet (mbodies, pathfuns) =(id × concat) ◦ unzip ◦ map(⟨⟨ ⟩⟩opρ ) outPats
in (id m ({oclType s : $g}) =let $id s = $g inif ⟨⟨guard ⟩⟩Gρ then mbodies else {}, pathfuns)
Translation rule for ATL rules (⟨⟨⟩⟩r )Main translation rule (⟨⟨⟩⟩)
GG⟨⟨e1 and e2 ⟩⟩Gρ = ⟨⟨e1 ⟩⟩ρ and ⟨⟨e2 ⟩⟩ρGG⟨⟨e1 or e2 ⟩⟩Gρ = ⟨⟨e1 ⟩⟩ρ or ⟨⟨e2 ⟩⟩ρGG⟨⟨not e⟩⟩ρ = not⟨⟨e⟩⟩ρ⟨⟨e.isEmpty()⟩⟩G
ρ = isEmpty(oclExp2select⟨⟨e.f ⟩⟩G=
isEmpty(ρ⟨⟨id t : oclType t (bindings)⟩⟩opρ =let (mbodies, pathfuns) =(id × concat) ◦ unzip ◦ map(⟨⟨ ⟩⟩bρ ) bindingsin ({oclType t : mbodies}, pathfuns)
ρ e)select {dummy:{}}where {Boolean:$g} in (oclExp2select ρ e.f ),{true:$dummy} in $g)
Translation rule for guards (⟨⟨⟩⟩G )⟨⟨id ← oclExp⟩⟩bρ =if isReference oclExp thenoclExp2sfuns ρ (id ← oclExp)
else({id : oclExp2select ρ oclExp}, [])Translation rule for output patterns (⟨⟨⟩⟩op ) and bindings(⟨⟨⟩⟩b )Fig. 10: ATL to UnQL Translation Rules
OCLUndefined could be translated similarly. Access to a boolean feature f of a model element istranslated to existence of subgraphs encoding thefeature. Due to this usage of existence, f should be
mandatory with cardinality one. The other predicates like comparison operations would be translated to existence of a combination that satisfies
such relation. This is left to our future work. Since
the source model element identifier and its typeis specified for each rule, this association is registered to the type environment ρ and passed to theauxiliary translation function ⟨⟨⟩⟩op . ⟨⟨⟩⟩r generates
one clause of the main function which traverses oneedge corresponding to oclType s and binds the subgraph pointed by the edge to variable $id s . Translation of each output pattern is delegated to ⟨⟨⟩⟩op .
The translation ⟨⟨⟩⟩op (Fig. 9d) in turn generates
one edge that encodes the output type oclType t ,while generation of the body expression of the mainfunction clause and the structural recursion function definition for each binding is delegated to ⟨⟨⟩⟩b .
A binding that accesses a non primitive type requires recursion, so the traversal path is translated

to a corresponding set of structural recursion definitions that traverse the path. It is similar tothe process of translating regular path patterns tomutually recursive structural recursion via the automaton that encodes the pattern in [2]. If insteadthe binding retrieves primitive data type values, thetranslation is almost identical to that in [27] thatuses select.
The above translation generates almost the same
UnQL transformation in Listing 2 generated from
ATL in Listing 1, except that it is augmented with
explicit model element identifier generation as in
Listing 4 correspondingly to the id-generation logic
like in Listing 3. See the long version [16] for fulllistings.
5. 2. 2 Discussions on the partiality oftranslation and limitations
The expressive power of the ATL language has
universality [1], while UnQL is expressed in firstorder logic extended with transitive closure [2] albeit its terminating property (any transformationin UnQL terminates by construction and so doesin GRoundTram in both forward and backward di-rection). This gap prohibits total translation from
ATL to UnQL. Essentially no fragment that exceeds the expressive power can be translated. For
example, in UnQL the recursion scheme of functions cannot be arbitrary, but is subject to a syntactic restriction called structural recursion.
We describe the gap in semantics and expressive
power of ATL and UnQL, and the partiality of thetranslation caused by this gap.
Non-translated ATL features
Language features like rule inheritance and OCL
helpers (useful to factorize commonly used OCL
expressions) may be in principle bidirectionalized
but they are not considered in our current translation. Exploring the exact ATL subset having thesame expressive power as UnQL is outside the scopeof this paper, we focus instead on the integration
problem.
Recursions in OCL
Even though UnQL has recursive functions
traversing graphs, the recursion scheme is limited
to the form of structural recursion function [2] fthat satisfies the following equations.
f ({})f ({l : g})f (g1 ∪ g2 )

=
=
=

{}
(l, g) ⊙ f (g)f (g1 ) ∪ f (g2 )These equations show that f is like a homomorphism. f returns empty graph for empty inputs(first equation). If the input is an edge labeled lconnecting to subgraph g, f returns the final result
by combining l and g and the result of the recursive call on g (second equation). If the input is theunion of two graphs, then the result is the union of
the recursive calls on these graphs (third equation).
The second equation suggests that recursive callis strictly limited to the subgraph (g) that is accessible from the target node of the edge (labeledl). Recursive calls like f ({a : {b : g}}) are disallowed. This restriction guarantees the termination of transformation in UnQL, producing finite
graphs.
Moreover, the results of the recursive calls canonly be used in constructors, and not passed asarguments to other functions or predicates. Soh(f (g)) is disallowed. Such composition is only allowed outside of recursive calls. It is also worth
noting that it is not permitted to call the outerfunctions from their nested inner functions. Therefore, an OCL expression containing recursions that

do not fit into the above recursion scheme is nottranslatable.
Multiple traversals from a node
In ATL, model elements are traversed multiple
times, e.g., in output-pattern bindings as in thefollowing one from Listing 1 line 34.
n a m e <− s . o w n e r . n a m e +’_ ’+ s . n a m e

As long as these references access the values ofprimitive data types, they can be encoded as asingle select construct, likeselect { n a m e :{ S t r i n g : {($s1 ˆ ’ _ ’ ˆ $s2 ):{}}}}
where { o w n e r . n a m e . S t r i n g :{$s1 : $dummy}} in $g,3{name . String :{$s2 : $dummy}} in $g
1

2This translation performs multiple traversals fromthe same graph variables using multiple whereclauses. If the traversed values are not primitive, then this translation cannot be used, because
beyond the complex values, structural recursion
should be applied. So the traversal should be implemented using sibling sfuns, the returned value
from which cannot be traversed because of the limitation on structural recursions.
5. 2. 3 Improvements from previous translation
Compared with the previous work [27], we havethe following diﬀerences: (1) We deal with partiality, so we cover non-restricted ATL at the user level.
Previously total translation from ATL to UnQL
was assumed, so the source ATL language was restricted to a bidirectionalizable subset. (2) We havea bigger translated subset, including guards. (3)The translated UnQL is more robust in the sensethat cycles are better maintained, translation ismetamodel-directed, and graph-model transformation is clearly defined based on XMI. See the long
version [16] for details.
5. 3 Well-behavedness of the entire bidirectional model transformation
As we wrote in the beginning of this section, weshow that the integrated bidirectional model transformation satisfies well-behavedness (Theorem 1)
by showing Properties 1,2, 3 and 4. We show thatthese properties hold for this combination of ATL
and GRoundTram.

Rule Additivity of ATL (Property 1)
Rule additivity can be derived by the instantiation of ≺M and ⊆MT in Section 5. 2 and informal
specifications of ATL, and we just assume that it
holds in this paper. Intuitively, ATL†6 satisfies rule
additivity because the more rules the transformation have, and the more output-pattern elements
the rule has, the more target elements are includedin the target model, and the more bindings each
output pattern has, the more features are includedin the target model elements. Note that for eachsource element, no more than one rule is applied.
If more than one rule is applicable to a source element, then a run-time error occurs. If no rule isapplicable to a source element, then no target element is produced from the source element.
Bijection between models and graphs(Property 2)
We have already shown this property by refinement to bidirectional transformation between models and graphs in Section 5. 1.
Soundness of ATL to UnQL Translation(Property 3)
We show that the target model created by
GRoundTram through forward transformation oftranslated UnQL is isomorphic to the target model
created by the ATL transformation. Fig. 8 sketches
the proof using our running case introduced in Section 2. For each rule r matching a source model
element es , ATL creates a target model element et .
In the figure es corresponds to Family model element of type Class and et corresponds to Family oftype Table. Suppose the entire rule is translated
to UnQL. Then the corresponding UnQL structural recursion function r() creates the corresponding target model, assuming each binding is successfully translated. In the figure, the name feature is encoded in the source graph as three consecutive edges as described in Section 5. 1, and therule Class2Table is translated to the clause of the
UnQL function as shown in lines 20–22 in Listing 2.
The transformation of the feature attr is delegatedto the col Class2Table sibling mutually recursivefunction. Note that rule additivity of ATL is trans†6 In this paper the term ATL refers to the rulebased declarative transformation language. The
ATL engine supports also the execution of imperative instructions that we do not consider.

lated to that of the translated UnQL code in thesense that when ATL rule is added, the corresponding clause in the main sfun of UnQL is added by
the definition of translation rule ⟨⟨ ⟩⟩. Similarly, themore outPat we have in an ATL rule, the morecomponents in the then clause is generated by thetranslation rule ⟨⟨⟩⟩r and, the more bindings we havein an output pattern, the more branches under theedge encoding oclType t are generated by the translation rule ⟨⟨⟩⟩op .
As for the translation of guards (⟨⟨⟩⟩G ), we showthat an enclosing guard holds if and only if thetranslated UnQL expression using isEmpty predicate holds. Since logical connectives can be treatedby simple induction, we focus on the rest of the twocases, both of which uses UnQL’s isEmpty predicate with oclExp2select auxiliary translation rules.
OCL expression e.isEmpty() evaluates true if theexpression exhibits non-empty collection. UnQL
translation of e generates corresponding graph withselect expression which returns dummy graph fragment if the translation of e captures the graph pattern that corresponds to patterns in the OCL expression. Example can be seen in lines 15-19 and24-30 of Listing 2. OCL Boolean predicate expressions can be treated similarly.
By the definition of translation rules, when we
have atarget model element created by an ATL rule,
we have the corresponding clause of main UnQL
sfun in GRoundTram that creates the corresponding target element. The correspondence is identified by the model element identifier xmi:id discussed in Section 3.
Formally, the above correspondence can beshown by induction on the number of rules, number of output patterns under the hypothesis on the
succesfull translation of the bindings. Base casewith no rule (rules = []) produces just the catchall clause with body producing empty graph, since(id × concat) ◦ unzip ◦ map(⟨⟨⟩⟩r ) produces the pairof empty lists for the empty input list. So bothM
ATL and GRoundTram (MG ↑ ◦ F [[⟨⟨T ⟩⟩]] ◦ G ↓) produce an empty model. As for the base case of ⟨⟨⟩⟩rwith empty output patterns, it still produces no element since mbodies and pathfuns are both emptyin ⟨⟨⟩⟩r for empty outPats. As for the base case of⟨⟨⟩⟩op with empty bindings, it produces the empty
skeleton of a model element of type oclType t , sincembodies and pathfuns are both empty in ⟨⟨⟩⟩op forempty bindings. Inductive case assumes translations of rules, output patterns and bindings as induction hypothesis and shows that a rule, an output pattern or a binding additionally produces thecorresponding element or binding. For each rule,the matching of source element type captured by
the from clause is translated as sfun’s patternmatch ({oclType s : $g}), and for each output pattern, an edge representing the output OCL typeof the produced element is produced by ⟨⟨⟩⟩op at{oclType t : mbodies}. For each binding, the corresponding feature name given by id in the rule of ⟨⟨⟩⟩bis used to create an edge labeled with id encodingthat feature name as {id : oclExp2select ρ oclExp}
in case of primitive values. These edges are translated to the corresponding elements and attributes
in XMI format by M
G ↑ instantiated in Section 5. 1.
Next we show that if we have a reference fromelement e1 in the target model created by ATL
to another element e2 in the same model, thenin the target graph created via GRoundTram wehave a corresponding sequence of edges from anode encoding e1 to another node encoding e2 . It
can be shown by the definition of translation rule⟨⟨⟩⟩b in which we have the corresponding bindingid ← oclExp that creates reference named id in thetarget model of ATL. Mutually recursive functions
that finally calls the main function of name id m willproduce such edges.
Well-behavedness of GRoundTram (Property 4)
This property is already shown in [14] [12].
Since we have shown all the properties necessary
to deduce well-behavedness, we can conclude thatthe entire bidirectional model transformation system exhibits well-behavedness.
As for the partiality, ATL language constructs
whose translation is not defined produce empty
subgraphs. For example, for an ATL rule whose
guard has no matching translation, the entire rule
is discarded by Π before ⟨⟨⟩⟩ is applied, which is captured by the catch-all clause like in Listing 4. At
the binding level, the model element of type Class
with name attribute Person will create key attributeof Table element in the ATL transformation, but
the corresponding key binding is discarded by Π before ⟨⟨⟩⟩ is applied as we exemplified in Section 2. 3.
This will cause the absence of key edge in the tar-

get graph and that of the target model generated
from the target graph (not depicted in Fig. 8).

6 Related Work
Bidirectionalization [25] [31] [22] [23] allows users
to write one direction of the transformation by using the unidirectional transformation language they
are used to. The language is overloaded with abackward semantics that enables to propagate in
the backward direction a set of changes to thetarget. Full bidirectionalization of the unidirectional model transformation is in general not possible without imposing restrictions to the forward
transformation language, and existing work [27] ismainly focused on maximizing the part of the unidirectional language that is bidirectionalized.
[27] fully bidirectionalized a small (e.g., without
guards) subset of ATL by translating it to bidirectionalized UnQL graph transformation [13] [14].
Since the translation itself was total, there was noneed to run the ATL engine. On the other hand,
our partiality supports the untranslatable part ofthe language in the forward direction, requiring theimage of the complement to be created by the unidirectional engine. Hence we run both the unidirectional and bidirectional engines in parallel andcombine the results. With respect to the translation, our improvements over Sasano et al. werealready summarized in Section 5. 2. 3. See also ourlong version [16] for technical details. As for correctness, Sasano et al did not formalize the overallbidirectional (round-tripping) property as we didin this paper.
The idea of partially translating programs has
been studied, for example by [26] and [24]. Magnusson’s objective is to accelerate the execution ofa sequential program by partially translating it toanother intermediate representation, and the rest
runs ordinarily. The control is passed between thetwo representations, so there is no overlap between
the executions of the two representations. Performance improvement also motivated [26], where thedynamic nature of the source language semantics
prevented its total compilation before execution. In
our setting, the original and the translated program
run concurrently and the results are merged. Our
objective is to bidirectionalize the source program,
and we have provided an integration framework, inaddition to a translation, between these two programs.
Our partial translation may be considered as an
abstraction so that work using Galois Connection
such as by [3] may be utilized to simplify parts ofour discussions in Sections 4 and 5. 3. Note that
Galois Connection is not directly applicable as our
backward transformation takes the original source
as well as the updated target.
Recent study by Stevens [29] mentions partial
transformation with a diﬀerent meaning, since thepartiality refers to the idea of tolerating imperfectconsistency between source and target. Her notionof subspace is interesting; subspace is a subset ofthe domain or codomain of the transformation inwhich the user agreed to stay during update propagation. The subspace also characterizes the degreeof consistency in that an element within a subspace
is more/less compatible than the others outside thesubspace. In our setting, the target subspace consists of the subset of the codomain covered by target models within which only the submodel createdby the partially translated transformation is modified, because only the submodel is allowed to be
updated, though we do not use this subspace tocharacterize the degree of consistency. We disallow
the modification outside of the subspace – Steven’s
partiality is not tolerated†7 .

7 Conclusion and Future Work
We proposed to bidirectionalize unidirectionalmodel transformation languages by partial compilation to bidirectional languages and coupled execution of the two language engines. Users canwrite the transformation in the unidirectional languages they are used to, while updates on wellseparated subregions of the target models are backpropagated by the bidirectional engine. We provedthat the well-behavedness of the global system canbe inferred from the well-behavedness of the bidi†7 The WPutGet property itself does tolerate imperfect consistency though, if the transformation
duplicates (part of) model elements. To be perfectly consistent, these duplicates are simultaneously updated to the identical values, but the
backward transformation accepts (tolerates) the
update to identical values on only a subset of these
duplicates.

rectional engine.
We applied our approach to combine ATL and
GRoundTram, but any other combination satisfying the properties described in this paper is possible. Application of the approach to new languages
requires to develop a partial mapping from the unidirectional language to the bidirectional one. Thisrequires in general a significant eﬀort, dependingon the chosen languages. The developer needs toclearly identify the translatable fragment and totally translate it, while translating the rest to nulltransformation (which generates nothing). A small
datamodel gap simplifies the translation. As a special case, a bidirectional engine with the PutGet,which is stronger than WPutGet, would make thewhole system satisfy PutGet.
In future work, we plan to extend the translatablepart of ATL, experiment with diﬀerent pairs oflanguages and use the properties of the approachto provide user-friendly feedback in model editors
for bidirectional systems.
Acknowledgments
We thank Frédéric Jouault, Zheng Cheng andthe members of IPL for their valuable comments
and suggestions. This research is funded by the
National Institute of Informatics and JSPS KAKENHI Grant 26330096 and by the MONDO (EUICT-611125) project.
References[ 1 ] Al-Sibahi, A. S.: On the Computational Expressiveness of Model Transformation Languages, ITU
Technical Report Series, (2015).
[ 2 ] Buneman, P., Fernandez, M. F., and Suciu,
D.: UnQL: a query language and algebra forsemistructured data based on structural recursion,
VLDB Journal: Very Large Data Bases, Vol. 9,
No. 1(2000), pp. 76–110.
[ 3 ] Cousot, P. and Cousot, R.: Comparing the
Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, PLILP ’92,
1992, pp. 269–295.
[ 4 ] Czarnecki, K., Foster, J. N., Hu, Z., Lämmel,
R., Schürr, A., and Terwilliger, J. F.: Bidirectional
Transformations: A Cross-Discipline Perspective,
ICMT’09, 2009, pp. 260–283.
[ 5 ] Czarnecki, K. and Helsen, S.: Feature-based
survey of model transformation Approaches, IBM
Syst. J., Vol. 45, No. 3(2006), pp. 621–645.
[ 6 ] Diskin, Z., Xiong, Y., Czarnecki, K., Ehrig, H.,
Hermann, F., and Orejas, F.: From State- to DeltaBased Bidirectional Model Transformations: TheSymmetric Case, MODELS’11, 2011, pp. 304–318.
[ 7 ] Ehrig, H., Ehrig, K., Prange, U., and Taentzer,
G.: Fundamentals of Algebraic Graph Transformation, Springer-Verlag, 2006.
[ 8 ] Eramo, R., Pierantonio, A., and Rosa, G.: Uncertainty in Bidirectional Transformations, Proc.
6th International Workshop on Modeling in Software Engineering (MiSE), ACM, 2014, pp. 37–42.
[ 9 ] Foster, J. N., Greenwald, M. B., Moore, J. T.,
Pierce, B. C., and Schmitt, A.: Combinators forbidirectional tree transformations: A linguistic approach to the view-update problem, ACM Trans.
Program. Lang. Syst., Vol. 29, No. 3(2007).
[10] Hidaka, S., Hu, Z., Inaba, K., Kato, H., Matsuda, K., and Nakano, K.: GRoundTram Version 0.9.3 User Manual, http://www.biglab.org/
download.html, 2012.
[11] Hidaka, S., Asada, K., Hu, Z., Kato, H., andNakano, K.: Structural Recursion for Querying Ordered Graphs, ICFP’13, September 2013, pp. 305–318.
[12] Hidaka, S., Hu, Z., Inaba, K., Kato, H., Matsuda, K., and Nakano, K.: Bidirectionalizing graphtransformations, ICFP’10, ACM, 2010, pp. 205–
216.
[13] Hidaka, S., Hu, Z., Inaba, K., Kato, H.,
and Nakano, K.: GRoundTram: An Integrated
Framework for Developing Well-Behaved Bidirectional Model Transformations (short paper), 26th
IEEE/ACM International Conference On Automated Software Engineering, IEEE, 2011, pp. 480–483.
[14] Hidaka, S., Hu, Z., Inaba, K., Kato, H.,
and Nakano, K.: GRoundTram: an integrated
framework for developing well-behaved bidirectionalmodel transformations, Progress in Informatics,
No. 10(2013), pp. 131–148.
[15] Hidaka, S., Hu, Z., Kato, H., and Nakano,
K.: Towards a compositional approach to modeltransformation for software development, SAC’09:
Proceedings of the 2009 ACM symposium on Applied Computing, New York, NY, USA, ACM, 2009,
pp. 468–475.
[16] Hidaka, S. and Tisi, M.: ATLGT: bidirectional
ATL on top of GRoundTram, https://github.com/
atlanmod/ATLGT, 2015. Accessed: 2015-05-15.
[17] Hidaka, S., Tisi, M., Cabot, J., and Hu, Z.:
Feature-based classification of bidirectional transformation approaches, Software & Systems Modeling, (2015), pp. 1–22.
[18] Jouault, F.: Loosely coupled traceability for
ATL, ECMDA Traceability Workshop (ECMDATW), 2005, pp. 29–37.
[19] Jouault, F., Allilaire, F., Bézivin, J., andKurtev, I.: ATL: A model transformation tool, Sci.
Comput. Program., Vol. 72, No. 1–2(2008), pp. 31–
39.
[20] Jouault, F. and Bézivin, J.: KM3: a DSL

for metamodel specification, 8th IFIP international
conference on formal methods for open objectbased distributed systems, LNCS, Vol. 4037, 2006,
pp. 171–185.
[21] Kolovos, D. S., Paige, R. F., and Polack, F. A.:
The epsilon transformation language, Theory andpractice of model transformations, Springer, 2008,
pp. 46–60.
[22] Liu, D., Hu, Z., and Takeichi, M.: Bidirectional Interpretation of XQuery, Proceedings of the2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation,
PEPM ’07, New York, NY, USA, ACM, 2007,
pp. 21–30.
[23] Liu, D., Hu, Z., and Takeichi, M.: An expressive
bidirectional transformation language for XQueryview update, Progress in Informatics, No. 10(2013),
pp. 89–129.
[24] Magnusson, P.: Partial Translation, Technical
Report T93:05, The Swedish Institute of Computer
Science, 1993.
[25] Matsuda, K., Hu, Z., Nakano, K., Hamana, M.,
and Takeichi, M.: Bidirectionalization Transformation based on Automatic Derivation of View Complement Functions, ICFP 2007, 2007, pp. 47–58.
[26] Pinter, R. Y., Vortman, P., and Weiss, Z.: Partial Compilation of REXX, IBM Systems Journal,
Vol. 30, No. 3(1991), pp. 312–321.
[27] Sasano, I., Hu, Z., Hidaka, S., Inaba, K., Kato,
H., and Nakano, K.: Toward Bidirectionalization of
ATL with GRoundTram, ICMT, LNCS, Vol. 6707,
Springer, 2011, pp. 138–151.
[28] Stevens, P.: Bidirectional model transformations
in QVT: semantic issues and open questions, Software and System Modeling, Vol. 9, No. 1(2010),
pp. 7–20.
[29] Stevens, P.: Bidirectionally Tolerating Inconsistency: Partial Transformations, Proceedings of the
17th International Conference on Fundamental Approaches to Software Engineering - Volume 8411,
New York, NY, USA, Springer-Verlag New York,
Inc., 2014, pp. 32–46.
[30] Tisi, M., Jouault, F., Fraternali, P., Ceri, S.,
and Bézivin, J.: On the Use of Higher-Order Model
Transformations, ECMDA-FA’09, LNCS, Vol. 5562,
2009, pp. 18–33.
[31] Voigtländer, J.: Bidirectionalization for free!
(Pearl), POPL ’09: ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages, New York, NY, USA, ACM, 2009, pp. 165–
176.
[32] Warmer, J. B. and Kleppe, A. G.: The Object
Constraint Language: Precise Modeling With UML,
Addison-Wesley Professional, 1998.
[33] Yang, F. and Hidaka, S.: Bidirectional Transformation on Ordered Graphs, Technical Report 201508, GRACE Center, 2015.

rule

1

Class2Table {

from

2

c : ClassDiagram ! Class

3

to

4

t : Relational ! Table5( _ _ x m i I D _ _ <−6

’ IN ’ . concat ( c . _ _ x m i I D _ _ . concat ( ’. C l a s s 2 T a b l e . t ’ ) ) ,78n a m e <−c . n a m e ,9k e y <−c . a t t r −>s e l e c t ( ac o l <−c . a t t r ,|o w n e r <−c . o w n e r ,a . name . e n d s W i t h ( ’ Id ’ ) ) )}10

Listing 3: Class2Table with identifier injection in ATL

1 select sfunc o l _ C l a s s 2 T a b l e ({ attr :$g}) = { col : C l a s s 2 R e l a t i o n a l ($g )}| c o l _ C l a s s 2 T a b l e ({$l :$g}) = {}4 and sfun o w n e r _ C l a s s 2 T a b l e ({ o w n e r :$g})5= { o w n e r : C l a s s 2 R e l a t i o n a l ($g )}6| o w n e r _ C l a s s 2 T a b l e ({$l :$g}) = {}7 and sfun (* main function *)8| C l a s s 2 R e l a t i o n a l ({ Cl as s :$g})=
9{ Ta b l e :(10(select { x m i _ i d :{ S t r i n g :{("IN"ˆ$idˆ".Class2Table.t"):{}}}}
11
where { x m i _ i d . _ :{$id :$dummy}} in $g )12
∪ (select { name : S t r i n g :$g} where { name . _ :$g} in $g )13
∪ c o l _ C l a s s 2 T a b l e ($g ) ∪o w n e r _ C l a s s 2 T a b l e ($g ))}14| C l a s s 2 R e l a t i o n a l ({$l :$g})= {}15
in C l a s s 2 R e l a t i o n a l ($db)
23

Listing 4: Class2Table with identifier injection in UnQL

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

= module i d ; create i d : i d from i d : i d ; r+r = rule i d from i n P a t to o u t P a t +inPat = id : o c l T y p e xguardx g u a r d = g u a r d | let i d : o c l t y p e = x O c l E x p in x O c l E x p| i d : i d ( . . . ) | x O c l E x p . x O c l E x p −>x O c l E x p | . . .
g u a r d = o c l E x p . isEmpty() | o c l E x p . i d| not g u a r d | g u a r d and g u a r d| g u a r d or g u a r doutPat = id : o c l T y p e b i n d i n g ∗b i n d i n g = id ← x O c l E x p
x O c l E x p = o c l E x p | let i d : o c l t y p e = x O c l E x p in x O c l E x p| i d : i d ( . . . ) | x O c l E x p . x O c l E x p −>x O c l E x p | . . .
oclExp = id
| o c l E x p . id
| string| oclExp + oclExp

ATL

Listing 5: ATL syntax given to projection Π