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_i. Purely 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 <= n, r_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
- Max intersection of direct enabling predecessors
- Incomplete recognition of potential conflict free summarized predecessors
- 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.