Critical Pair Analysis in   

 

 

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.  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. 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.   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 Reset Sets a current selected grammar to be the grammar for critical pair analysis. Unlock Allows 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. . Generate Sets 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. Stop Stops generating critical pairs. Debug Generates 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. Empty Removes current critical pairs. Load Loads critical pairs file ( .cpx ) already saved before. Save Saves 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. back Returns 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"

 

Revision: