arXiv CSopen access

Conflict Essences for Transformation Rules with Nested Application Conditions -- Long Version

Conflict Essences for Transformation Rules with Nested Application Conditions – Long Version Alexander Lauer1

, Jens Kosiol1 , Leen Lambers2 , and Gabriele Taentzer1

arXiv:2605.04947v1 [cs.SE] 6 May 2026

1

Philipps-Universität Marburg, Marburg, Germany [email protected] {kosiolje,taentzer}@mathematik.uni-marburg.de 2 Brandenburg University of Technology Cottbus-Senftenberg, Cottbus, Germany [email protected]

Abstract. Conflict and dependency analysis is an important static analysis tool that provides an overview of the potential interactions of (graph) transformation rules. This analysis is based on critical pairs and initial conflicts, which represent conflicting transformations in a minimal context. However, the crucial information about a conflicting transformation pair is contained in much smaller structures, called disabling/conflict essences in existing research. Recently, we introduced disabling essences for rules with application conditions which contain the information on how an application condition can be violated by another rule. In this paper, we extend the notion of disabling essences to support not only application conditions in Alternating Quantifier Normal Form, but also arbitrary nested conditions. We introduce (symbolic) conflict essences that are constructed from disabling essences and which capture the interaction between two rules. We show that a transformation pair is parallel dependent if and only if a symbolic conflict essence can be embedded into it and relate symbolic conflict essences to initial conflicts for transformation rules with application conditions. We present our results for adhesive HLR categories, which includes several types of graph-like structures. Keywords: Graph transformation · Critical pair analysis · Static analysis · Adhesive HLR categories

1

Introduction

The algebraic approach to graph transformation [4,5] has a broad range of interesting applications, especially in software engineering [11]. Transformation rules specify how graphs can be modified by either deleting existing elements or creating new elements. In addition, rules may be equipped with a nested application condition to further model the situations in which a rule is allowed to be applied. When multiple rules are to be applied to the same graph, they can interact in the sense that one rule might prevent the application of the other by either deleting elements that are used in the other transformation or by inserting or deleting

2

Lauer et al.

Initial Conflict [15]

induces [15]

is extended to [17]

Conflict Essence [3]

uniquely determines [3] represented by unique [15]

represented by unique [3]

Conflict

contained in (Def. 11)

Conflict Essence (Def. 11) induces [17]

For rules without nested application conditions

contained in [20] partly contained (Def. 11)

Disabling Essence [20]

For rules with nested application conditions

induces (Th. 2) represented by (Th. 2)

(Symbolic) Initial Conflict [17]

Disabling Essence [3]

induces [3] represented by (Cor. 2)

represented by unique [17]

contained in [3]

relates to unique (Th. 3) has at least one (Th. 3)

contained in (Def. 12)

Symbolic Conflict Essence (Def. 13)

Fig. 1: Overview of concepts for conflicts between rules with and without nested application conditions (where square brackets contain literature references and round brackets refer to concepts and results of this paper). elements so that the application condition is not satisfied anymore. Then one rule is said to cause a conflict for the other. Statically analysing rules for these interactions plays an important role in applications such as feature interaction detection, model versioning, test case generation, and graph parsing (see [18] for an overview of such applications). Each of these analysis techniques provides an overview of all potential conflicts for a given rule set with different types of granularities. Critical pairs describe conflictual transformation pairs in a minimal context [7], whereas initial conflicts (a subset of the set of critical pairs of a rule pair) describe conflictual transformation pairs with minimal overlaps. Since critical pairs contain unnecessary information for many applications [18], research has been conducted to extract only the essential information about potential conflicts [3, 14, 16, 18, 20]. All notions developed for plain rules (i.e., those without application conditions) are closely related as shown at the top of Figure 1. Conflict reasons [14] or conflict essences [3] show the core information of a conflict, namely, the elements whose deletion leads to a conflict. Both approaches only consider plain rules. Since practical applications usually involve rules with conditions and these can be involved in conflicts, this is a significant gap in the research. We have started to address this gap by introducing disabling essences for rules with application conditions in Alternating Quantifier Normal Form (ANF) [20]. These essences describe how a rule can prevent the application of another rule by either deleting its used elements or by violating its application condition. We showed that in each pair of conflicting transformations a disabling essence can be embedded. Conversely, an embedding of a disabling essence does not imply that the transformations are in conflict, which is a limitation of the theory. In this paper, we continue our work on disabling essences for rules with application conditions as follows: (1) We generalise our construction to support arbitrary nested application conditions. (2) We introduce conflict essences for rules with application conditions, which describe situations in which both transformations cause a conflict for the other. To achieve this, we present a construction for composing disabling essences and conflict essences. (3) We define symbolic conflict essences, which are conflict essences with additional application conditions

Conflict Essences for Nested Application Conditions

3

that ensure they are only embeddable in conflictual transformation pairs. (4) We relate symbolic conflict essences to initial conflicts for rules with application conditions (see Figure 1). Whereas contribution (1) is a rather straightforward extension of our work in [20], contributions (2)–(4) are results we did not already obtain for conditions in ANF there. The paper is structured as follows: Section 2 presents related work on conflict analysis. Section 3 presents the example used throughout the paper. Section 4 presents the formal preliminaries, Section 5 introduces our generalised construction for disabling essences, Section 6 addresses conflict essences, and Section 7 introduces symbolic conflict essences and relates them to initial conflicts. Appendices contain all proofs (Section A) and additional examples (Section B).

2

Related Work

We have thoroughly discussed related work on the topic of this paper in [20]. Therefore, we here just focus on providing the immediate context of our work. A critical pair is a pair of conflicting transformations in a minimal context and the set of all critical pairs gives an overview of all conflicts of a graph transformation system (completeness). Since critical pairs tend to be large objects, and even small transformation systems can induce large sets of critical pairs, two orthogonal research directions have been pursued: (1) reducing the number of critical pairs that must be computed while ensuring completeness and (2) identifying objects that contain the core information about conflicting transformations more compactly than critical pairs do. Both has been addressed first for plain rules and subsequently also for rules with application conditions. Regarding (1), it has been found that (under certain technical conditions) so-called initial conflicts are the smallest set of critical pairs that is still complete [15]; this also holds in the presence of application conditions (where initial conflicts then become symbolic) [17]. Regarding (2), i.e., computing the core information contained in a conflict, we [14] as well as Azzi et al. [3] introduced (minimal) conflict reasons and conflict essences, respectively, as suitable such objects and also showed their unique correspondence to initial transformations. Importantly, these works only treat plain rules. That is, a notion of conflict essences and clarification of their relation to initial conflicts is still missing in the presence of application conditions. We started work in this direction in [20], were we lift the notion of disabling essences of Azzi et al. to the setting of rules with application conditions. However, we only addressed application conditions in ANF and did not develop a composition of disabling essences to yield conflict essences (considering the conflicts caused by each of the two transformations for the other simultaneously) or relate them to initial conflicts – both of which we do in this paper for general application conditions.

4

Lauer et al. Rule decapsulateAttribute(in N:EString, in cIN:EString)

«preserve» 1:Class name=cIN

«delete» methods

«preserve» variables

Rule pullUpEncapsulatedAttribute(in subCIN:EString, in superCIN:EString, in N:EString)

«delete» 3:Method name="set" + N «delete» methods

«preserve» 4:Attribute name=N visibility="private"->"public"

«delete» 2:Method name="get" + N

«preserve» generalizes

«preserve» 6:Class name=subCIN «delete» variables «preserve» 8:Attribute name=N

«preserve» 5:Class name=superCIN «create» methods «create» methods «preserve» «delete» 7:Method methods name="set" + N

«create» variables

«delete» methods «preserve» 9:Method name="get" + N

Fig. 2: Henshin rules of our running example

P3 P2

P1 5:Class

10:Class generalizes

10:Class

10:Class

variables

methods

12:Method name = " set" + N

11:Attribute

variables

name = N vis. = " public"

11:Attribute

13:Method

name = N vis. = " private"

name = "get" + N

methods

Fig. 3: Additional application condition for rule pullUpEncapsulatedAttribute

3

Running Example

To illustrate our work, we will consider two refactoring methods [8]. Typically, a sequence of refactorings is required to achieve a larger system design improvement. Due to the potential of implicit conflicts and dependencies between refactorings, developers may have difficulties determining which refactorings to use and in what order. The identification of potential conflicts and dependencies can help developers in specifying correct refactorings. Assuming graphs that model the class design of software systems, we consider Figure 2 for two class model refactorings being specified as graph-based transformation rules. These rules are depicted in an integrated form (as used, e.g., in the model transformation tool Henshin [1]), with annotations specifying which graph elements are deleted, preserved, or created. The preserved and deleted elements form the Left-Hand Side (LHS) of a rule, and the preserved and created elements form the Right-Hand Side (RHS). Rule decapsulateAttribute removes the getter and setter methods for a given attribute, thus inverting the well-known encapsulate attribute refactoring. Rule pullUpEncapsulatedAttribute takes an attribute with its getter and setter methods and moves them to a superclass. The rule pullUpEncapsulatedAttribute has an additional nested application condition that is depicted in Figure 3. This condition specifies that all subclasses of 5:Class must also have a private attribute named N and corresponding getter and setter methods or a public attribute named N. In our presentation of the application condition, we omit morphisms and recurring parts of graphs.

Conflict Essences for Nested Application Conditions

4

5

Preliminaries

In this section, we present the preliminaries of our work. For reasons of space, we omit standard background information and technical details that are required for the proofs, but which are not necessary for understanding the main ideas of the paper. In particular, we assume familiarity with basic category theory (including the concept of adhesiveness) and the double-pushout approach to graph transformation [4, 5, 13]. A full introduction that covers all the necessary details can be found in [3]. Here, we recall nested conditions and concepts related to parallel independence. Throughout our work, we make the following assumptions: we work in an adhesive HLR category (C, M) with all pullbacks, initial pushouts over M-morphisms, an M-initial object ⊥, whose outgoing arrows are denoted by !A : ⊥ ,→ A for any object A, initial transformations, binary coproducts, and a unique E ′ -M factorization of cospans of morphisms. The semantics we assume for transformations in this paper is the doublepushout approach [5]. Thus, a transformation t : G =⇒ρ,m H comes with a g

h

span G ← −- D ,− → H of M-morphisms that has been computed via two pushouts l

r

for some transformation rule ρ = (L ←−- K ,−→ R, ac) and a match m of ρ in G (satisfying the application condition ac of ρ); G is the input (graph) of t, the context (graph) D is computed as a pushout complement (by deleting the elements specified by ρ from G), and H is computed as a pushout (by creating the elements specified by ρ on top of D). An ac-disregarding transformation is one for which the match does not need to satisfy the rule’s application condition. Nested Conditions. In the context of graph transformation, nested conditions and constraints have been developed as a suitable (graphical) formalism for expressing properties of graphs and graph homomorphisms. They have been shown to be expressively equivalent to first-order logic on graphs [10, 22], but can be defined for arbitrary categories. Definition 1 (Nested condition). A nested condition over an object P0 is defined recursively as follows: true is a condition over P0 , each Boolean combination of conditions over P0 is a condition over P0 , and ∃ (p1 : P0 → P1 , d) is a condition over P0 if d is a condition over P1 . A morphism q : P0 → G satisfies a condition c = ∃ (p1 : P0 → P1 , d), denoted by q |= c, if there is an M-morphism q1 : P1 ,→ G ∈ M so that q = q1 ◦ p1 and q1 |= d. Satisfaction for nested conditions composed by Boolean operators is defined as usual. We use the abbreviation ∀ (p0 : P0 → P1 , d) := ¬∃ (p0 : P0 → P1 , ¬d). The object P1 in a condition of the form ∃ (p0 : P0 → P1 , d) is called existentially bound and the object P1 in a condition of the form ∀ (p0 : P0 → P1 , d) is called universally bound. In this paper, we make the following assumptions about all conditions: (i) All morphisms appearing in a condition are M-morphisms, except potentially those

6

Lauer et al. k1′

B

C

(3)

A′1

c

A

k1 a1

(2)

R1

r1

K1

L1

l1

n1

a2

(4)

L2

(1) m1

l2

h1

D1

K2

r2

m2

R2 n2

d1

H1

A′2

k2

d2 g1

G

g2

D2

h2

H2

Fig. 4: Parallel independence and construction of disabling essence starting at the object P0 over which the condition is defined (i.e., the condition is in M-normal form); (ii) no isomorphisms appear in a condition; (iii) all negations are pushed inward as far as possible by eliminating double negations, replacing existential quantifiers with universal ones (and vice versa), and applying De Morgan’s law (in this way, it is unambiguous whether an object is bound existentially or universally). These assumptions do not restrict the expressivity of the considered conditions; the desired presentation can be achieved by applying well-established equivalence rules [10, 21]. Conditions can be shifted along morphisms and left-translated along rules using operations called Shift and Left, respectively, in such a way that the semantics of the conditions are preserved [5, 10]. We will use these operations in the following without recalling their definitions. Parallel independence. Two parallel independent transformations do not interfere with each other. This concept is formally captured by the Local Church–Rosser theorem [4], which states that two such transformations can be applied in any order. We recall the definition of parallel independence and revisit the notion of a disabling essence [3] for analysing transformations that conflict with each other, i.e., those that are not parallel independent. Definition 2 (Parallel independence). Given two rules ρj = (Lj ←- Kj ,→ Rj , acj ), with j = 1, 2, two transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 H1 , G =⇒ρ2 ,m2 H2 ) are parallel independent if there are morphisms d1 : L2 → D1 and d2 : L1 → D2 to the contexts of t1 and t2 so that m2 = g1 ◦ d1 , m1 = g2 ◦ d2 , h1 ◦ d1 |= ac2 , and h2 ◦ d2 |= ac1 (as shown in Figure 4). If the morphism d1 does not exist, or if h1 ◦ d1 ̸|= ac2 , we say that t1 causes a conflict for t2 . We say that t1 and t2 are parallel independent ac-disregarding if both morphisms dj exist. A transformation via a plain rule causes a conflict with another such transformation if it deletes items that the second transformation also requires. A disabling essence captures exactly this problematic structure and its occurrence in conflicting transformations. The construction can be introduced for arbitrary cospans of the LHSs of rules, leading to the notion of a proto-essence, whereas only matches for transformations lead to a disabling essence.

Conflict Essences for Nested Application Conditions

7

Definition 3 (Proto-/disabling essence [3]). Given two plain rules ρj = Lj ←- Kj ,→ Rj and morphisms mj : Lj → G, with j = 1, 2, the proto-essence for (m1 , m2 ) under l1 , denoted by essl1 (m1 , m2 ), is defined as (a1 ◦ c, a2 ◦ c), where the squares (1) and (2) in Figure 4 are pullbacks and (3) is the initial pushout over k1 . C is called the essence object. A proto-essence essl1 (m1 , m2 ) is a disabling essence if m1 and m2 are matches for transformations t1 and t2 as in Figure 4; in that case, it is denoted as essdbl (t1 , t2 ) and called the disabling essence of (t1 , t2 ). For ease of notation, we will sometimes drop the morphism c in proto-essences if it is not needed. Crucially, transformation t1 causes a conflict for t2 if and only if the disabling essence essdbl (t1 , t2 ) is not trivial, i.e., if it is not the pair of morphisms (!L1 : ⊥ → L1 , !L2 : ⊥ → L2 ) [3, Theorem 3.13]. Initial conflicts. Starting with the notion of critical pairs, parallel (in)dependence of transformation pairs has been related to the kind of transformation pairs they extend, culminating in the concept of initial conflicts [14,17] and, for plain rules, the construction of initial conflicts from conflict reasons [3, Theorem 4.4]. In this paper, we continue this line of research to complete the picture for rules with application conditions. The following definitions briefly introduce the necessary concepts. For a detailed introduction to symbolic transformation pairs, the construction of the corresponding application conditions, and initial conflicts, we refer to [3, 6, 17]. Definition 4 (Extension of transformation. Initial transformation pair). Given a transformation t = G =⇒ρ,m H, an extension of t is a transformation t′ = G′ =⇒ρ,m′ H ′ such that there is an extension morphism f : G → G′ with f ◦ m = m′ such that f is a match in G′ for the transformation t : G ←- D ,→ H when considered as rule. Given a transformation pair (t1 , t2 ), an initial transformation pair for (t1 , t2 ) is an ac-disregarding transformation pair (tI1 , tI2 ) such that (i) there is a common extension morphism f I from the transformation tI1 to t1 and from tI2 to t2 and (ii) the transformation pair (tI1 , tI2 ) factors uniquely through any other transformation pair that (t1 , t2 ) extends by a common extension morphism. Definition 5 (Symbolic transformation pair and initial conflict). Given two rules ρ1 and ρ2 , a symbolic transformation pair stpG = (tpG , ac G , ac ∗G ) consists of a pair tpG : H1 ρ1 ,m1 ⇐= G =⇒ρ2 ,m2 H2 of ac-disregarding transformations and conditions ac G , ac ∗G over G defined as ac G = Shift(m1 , ac1 ) ∧ Shift(m2 , ac2 ) and ac ∗G = ¬(ac∗G,d1 ∧ ac∗G,d2 ), where ac∗G,d1 = false if d1 does not exist and ac∗G,d1 = Left(G ←- D1 ,→ H1 , Shift(h1 ◦ d1 , ac2 )) otherwise (analogously for ac∗G,d2 ). An initial conflict for two rules ρ1 and ρ2 is a symbolic transformation pair stpK = (tpK , ac K , ac ∗K ) such that tpK is (i) an initial transformation pair for itself and (ii) is conflict-inducing, i.e., it extends to at least one conflicting pair of transformations H1 m1 ,ρ1 ⇐= G =⇒m2 ,ρ2 H2 .

8

Lauer et al.

A1L1P3

A3L1P3

A2 L1P3 C1L1P3

C3 L1P3

C2 L1P3

methods

4,11:Attribute

variables

name = N vis. = " private"

methods

A4 L1P3 C4 L1P3

1,10:Class

methods

3,12:Method

4,11:Attribute

name = " set" + N

name = N vis. = " private"

1,10:Class

4,11:Attribute

C 3L1P3

C2 L1P3

C1L1P3

4,11:Attribute variables

1,10:Class methods

2,13:Method

2,13:Method

name = "get" + N

name = "get" + N

A1L2L1 C 1L2L1

3,7:Method name = " set" + N

methods

name = " set" + N

CL1L2

methods

1,10:Class 3,12:Method

AL1L2

1,6:Class

variables

name = N vis. = " private"

1,6:Class

methods

2,9:Method name = "get" + N

name = N vis = " private"

Comp(AL1L2,A2 L2L1)

Comp(AL1L2,A 1L2L1)

A2 L2L1 1,6:Class

C2 L2L1

methods

3,7:Method name = " set" + N

methods

1,6:Class

methods

1,6:Class

methods

3,7:Method name = " set" + N

methods

4,8:Attribute

4,8:Attribute

2,9:Method

name = N

name = N

name = "get" + N

Fig. 5: Disabling essences of decapsulateAttribute and pullUpEncapsulatedAttribute and composed essences In the construction of symbolic transformation pairs, ac G indicates when extending transformation pairs satisfy the rules’ application conditions and ac ∗G indicates when an extending pair of transformations is in conflict. A transformation pair is in conflict if and only if an initial conflict stpK = (tpK , ac K , ac ∗K ) extends to it and the extension morphism satisfies the condition ac K ∧ ac ∗K . Given two rules, the initial conflict (R1 + L2 iL1 ,ρ1 ⇐= L1 + L2 =⇒iL2 ,ρ2 L1 + R2 , acL1 +L2 , ac∗L1 +L2 ), where iL1 and iL2 are obtained by the universal property of the coproduct, plays an important role in Section 7 of this paper, as it is the only initial conflict that indicates a conflict caused solely by violations of the application conditions. We refer to it as the symbolic initial conflict.

5

Construction and Embedding of Disabling Essences

In this section, we extend the notion of disabling essences to cover arbitrary nested application conditions and develop a concept for embedding these into transformation pairs. To convey some intuition, we first continue our running example and then develop the formal details. Example 1 (Disabling essences). Figure 5 shows a selection of the disabling essences for the two rules in Figure 2. The graphs with gray borders show how the LHSs and/or application condition graphs need to overlap in a pair of transformations for a conflict to potentially occur. The inner graphs with orange borders constitute the essence graphs, and the identifiers in the nodes indicate how the graphs are mapped to the LHSs and/or application condition graphs. First, both rules can conflict with each other by matching to the same Methods and/or Attribute. The disabling essences AL1L2 , A1 L2L1 , and A2 L2L1 can be

Conflict Essences for Nested Application Conditions

9

computed using the methods developed for plain rules in [3, 14]. Importantly, when the two rules are matched as indicated by one of these essences, the resulting transformation pair is guaranteed to be conflicting. Second, the decapsulateAttribute rule can conflict with the pullUpEncapsulatedAttribute rule by invalidating its application condition. To capture the core structure of these conflicts in a manner similar to that of classic disabling essences for plain rules, we expect results as displayed in the first and second row of Figure 5 (cases A1 L1P3 –A4 L1P3 ). The decapsulateAttribute rule can invalidate pullUpEncapsulatedAttribute’s application condition by deleting an occurrence of P3 in Figure 3, for which there are different possibilities (e.g. deleting the getter or setter method, setting the visibility to public, or combinations thereof. While not possible in this example (given the semantics of the decapsulateAttribute rule), in principle pullUpEncapsulatedAttribute’s application condition can also be invalidated by a rule creating an occurrence of the graph P1 or deleting an occurrence of P2 . This occurs, for instance, with the rule encapsulateAttribute, the inverse of decapsulateAttribute, which switches the visibility of the attribute from public to private. On closer inspection of the example, it becomes apparent that, in principle, disabling essences between rules and application conditions can be found through overlaps in the same way as disabling essences between plain rules. The central structural difference is that these overlaps are no longer restricted to the LHSs of the rules, but also involve the application condition graphs. Moreover, conflicts cannot only arise from the deletion of existentially bound graphs of the application condition (as illustrated above) but also from the creation of universally bound graphs: A further refactoring rule could invalidate applications of pullUpEncapsulatedAttribute by creating occurrences of P1 (newly inserting inheriting classes). Importantly, (i) at points of bifurcation (like the disjunction in our example) all options have to be considered because each one can be the source of a conflict, and (ii) creating actions can also cause conflicts. Finally, the central semantic difference from the situation with plain rules is that matching a pair of rules as indicated by a disabling essence no longer guarantees a conflicting transformation pair. In our example, the deletion of an occurrence of P3 may be compensated for by the presence of an occurrence of P2 , and vice versa. Moreover, even though it is semantically dubious in our specific example, there could be several occurrences of the graphs P2 and P3 , such that deleting one of them would not invalidate the application condition. In this section, we present the construction of disabling essences for rules with arbitrary nested application conditions. We started this work in [20], where we computed disabling essences for application conditions in ANF. This is a special case in which a condition is essentially a chain of morphisms (i.e., there are no points of bifurcation caused by conjunction or disjunction). The restriction in [20] mainly served to simplify the presentation. When conditions are in ANF, disabling essences can be computed using the construction developed in [2, 3] for plain rules, which is then applied iteratively along the chain of morphisms that constitute the condition. For arbitrary conditions, whose morphisms form a

10

Lauer et al.

B

A′

K1

qi′

C

(IPO)

c

qi

A

(PB)

a1

(PB)

ePi

l1

L1

pL1

L1 Pn

bi

Pi

pi−1 ◦ . . . ◦ p1

L2

Fig. 6: Construction of proto-essences for rules with application conditions tree structure (which we will introduce next; compare also [23]), the situation is slightly more involved. The construction must be applied iteratively along each path from the root to a leaf of the tree. Definition 6 (Tree structure of a condition). Given a condition c over an object P0 , the tree structure of c is a graph Tr(c) = (VTr(c) J , ETr(c) ,i srcTr(c) , tarTr(c) ) which is recursively constructed as follows: If c = i∈I Q(p1 : P0 → i P , d ) for some index set I, ⊙ ∈ {∨, ∧}, and Q ∈ {∃, ∀}, we S1 i S S set VTr(c) = i V ∪ {P }, E = (E ∪ {p }), src = 0 Tr(c)S Tr(di ) Tr(c) 1 i∈I Tr(di ) i∈I i∈I (srcTr(di ) ∪ {(pi1 , P0 )}), and tarTr(c) = i∈I (tarTr(di ) ∪{(pi1 , P1i )}). If c = true is a condition over Pi , we set Tr(true) = (Pi , ∅, ∅, ∅), and Tr(c) = Tr(c′ ) if c = ¬c′ . Each node of Tr(c) without outgoing edges is called a leaf, the set of all leaves is denoted by Leaves(Tr(c)). Example 2 (Tree structure). Figure 3 shows the application condition of the pullUpEncapsulatedAttribute rule. The tree structure of this condition has four nodes starting with the LHS of the rule as root, which is embedded into graph P1 , which is again embedded into P2 and into P3 , the two leaves of the tree. Next, we define proto-essences for rules with application conditions; these are later filtered to obtain disabling essences. For their construction, we consider each path p in the tree structure of the second rule’s application condition that starts at the root and ends at a leaf. For each overlap (cospan) between the LHS L1 of the first rule and a leaf Pn , we iteratively calculate whether applying the rule can destroy an occurrence of a graph Pi contained within the path. We achieve this by applying the computation of proto-essences of plain rules to L1 and Pi for all i ≤ n. If such an object is found, a proto-essence by deletion has been identified. To account for the fact that the first rule might also invalidate the second rule’s application condition by creating an occurrence of one of its objects Pi , we also define proto-essences by insertion. These are computed analogously to the ones by deletion, just using the RHS R1 of the first rule instead of its LHS L1 . Definition 7 (Proto-essence for rules with conditions). Let two rules lj

rj

ρj = (Lj ← −- Kj ,− → Rj , ac j ), with j = 1, 2, the tree-representation Tr(ac 2 ) of ac 2 , an object Pn ∈ Leaves(Tr(ac 2 )) ∪ {L2 }, a path pL2 = pn ◦ . . . p1 from L2 to Pn in Tr(ac2 ), and a cospan (eL1 : L1 → L1 Pn , ePn : Pn ,→ L1 Pn ) ∈ E ′ be given.

Conflict Essences for Nested Application Conditions A' 0

11

A0

P1 generalizes

10:Class A' 1

5:Class name = superCIN generalizes

A1

6:Class name = subCIN

1,10:Class

1,10:Class variables

methods

methods

8:Attribute

9:Method

7:Method

name = N

name = "get" + N

name = " set" + N

P3 A' 2

5:Class

A2

name = superCIN generalizes

1,10:Class

1,10:Class

methods

variables

4,11:Attribute name = N

variables

4,11:Attribute name = N vis. = " private"

generalizes

3,12:Method name = " set" + N methods

2,13:Method

11:Attribute name = N vis. = " private" methods

6:Class

variables

10:Class methods

name = subCIN

variables

methods

methods

name = "get" + N

13:Method

12:Method

8:Attribute

9:Method

7:Method

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

Fig. 7: Central extract of the construction of proto-essences by deletion of the rules decapsulateAttribute and pullUpEncapsulatedAttribute The proto-essence by deletion of eL1 and ePn at level 1 ≤ i ≤ n, denoted as DPEssi (eL1 , ePn ), is defined as DPEss0 (eL1 , ePn ) := essl1 (eL1 , eP1 ◦ p1 ), ( DPEssi−1 (eL1 , ePn ) i DPEss (eL1 , ePn ) := essl1 (eL1 , ePi )

if DPEssi−1 (eL1 , ePn ) ̸= (!L1 , !Pi−1 ) , if DPEssi−1 (eL1 , ePn ) = (!L1 , !Pi−1 )

where pn ◦ . . . ◦ pi+1 is the path from Pi to Pn in Tr(ac 2 ) (and Pi is an object contained in the path from L2 to Pn ) and ePi := ePn ◦pn ◦. . .◦pi+1 (see Figure 6). The set of proto-essences by deletion of ρ1 in ρ2 , denoted by DPEss(ρ1 , ρ2 ), is the set of all proto-essences by deletion at level n of morphism pairs (eL1 : L1 → L1 Pn , ePn : Pn ,→ L1 Pn ) ∈ E ′ of all leaves Pn contained in Tr(ac 2 ). The set of proto-essences by insertion, denoted by IPEss(ρ1 , ρ2 ) is defined as IPEss(ρ1 , ρ2 ) := DPEss(ρ−1 1 , ρ2 ) where we stop the recursion at i = 1. Example 3 (Construction of a proto-essence by deletion). In this example, we sketch the computation of a proto-essence by deletion between L1 of decapsulateAttribute and the path L2 , p1 , P1 , p3 , P3 in the application condition of pullUpEncapsulatedAttribute; a detailed version is provided as Example 6 in Section B. Figure 7 shows the crucial part of the computation, not displaying graphs that are already known or identical to other graphs displayed. The construction starts with the overlap L1 P3 = P3 of L1 and P3 , to which P3 is mapped via the identity morphism eP3 = id P3 and L1 by the morphism

12

Lauer et al. C

c bj

R1

r1

K1

L1

l1

pL1 /idL1

Pj /L1

bi

h1

g1

D1

l2′

K2′

(3)

pL2

L2

l2

K2

r2

mi2

R2 n2

m2

m1

H1

(2)

Pi

(1)

mj1

n1

L′2

A

g1

G

D2

h1

H2

Fig. 8: Diagram for the embedding of rule overlaps and ac-conflicting disabling essences. Consider the alternatives Pj for the embedding of rule overlaps and L1 (separated by “/”) for ac-conflicting disabling essences that is fixed by mapping 1:Class to 10:Class. It proceeds by computing the protoessence by deletion at level 0, which is done by computing the pullback for L1 and L2 in L1 P3 , resulting in A0 (the empty graph), followed by computing the pullback of A0 and K1 in L1 , resulting in A′0 (also the empty graph). That A0 and A′0 are isomorphic indicates that the proto-essence at this level will be trivial; we therefore continue to further levels, which are computed analogously. The computation at level 1 is done using P1 instead of L2 , leading to isomorphic graphs A1 and A′1 , again indicative of a trivial proto-essence at this level. At level 2, we then use P3 instead of L2 and compute A2 and A′2 , which are not isomorphic. Because the proto-essences computed at lower levels were trivial, the proto-essence by deletion at level 2 turns out to be the proto-essence by deletion for the considered overlap L1 P3 . The actual essence graph is obtained by computing the initial pushout over the morphism from A′2 to A2 . It indicates as potential cause of a conflict that decapsulateAttribute simultaneously deletes the getter and setter methods and disables the attribute’s visibility necessary for pullUpEncapsulatedAttribute’s application condition to be valid. It is displayed as A1 L1P3 in Figure 5. To define disabling essences, we need a notion of embeddability for protoessences. To be able to provide a single definition of embeddability that also covers the further kinds of essences we introduce in this paper, we first define rule overlaps (capturing the structure all essences have) and then define embeddings for rule overlaps. Definition 8 (Rule overlap. Embedding of rule overlap). Given two rules l1

r1

l2

r2

ρ1 = (L1 ←−- K1 ,−→ R1 , ac1 ), ρ2 = (L2 ←−- K2 ,−→ R2 , ac2 ), an overlap of ρ1 and ρ2 is a tuple ro = (bj : A → Pj , bi : A → Pi , pL1 : L1 → Pj , pL2 : L2 → Pi ). Here, Pj = L1 and/or Pi = L2 is allowed. A pair of morphisms (mj1 : Pj → G, mi2 : Pj → G) is an embedding of ro in a transformation pair (t1 , t2 ) = (G =⇒ρ1 ,m1 H1 , G =⇒ρ2 ,m2 H2 ) if m1 = mj1 ◦ pL1 , m2 = mi2 ◦ pL2 and the square (1) in Figure 8 is a pullback. Disabling essences for rules with application conditions can now be defined analogously to [20]. For reasons of space, the exact construction will not be

Conflict Essences for Nested Application Conditions

13

presented in this section, as it involves a somewhat lengthier construction to shift proto-essences by insertion so that both kinds of essences are defined as the same kinds of spans. Intuitively, the definition of disabling essences filters out proto-essences that can never indicate a conflict by requiring that a disabling essence (i) is non-trivial, (ii) can actually be embedded in a transformation pair, and (iii) indicates the creation of a universally bound object or the deletion of an existentially bound one (but not vice versa); this final requirement is well-defined if conditions are given as assumed here, i.e., if all negations are pushed inwards as far as possible. Importantly, given the more general definition of proto-essences here, the requirements for disabling essences remain identical to those presented in [20]. Moreover, each result presented in [20] directly transfers to our extended construction. We have included the concrete definition of disabling essences and re-proved the main results of [20] in Appendix A.1.

6

From Disabling Essences to Conflict Essences

The disabling essences constructed in the previous section are “asymmetric” in that they only indicate potential conflicts in one direction. Next, we introduce conflict essences for rules with application conditions that capture potential conflicts between rules in both directions simultaneously. These conflict essences are defined by composing the disabling essences for both directions. When we start to compose disabling essences, i.e., when we consider the effects of both transformations on each other, some of the disabling essences that we previously computed become obsolete: A disabling essence de = (b1 ◦ c : C → L1 , bi ◦ c : C → Pi ) ∈ DEss(ρ1 , ρ2 ) indicates that the application of ρ1 can prevent the application of ρ2 by invalidating its application condition (by destroying an occurrence of Pi ). However, when the roles are switched, the overlap used to compute de may instead produce a disabling essence de′ = (b2 ◦ c′ : C → L2 , b′1 ◦ c′ : C ′ → L1 ) ∈ DEss(ρ2 , ρ1 ), which indicates that the application of ρ2 can prevent the application of ρ1 by destroying its match. In other words, when this disabling essence is embedded in a pair of transformations, the underlying ac-disregarding transformations are already in conflict. We introduce ac-conflicting rule overlaps which imply ac-disregarding parallel independence (i.e., neither transformation destroys the match of the other) when embedded in a transformation pair. Once again, we use rule overlaps to ensure that the definition can be applied to any kind of essence considered in this paper. Definition 9 (Ac-conflicting rule overlap). Given rules ρ1 and ρ2 , a rule overlap ro of them is called ac-conflicting if there is an ac-disregarding parallel independent transformation pair (t1 , t2 ) via ρ1 and ρ2 into which ro embeds. The following result shows that each transformation pair in which an acconflicting rule overlap is embedded is parallel independent ac-disregarding. Proposition 1 (Disjoint sets of ac-conflicting and non-ac-conflicting rule overlaps). If a rule overlap ro is ac-conflicting, then each transformation pair (t1 , t2 ) such that ro is embeddable in (t1 , t2 ) is parallel independent

14

Lauer et al. Pi

A

bi

A′

Pi′

b′i

eP ′

ePi

i

Pi∗

∗

b∗ i

A

(1)

b∗ j

eP ∗

Pj∗ e

bj eP ∗ i

K∗

j

Pj

Pj

∗

A

b∗ i

Pi∗

b∗ j

(1)

eP ∗

Pj∗

eP ∗

K∗

b′j

Pj′ e

P′ j

j

i

Fig. 9: Diagram for the composition of rule overlaps ac-disregarding. Moreover, if a non-ac-conflicting rule overlap is embeddable in a transformation pair (t1 , t2 ), this pair is parallel dependent ac-disregarding. The following criterion can be used to decide whether a disabling essence (b1 : A → L1 , bj : A → Pj ) of a rule pair is ac-conflicting; we illustrate its use in Example 8 in Section B. Proposition 2 (Ac-conflicting disabling essences). Given rules ρ1 and ρ2 , a disabling essence ce = (b1 : A → L1 , bi : A → Pi , idL1 , pL2 ) ∈ DEss(ρ1 , ρ2 ) is ac-conflicting if and only if the morphism l2′ , which is obtained by computing the pullbacks (2) and (3) shown in Figure 8, is an isomorphism. We now develop a construction for composing rule overlaps (encompassing disabling essences) in such a way that composed overlaps can be embedded in a transformation pair if the individual overlaps are embedded in it, and vice versa. Definition 10 (Composition of rule overlaps). Given two rule overlaps bj

b

b′

b′j

i i ro = (Pi ←− A −→ Pj , eL1 , eL2 ) and ro′ = (Pi′ ←− A′ −→ Pj′ , e′L1 , e′L2 ), the set of ′ compositions of ro and ro , denoted by Comp(ro, ro′ ), contains each rule overlap

b∗ j

b∗ i

(Pj∗ ←−- A∗ ,−→ Pi∗ , ePj ◦ pL1 , ePi ◦ pL2 ) so that (ePj : Pj → Pj∗ , ePj′ : Pj′ → Pj∗ ), (ePi : Pi → Pi∗ , ePi′ : Pi′ → Pi∗ ), (ePj∗ : Pj∗ ,→ K ∗ , ePi∗ : Pj∗ ,→ K ∗ ) ∈ E ′ , ePj ◦pL1 = ePj′ ◦p′L1 , ePi ◦pL2 = ePi′ ◦p′L2 , the outer squares in the diagrams shown in Figure 9 are pullbacks and b∗j and b∗i are obtained by computing the pullback (1). The following example briefly illustrates the result of composing rule overlaps; we illustrate a computation in detail as Example 9 in Section B. Example 4 (Composed rule overlap). The composed rule overlap Comp(AL1L2 , A1L2L1 ) in Figure 5 indicates that AL1L2 and A1L2L1 can be embedded in the same transformation by identifying 1,6:Class. An occurrence of this composed overlap simultaneously indicates (i) that decapsulateAttribute causes a conflict with pullUpEncapsulatedAttribute by destroying 3,7:Method and (ii) that pullUpEncapsulatedAttribute causes a conflict with decapsulateAttribute by destroying the edge leading to 2,9: Method. We show that the desired property of composed rule overlaps is satisfied, i.e., that a composed overlap is embedded in a transformation pair if and only if both of its constituent rule overlaps are also embedded in the pair.

Conflict Essences for Nested Application Conditions

15

Theorem 1 (Embedding of composed rule overlaps). Given two rule overlaps ro and ro′ of two rules ρ1 , and ρ2 , if both rule overlaps ro and ro′ are embeddable in a transformation pair (t1 , t2 ) via ρ1 and ρ2 , then there is a composed overlap co ∈ Comp(ro, ro′ ) that is also embeddable in (t1 , t2 ). Conversely, if any composed overlap co ∈ Comp(ro, ro′ ) is embedded in a transformation pair (t1 , t2 ) via ρ1 and ρ2 , then both ro and ro′ are also embedded in (t1 , t2 ). A crucial observation is that if both rule overlaps are ac-conflicting, then so are all composed overlaps. This statement follows directly from the second part of Theorem 1. We will use this result later on when comparing conflict essences (which encompass composed disabling essences) with initial conflicts for rules with application conditions. Corollary 1 (Inheritance of ac-conflicting rule overlaps). Given two acconflicting rule overlaps ro and ro′ of rules ρ1 and ρ2 , each composed overlap ce ∈ Comp(ro, ro′ ) is ac-conflicting. We now define conflict essences, which provide an overview on how two transformations can cause a conflict for each other. To construct conflict essences, we compose rule overlaps, in which the first transformation causes a conflict with the second and the second transformation causes a conflict with the first. All disabling essences from Figure 5 and, in particular, the composed rule overlap from Example 4 are conflict essences. Definition 11 (Set of conflict essences). Given two rules ρj = (Lj ←- Kj ,→ Rj , acj ), with j = 1, 2, the set of conflict essences of ρ1 and ρ2 , denoted by CEss(ρ1 , ρ2 ), is recursively defined as follows: 1. A disabling essence de = (bi : A → Pi , bj : A → Pj ) ∈ DEss(ρ1 , ρ2 )∪DEss(ρ2 , ρ1 ) is a conflict essence for ρ1 and ρ2 if and only if (i) de is ac-conflicting or (ii) Pi = L1 and Pj = L2 . 2. If ce1 and ce2 are conflict essences so that both are either ac-conflicting or non-ac-conflicting, then every composed rule overlap ce∗ ∈ Comp(ce1 , ce2 ) is a conflict essence. The following corollary directly follows from the fact that, for each parallel dependent transformation pair, there is a disabling essence that embeds in it [20]. This is because the set of conflict essences contains each ac-conflicting disabling essence in both directions. For ac-disregarding parallel dependent transformations, the claim follows from the fact that the set of conflict essences contains each conflict essence for plain rules, together with the results shown in [3]. Corollary 2 (Embedding of conflict essences). Given a pair of parallel dependent transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 H1 , G =⇒ρ2 ,m2 H2 ) via rules ρ1 and ρ2 , there is a conflict essence ce ∈ CEss(ρ1 , ρ2 ) that is embeddable in (t1 , t2 ).

16

7

Lauer et al.

Symbolic Conflict Essences and Initial Conflicts

In this section, we introduce symbolic conflict essences, which consist of conflict essences accompanied by a nested condition. As with initial conflicts, the embedding morphisms of a conflict essence satisfy the corresponding condition if and only if the transformation pair is parallel dependent. This ensures that a symbolic conflict essence is embedded in a transformation pair if and only if the transformation pair is parallel dependent. Moreover, each embedded symbolic conflict essence indicates a location at which an occurrence of an application condition object is destroyed (or created), or a rule match is destroyed. We relate each symbolic conflict essence to a unique initial conflict. We then use the condition of the initial conflict to construct the condition of the conflict essence using the well-known shift operator for nested conditions [10]. To ensure that the condition of a symbolic conflict essence is satisfied if and only if the transformation pair is parallel dependent, both embedding morphisms of the conflict essence embedding must satisfy the corresponding condition. To achieve this, we introduce cospan conditions, which establish a way to restrict the satisfaction of conditions. Rather than using a single morphism, we will use a cospan on the first nesting level of the condition (whereas the condition itself is a nested condition as usual). p1

Definition 12 (cospan condition). Given two objects P0 and P0′ , cc = ∃(P0 −→ p′1

P1 ←− P0′ , d) is a cospan condition over P0 and P0′ if d is a condition over P1 . Morever, every Boolean combination of cospan conditions over P0 and P0′ is a cospan condition over P0 and P0′ . Two morphisms q : P0 → G and q ′ : P0′ → G satisfy the cospan condition cc, denoted by (q, q ′ ) |= cc, if there is a morphism q1 : P1 → G so that q1 |= d, q = q1 ◦ p1 and q ′ = q1 ◦ p′1 . Next, we introduce symbolic conflict essences. To relate each conflict essence to an initial conflict, we must consider two different cases: Either the conflict essence is ac-conflicting, or it is not. For a non-ac-conflicting conflict essence, there is no need of an additional condition to check for parallel dependence, since an embedding of a non-ac-conflicting conflict essence already shows (acdisregarding) parallel dependence (Proposition 1). Therefore, the condition of ac-conflicting conflict essences is true. If an ac-conflicting conflict essence is embeddable in a transformation pair, the pair is parallel independent and ac-disregarding (Proposition 1). This means that the symbolic initial conflict is also embeddable in this transformation pair [17, Lemma 4], and we can use the condition of the symbolic initial conflict to construct the condition for the conflict essence. If the symbolic initial conflict is embedded in a transformation pair, the transformation pair is parallel dependent ac-disregarding. Although each symbolic conflict essence uniquely corresponds to an initial conflict, the conflict essence is much more informative because it compactly encodes the root cause(s) of the conflicts present in the transformation pairs in which it is embedded.

Conflict Essences for Nested Application Conditions

17

A bj

bi

L1

pL1

Pi

Pj

(1) b′j

D

iL1

pL2

L2

b′i m∗

iL2

L1 + L2

Fig. 10: Construction of symbolic conflict essences Definition 13 (Symbolic conflict essence). Given two rules ρj = (Lj ←Kj ,→ Rj , acj ), with j = 1, 2, and a conflict essence ce = (bi ◦ c : C → Pi , bj ◦ c : C → Pj ) ∈ DEss(ρ1 , ρ2 ), the pair (ce, acce ) is a symbolic conflict essence where ′ bj

b′

i acce := ∃(Pi −→ D ←− Pj , Shift(m∗ , acL1 +L2 ∧ ac∗L1 +L2 ))

if ce is ac-conflicting, and acce := true otherwise. The morphism b′j is obtained by computing the pushout (1) in Figure 10, m∗ : L1 + L2 → D is the morphism obtained by the universal property of the coproduct L1 +L2 and (R1 +L2 iL1 ,ρ1 ⇐= L1 + L2 =⇒iL2 ,ρ2 L1 + R2 , acL1 +L2 , ac∗L1 +L2 ) is the symbolic intitial conflict. The set of symbolic conflict essences of the rules ρ1 and ρ2 , denoted by SCEss(ρ1 , ρ2 ), is defined as SCEss(ρ1 , ρ2 ) := {(ce, acce ) | ce ∈ CEss(ρ1 , ρ2 )}. Remark 1. The pushout (1) in Figure 10 exists if the considered conflict essence is ac-conflicting because either bi or bj is an M-morphism: If the essence is composed, both morphisms are M-morphisms by construction (see Definition 10). Moreover, for disabling essences of the form (b1 : A → L1 , bj : A → Pj ) where Pj ̸= L2 , we have b1 ∈ M by construction (Definition 16). Disabling essences of the form (b1 : A → L1 , bj : A → L1 ) are also disabling essences for plain rules [20, Proposition 3], which directly implies that they are not ac-conflicting. The following example briefly illustrates symbolic conflict essences; we illustrate a symbolic conflict essence in detail as Example 10 in Section B. Example 5 (Symbolic conflict essence). Together with a cospan condition acce , each conflict essence shown in Figure 5 forms a symbolic conflict essence. For AL1L2 , A1 L2L1 , A2 L2L1 , and the composed essences, which are not ac-conflicting, acce is equal to true. For the remaining ones, acce is non-trivial and ensures that (i) both rules satisfy their application conditions before the transformations and that (ii) the transformation pair is parallel dependent. Because symbolic conflict essences consist of a conflict essence and a condition, we need to extend the notion of embeddability to also account for the condition: the embedding morphisms must satisfy it. Definition 14 (Embeddability of symbolic conflict essences). Given a pair of transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 H1 , G =⇒ρ2 ,m2 H2 ) via rules ρ1 and ρ2 , a symbolic conflict essence (ce, acce ) ∈ SCEss(ρ1 , ρ2 ) is embeddable in (t1 , t2 ) if ce is embeddable in (t1 , t2 ) via embedding morphisms mj1 and mi2 and (mj1 , mi2 ) |= acce .

18

Lauer et al.

We can now establish the main results of this paper, namely that symbolic conflict essences play the same role for rules with application conditions that conflict essences do for plain rules (compare Figure 1): They unambiguously indicate a transformation pair to be in conflict and correspond to (symbolic) initial conflicts. Theorem 2 (Correctness of symbolic conflict essences). Two transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 H1 , G =⇒ρ2 ,m2 H2 ) via rules ρ1 and ρ2 are parallel dependent if and only if a symbolic conflict essence (ce, acce ) ∈ SCEss(ρ1 , ρ2 ) is embeddable in (t1 , t2 ). Theorem 3 (Relation of symbolic conflict essences and initial conflicts). For each symbolic conflict essence ce, there is a unique initial conflict so that the initial conflict is embeddable in a transformation pair via an extension diagram if ce is embeddable in the transformation pair. Moreover, when an initial conflict is embedded in a transformation pair, there is at least one symbolic conflict essence that is also embedded in this transformation pair.

8

Conclusion

In this paper, we continue our work on providing techniques to statically analyse the interactions of (graph) transformation rules. Concretely, we introduce conflict essences for rules equipped with application conditions; these objects encapsulate the essential information about how two rule applications can cause a conflict with each other, potentially by invalidating one another’s application condition. This closes an important gap because the construction was previously only available for plain rules (i.e., rules without application conditions). Our construction builds on the existing one, enabling us to lift the most important results from the “plain situation” to the case of application conditions. To achieve this, we construct symbolic conflict essences (which are conflict essences equipped with an application condition), which uniquely correspond to a symbolic initial conflict [17] and embed in a transformation pair if and only if that pair is conflicting. For a conflicting transformation pair, the set of embedded symbolic conflict essences is not minimal, in the sense that each embedded symbolic conflict essence signals a spot that causes the conflict. In the future, we plan to further investigate our composition operation. For example, we aim to identify the “maximal” ones that cannot be extended by additional spots. Moreover we intend to use this analysis to investigate the effects of rules on constraints to refine the graph repair approaches presented in [9, 19] and to identify effective mutation orders in model-driven optimisation [12]. Acknowledgments. This work was partially funded by the German Research Foundation (DFG), project “Triple Graph Grammars (TGG) 3.0” and “ModelDriven Optimization in Software Engineering”. The authors would like to thank the ICGT reviewers for their insightful comments.

Conflict Essences for Nested Application Conditions

19

Disclosure of Interests. The authors have no competing interests to declare that are relevant to the content of this article.

References 1. Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: Advanced Concepts and Tools for In-Place EMF Model Transformations. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) Model Driven Engineering Languages and Systems – 13th International Conference, MODELS 2010, Oslo, Norway, October 3– 8, 2010, Proceedings, Part I. pp. 121–135. Lecture Notes in Computer Science, Springer (2010). https://doi.org/10.1007/978-3-642-16145-2_9 2. Azzi, G.G., Corradini, A., Ribeiro, L.: On the essence and initiality of conflicts. In: Lambers, L., Weber, J.H. (eds.) Graph Transformation – 11th International Conference, ICGT 2018, Held as Part of STAF 2018, Toulouse, France, June 25– 26, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10887, pp. 99–117. Springer (2018). https://doi.org/10.1007/978-3-319-92991-0_7 3. Azzi, G.G., Corradini, A., Ribeiro, L.: On the essence and initiality of conflicts in M-adhesive transformation systems. J. Log. Algebraic Methods Program. 109 (2019). https://doi.org/10.1016/J.JLAMP.2019.100482 4. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series, Springer (2006). https://doi.org/10.1007/3-540-31188-2 5. Ehrig, H., Ermel, C., Golas, U., Hermann, F.: Graph and Model Transformation – General Framework and Applications. Monographs in Theoretical Computer Science. An EATCS Series, Springer (2015). https://doi.org/10.1007/ 978-3-662-47980-3 6. Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: M-Adhesive Transformation Systems with Nested Application Conditions. Part 2: Embedding, Critical Pairs and Local Confluence. Fundam. Informaticae 118(1–2), 35–63 (2012). https://doi.org/10.3233/FI-2012-705 7. Ehrig, H., Habel, A., Padberg, J., Prange, U.: Adhesive high-level replacement categories and systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) Graph Transformations, Second International Conference, ICGT 2004, Rome, Italy, September 28 – October 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3256, pp. 144–160. Springer (2004). https://doi.org/10.1007/ 978-3-540-30203-2_12 8. Fowler, M.: Refactoring: improving the design of existing code. Addison-Wesley Professional (2018) 9. Fritsche, L., Lauer, A., Kratz, M., Schürr, A., Taentzer, G.: Using weakest application conditions to rank graph transformations for graph repair. Log. Methods Comput. Sci. 22(1) (2026). https://doi.org/10.46298/LMCS-22(1:10)2026 10. Habel, A., Pennemann, K.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009). https://doi.org/10.1017/S0960129508007202 11. Heckel, R., Taentzer, G.: Graph Transformation for Software Engineers – With Applications to Model-Based Development and Domain-Specific Language Engineering. Springer (2020). https://doi.org/10.1007/978-3-030-43916-3

20

Lauer et al.

12. John, S., Kosiol, J., Lambers, L., Taentzer, G.: A graph-based framework for model-driven optimization facilitating impact analysis of mutation operator properties. Softw. Syst. Model. 22(4), 1281–1318 (2023). https://doi.org/10.1007/ S10270-022-01078-X 13. Lack, S., Sobocinski, P.: Adhesive and quasiadhesive categories. RAIRO Theor. Informatics Appl. 39(3), 511–545 (2005). https://doi.org/10.1051/ITA:2005028 14. Lambers, L., Born, K., Kosiol, J., Strüber, D., Taentzer, G.: Granularity of conflicts and dependencies in graph transformation systems: A two-dimensional approach. J. Log. Algebraic Methods Program. 103, 105–129 (2019). https://doi.org/10.1016/ J.JLAMP.2018.11.004 15. Lambers, L., Born, K., Orejas, F., Strüber, D., Taentzer, G.: Initial conflicts and dependencies: Critical pairs revisited. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets – In Memory of Hartmut Ehrig. Lecture Notes in Computer Science, vol. 10800, pp. 105–123. Springer (2018). https://doi. org/10.1007/978-3-319-75396-6_6 16. Lambers, L., Kosiol, J., Strüber, D., Taentzer, G.: Exploring conflict reasons for graph transformation systems. In: Guerra, E., Orejas, F. (eds.) Graph Transformation – 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Eindhoven, The Netherlands, July 15–16, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11629, pp. 75–92. Springer (2019). https://doi.org/10. 1007/978-3-030-23611-3_5 17. Lambers, L., Orejas, F.: Transformation rules with nested application conditions: Critical pairs, initial conflicts & minimality. Theor. Comput. Sci. 884, 44–67 (2021). https://doi.org/10.1016/J.TCS.2021.07.023 18. Lambers, L., Strüber, D., Taentzer, G., Born, K., Huebert, J.: Multi-granular conflict and dependency analysis in software engineering based on graph transformation. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 – June 03, 2018. pp. 716–727. ACM (2018). https://doi.org/10.1145/3180155.3180258 19. Lauer, A., Kosiol, J., Taentzer, G.: Empowering model repair: a rule-based approach to graph repair without side effects - extended version. Innov. Syst. Softw. Eng. 20(4), 597–618 (2024). https://doi.org/10.1007/S11334-024-00587-W 20. Lauer, A., Kosiol, J., Taentzer, G.: Granular conflict analysis for transformation rules with application conditions. In: Endrullis, J., Tichy, M. (eds.) Graph Transformation – 18th International Conference, ICGT 2025, Held as Part of STAF 2025, Koblenz, Germany, June 11–12, 2025, Proceedings. Lecture Notes in Computer Science, vol. 15720, pp. 63–90. Springer (2025). https://doi.org/10.1007/ 978-3-031-94706-3_4 21. Pennemann, K.: Development of correct graph transformation systems. Ph.D. thesis, University of Oldenburg, Germany (2009), https://nbn-resolving.org/urn:nbn: de:gbv:715-oops-9483 22. Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) Graph Transformations, Second International Conference, ICGT 2004, Rome, Italy, September 28 – October 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3256, pp. 319–335. Springer (2004). https://doi.org/10.1007/978-3-540-30203-2_23 23. Rensink, A., Corradini, A.: On categories of nested conditions. In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M. (eds.) Principles of Verification: Cycling the Probabilistic Landscape – Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part

Conflict Essences for Nested Application Conditions

21

I. Lecture Notes in Computer Science, vol. 15260, pp. 393–418. Springer (2024). https://doi.org/10.1007/978-3-031-75783-9_16

22

Lauer et al.

A

Additional formal Results and Proofs

First, we show a property of pullbacks which we will use throughout the proofs. Lemma 1. Consider the diagram below so that g ′′ = m ◦ g and f ′′ = m ◦ f , the inner square (g ◦ f ′ , f ◦ g ′ ) is a pullback if and only if the outer square (g ′′ ◦ f ′ , f ′′ ◦ g ′ ) is a pullback. B h f′

X

x

g

A

g ′′

D g′

f

m

E

f ′′

k

C Proof. 1. Let us first assume that the inner square (g ◦ f ′ , f ◦ g ′ ) is a pullback. We need to show that the outer square is also a pullback. Let h : X → B and k : X → C be morphisms so that f ′′ ◦ k = g ′′ ◦ h. For the outer square to be a pullback, we need to show that there is a morphism x : X → A with h = f ′ ◦ x and k = g ′ ◦ x. In particular, we have g ′′ ◦ h = f ′′ ◦ k

⇐⇒

m◦f ◦k =m◦g◦h

⇐⇒

f ◦ k = g ◦ h. Now, because the inner square is a pullback, there must be a morphism x : X → A with k = g ′ ◦ x and h = f ′ ◦ x. 2. Let us assume that the outer square (f ′′ ◦ g ′ , g ′′ ◦ f ′ ) is a pullback. Now we want to show that the inner square is a pullback. Again, let h : X → B and k : X → C be morphisms so that g ◦ h = f ◦ k. This implies that g◦h=f ◦k

⇐⇒

m◦g◦h=m◦f ◦k

⇐⇒

′′

′′

g ◦ h = f ◦ k. Because the outer square is pullback, there is a morphism x : X → A with h = f ′ ◦ x and k = g ′ ◦ x. ⊓ ⊔ A.1

Transfer of Definitions and Results from [20]

In the following we present the definition of the shift operator for proto-essence, the definition of disabling essences and the results of [20] that directly apply to our extended construction of proto-essences presented in Section 5.

Conflict Essences for Nested Application Conditions

23

Definition 15 (Shift of proto-essence by insertion [20, Definition 8]). l1

r1

l2

r2

Given two rules (L1 ←−- K1 ,−→ R1 , ac1 ) and (L2 ←−- K2 ,−→ R2 , ac2 ) and a proto essence by insertion pe := (a ◦ c : C → R1 , bi ◦ c : C → Pi ) ∈ IPEss(ρ1 , ρ2 ), the shift of pe over ρ1 , denoted by PEShiftρ1 (pe), is defined as PEShiftρ1 (pe) = (a′ ◦ c′ , b′i ◦ c′ ) where (1) in the diagram below is a pullback, (IPO) is the initial pushout over ki (both stem from the computation of pe and (2) is a pushout constructed by computing the pushout complement of bi and ki . B

ki′

C

c′

(IPO)

c

A′i

ki

Ai

(1)

a

r1

R1

a′

L1

l1

K1

A′i

ki

bi

Pi

(2)

b′i

p′P ′

Pi′

Definition 16 (Disabling essence [20, Definition 9]). l1

r1

l2

i

Given two rules

r2

(L1 ←−- K1 ,−→ R1 , ac1 ) and (L2 ←−- K2 ,−→ R2 , ac2 ), a proto essence by deletion (a ◦ c : C → L1 , bi ◦ c : C → Pi ) ∈ DPEss(ρ1 , ρ2 ) is a disabling essence by deletion of ρ1 in ρ2 if 1. if it is embedded in a transformation pair (L1 Pi =⇒eL1 ,ρ1 H1 , L1 Pi =⇒ePi ◦pL2 ,ρ2 H2 ) where (eL1 : L1 → L1 Pi , ePi : Pi → L1 Pi ) ∈ E ′ , 2. Pi is existentially bound in ac2 or Pi = L2 , and 3. (a, bi ) ̸= (!L1 , !Pi ), Given a proto-essence by insertion (a◦c : C → R1 , bi ◦c : C → Pi ) ∈ IPEss(ρ1 , ρ2 ), the span PEShiftρ1 (a ◦ c, bi ◦ c) is a disabling essence by insertion of ρ1 in ρ2 if 1. if it is embedded in a transformation pair (L1 Pi =⇒eL1 ,ρ1 H1 , L1 Pi =⇒ePi ◦pL2 ,ρ2 H2 ) where (eL1 : L1 → L1 Pi , ePi : Pi → L1 Pi ) ∈ E ′ , 2. Pi is universally bound in ac2 , and 3. (ai , bi ) ̸= (!R1 , !Pi ). The set of all disabling essences of two rules ρ1 and ρ2 is denoted by DEss(ρ1 , ρ2 ). The following proposition shows that the set of disabling essences for rules with application conditions is an extension of disabling essences for plain rules [3]. For this, we show that the set of disabling essences for rules with application conditions contains the set disabling essences for plain rules. Moreover, each disabling essence, where both morphisms have the LHSs of the rules as codomain, are also disabling essences for plain rules. This means that our approach exactly computes disabling essences for plain rules.

24

Lauer et al.

Proposition 3 (Containment of disabling essence for plain rules). l1

r1

l2

r2

Given two rules ρ1 = (L1 ←−- K1 ,−→ R1 , ac1 ), ρ2 = (L2 ←−- K2 ,−→ R2 , ac2 ), the set of disabling essence by deletion of ρ1 in ρ2 contains the set of disabling l1

r1

l2

r2

essences for the plain rules of L1 ←−- K1 ,−→ R1 in L2 ←−- K2 ,−→ R2 . Moreover, each disabling essence by deletion of the form b1 ◦c : C → L1 , b2 ◦c : C → L2 l1

r1

l2

r2

is a disabling essence of L1 ←−- K1 ,−→ R1 in L2 ←−- K2 ,−→ R2 . Proof (of Proposition 3). Let a disabling essence by deletion de = (b1 ◦ c : C → L1 , b2 ◦ c : C → L2 ) ∈ DEss(ρ1 , ρ2 ) be given. By Definition 7 there is either a pair of morphism (eL1 : L1 → L1 Pn , ePn : Pn → L1 Pn ) ∈ E ′ , where Pn is either a leaf of the tree-repesentation of ac2 or the LHS L2 of ρ2 so that DPEssn (eL1 , ePn ) = de. In both cases, the morphism b2 ◦ c has codomain L2 if and only if DPEssn (eL1 , ePn ) = DPEss0 (eL1 , ePn ) = essl1 (eL1 , ePn ◦ . . . ◦ p1 ) ̸= (!L1 , !L2 ). Because the first iteration of our construction is identical to the construction of disabling essences for plain rules [3, Definition 3.8], de is also a disabling essence for plain rules. Finally, we must show that each disabling essence for plain rules is contained in DEss(ρ1 , ρ2 ): Disabling essence of plain rules are defined as essl1 (m1 , m2 ) for some cospan (m1 : L1 → G, m2 : L2 → G). I.e. the construction starts by calculating the pullback of (m1 , m2 ) as shown in the diagram below. By E ′ -M factorization there is a pair of morphisms (eL1 : L1 → L1 L2 , eL2 : L2 → L1 L2 ) ∈ E ′ and a monomorphism m∗ : L1 L2 ,→ G ∈ M with m1 = m∗ ◦ eL1 and m2 = m∗ ◦ eL2 . By Lemma 1 the square (1) is also a pullback and essl1 (m1 , m2 ) = essl1 (eL1 , eL2 ) = DPEssn (eL1 , eL2 ), i.e., this is also a disabling essence for rules with application conditions. ⊔ ⊓ L1 A

m1

eL1

b1

L1 L2

(1) b2

eL2

m∗

G

m2

L2

Finally, we show that a disabling essence is embedded in each parallel dependent transformation pair. Theorem 4. For each pair of parallel dependent transformations (t1 , t2 ) via rules ρ1 and ρ2 , there is a disabling essence de ∈ DEss(ρ1 , ρ2 ) that is embedded in (t1 , t2 ). Proof (of Theorem 4). Given a pair of transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 l1

r1

l2

H1 , G =⇒ρ2 ,m2 H2 ) via rules ρ1 = (L1 ←−- K1 ,−→ R1 , ac1 ) and ρ2 = (L2 ←−r2 K2 ,−→ R2 , ac2 ) so that t1 causes a conflict for t2 . For this, there are two possibilities, either t1 destroys the match m2 of t2 , or it introduces a violation of the application condition ac2 of ρ2 . If the conflict is caused by destroying the match m2 , Proposition 3 implies that a disabling essence of ρ1 in ρ2 embeds into the transformation pair [3, Theorem 3.13].

Conflict Essences for Nested Application Conditions

25

Otherwise, if the application condition ac2 is violated, the proof is analogous to the proof of [20, Theorem 2]. The only difference is that we consider morphisms that lead to the leaves of the tree representation of the application condition (instead of just considering the morphisms in a condition in ANF) and that we need to obtain a morphism pair contained in E ′ to argue that the embedded span is actually contained in DEss(ρ1 , ρ2 ). This morphism pair can obtained by using E ′ -M factorization at an appropriate point and using Lemma 1. ⊓ ⊔

A.2

Proofs li

ri

Proof (of Proposition 1). Let two rules ρi = (Li ←−- Ki ,−→ Ri , aci ), with i = 1, 2, an ac-conflicting rule overlap ro = (bi : A → Pi , bj : A → Pj , pL1 , pL2 ) of ρ1 and ρ2 , and a transformation pair (t1 , t2 ) be given so that ro is embedded in (t1 , t2 ). We want to show that (t1 , t2 ) is parallel independent ac-disregaring. Because ro is ac-conflicting, there is an ac-disregarding parallel independent transformation pair (t′1 , t′2 ) = (G′ =⇒ρ1 ,m′1 H1′ , G′ =⇒ρ2 ,m′2 H2′ ) so that ro is embedded via morphisms mi1 and mj2 as shown in the diagram below. We can construct the pullback of m′1 and m′2 by calculating the pullbacks (2), (3) and (4). Because t′1 and t′2 are parallel independent ac-disregarding, the morphisms l1′ and l2′ constructed by calculating the pullbacks (5) and (6) are isomophisms. We can use (2), (3) and (4) to also construct the pullback of m1 and m2 which results in the same morphisms as for m′1 and m′2 . This implies that t1 and t2 are parallel independent ac-disregarding. K1′

A′

l1′

(5)

K1

l1

D1

(4)

D2

(2)

A

(3)

L1 pL1

(6)

L2

l2

K2

pL2

Pi m1 /m′1

K2′

l2′

(1)

Pj

′

′

mi1 /mi1

m1 /m′1

mj2 /mj2

G/G′

We show the second part of the claim by contradiction: If a non-ac-conflicting rule overlap is embedded in a ac-disregarding parallel independent transformation, this implies that the rule overlap is ac-conflicting (by definition). ⊓ ⊔

26

Lauer et al.

Proof (of Proposition 2). Given a pair of transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 l1

r1

p′L2

L′2

l2

H1 , G =⇒ρ1 ,m1 H1 ) via rules ρ1 = (L1 ←−- K1 ,−→ R1 , ac1 ) and ρ2 = (L2 ←−r2 K2 ,−→ R2 , ac2 ) and a disabling essence de = (b1 : A → L1 , bj : A → Pj , idL1 , pL2 ) that is embedded in (t1 , t2 ) via morphisms m1 : L1 → G and mj2 : Pj → G as shown in the diagram below. To show the claim, we must show that (a) l2′ (constructed by the pullbacks (2) and (3) shown in the diagram below) is an isomorphism if de is ac-conflicting and that (b) de is ac-conflicting if l2′ is an isomorphism. We start by showing (a): Because de is ac-conflicting, we know that the transformation pair (t1 , t2 ) is parallel independent ac-disregarding (Definition 9 and Proposition 1). The square (1) + (2) (as composition of pullbacks) is a pullback of m1 and m2 . By the definition of parallel independence (Definition 2), the morphism l2′ obtained by calculating the pullback (3) (and also by calculating (2) and (3)) must be an isomorphism. To show (b), we assume that l2′ is an isomorphism and we must show that the embedding of de implies that t1 and t2 are parallel independent ac-disregarding. Let us first show that t1 does not cause a conflict for t2 : A bj

b1

R1

r1

K1

L1

l1

mj2

m1

H1

h1

D1

g1

(2)

Pj

(1)

l2′

K2′

(3)

L2

pL2

l2

K2

r2

R2

D2

h2

H2

m2 g2

G

Again, the square (1) + (2) is a pullback of of m1 and m2 . Since l2′ is an isomorphism, Definition 2 implies that t1 does not cause a conflict for t2 . To show that t2 does not cause a conflict for t1 we must consider whether de is an inserting or a deleting essence. We start by assuming that de is a deleting essence: K1′

L′1

l1′ (4)

K1

l1

L1

(1) + (2) m1

L2

m2

G Since de is a disabling essence of ρ1 in ρ2 , we know that (b1 , bj ) is calculated as pullback of some morphism pair (eL1 , ePn ◦ . . . ◦ pj+1 ) ∈ E ′ during the construction of disabling essences. Moreover, we know that (1) + (2) and (4) are also

Conflict Essences for Nested Application Conditions

27

computed during the computation of the disabling essences (in the first iteration in Definition 7). This implies that l1′ must be an isomorphism (as otherwise de would not be a disabling essence of ρ1 and ρ2 when starting the construction with (eL1 , ePn ◦ . . . ◦ pj+1 )). I.e., t2 does not cause a conflict for t1 .

k

L′2

(6)

p′L2

A

idA

A

a

(5)

b1

K

l1

L1

D

bj

Pj mj2

m1 g1

D1

G

If ce is a inserting essence, by construction of the shift of proto-essences (Definition 15), there is a morphism a : A → L1 with b1 = l1 ◦ a. This implies that the square (5) shown in the figure above is a pullback. Then, we construct pullback (6) (where L′2 is obtained by computing the pullback of m1 and m2 as shown above) and the square (5) + (6) is also a pullback (as composition of pullbacks). Because pullbacks are stable under isomorphisms, k : D → L′2 is an isomorphism, i.e., t2 does not cause a conflict for t1 . ⊔ ⊓

Proof (of Theorem 1). Given a pair of transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 l1

r1

l2

H1 , G =⇒ρ2 ,m2 H2 ) via rules ρ1 = (L1 ←−- K1 ,−→ R1 , ac1 ) and ρ2 = (L2 ←−bj

r2

b

i K2 ,−→ R2 , ac2 ), and two rule overlaps ro = (Pj ←− A −→ Pi , pL1 : L1 →

b′j

b′

i Pi′ , p′L1 : L1 → Pj′ , p′L2 : L2 → Pi′ ) that are Pj , pL2 : L2 → Pi ) and (Pj′ ←− A′ −→ embeddable in (t1 , t2 ) as shown in Figure 11. We want to show that there is a composed overlap co ∈ Comp(ro, ro′ ) that is also embedded in (t1 , t2 ). To do so, well will construct a composed overlap on the basis of Definition 10 that is embedded in the transformation pair.

As shown in the diagram in Figure 12 below, by E ′ -M factorization, there are morphism pairs (ePi : Pi → Pi∗ , ePi′ : Pi′ → Pi∗ ) ∈ E ′ and (ePj : Pj → Pj∗ , ePj′ : Pj′ → Pj∗ ) and morphisms m∗i : Pi∗ ,→ G ∈ M and m∗j : Pj∗ ,→ G ∈ M so

28

Lauer et al.

A b′j

R1

l1

K1

r1

L1

pL1

b′i

Pj

Pi Pj

mj1

H1

h1

D1

L2

l1

K2

r1

R2

n2

mi2

m∗

m1 g1

pL2

ePi

eP j n1

Pi

(1)

m2 g2

G

D2

h2

H2

A bj

R1

l1

K1

r1

L1

p′L1

bi

Pj′

′

m1

H1

g1

D1

h1

L2

l1

K2

r1

R2

i

j

mj1

p′L2

eP ′

eP ′ n1

Pi′

(2)

Pi′ Pj′ mi2′ m∗

n2

m2

G

g2

D2

h2

H2

Fig. 11: Embedding of two rule overlaps in a transformation pair

that mi1 = m∗i ◦ ePi , ′

mi2 = m∗i ◦ ePi′ , mj1 = m∗j ◦ ePj , and ′

mj2 = m∗j ◦ ePj′ .

Moreover, there is another morphism pair (ePi∗ : Pi∗ ,→ K ∗ , ePj∗ : Pj∗ ,→ K ∗ ) ∈ E and a morphism m∗ : K ∗ ,→ G ∈ M so that the left side of the diagram in Figure 13 commutes. The fact that ePi∗ and ePj∗ are M-morphisms, follows because m∗i and m∗j are M-morphisms and the class M is closed under decomposition. We get the object A∗ and the morphisms b∗i and b∗j by computing the pullback (1) of (ePi∗ , ePj∗ ). By Lemma 1, the square (m∗i ◦ b∗i , m∗j ◦ b∗j ) is also a pullback ′

Conflict Essences for Nested Application Conditions

29

A bj

bi

Pi ePi

Pi∗

Pj mi1

m∗ i

′

eP ′

mj2

mi1

i

Pj∗

m∗ j

G ′

eP ′

eP j

mj2

Pi′

j

Pj′ b′j

b′i

A′

Fig. 12: Construction of composed rule overlaps on the basis of two embeddings

and we have m1 = mi1 ◦ pL1 = m∗i ◦ ePi ◦ pL1 . and m2 = mj2 ◦ pL2 = m∗j ◦ ePj ◦ pL2 . b∗ i

b∗ j

This means that the rule overlap co = (Pi∗ ,−→ A∗ ←−- Pj∗ , ePi ◦ pL1 , ePj ◦ pL2 ) is embedded in (t1 , t2 ). Secondly, we must show that ce ∈ Comp(ro, ro′ ): For this, we need to show that the squares (ePi∗ ◦ePi ◦bj , ePj∗ ◦ePj ◦bj ) and (ePi∗ ◦ePi′ ◦b′j , ePj∗ ◦ ePj′ ◦ b′j ) in the diagram in Figure 13 are pullbacks. This follows directly with ′

′

Lemma 1 since both squares (mi1 ◦bi , mj2 ◦bj ) and (mi1 ◦b′i , mj2 ◦b′j ) are pullbacks because both rule overlaps ro and ro′ are embedded in the transformation pair ′ ′ via mi1 , mj1 , mi1 and mj2 , respectively. We also need to show that if a composed essence co ∈ Comp(ro, ro′ ) is embedded in (t1 , t2 ) via morphisms m∗i : Pi∗ → G and m∗j : Pj∗ → G (shown Figure 13), then both overlaps ro and ro′ are embedded in (t1 , t2 ): First, we will show that ro is embedded in (t1 , t2 ). Since co is a composition of ro and ro′ , there is a morphism pair (ePj∗ , ePi∗ ) ∈ M so that square (1) and the overall square (involving bi and bj ) is a pullback. The same square can be constructed by computing the pullback (2), (3), and (4) in Figure 14 which will now use to show that ro is embedded in (t1 , t2 ): Because co is embedded in (t1 , t2 ) there is an morphism pair (ePi∗ : Pi∗ → ∗ ∗ Pi Pj , ePj∗ : Pj∗ → Pi∗ Pj∗ ) ∈ E ′ and a morphism m∗ : Pi∗ Pj∗ ,→ G ∈ M so that

30

Lauer et al. L1

A

pL1

L2 pL2

bj

bi

A∗

Pi

Pi′

eP j

A∗ eP ′

mi1

Pj∗

(1) eP ∗

eP ∗

i

m∗ i

j

K

∗

Pi∗

j

eP ∗

i

m∗ j

eP ′

Pj∗

(1) eP ∗

mj2

Pj′ b∗ j

b∗ i

i

Pi∗

bj

bi

Pj b∗ j

b∗ i

ePi

A′

j

K

∗

m∗

G

Fig. 13: Construction of composed rule overlaps on the basis of two embeddings bj

A

D2 (3)

ePi

A∗

b∗ j

Pj∗

(2)

b∗ i

(1)

eP ∗

ePj

Pi∗

eP ∗

K∗

(4) bi D1

Pi

Pj

j

j

Fig. 14: consturction of an embedding out of the embedding of a rule overlap

m∗i = m∗ ◦ ePi∗ and m∗j = m∗ ◦ ePj∗ by E ′ -M factorization. Moreover, Lemma 1 implies that the square (5) (shown in the diagram below) is a pullback (shown in Figure 15). We continue by constructing the pullbacks (2), (3) and (4). The overall square (2) + (3) + (4) + (5) is also a pullback (as composition of pullbacks). If we choose mi1 := m∗i ◦ ePi and mj2 := m∗j ◦ ePj , the overall squares commutes and Lemma 1 implies that the outer square (consisting of mi1 ◦ bi and mj2 ◦bj ) is a pullback, i.e., ro is embedded in (t1 , t2 ) via mi1 and mj2 . Analogously, we can also show that ro′ is embedded in (t1 , t2 ). ⊔ ⊓ Proof (of Theorem 2). Given a pair of transformations (t1 , t2 ) = (G =⇒ρ1 ,m1 l1

r1

l2

H1 , G =⇒ρ2 ,m2 H2 ) via rules ρ1 = (L1 ←−- K1 ,−→ R1 , ac1 ), and ρ2 = (L2 ←−r2 K2 ,−→ R2 , ac2 ). To show the claim, we need to show that (i) a symbolic conflict

Conflict Essences for Nested Application Conditions L1

A

31

L2 bj

bi pL1

D1

(4)

D2

pL2

Pi

(2)

A∗

(3)

Pj

b∗ j

b∗ i

eP i

Pi∗

Pj∗

(5) eP ∗

eP ∗

i

mi1 m∗ i

ePj

j

mj2

Pi∗ Pj∗ m∗j m∗

G

Fig. 15: composition of an embedding out of an embedding of a composed essence

essence of ρ1 and ρ2 is embeddable in (t1 , t2 ) if the transformation pair is parallel dependent and that (ii) the embeddability of a symbolic conflict essence in (t1 , t2 ) implies parallel dependence. 1. We start by assuming that (t1 , t2 ) is parallel dependent and show that a symbolic conflict essence is embedded in (t1 , t2 ): By completeness of conflict essences (Corollary 2), there is a symbolic conflict essence (ce, acce ) ∈ SCEss(ρ1 , ρ2 ), so that ce is embedded in (t1 , t2 ). Therefore, it remains to show that the embedding morphisms mj1 and mi2 satisfy acce . If ce is not ac-conflicting, acce = true and (mj1 , mi2 ) |= acce . Otherwise, if ce is ac-conflicting, Proposition 1 implies that (t1 , t2 ) is ac-disregarding parallel independent. Moreover, there is an morphism m∗∗ : D → G where (1) is the figure below is a pushout (which exists, because either bj or bi is an M-morphism) so that mj1 = m∗∗ ◦ b′i and mi2 = m∗∗ ◦ b′j . Because (t1 , t2 ) are parallel independent ac-diregardingly there is the extension shown in Figure 17 diagram where m∗ : L1 + L2 → D is the coproduct morphism of (L1 +L2 , iL1 , iL2 ) so that m∗ ◦iL1 = b′i ◦pL1 and m∗ ◦iL2 = b′j ◦pL2 [17, Lemma 4] (shown in Figure 10). Because (L1 + L2 =⇒ρ1 ,iL1 R1 + L2 , L1 + L2 =⇒ρ2 ,iL2 R1 + L2 , acL1 +L2 ∧ ac∗L1 +L2 ) is a critical pair for ρ1 and ρ2 [17, Theorem 5], and the transformations are parallel dependent, m∗∗ ◦ m∗ |= acL1 +L2 ∧ ac∗L1 +L2 [6, Lemma 6.2]. With correctness of the shift operator, we also have m∗∗ |= Shift(m∗ , acL1 +L2 ∧ b′

b′j

i ac∗L1 +L2 ). It follows that (mj1 , mi2 ) |= ∃(L1 ←− D −→ L2 , Shift(m∗ , acL1 +L2 ),

32

Lauer et al. A bj

R1

l1

K1

r1

pL1

L1

Pj

bi

mj1 m1

H1

g1

h1

D1

pL2

L2

l1

K2

r1

R2

b′j

b′i n1

Pi

(1)

D

n2

mi2

m∗∗

m2 g2

G

D2

h2

H2

Fig. 16: Embedding of a conflict essence in a transformation pair R1 + L2

ρ1 , iL1

L1 + L2

ρ2 , iL2

L1 + R2

m∗∗ ◦ m∗

H1

ρ1 , m1

G

ρ2 , m2

H2

Fig. 17: Extension diagram for ac-diregarding parallel independent transformations because we also have mj1 = m∗ ◦ b′i and mi2 = m∗ ◦ b′j . This means, that (ce, acce ) is embedded in (t1 , t2 ) via mj1 and mi2 . 2. Let us now assume that a symbolic conflict essence (ce, acce ) ∈ CEss(ρ1 , ρ2 ) is embedded in (t1 , t2 ) via morphisms mj1 : Pj → G and mi2 : Pi → G. We want to show t1 and t2 are parallel dependent. For this, we need to distinguish whether (ce, acce ) is ac-conflicting or not. If (ce, acce ) is not ac-conflicting, Proposition 1 implies that t1 and t2 are parallel dependent. Secondly, let us assume that ce is ac-conflicting. This means that the transformation pair (t1 , t2 ) is parallel independent ac-disregarding (Proposition 1). Again, there is an extension diagram as shown in Figure 17 [17, Lemma 4]. Moreover, because (1) in Figure 16 is a pushout (which exists because ce is ac-conflicting), the morphism m∗∗ : D → G, so that mj1 = m∗∗ ◦ b′i and mi2 = m∗∗ ◦ b′j , is unique and because (mj1 , mi2 ) |= acce , we have m∗∗ |= Shift(m∗ , acL1 +L2 ∧ac∗L1 +L2 ). This implies that m∗∗ ◦m∗ |= acL1 +L2 ∧ ac∗L1 +L2 , i.e., the transformation pair (t1 , t2 ) is parallel dependent [6, Lemma 6.2]. ⊓ ⊔ Proof (of Theorem 3). To relate each symbolic conflict essence sce = (ce, acce ) to a unique initial conflict, we need to distinguish whether the included conflict essence is ac-conflicting or not. Let us start by assuming that ce is not ac-conflicting. Here, ce is either also a disabling essence or an composed essence.

Conflict Essences for Nested Application Conditions

33

If ce is a disabling essence, the filtering in Definition 16 implies that ce is also a disabling for the plain rules and ce can be uniquely related to an initial conflict [3]. If ce is a composed essence, we know that by Theorem 1, both conflict essences ce has been composed by are embedded in a transformation pair if ce is embedded in it. This means that both of these essences related to the same initial conflict, since at most one initial conflict embeds in a parallel dependent transformation pair [17]. Therefore, we can also relate sce to this initial conflict. If ce is ac-conflicting, an embedding of ce in a transformation pair implies ac-disregarding parallel independence. Now, the symbolic intial conflict is also embedded in this transformation pair [17, Lemma 4] and because this the only initial conflict that embeds in ac-disregarding parallel independent transformation pairs, we can uniquely relate sce to the symbolic initial conflict. The second part of the claim follows from the facts that an initial conflict can be embedded in each parallel dependent transformation pair and Theorem 2 which shows the same statement for symbolic conflict essences. ⊓ ⊔

B

Additional Examples

The following example is a more detailed version of Example 3. Example 6 (Construction of a proto-essence by deletion). Figure 18 shows the construction of a proto-essence by deletion of the rules decapsulateAttribute and pullUpEncapsulatedAttribute. In this example, we chose the path L2 , p1 , P1 , p3 , P3 as already described in Example 2. Please note that the graphs P1 , P2 and P3 now also show the included occurrence of the LHS of pullUpEncapsulatedAttribute. The construction starts with the overlap L1 P3 of the LHS L1 of decapsulateAttribute and P3 . Obviously, L1 P3 is equal to P3 ; the embedding of L1 is implicitly described by the node identifiers. For instance, the node 1:Class is mapped to the node 1,10:Class and so on. The edges are mapped according to the mapping of their source and target nodes. In the first step of the construction, we construct the pullback of eL1 and eP3 ◦ p3 ◦ p1 which results in the graph A0 . For graphs, the pullback object is the smallest subgraph of L1 P3 so that elements of L1 and L2 overlap. Clearly, for L1 P3 no elements of the both LHSs overlap, which means that A0 is the empty graph. We continue by calculating the pullback of l1 and A0 → L1 (which was obtained by the first pullback). As A0 is the empty graph, the resulting object A′0 is also the empty graph. Clearly, the morphism from A′0 to A0 is an isomorphism, i.e., we proceed by considering the interactions of decapsulateAttribute and P1 . The results of the pullbacks in the second iteration are the graphs A1 and A′1 . L1 and P1 only overlap at the node 1,10:Class in L1 P3 , and since decapsulateAttribute does not delete any nodes, the result A′1 of the second pullback also contains the node 1,10:Class. Once again, there is an isomorphism from A′1 to A1 (the identity morphism) and we proceed with the next iteration. In the third iteration, we obtain the graphs A2 and A′2 . When the rule decapsulateAttribute is applied and overlaps with P3 as described in the overlap L1 P3 , it will delete the nodes 3:Method, 2:Method and their incoming edges.

34

Lauer et al.

This means that the nodes 3,12:Method, and 2,13:Method contained in A2 will be deleted. In consequence, the result A′2 of the second pullback will now contain the nodes 1,10:Class, 4,11:Attribute and the variables edge that connects them. This, in particular, means that there is no isomorphism from A′2 to A2 and we have found a situation in which an application of decapsulateAttribute can delete an occurrence of P3 .

L2 5:Class name = superCIN generalizes

A' 0

A0 6:Class name = subCIN

variables

methods

9:Method

7:Method

name = N

name = "get" + N

name = " set" + N

P1

p1 generalizes

10:Class A' 1

methods

8:Attribute

5:Class name = superCIN generalizes

A1

6:Class name = subCIN

1,10:Class

1,10:Class variables

methods

9:Method

7:Method

name = N

name = "get" + N

name = " set" + N

P3 A' 2

methods

8:Attribute

p3

5:Class

A2

name = superCIN generalizes

1,10:Class

1,10:Class

methods

generalizes

3,12:Method 11:Attribute

name = " set" + N variables

variables

methods

4,11:Attribute

4,11:Attribute

2,13:Method

name = N vis. = " private"

name = N

6:Class

variables

10:Class

name = N vis. = " private" methods

name = subCIN

methods

variables

methods

13:Method

12:Method

8:Attribute

9:Method

7:Method

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

L1P3 K1

methods

name = "get" + N

eP3

5:Class

L1

name = superCIN generalizes

1:Class

1:Class

name = cIN

name = cIN

methods

variables

generalizes

3:Method 4,11:Attribute

name = " set" + N

l1

eL1 variables

methods

4:Attribute

4:Attribute

2:Method

name = N

name = N

name = "get" + N

name = N vis. = " private"

6:Class

variables

1,10:Class

name = subCIN

methods

methods

variables

2,13:Method

3,12:Method

8:Attribute

9:Method

methods

7:Method

methods

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

Fig. 18: Construction of proto-essences by deletion of the rules decapsulateAttribute and pullUpEncapsulatedAttribute

In the final step of the computation, we calculate the initial pushout of the morphism A′2 → A2 as shown in Figure 19. Intuitively, the graphs B and C of the initial pushout describe the elements that are deleted by decapsulateAttribute and their boundary, i.e., each node that is attached to a deleted edge, i.e., the Method nodes, their incoming edges, and the Class node. Moreover, the graph B shows the elements that are not deleted but needed in C, i.e., all those nodes that are not deleted but have an incoming or outgoing edge that is deleted. In

Conflict Essences for Nested Application Conditions

35

this particular case, this only applies for the node 1,10:Class. The computation

C B

1,10:Class

methods

3,12:Method name = " set" + N

1,10:Class

methods

2,13:Method name = "get" + N

A' 2

A2 1,10:Class

1,10:Class

methods

3,12:Method name = " set" + N

variables

variables

methods

4,11:Attribute

4,11:Attribute

2,13:Method

name = N

name = N

name = "get" + N

Fig. 19: Initial pushout that concludes the construction of proto-essences by deletion of of the rules decapsulateAttribute and pullUpEncapsulatedAttribute

of the initial pushout concludes the construction and the resulting proto-essence (a ◦ c : C → L1 , b ◦ c : C → P3 ) is shown in Figure 20. Applying the just illustrated computation to all possible overlaps, considering both directions and also insertions, provides the set of proto-essences of the rule pair decapsulateAttribute and pullUpEncapsulatedAttribute; in our example, all proto-essences turn out to be disabling essences. We discussed this set in Example 1 at the start of Section 5. The following example explains the individual essences in more detail. Example 7 (Disabling essence). Figure 5 shows six disabling essences of the decapsulateAttribute and pullUpEncapsulatedAttribute rules. Moreover, they also represent rule overlaps of the rules. Only the objects A (in the grey boxes) and C (in the orange boxes) are displayed. The morphisms to the rules’ LHSs and the objects in the application condition are given through the node identifiers. The graph contained in A1L1 P3 shows that decapsulateAttribute could violate the application condition of pullUpEncapsulatedAttribute by destroying an occurrence of P3 , which is existentially bound in the application condition of pullUpEncapsulatedAttribute. In this disabling essence, the node 4,11:Attribute is mapped to 4:Attribute in the LHS of decapsulateAttribute and to 11:Attribute in P3 . Whereas A1L1P 3 shows the elements that must be overlapped when this essence is embed1 ded in a transformation pair, CL1P 3 indicates the exact elements that cause a

36

Lauer et al. C 1,10:Class

methods

3,12:Method name = " set" + N methods

2,13:Method name = "get" + N

P3 L1

c

A

5:Class name = superCIN generalizes

1:Class name = cIN

methods

1,10:Class

3:Method name = " set" + N

methods

11:Attribute

name = " set" + N a

variables

generalizes

3,12:Method b

methods

variables

4:Attribute

2:Method

4,11:Attribute

2,13:Method

methods

name = N

name = "get" + N

name = N

name = "get" + N

name = N vis. = " private" methods

6:Class

variables

10:Class methods

name = subCIN

variables

methods

methods

13:Method

12:Method

8:Attribute

9:Method

7:Method

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

Fig. 20: Proto-essence by deletion of the rules decapsulateAttribute and pullUpEncapsulatedAttribute

conflict: When embedded in a transformation pair, decapsulateAttribute destroys both methods edges leading from 1,10:Class to 3,12:Method and from 1,10:Class to 2,13:Method. The existence of an embedding of this disabling essence implies that an occurrence of P3 is destroyed. However, this does not imply that the application condition of pullUpEncapsulatedAttribute is violated: The matched class 1,10:Class might contain other methods that, together with 1,10:Class, form another occurrence of P3 . A2L1P 3 and A3L1P 3 show two other ways so that decapsulateAttribute can destroy an occurrence of P3 . Either decapsulateAttribute only destroys the method edge to the getter-method of P3 (shown in A3L1P 3 ) or it only destroys the method edge to the setter-method of P3 (shown in A2L1P 3 ). In the middle row of Figure 5, we display disabling essences indicating that decapsulateAttribute causes a conflict by destroying the LHS of pullUpEncapsulatedAttribute, and vice versa. Note that these essences are also calculated by the approach for plain rules as presented in [3]. When AL1L2 is embedded in a transformation pair, decapsulateAttribute destroys the match of pullUpEncapsulatedAttribute by destroying the setter method and its incoming methods edge, which are also matched by pullUpEncapsulatedAttribute. A1L2L1 describes an similar conflict, but in this case it is the getter method and its edge that are destroyed. These two disabling essences also describe conflicts caused by pullUpEncapsulatedAttribute, because pullUpEncapsulatedAttribute destroys the respective methods edge, which is also matched by decapsulateAttribute. Finally, A2L2L1 describes a conflict caused by pullUpEncapsulatedAttribute that arises when pullUpEncapsulatedAttribute destroys the methods edge leading to 4,8:Attribute, which is also matched by decapsulateAttribute. (The bottom row of Figure 5 will be explained in Example 4.) The following two examples illustrate constructions from Section 6. First, we illustrate the use of our criterion for checking rule overlaps to be ac-conflicting. Example 8 (Ac-conflicting disabling essence). In Figure 21, we check whether a conflict essence of decapsulateAttribute and pullUpEncapsulatedAttribute (shown in Figure 5) is ac-conflicting. For this, we compute the two pullbacks shown in

Conflict Essences for Nested Application Conditions

37

Figure 21, where the first computes the elements of P3 in which A3L1 P3 and L2 overlap. The result is the graph L′2 which is equal to the empty graph. In the second step, we compute the pullback of l2 and L′2 → L2 to check which elements will be deleted by pullUpEncapsulatedAttribute. Since L′2 is the empty graph, K2′ is also equal to the empty graph, i.e., the disabling essence is ac-conflicting. A3 L1P3 C3 L1P3

L' 2

4,11:Attribute name = N vis. = " private"

K' 2

1,10:Class l' 2

methods

variables

3,12:Method name = " set" + N

P3

L2

b

K2

5:Class

5:Class

5:Class

name = superCIN

name = superCIN

name = superCIN

generalizes generalizes

generalizes

11:Attribute name = N vis. = " private" methods

6:Class

variables

10:Class methods

variables

methods

generalizes

6:Class p L2

name = subCIN

6:Class l2

name = subCIN

name = subCIN

methods variables

methods

methods

13:Method

12:Method

8:Attribute

9:Method

7:Method

8:Attribute

9:Method

7:Method

8:Attribute

9:Method

7:Method

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

name = N

name = "get" + N

name = " set" + N

Fig. 21: Check whether a disabling essence for the rules decapsulateAttribute and pullUpEncapsulatedAttribute is ac-conflicting

The following extends Example 4 by providing a detailed computation of a composed rule overlap. Example 9 (Composed rule overlap). Figure 5 shows two composed rule overlaps of disabling essences of decapsulateAttribute and pullUpEncapsulatedAttribute. Comp(AL1L2 , A1L2L1 ) indicates that AL1L2 and A1L2L1 can be embedded in the same transformation by identifying 1,6:Class. An occurrence of this composed overlap indicates that decapsulateAttribute causes a conflict with pullUpEncapsulatedAttribute by destroying 3,7:Method, which is matched by pullUpEncapsulatedAttribute. It also indicates that pullUpEncapsulatedAttribute causes a conflict with decapsulateAttribute by destroying the edge leading to 2,9: Method. When Comp(AL1L2 , A2L2L1 ) is embedded in a transformation pair, decapsulateAttribute will destroy the match of pullUpEncapsulatedAttribute by deleting the edge leading to 3,7:Method and pullUpEncapsulatedAttribute will destroy the match of decapsulateAttribute by deleting the edge leading to 4,8:Attribute. The exact computation of Comp(AL1L2 , A2L2L1 ) is shown in Figure 22. As both disabling essences involved signal a conflict for the plain rules, they are of the form (a : C → L1 , b : C → L2 ) This means that in the first step of the computation (when we are searching for an overlap of the codomains of a and a′ and of b and b′ ), we can simply chose L1 and L2 , i.e., the LHSs of decapsulateAttribute and pullUpEncapsulatedAttribute. The second overlap K ∗ is now an overlap of L1 and L2 as shown in the bottom

38

Lauer et al. L1 AL1L2 1:Class

methods

name = cIN

3:Method

CL1L2

name = " set" + N

variables

methods

1,6:Class

4:Attribute

2:Method

name = N

name = "get" + N

L1

3,7:Method

methods

name = " set" + N

Comp(AL1L2,A2 L2L1) 1:Class name = cIN

methods

3:Method 1,6:Class

name = " set" + N

3,7:Method

methods

name = " set" + N methods

variables

methods

4,8:Attribute

4:Attribute

2:Method

name = N

name = "get" + N

name = N

K*

L2

L2

5:Class

5:Class

5:Class

name = superCIN

name = superCIN

name = superCIN

generalizes

2:Method

methods

name = "get" + N

variables

generalizes

generalizes

1,6:Class

6:Class

6:Class

name = subCIN

name = subCIN

name = subCIN

methods

variables

methods

variables

4,8:Attribute

9:Method

3,7:Method

8:Attribute

9:Method

7:Method

8:Attribute

9:Method

7:Method

name = N

name = "get" + N

methods

name = " set" + N

name = N

name = "get" + N

methods

name = " set" + N

name = N

name = "get" + N

methods

name = " set" + N

methods

Fig. 22: Composed disabling essence of the rule decapsulateAttribute and pullUpEncapsulatedAttribute left of Figure 22. We now obtain the morphisms a∗ ∈ M and b∗ ∈ M by computing the pullback of eL1 and eL2 . The result contains the three nodes 1,6:Class, 3,7:Method, 4,8:Class, and their outgoing as these are the elements in K ∗ that are matched by both eL1 (L1 ) and eL2 (L2 ). Example 10 (Symbolic conflict essence). Together with a cospan condition, each conflict essence shown in Figure 5 forms a symbolic conflict essence. For AL1L2 , A1 L2L1 , A2 L2L1 , and the composed essences, which are not ac-conflicting, the application condition is equal to true. The remaining conflict essences are equipped with a non-trivial cospan condition of the form a′

b′

acce := ∃(Pi −→ D ← − Pj , Shift(m∗ , acL1 +L2 ∧ ac∗L1 +L2 )), where d := Shift(m∗ , acL1 +L2 ∧ ac∗L1 +L2 ) ensures that 1. both rules satisfy their application conditions before the transformations (checked by acL1 +L2 ) and that 2. the transformation pair is parallel dependent (checked by ac∗L1 +L2 ). This means that ac∗L1 +L2 checks whether both application conditions are satisfied after the transformations, or not. Through the cospan, we can use both embedding morphisms of the symbolic conflict essence to check the satisfaction of d. Figure 23 shows a symbolic conflict essence for the rules decapsulateAttribute and pullUpEncapsulatedAttribute. The contained conflict essence is displayed at

Conflict Essences for Nested Application Conditions

39

the top, and the corresponding cospan condition at the bottom of the figure. As explained in Example 1, the conflict essence signals that decapsulateAttribute deletes the getter and setter methods of the private attribute 4,11:Attribute which could lead to a violation of the application condition of pullUpEncapsulatedAttribute if the class 1,10:Class does not contain other getter or setter methods for this attribute, or a public attribute with the name N. The first row of the cospan condition contains the cospan that is constructed by calculating the pushout of the two morphisms contained in the conflict essence (compare Definition 13). In this case, the obtained graph D is equal to P3 , and we just add a morphism from L1 in D accoring to the node identifiers. Moreover, the graph D is exactly the graph that has initially been used to construct the conflict essence A1L1P 3 . The second row of the condition shows acL1 +L2 that checks whether both rules satisfy their respective application condition before the transformation. As decapsulateAttribute has no application condition, we only need to check the application condition of pullUpEncapsulatedAttribute. Since pullUpEncapsulatedAttribute will move the node 8:Attribute and its getter and setter method from 6:Class to 5:Class, we need to check whether each subclass of 5:Class contains an attribute with name N that is either public or has corresponding getter and setter methods contained in the same class. This is why in P1′ we are searching for any other subclass of 5:Class. Each of these classes must now contain an attribute with name N that is either 1. public, as checked by P2′ or 2. private and has getter and setter methods contained in the same method (as checked by P3′ ). Please note that we omit another graph that checks whether 1,10:Class contains an public attribute with name N for space reasons. This graph is essentially equal to P2′ with the difference that, instead of in 16:Class, the attribute 17:Attribute is contained in 1,10:Class and the class 16:Class does not exist. The bottom row of the condition shows ac∗L1 +L2 that checks whether pullUpEncapsulatedAttribute will still satisfy its application condition after decapsulateAttribute was applied. For this, we only need to check whether 1,10:Class still satisfies the remaining part of the condition. This is because decapsulateAttribute only changes structure contained in this class. There are two possibilities so that 1,10:Class still satisfies the condition, either 1. it contains another attribute with name N that is public, as modelled in P4′ , or 2. it contains two other getter and setter methods for 4,11:Attribute that are not deleted by decapsulateAttribute as modelled in P5′ . If this condition is satisfied, we know that 1,10:Class still satisfies the condition after an application of decapsulateAttribute and, in particular, that pullUpEncapsulatedAttribute will satisfy its application condition after decapsulateAttribute was applied.

Lauer et al. 40

L1 1:Class name = cIN

methods

3:Method name = " set" + N methods

2:Method

variables

name = "get" + N

1,10:Class

16:Class

name = N

variables

4:Attribute

P' 1

name = N vis. = " private"

4,11:Attribute

generalizes

generalizes

D

4,11:Attribute name = N vis. = " private"

A1L1P3

C1L1P3

name = N vis. = " private"

4,11:Attribute variables

C1L1P3

methods

methods

1,10:Class

3,12:Method name = " set" + N

2,13:Method name = "get" + N

P3

generalizes

5:Class

6:Class name = subCIN

7:Method

methods

name = " set" + N

generalizes

5:Class

variables

name = superCIN

11:Attribute

generalizes

6:Class

10:Class

name = superCIN

name = N vis. = " private"

9:Method

generalizes

name = subCIN

name = "get" + N

methods

8:Attribute

variables

12:Method

methods

13:Method

methods

7:Method

variables

1,10:Class

methods

9:Method

methods

8:Attribute

variables

3,12:Method

name = N

methods

2,13:Method

name = " set" + N

3,12:Method

name = N

8:Attribute

name = "get" + N

9:Method

name = " set" + N

7:Method

methods

19:Method

generalizes

generalizes

name = " set" + N

16:Class

18:Method

variables

1,10:Class

5:Class

generalizes

name = superCIN

6:Class name = subCIN

name = "get" + N

9:Method

name = " set" + N

7:Method

methods

name = N

8:Attribute

variables

3,12:Method

methods

name = " set" + N

variables

2,13:Method

methods

name = "get" + N

methods

name = N vis. = " private"

4,11:Attribute

name = N vis. = " private"

17:Attribute

name = "get" + N

P' 3

name = "get" + N

generalizes

name = superCIN

6:Class name = subCIN

7:Method

name = " set" + N

methods

name = " set" + N

1,10:Class

5:Class

name = "get" + N

variables

generalizes

name = N

name = N vis. = " private"

4,11:Attribute

16:Class

name = " set" + N

name = N vis. = " public"

17:Attribute

P' 2 5:Class

6:Class

variables

name = "get" + N

methods

generalizes

methods

9:Method

methods

8:Attribute

variables

3,12:Method

methods

2,13:Method

methods

name = subCIN

generalizes

name = superCIN

methods

7:Method

name = " set" + N

methods

9:Method

name = "get" + N

variables

8:Attribute

name = N

methods

3,12:Method

name = " set" + N

methods

2,13:Method

name = "get" + N

name = subCIN

6:Class

generalizes

name = superCIN

5:Class

name = " set" + N

generalizes

name = "get" + N

P' 5 20:Attribute

1,10:Class

variables

name = N

5:Class

name = N vis. = " public"

6:Class

generalizes

name = superCIN

name = N vis. = " private"

4,11:Attribute

2,13:Method

methods

name = " set" + N

15:Method generalizes

name = subCIN

name = "get" + N

methods

7:Method

variables

name = " set" + N

methods

9:Method

methods

name = "get" + N

variables

name = "get" + N

14:Method

methods

1,10:Class

methods

name = " set" + N

P' 4

variables

name = "get" + N

4,11:Attribute name = N vis. = " private"

methods

name = N

8:Attribute

methods

3,12:Method

variables

name = " set" + N

methods

2,13:Method

methods

name = "get" + N

Fig. 23: Symbolic conflict essence of the rules decapsulateAttribute and pullUpEncapsulatedAttribute