%\vspace{-0.5cm}
\section{Related Work}\label{sec:related}
%\vspace{-0.3cm}

As already mentioned, model transformation is intrinsically difficult, and its nature poses a number of obstacles in providing adequate support for bidirectionality and change propagation. As a consequence a large number of proposals impose relevant restrictions of the characteristics of the involved transformations, i.e. mappings are required to be bijective. Such comparison is discussed in~\cite{HLR08}.
\cite{Stevens07} organizes the existing bidirectional transformation solutions in different categories
by distinguishing approaches based on QVT-R, graph transformation techniques, and XML-based options, to mention a few.
Characterizations of model transformation languages based on the features they satisfy are presented in ~\cite{CH06,MVG06}. The taxonomy proposed in the latter aims to help developers in deciding which model transformation approach is best suited to deal with a particular scenario.


%Declarative approaches to model transformations offer several benefits like for example implicit source model traversal, automatic traceability management, implicit target object creation, and implicit rule ordering 

%For instance, approaches like ~\cite{PMD05,GW06,MHT04,FGMPS07} require the mappings to be total, while ~\cite{PMD05,GW06,XSHT09} impose the existence of some kind of bijection between the involved source and target. 

%A similar comparison to the one developed for this work was already discussed in ~\cite{HLR08} 
%Czarnecki ~\cite{CH06}  %Although not focused on the bidirectional approaches the survey highlights some interesting features strictly related to the typical restrictions. 

Stevens, in ~\cite{S09}, discusses bidirectional transformation focusing on basic properties which such transformations should satisfy: %In particular, (i) correctness ensures a bidirectional transformation does something useful according to its consistency relation, (ii) hippocraticness prevents a transformation from does something harmful if nether model is modiﬁed by users, (iii) ﬁnally, undoability is about the ability whether a performed transformation can be deleted. 
the paper considers QVT-R as applied to the specification of bidirectional transformation and analyse requirements and open issues. Furthermore, it points out some ambiguity about whether the language is supposed to be able to specify and support non-bijective transformations. Despite the potentiality of the language, its tool support remains limited. Currently Medini QVT \footnote{http://projects.ikv.de/qvt} and ModelMorf \footnote{http://www.tcs-trddc.com/trddc\_website/ModelMorf/ModelMorf.htm} are two of the most used tools. 

A number of different approaches based on TGGs have been proposed. Remarkable is the PROGRES approach ~\cite{BHLW07} a TGG solution to create integration tools also taking care of non-deterministic cases. %Such work detects ambiguities and asks the user for choices whenever they happen. 
PROGRES demands users’ intervention to rule execution, meaning that users will have to foresee the effects of each rule application and choose the desired behaviour.
Furthermore, a series of works dealing with correctness and functional behaviour of model transformations and model synchronizations based on TGGs exists. In particular, \cite{HEGO10} shows how to increase the efficiency of TGGs without losing correctness and completeness and how the so-called filter NACs can be used to reduce the non-determinism of TGGs. ~\cite{HEOCDX11} proposes a formal framework for model synchronisation where TGGs are used to generate bidirectional update propagation operations. Furthermore, the authors prove the correctness and completeness of the framework. 

Some interesting solutions have been proposed as based on lenses~\cite{FGMPS07}, where lenses define a state-based framework for asymmetric synchronization. Lately the works on lenses shift the focus on the delta-based framework for considering the symmetric synchronization~\cite{DXCEHO11}. Unfortunately, the management of non-bijective problems is not clearly addressed, even though it could be theoretically supported by means of delta merging and conflict resolution. Moreover, at now there exist no available implementations relying on such theories.


  %In this way, mappings can be described in terms of cause and effect relations between source and target model deltas, respectively. 
%The authors developed an extensive theory based on lenses and properties of related operators. Unfortunately, the management of non-bijective problems is not clearly addressed, even though it could be theoretically supported by means of delta merging and conﬂict resolution. % However, at now, there exist no available implementations based on such theories.

%In ~\cite{XSHT09} an attempt is proposed to automate model synchronization from model transformations. It is based on QVT-R and supports concurrent modiﬁcations on both source and target models; moreover, it propagates both sides changes in a non destructive manner. However, some issues come to light: in fact, conﬂicts may arise when merging models obtained by the propagation with the ones updated by the user. Additionally, it is not possible to manage manipulations that makes the models to go outside the domain of the transformation.

A number of interesting applications is available, varying from incremental techniques~\cite{HLR06,GW09} to the automation of transformation specifications by means of the inductive construction of first-order clausal theories from examples and background knowledge ~\cite{BV08}. 


%The formal definition of a round-trip engineering process taking into account the non-totality and non-injectivity of model transformations is presented in ~\cite{HLR08}. %The valid modiﬁcations on target models are limited to the ones which do not induce backward mappings out the source metamodel and are not operated outside the transformation domain.
