Critical Pair Analysis
Critical pair analysis is known from term rewriting and usually used to check if a term rewriting system has a functional behavior, i.e. is confluent. Critical pair analysis has been generalized to graph rewriting . Critical pairs formalize the idea of a minimal example of a conflicting situation. From the set of all critical pairs we can extract the objects and links which cause conflicts or dependencies.
A critical pair is a pair of transformations (p1, p2) , where p1(m1) : G => H1 and p2(m2) : G => H2 which are in conflict, and such that graph G is minimal, i.e., G is gluing of the left-hand sides of the rules p1 and p2. It can be computed by overlapping L1 and L2 in all possible ways, such that the intersection of L1 and L2 contains at least one item that is deleted or changed by one of the rules and both rules are applicable to G at their respective occurences.
The set of critical pairs represents precisely all potential conflicts, that is there exists a critical pair like above if, and only if, p1 may disable p2, or, vice versa, p2 may disable p1.
After computation of critical pairs the overall rule set is structured into conflict free and conflicting rules. In the following, we explain when two rule applications are in conflict and how all critical situations can be found.
There are three reasons why rule applications can be conflicting: The first two are related to the graph structure while the last one concerns the graph attributes.
Two rule applications are in conflict if at least one of the conditions above is fulfilled. To find all conflicting rule applications, minimal critical graphs are computed to which rules can be applied in a conflicting way. Basically we consider all overlapping graphs of the left-hand sides of two rules with the obvious matches and analyze these rule applications. All conflicting rule applications we found are called critical pairs. If one the rules contains negative application conditions, the overlapping graphs of one left-hand side with a part of the NAC have to be considered in addition.
- One rule application deletes a graph object which is in the match of another rule application.
- One rule application generates graph objects in a way that a graph structure would occur which is prohibited by a negative application condition (NAC) of another rule application.
- One rule application changes attributes being in the match of another rule application.
If the graph grammar analised is layered, the critical pair analysis can be optimized in the way that critical pairs are searched for rules in the same layer only.
Note: If you use attributed graph grammar please do not forget to set attribute members of the graph objects in all rules before critical pairs will be computed :
- use constants or variables in the left-hand side of a rule
- use constants, variables or expressions in the right-hand side of a rule
The critical pair analysis for grammar rules can be more efficient if a type graph is defined for the graph grammar containing multiplicity constraints. Upper bounds of multiplicity constraints are used to reduce the set of critical pairs by throwing out the meaningless ones. Dependent on the graph grammar the number of critical pairs can be reduced drastically by the use of multiplicitiy constraints.
Nevertheless, the critical pair analysis may take time, even for one particular rule pair.
Graphical user interface
Since the critical pair analysis is an interesting analysis technique in its own and has many more application areas besides parsing we provide a separate graphical user interface for it. This interface is convenient to consider all critical pairs or just a part of them in all detail. I.e. for each two rules all overlapping graphs and corresponding matches can be considered.
In the following, we consider the menus and options of the critical pair analysis.
The menu is Analyzer / Critical Pair Analysis. The available menu items are shown in Figure 1. Its availability depends on the state of the critical pair analysis.
Figure 1. Critical Pair Analysis menu
- ResetSets a current selected grammar to be the grammar for critical pair analysis.
- UnlockAllows edit operations on the grammar for critical pair analysis.
Please note: It is necessary to reset the grammar for critical pair analysis after giving allowance for changes of the grammar.
- GenerateSets critical pair analysis GUI and starts to generate critical pairs. Critical pairs will be generated for all rules of the selected graph grammar. After finishing the generation you can select rule pairs to see results.
Please note: It is not possible to edit the grammar after returning to main GUI. Use Unlock to make the grammar editable. Unlock is enabled when generating is finished or stopped.
- StopStops generating critical pairs.
- DebugGenerates critical pairs step by step. After selecting a rule pair the critical pair computation of this pair will be started.
Please note: You can select one new rule pair, if the computation of the already selected pair has finished.
It is not possible to edit the grammar after returning to main GUI. Use Unlock to make the grammar editable. Unlock is enabled when generating is finished or stopped.
- EmptyRemoves current critical pairs.
- LoadLoads critical pairs file ( .cpx ) already saved before.
- SaveSaves critical pairs. Saved critical pairs can be used for the parsing process later. Using Save after Debug offers the possibility to save only a subset of critical pairs.
- backReturns to main GUI.
The options for the critical pair analysis : menu Preferences / Options...
Figure 2 shows possible settings.
Figure 2. Options of critical pair analysis
The settings allow to choose the algorithm for critical pair analysis. Usually, critical pairs express exclude relations between rules only. In the literature also causal dependencies of rule applications are considered. In this case, a before relation would be computed. The computation requested can be set by the upper combobox , choosing <exclude only> or <exclude and before> (Figure 3). Please note that the setting <exclude and before> is not yet implemented.
Figure 3. Algorithm of critical pair analysis
We can distinguish between layered and non-layered critical pairs. This option can be set by the checkbox Layered. For layered graph grammars, critical pairs are computed within layers only.
Setting Complete in Figure 2 means the complete computation of all critical pairs. If this option is not set, the computation of critical pairs is stopped after the first critical pair has been found.
Further settings determine the graphical representation of the analysis results on the screen. Figure 4 shows the possible display options:
Figure 4. Display options for critical pair analysis
For a better overview, the maximal number of crticial pairs shown may be set, in the default case all pairs are shown. Furthermore, the initial window size for overlapping graphs may be set.
Viewing critical pairs The graphical user interface of viewing computed critical pairs is shown and described in Figures 14 and 15 of the ''Shopping`` example below.
Sample Critical Pair Analysis in AGG
As example we use the grammar ''Shopping`` described in Detection of Conflicting Functional Requirements in a Use Case-Driven Approach by Jan Hendrik Hausmann, Reiko Heckel and Gabi Taentzer.
The type graph of the grammar is shown in Figure 6.
Figure 6. The type graph.
A possible start graph of the grammar is shown in Figure 7.
Figure 7. The start graph.
The rules are shown below:
Figure 8. Rule: takeCart.
Figure 9. Rule: selectCart.
Figure 10. Rule: payBill.
Figure 11. Rule: createBillt.
Figure 12. Rule: billGood.
Figure 13. Rule: settleBill.
Viewing critical pairs Selecting one rule from the top rule list and one rule from the bottom rule list of the left panel below has the following effect:- The left-hand side of the first selected rule is shown in the left top subpanel of the right panel.
- The left-hand side of the second selected rule is shown in the right top subpanelof the right panel.
- Computed critical pairs will be shown in the bottom of the right panel.
- The mappings between graph objects will be shown through equal numbers.
- If no critical pairs exist, a message 'not critical' will be shown.
Back to our example:
The critical pairs of rules 'payBill' and 'settleBill' are shown in Figure 14.
Both transformations destroy the owns links between the good and the shop. Thus, they overlap in an item which is deleted. As a consequence, each of the two rule applications disables the other one, i.e. they cannot be part of the same transformation sequence.
Figure 14. A conflict between 'payBill' and 'settleBill' .
The pair of rules 'payBill' and 'selectGood' is not critical as shown in Figure 15.
Figure 15. Rule pair: 'payBill' and 'selectGood' .
Graph grammar ''Shopping`` is saved in shopping.ggx .
The critical pairs of its rules are saved in shopping.cpx .
Using a type graph with multiplicity constraints at the edges leads to considerably less critical pairs. Please compare the following two tables. The upper table shows the number of critical pairs for each pair of rules without using the type graph in Figure 6, while the lower table shows the number of critical pairs for each pair of rules using the type graph.
Critical pair analysis is described in: Confluence of Typed Attributed Graph Transformation Systems by Reiko Heckel, Jochen Malte Küster and Gabriele Taentzer Critical pair analysis is used in: Detection of Conflicting Functional Requirements in a Use Case-Driven Approach by Jan Hendrik Hausmann, Reiko Heckel and Gabriele Taentzer. Efficient Parsing of Visual Languages based on Critical Pair Analysis and contextual Layered Graph Transformation by P. Bottoni, A. Schürr and G. Taentzer (full paper) More about the facilities of the parser and the critical pair analysis in AGG can be read in the diploma thesis of Thorsten Schultzke (in German):
"Entwicklung und Implementierung eines Parsers für visuelle Sprachen basierend auf kritischer Paaranalyse"