Applicability and Non-Applicability Check for Rule Sequences

The satisfaction of the applicability (resp. non-applicability) criteria described below is sufficient for the applicability (resp. non-applicability) of a rule sequence to a graph. These criteria can be checked in a static way, since they are based mainly on the dependence or independence of rules. Moreover, the non-satisfaction of one of the criteria gives a hint to the reason for a rule sequence to be applicable or not.

Applicability Criteria of Rule Sequences

Given a sequence s : r_1, r_2 ... r_n  of n  rules and a graph G  on which this sequence should be applied. The satisfaction of (1),(2),(3) and (4a),(4b) or (4c) for each rule in s  guarantee that s  will be applicable in G .

(1) The initialization  criterion: r_1  is applicable on G  via an injective match.

(2) The no node-deleting rules  criterion: each rule in s  is non-deleting on nodes, to avoid dangling edges. In case of node-deleting, each rule has to delete all adjacent edges explicitly.
(In AGG the user can turn off this rule applicability condition.)

(3) The no impeding predecessors  criterion: it ensures that the applicability of a rule r_i  in s  is not impeded by one of the predecessor rules r_j  of r_i . This is the case if rule r_i  is not in conflict with r_i .

(4a) The pure enabling predecessor  criterion: it ensures that the applicability of a rule r_i , which is not applicable on graph G , because it is purely sequential dependent  from a rule r_j  occurring somewhere before r_i  in the sequence s.  In this case r_j  triggers the applicability of r_iPurely sequential dependency  means that there exists an injective morphism from the LHS of rule r_i  into the RHS of rule r_j. Moreover, each NAC of r_i  forbids at least one graph element of type t  such that an element of type t  is neither present in G  nor produced by any predecessor of r_i.

(4b) The partial enabling predecessor(s)  criterion: there exists a concurrent rule r_c  of a not necessarily direct predecessor rule r'  and rule r  such that r_c  is applicable to G , and all predecessors of r_c  do not cause a conflict with r_c . Moreover, r'  is self-enabled such that its match can be forwarded to the match of r_c .

(4c) The direct enabling predecessor(s)  criterion: it ensures the applicability of a rule r_i , which is not applicable on graph G , because it is triggered by a (resp. some) direct predecessor rule(s) r_i-1  (r_i-2  r_i-3 ...) since it (resp, they) delete(s) graph parts (edges) forbidden by r_i  or produces graph parts needed by r_i . This is expressed by the fact that a concurrent rule r_c  of r_i  and r_i-1  (r_i-2  r_i-3 ...) exists which is applicable via an injective match on the start graph G . Moreover, r_j  with  j < (i-1)   is no impeding predecessor for r_c  and r_c  is no impeding predecessor for r_j  with  i < j <= n.

(4d) The not needed  predecessor criterion: rule r_i  itself is applicable to graph G .

Note that the criteria above are sufficient but not necessary for a rule sequence to be applicable on a graph.

Non-Applicability criteria of Rule Sequences

Given a sequence s : r_1, r_2 ... r_n  of n  rules and a graph G  on which this sequence should not be applicable. The satisfaction of one of the following criteria guarantee that this sequence will not be applicable on G.

(1) The initialization error  criterion: r_1  is not applicable on graph G.

(2) The no enabling predecessor  criterion: there exists r_i  which is not applicable on graph G  and for all rules r_j  in s  with 1 <= j < i <= nr_i  is asymmetrically sequential independent on r_j. This means that r_i  would need some predecessor rule producing or deleting a graph part to become applicable and such a rule does not exist.

Additionally, our Technical Report Sufficient Criteria for Applicability and Non-Applicability of Rule Sequences  written by L.Lambers, H.Ehrig and G.Taentzer  gives you a detailed explanation to this matter. You can find it in the example folder Pizza  which is a part of the AGG  Examples_V164.

GUI of Applicability of Rule Sequences

The GUI dialog allows to select a rule sequence in order to check its applicability (resp. non-applicability). It combines two tables and some buttons.

The first table shows defined rule sequences.
To create a new rule sequence please use the pop-up menu GraGra -> New -> Rule Sequence. A new RuleSequence item will appear in GraGra tree view. You can rename it. By selecting this tree item a dialog will be opened which allows to define this rule sequence.

With aim to be used for applicability (resp. non-applicability) checking the defined rule sequence will be flattened in a plain sequence:
- each subsequence (resp. each rule) is repeated iterations times;
- the star (*) is converted by two times.
Such flattened rule sequence is then shown in the first table of this dialog.
The second table shows the rules of the currently selected sequence.

The start graph on which a rule sequence should be applied is set automatically. It is the current host graph of the grammar which is visible in the AGG  editor. Changing the start graph for the selected rule sequence is possible by selecting another graph item of the current grammar in the GraGras  tree view of the AGG  application.

In many cases though a rule sequence is given without a graph. To check a such sequence is possible when the button Use graph is not selected. Please note, the current implementation of this case is still in progress.

Options for computing concurrent rules

For the applicability criteria we need to compute for criterion 4b and 4c concurrent rules  which can be constructed from a sequence of single rules. Such a concurrent rule  establishes in one transformation step the same effect as single rules would establish in consecutive transformation steps. Thus, a concurrent rule  summarizes in one rule which parts of graph should be preserved, deleted and produced when applying the corresponding rule sequence to this graph. Moreover, a summarized set of NACs on the concurrent rule  expressing which graph parts are forbidden.
The computation of concurrent rules  may be time and space expensive. Using next three options

allows to decrease the number of concurrent rules  being built and checked and so their costs. If no size is set, the computation of concurrent rules  and their checking will run as long as needed.
    - Number of direct enabling predecessors expresses from how many direct predecessors a rule is considered to be dependent. Thus it gives the length of a sequence of single rules which are used to construct a concurrent rule  from.
    - Max intersection of direct enabling predecessors means that only the biggest overlapping of rhs and lhs rule parts is taken in account when computing concurrent rules. It is assumed in this case that rules use as much as possible elements produced or preserved by their predecessor rules. If this option isn't selected, all possible overlapping are computed.
    - Incomplete recognition of potential conflict free summarized predecessors means that only single rules which are used to construct a concurrent rule  from will be checked by Critical Pair Analysis (CPA) for conflicts with predecessors and successors in the corresponding rule sequences. If this option isn't selected, also the concurrent rule  itself will be checked by CPA for conflicts with predecessors and successors.
Note that usage of these options may cause that the corresponding rule sequence doesn't satisfy anymore the applicability criteria, although it would satisfy them if no option of these three options is used.

Buttons

The buttons Check and Result allow to check applicability criteria of the currently selected rule sequence and show tables with results. Additionally, the button Uncheck for reseting results and the button Refresh to refresh the rule sequence after the current grammar was changed.

There are two tables with results : Applicability  table and Non-Applicability  table. A green field of the Applicability  table (resp. a red field of the Non-Applicability  table) shows the satisfaction of a criterion for the corresponding rule, an orange field corresponds to the non-satisfaction of a criterion, a gray field denotes that it was not necessary to check a criterion for the corresponding rule.

The button Use defined object flow is enabled when an object flow is defined for the current rule sequence. If the button is selected, the object flow is involved during checking applicability (resp. non-applicability) criteria. It used for rule matching and for construction of concurrent rules.

The content of this dialog can be reset by selecting another grammar in the GraGras  tree view.

Rule sequences together with results of the checking applicability (resp. non-applicability) criteria and corresponding graph grammar can be saved (button Save)  in a (.srx) file and loaded later again.