Table of Contents
Fetching ...

Using weakest application conditions to rank graph transformations for graph repair

Lars Fritsche, Alexander Lauer, Maximilian Kratz, Andy Schürr, Gabriele Taentzer

TL;DR

The paper introduces a dynamic framework to rank graph-transformations by their potential to repair inconsistencies, using impairment- and repair-indicating application conditions derived from nested graph constraints. A central theorem connects the gain in consistency to the difference between repairs and impairments, enabling look-ahead and greedy optimization for graph repair. The approach is instantiated on the CRA problem, implemented in eMoflon, and evaluated against an ILP-based GIPS baseline, demonstrating scalable performance and competitive solution quality. The work extends prior constraint-checking and repair techniques by accommodating arbitrary nested constraints and providing a principled, weakest-direct-conditions characterization for consistency-preserving transformations.

Abstract

When using graphs and graph transformations to model systems, consistency is an important concern. While consistency has primarily been viewed as a binary property, i.e., a graph is consistent or inconsistent with respect to a set of constraints, recent work has presented an approach to consistency as a graduated property. This allows living with inconsistencies for a while and repairing them when necessary. For repairing inconsistencies in a graph, we use graph transformation rules with so-called {\em impairment-indicating and repair-indicating application conditions} to understand how much repair gain certain rule applications would bring. Both types of conditions can be derived from given graph constraints. Our main theorem shows that the difference between the number of actual constraint violations before and after a graph transformation step can be characterised by the difference between the numbers of violated impairment-indicating and repair-indicating application conditions. This theory forms the basis for algorithms with look-ahead that rank graph transformations according to their potential for graph repair. An evaluation shows that graph repair can be well-supported by rules with these new types of application conditions in terms of effectiveness and scalability.

Using weakest application conditions to rank graph transformations for graph repair

TL;DR

The paper introduces a dynamic framework to rank graph-transformations by their potential to repair inconsistencies, using impairment- and repair-indicating application conditions derived from nested graph constraints. A central theorem connects the gain in consistency to the difference between repairs and impairments, enabling look-ahead and greedy optimization for graph repair. The approach is instantiated on the CRA problem, implemented in eMoflon, and evaluated against an ILP-based GIPS baseline, demonstrating scalable performance and competitive solution quality. The work extends prior constraint-checking and repair techniques by accommodating arbitrary nested constraints and providing a principled, weakest-direct-conditions characterization for consistency-preserving transformations.

Abstract

When using graphs and graph transformations to model systems, consistency is an important concern. While consistency has primarily been viewed as a binary property, i.e., a graph is consistent or inconsistent with respect to a set of constraints, recent work has presented an approach to consistency as a graduated property. This allows living with inconsistencies for a while and repairing them when necessary. For repairing inconsistencies in a graph, we use graph transformation rules with so-called {\em impairment-indicating and repair-indicating application conditions} to understand how much repair gain certain rule applications would bring. Both types of conditions can be derived from given graph constraints. Our main theorem shows that the difference between the number of actual constraint violations before and after a graph transformation step can be characterised by the difference between the numbers of violated impairment-indicating and repair-indicating application conditions. This theory forms the basis for algorithms with look-ahead that rank graph transformations according to their potential for graph repair. An evaluation shows that graph repair can be well-supported by rules with these new types of application conditions in terms of effectiveness and scalability.
Paper Structure (29 sections, 19 theorems, 32 equations, 25 figures, 1 table)

This paper contains 29 sections, 19 theorems, 32 equations, 25 figures, 1 table.

Key Result

Lemma 5.6

Given two graphs $G$ and $H$, two overlaps $(i_G, i_H), (i'_G, i'_H) \in \mathop{\mathrm{OL}}\nolimits(G,H)$ with overlap graphs $GH$ and $GH'$, and a morphism $p \colon GH \mathop{\mathrm{\hookrightarrow}}\nolimits X$ into some graph $X$. Then $(i_G, i_H) \cong (i'_G, i'_H)$ if and only if there is

Figures (25)

  • Figure 1: Class diagram (left) and feature dependencies (right)
  • Figure 2: Refactoring rules moveAttribute and moveMethod and constraints: h$_1$: A method must not be contained in more than one class. h$_2$: An attribute must not be contained in more than one class. w$_1$: Two methods within the same class $\textsf{c}'$ should have at least one dependency on a common attribute within the same class $\textsf{c}'$. w$_2$: A method should not depend on an attribute from another class. w$_3$: Methods contained within the same class must have at least one dependency on each other. w$_4$: A method should not depend on a method of another class.
  • Figure 3: Repair-indicating application conditions for the rules moveAttribute and moveMethod w.r.t. the constraints $\textsf{w}_1$ and $\textsf{w}_2$. The node labels implicitly denote the mappings of the LHS of the rule and the premise of the constraint. For example, the label $c_2/c'$ indicates that the node $c_2$ from the LHS of moveAttribute and $c'$ from the premise of $\textsf{w}_1$ are mapped to the node $c_2/c'$.
  • Figure 4: Type graph (top) and typed graph (bottom)
  • Figure 5: Graph transformation
  • ...and 20 more figures

Theorems & Definitions (71)

  • Definition 3.1: Graph and graph morphism
  • Example 3.2
  • Definition 3.3: Typed graph, typed graph morphism
  • Example 3.4
  • Definition 3.5: Nested graph conditions
  • Example 3.6
  • Definition 3.7: Semantics of condition
  • Example 3.8
  • Definition 3.9: Graph transformation rule and application condition
  • Example 3.10
  • ...and 61 more