Triple graph grammars (TGGs) have been applied successfully for specifying and analysing bidirectional model transformations. Recently, a formal approach to concurrent model synchronisation has been presented, where source and target modifications are synchronised simultaneously. In addition to methods for update propagation, the approach includes a semi-automatic strategy for conflict resolution. Up to now, this approach has been limited to deterministic propagation operations. In this paper, we generalise the approach to arbitrary TGGs and consider nondeterministic operations which might yield di erent results and require backtracking. We show correctness and completeness of the extended approach and provide a technique for reducing and possibly eliminating backtracking to improve e ciency.
Bidirectional model transformations have been specified and analysed successfully using triple graph grammars (TGGs) [17,18]. More recently, TGGs have also been applied in case studies for model integration and model synchronisation [14,5,7]. Model synchronisation aims to propagate updates between interrelated domains in order to derive updated models that are consistent with each other. The formal results concerning correctness and completeness are a major advantage of TGGs in this field [12]. Consistency conditions are specified in a concise way and they are automatically respected by the synchronisation process. In an industrial project on model transformations for satellite systems, we make explicit use of these properties with great advantage [13].
Since model changes may occur concurrently in related domains and in a distributed way, model synchronisation has to cope with update propagation, update merging, and conflict resolution. In this paper, we use the concurrent model synchronisation approach based on triple graph grammars [9]. Possible conflicts are resolved in a semi-automated eWilly Wilson ineBase=500 traBonus=0 eWilly Wilson ineBase=500 traBonus=0 d1S
Alex Archer Base=3000 Bonus=1000 Alex Archer Base=3000 Bonus=1500 r 0 way. The operations are realised by model transformations based on TGGs [12] and tentative merge constructions solving conflicts [9].
Fig. 1 illustrates the running example of this paper in concrete syntax. The source domain (left) contains employees of the marketing department and trainees (indicated by a box trainee). The target domain (right) contains all employees. Upper right boxes indicate their assignment to departments (M = Marketing, empty = trainees). In target update d1T , Willy Wilson and Molly Murphy get hired by the marketing department. Bonus and salary values for Alex Archer are increased synchronously on both domains.
The synchronisation framework presented in [9] is limited to a restricted kind of TGGs that ensure deterministic propagation operations. This requirement is often complex to check for medium and large scale applications. In this paper, we generalise the approach to arbitrary TGGs, such that the operations are in general non-deterministic. This includes the deterministic case, but we do not have to check for determinism. Nondeterminism means that the operations may require backtracking and may yield several possible results. In our first main result (Thm. 2.5), we show that the derived nondeterministic synchronisation framework is correct and complete for any given TGG.
In order to reduce backtracking e orts, we eliminate conflicts between operational rules by adding additional negative application conditions (NACs), called filter NACs. This concept was already applied successfully in the area of model transformations [10]. In a second step, the synchronisation operations are extended automatically with compatible NACs and we show in the second main result (Thm. 3.4) that these changes do not a ect the correctness and completeness results for the derived synchronisation framework. In case that all relevant conflicts are eliminated, this ensures that concurrent model synchronisation can be performed e ciently, i.e., without backtracking.
Sec. 2 generalises the formal framework for concurrent model synchronisation [11,9] to non-deterministic forward and backward propagation operations. Sec. 3 provides an automated technique for improving e ciency. After discussing related work in Sec. 4, we conclude the paper and discuss directions for future work in Sec. 5. We provide full details of the example and the formal theory in an accompanying technical report [6]. 2
The synchronisation of concurrent model updates in two domains means to derive a new consistent integrated model together with corresponding updates on both domains. This section generalises the formal framework in [11,9] to the non-deterministic case.
G = (GS o sG
GC tG / GT ) m mS mC
mT H = (HS o sH
HC tH / HT ) graph morphism
L tr / R m (PO) n
G t / H
(PO)
Triple graph grammars (TGGs) are a suitable formal approach for defining a language of consistently integrated models [17,3]. An integrated model is represented by a triple graph G consisting of graphs GS , GC, and GT , called source, correspondence, and target graphs, together with two mappings (graph morphisms) sG : GC ! GS and tG : GC ! GT for specifying the correspondence links between elements of GS and GT .
Triple graphs are related by triple graph morphisms m : G ! H [17,3] consisting of three graph morphisms that preserve the associated correspondences (i.e., left diagrams in Fig. 2 commute). Triple graphs are typed over a triple type graph TG and attributed according to [3]. For a triple type graph TG = (TGS TGC ! TGT ), we use L(T G), L(T GS ), and L(T GT ) to denote the classes of all graphs typed over TG, TGS , and TGT , respectively.
A triple graph grammar TGG = (TG; S ; TR) consists of a triple type graph TG, a triple start graph S and a set TR of triple rules, and generates the triple graph language of consistently integrated models L(TGG) L(TG) with consistent source and target languages LS = fGS j (GS GC ! GT ) 2 L(TGG)g and LT = fGT j (GS GC ! GT ) 2 L(TGG)g. A model update d : G ! G0 is specified as a graph modification d = (G i1 I !i2 G0) with inclusions i1 : I ,! G and i2 : I ,! G0. Intuitively, all elements in G n I are deleted and all the elements in G0 n I are added by d. Example 2.1 (Triple Type Graph). Triple type graph T G in Fig. 3 specifies the structure of source and target models. In FirstNPameres:oSntring the source domain, persons are attributed LastName: String twaiitlehdtshaeliarryfiirnstfoarnmdatliaosnt (nbaamseea,ntdhebiorndues-) IBBsaoTsnraeu:isn:ReReeea:laBloolean PP and their state of employment (trainee or permanent). Persons in the target domain Fig. 3. Triple type graph are attributed with their first and last name, birth date and their total salary. The membership to a department is provided by a direct link to the department. Trainees have no link to any department.
A triple rule tr = (trS ; trC; trT ) is non-deleting and therefore, can be formalised as an inclusion from triple graph L (left hand side) to triple graph R (right hand side), represented by tr : L ,! R. The application of a triple rule tr via a match morphism m : L ! G yields a triple graph transformation (TGT) step G =t=r=;m) H with triple graph H defined by the pushout diagram (PO) in Fig. 2 (L is replaced by R in G) [18].
:Person IsTrainee = F ++ ++ ++ :PP ++
FirstN:Paemrseon= n++ :PP :Department name=“Marketing“ ++ :dep :Person ++ N :Department AC name=“Marketing“ ++ :Person FirstName = n++
++ ++ :Person IsTrainee = F ++
Moreover, triple rules can be extended by negative application conditions (NACs) for restricting their application to specific matches [10].
Example 2.2 (Triple Graph Grammar). The TGG of our scenario is given by the triple type graph shown in Fig. 3, the empty start graph and the set of triple rules illustrated in compact notation in Fig. 4. All elements (nodes, edges or attributes) that are marked with ++ (green border) are added by a triple rule. Parts marked with a rectangle containing the label NAC (red border) describe negative application conditions [10]. The first triple rule Person2FirstMarketingP inserts a new department called “Marketing” into the target domain. The NAC ensures that there is no other department with the same name. In addition, this rule creates a person in both, the target and the source domain and creates a link to the marketing department (edge :dep). Attribute IsTrainee is set to F. Rule Person2NextMarketingP extends the model with a new person employed at the marketing department. Rule FName2FName sets the first name of a person in both, the source and the target domain. Rule Trainee2Trainee adds a trainee in both domains and creates a correspondence. The full TGG is presented in [6].
The signature of the concurrent synchronisation operation CSync is formalised in Fig. 5 (left) and specifies the type of the in- and output elements. Given an integrated model G0 = (GS0 $ G0T ), source model update d1S = (GS0 ! GS1 ) and target model update d1T = (G0T ! G1T ), we need to find source update d2S = (GS1 ! GS2 ) and target update d2T = (G1T ! G2T ) together with a new integrated model G2 = (GS2 $ G2T ) [9]. The integrated model may not be unique in the case of a non-deterministic synchronisation operation. Correctness (right of Fig. 5) ensures that any resulting integrated model G2 = (GS2 $ G2T ) is consistent (law (a)), i.e., G2 2 L(TGG). Furthermore, if the given input is initially consistent and the updates do not change anything, then one of the possible outputs of operation CSync is identical to the input itself (law (b)). In case of deterministic TGGs, law (b) requires that the output is always the identity, because there is exactly one output. Completeness means that CSync yields at least one possible output for any input.
Definition 2.3 (Non-Deterministic Concurrent Synchronisation Problem and Framework). Given a triple type graph TG, the concurrent synchronisation problem is to construct a non-deterministic operation CSync leading to the signature diagram
S T GS o d1 GS o r0 / G0T d1 / G1T
1 0 d2S GS o 2 :CSync r2
d2T / G2T
GS o
2 d2S
S T GS o d1 GS o r0 / G0T d1 / G1T 1 0 +:CSync
d2T / G2T r2:L(TGG) (a)
8 c 2 L(TGG) : GS o 1 GS o c / GT 1 / GT 1 1 GS o / GT +:CSync c (b) in Fig. 5 with concurrent synchronisation operation CSync. Given a triple graph grammar TGG = (TG; ?; TR) and a concurrent synchronisation operation CSync, the nondeterministic concurrent synchronisation framework CSync(TGG; CSync) is called correct, if laws (a) and (b) in Fig. 5 are satisfied; and it is called complete, if operation CSync is a left total relation.
The formal approach to concurrent model synchronisation based on TGGs [9] is performed in five steps (see Fig. 6). We describe the forward case (operation fSync), i.e., the synchronisation is initiated in the source domain. The symmetric backward case (bSync) works analogously by switching the roles of source and target domains and exchanging fPpg with bPpg, and CCS (consistency creating on source domain) with CCT (consistency creating on target domain). The concurrent synchronisation operation CSync = (fSync [ bSync) is defined by the union of both cases.
Concept 2.4 (Execution of non-deterministic synchronisation framework). In contrast to previous work [9], we do not require deterministic TGGs, such that all five steps may yield several results and steps 1,2,4, and 5 may require backtracking. The first step (1:CCS) is executed via consistency creating operation CCS on the source domain and computes a maximal sub-model GS1;C 2 LS of the given model GS1 that is consistent with respect to the language LS (language of consistent source models). We obtain source update d1S;CC : G0S ! GS1;C. In general, consistency creating operations CCS (source domain, step 1) and CCT (target domain, step 4) remove strucG2;FCB = (GS2;FCB $ G2T;FCB). tures that cannot be translated, i.e., those that cannot appear in any consistent integrated model. In step 2, we apply forward propagation operation fPpg (Fig. 6) to propagate the changes to the target domain and we obtain target update d T 1;F and integrated model G1;F = (GS1;C $ G1T;F ). In step 3, we apply conflict resolution operation Res [9] in order to merge the two updates on the target domain: the propagated update d1T;F and the given update d1T . This leads to a new target update d02T;FC : G1T;F ! G2T;FC. We apply consistency creating operation CCT to obtain the maximal consistent sub-model of G2T;FC and derive the target updates dT : G2T;FC ! G2T;FCB and d2T;CC : G1T;F ! G2T;FCB. Finally, we
B
T propagate update d2;CC from the target to the source domain via backward propagation operation bPpg leading to source update d2S;CB : GS1;C ! GS2;FCB and integrated model
Our first main result (Thm. 2.5) shows that the non-deterministic concurrent synchronisation framework is correct and complete, such that all outputs are consistent and all all inputs can be processed. Termination is ensured, if each operational translation rule changes at least one translation attribute, which can be e ciently checked [9,12]. Theorem 2.5 (Correctness and Completeness of Non-Deterministic Concurrent Synchronization Framework). Given a triple graph grammar TGG, the derived nondeterministic concurrent synchronisation framework CSync(TGG; CSync) is correct and complete.
Proof (Idea). We extend the result for deterministic TGGs in [9] using the general composition and decomposition theorem for TGGs [3]. The main step is to show that backtracking of forward propagation (step 2) and backward propagation (step 5) ensures that the approach computes a correct sequence. For the full formal construction and This section shows how to reduce and possibly eliminate backtracking of the general non-deterministic concurrent model synchronisation framework in Sec. 2 by removing conflicts between the operational rules of a TGG using the concept of filter NACs [10].
The derived operational rules of a TGG consist of consistency creating rules TRCC, forward translation rules TRFT , and backward translation rules TRBT [12]. These rules contain additional Boolean valued translation attributes, which are used to mark the elements (nodes, edges or attributes) that are translated by the rules (TRFT and TRBT ) or marked as consistent (TRCC), respectively. The translation attributes are named tr x, where x is the name of the respective element. See for example the rules in Fig. 7. Forward translation rules translate elements from the source domain and add the missing elements in the correspondence and target components according. Analogously, backward translation rules translate elements of the target domain and consistency creating rules mark the elements that are consistent.
A filter NAC specifies a context of a translation rule, which will always lead to an incomplete translation [10]. This means that applying the rule in any context containing the NAC pattern will require to backtrack this step. Such steps are avoided by the NAC. proof see [6]. 3
E ciency Improvement tu
++ Example 3.1 (Addition of Filter NACs). The target model update GT ! G0T in Fig. 1 creates the person Molly Murphy belonging to the marketing department. During the synchronisation process of this update, backtracking is necessary for the following reason. Fig. 4 shows the derived and the extended operational translation rules for triple rule Trainee2Trainee in Fig. 4. These rules use translation attributes (prefix tr) for flagging the elements that have been translated already. Backward translation rule Trainee2TraineeBT (top left in Fig. 7) is applicable to the new target model G0T in the backward propagation phase of the update. But it leads to an incomplete translation, because the adjacent edge of type : dep will remain untranslated. Instead, if one of the two rules fPerson2FirstMarketingBT ; Person2NextMarketingBT g that are derived from the triple rules in Fig. 4 would be applied, then the problematic edge would be translated in the same step. The solution for eliminating this need for backtracking is to introduce a filter NAC yielding the new rule Trainee2TraineeBN (top right of Fig. 7). The NAC was obtained via the automated generation technique for filter NACs in [10]. It avoids an application to persons that belong to a marketing department. The new set of backward translation rules does not require backtracking any more, which we checked with the automated analysis of the tool AGG as described in [10].
The introduction of filter NACs causes a new problem for model synchronisation: the consistency creating rules TRCC used for marking the already consistent elements are no longer compatible with the modified backward translation rules (see Ex. 3.2). Extending the consistency creating rules TRCC by propagating the filter NACs solves the problem of incompatibility between TRCC and TRBT . Moreover, this does not introduce new incompatibilities with TRFT , if each filter NAC is domain specific, i.e., it does not forbid structure on the source and target domains simultaneously.
Example 3.2 (Extension of Consistency Creating Rules). The consistency creating rule Trainee2TraineeCC (bottom left of Fig. 7) is used for marking consistent occurrences of a trainee in both domains. However, the rule can also be applied to full employees. In that case, the update propagation process will finally have to backtrack. Consider our running example illustrated in Fig. 1. Trainee Willy Wilson becomes a full employee. Therefore, he gets assigned to a department. The initial target update would be an addition of an edge of type : dep. Therefore, the consistency creating rules will still mark every element of the integrated model G to be consistent except the new edge. However, the backward translation cannot continue at this point, because the additional edge cannot be translated separately by any rule. Hence, we introduce a corresponding NAC and derive the consistency creating rule Trainee2TraineeCN (bottom right of Fig. 7). Concept 3.3 (Extension of non-deterministic concurrent synchronisation framework with filter NACs). Let the sets TRFN and TRBN be derived from the operational triple rules TRFT and TRBT of a given TGG, respectively, by adding domain specific filter NACs to the rules. For each of these filter NACs we propagate the filter NACs to the rules in TRCC leading to an updated set TRCN of consistency creating rules. The formal definition of filter NAC propagation is given in [6]. Altogether we obtain a concurrent synchronization framework with filter NACs CSync(TGG; CSyncFN ) based on the extended sets operational rules TRCN ; TRFN , and TRBN .
Our second main result (Thm. 3.4) shows that domain specific filter NACs do not a ect the formal properties of correctness and completeness. Filter NACs concerning adjacent edges as in our example can be generated automatically [10]. Using the tool AGG, TGGs can be verified to ensure deterministic operations [12]. Moreover, conservative policies can be introduced to eliminate backtracking for attribute computations [12]. Thus, concurrent model synchronisation can be performed e ciently also in cases where the TGG operations initially require backtracking, but do not require backtracking using the generated filter NACs.
Theorem 3.4 (Correctness of Concurrent Synchronization Frameworks with Efficiency Improvement by Filter NACs). Given a triple graph grammar TGG and a set of domain specific filter NACs for the operational translation rules that have been propagated to the consistency creating rules TRCC. Then, the derived nondeterministic concurrent synchronisation framework with domain specific filter NACs CSync(TGG; CSyncFN ) is correct and complete.
Proof (Idea). The equivalence result of complete forward translation sequences with and without filter NACs in [10] has to be extended to the more complex case of forward and backward propagation. The precondition of domain specific filter NACs ensures that the propagation of filter NACs towards the consistency creating rules has no e ect for further operational rules. For the full technical details and proof see [6]. tu 4
Triple Graph Grammars were introduced in [17] and since then have been applied successfully, among others, for (concurrent) model synchronisation [5,11,9] using the generated operations for bidirectional model transformations [18,10]. The (concurrent) model synchronisation approach we use in this paper is inspired by the symmetric delta lens (sd-lens) approach introduced in [2].
Several works focus on correctness properties and functional behaviour of the model synchronisation based on triple graph grammars [11,9,16]. In [4], a categorical merge construction for two conflicting model updates is given. In [9], a general synchronisation framework for concurrent model updates is given using the results from [4] for resolving conflicts between concurrent model updates. In this work, we extend the concept of filter NACs, which were introduced in [10] for model transformation, to concurrent model transformation.
Xiong et. al. [19] introduce requirements, which shall hold for all bidirectional model updates, namely consistency, stability and preservation. These requirements are in close correspondence with the laws of correctness and identity ensured for the synchronisation framework in this present paper. The concurrent synchronisation framework in [19] requires conflict-free updates as input and is based on model di erence approaches. Our approach does not require conflict freeness and occurring conflicts are resolved in a semi-automated way. Moreover, model updates are formalised as graph modifications, which are either available directly from the used modelling tool or can be derived automatically from model di erence plugins.
In [15] an e cient control algorithm for bidirectional model transformation based on triple graph grammars is introduced and its correctness, completeness and e ciency is proven. The idea of the control algorithm is to determine dependencies of forward rules (and backward rules, respectively) in order to reduce non-deterministic behaviour in selecting the appropriate rule sequence for the transformation. This work is extended to model synchronisation in [16]. In both works, this algorithm either provides correct models as result or an error. In our approach, conflicts do not lead to errors, but are made explicit and solved semi-automatically via operations (operation Res, CCS and CCT). 5
In this paper, we have shown how concurrent modifications in source and target models that are linked by a TGG can be synchronised. More precisely, we have first introduced a non-deterministic concurrent synchronisation framework generalising the existing approach [9] to arbitrary TGGs. Furthermore, we have used filter NACs to improve the e ciency of the forward and backward propagations avoiding backtracking in cases, where parts of the models would remain untranslated.
We already applied TGGs and Henshin [
ICMT’13, LNCS, vol. 7909, pp. 50–51. Springer (2013) 14. Kindler, E., Wagner, R.: Triple Graph Grammars: Concepts, Extensions, Implementations, and Application Scenarios. Tech. Rep. TR-ri-07-284, Department of Computer Science, University of Paderborn, Germany (2007) 15. Lauder, M., Anjorin, A., Varro´ , G., Schu¨ rr, A.: Bidirectional Model Transformation with Precedence Triple Graph Grammars. In: Proc. ECMFA’12. LNCS, vol. 7349, pp. 287–302.
Springer (2012) 16. Lauder, M., Anjorin, A., Varro´ , G., Schu¨ rr, A.: E cient Model Synchronization with Precedence Triple Graph Grammars. In: Proc. ICGT’12. LNCS, vol. 7562, pp. 401–415. Springer (2012) 17. Schu¨rr, A.: Specification of Graph Translators with Triple Graph Grammars. In: Proc.
WG’94. LNCS, vol. 903, pp. 151–163. Springer (1994) 18. Schu¨rr, A., Klar, F.: 15 Years of Triple Graph Grammars. In: Proc. ICGT’08. pp. 411–425.
No. 5214 in LNCS, Springer (2008) 19. Xiong, Y., Song, H., Hu, Z., Takeichi, M.: Synchronizing concurrent model updates based on bidirectional transformation. SoSyM 12, 89–104 (2013)