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 dependency or independency 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. It avoids dangling edges.
(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 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.
(4c) 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 define a rule sequence in order to check its applicability (resp. non-applicability). It combines three tables and some buttons.
The first table contains the rules of the currently selected grammar.
The second table shows defined rule sequences. You can create a new empty sequence by clicking the button New Sequence. The sequences are ordered by its position in the second table. The order can be changed by pressing and dragging of the middle mouse button.
The third table shows the rules of the currently selected sequence.By selecting one or more rules in the first table and clicking on the button Add the rule(s) will be put into the last created or currently selected sequence. The rule order of the third table can be changed by pressing and dragging of the middle mouse button.
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 node of the corresponding 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 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 conflictfree 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 buttons Uncheck, Copy and Delete allow to manipulate already defined rule sequences.
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 content of this dialog can be cleaned (button Clear) and refreshed by selecting an other grammar node 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.
From applicable rule sequence to transformation rule sequence
Buttons SetTrafoRS and AddTrafoRS allow to set (add) currently selected applicable rule sequence to transformation rule sequence(s) of the current grammar and perform graph transformation along the rule matches which are computed during applicability check. Surely, this is useful when applicability check was successful.
When one of the buttons SetTrafoRS and AddTrafoRS clicked the transformation mode ST (transformation by rule sequences) is activated in the GraGra editor. Additionally, graph display settings wait after step and select new objects after step are set.
After the button Start clicked the first rule of a rule sequence is loaded in the Rule editor and applied on a match which corresponds as near as possible to a match that was computed during rule applicability check. The user can see changes of the host graph in the Graph editor. By clicking any key of the keyboard the second rule of the sequence is loaded and applied, and so on.
In case when a rule match for graph transformation cannot be derived from its corresponding rule applicability match, the next valid match is taken into account. This is the reason why graph transformation along an applicable rule sequence sometimes deviates from the expected match order.
Please note, information about matches of rule applicability check of a rule sequence is not written in a (.rsx) file when saving rule sequences. After a (.rsx) file was loaded there is needed to perform applicability check again.
A way to improve graph transformation along an applicable rule sequence is to define an object flow between the rules. This is the future work of AGG development.