In AGG termination criteria are implemented for Layered Graph Transformation Systems (LGTS).
Termination of the rule applying of a certain layer is not always guaranteed. The following conditions have to be satisfied for all rules.For each rule r we have a rule layer rl (r) with 0 <= rl (r) <= k0 ( rl (r) , k0 in IN ), where k0 + 1 is the number of layers, and for each label l a creation layer cl (l) in IN and a deletion layer dl (l) in IN .
(1) Deletion Layer Conditions
-----------------------------------------
If k is a deletion layer, then
1. each rule r decreases the number of graph items, or
2. each rule r decreases the number of graph items of one special type.
(2) Deletion Layer Conditions
-----------------------------------------
If rule layer k is a deletion layer, then
1. r deletes at least one item,
2. 0 <= cl (l) <= dl (l) <= k0 for all l ,
3. if r deletes l then dl (l) <= rl (r) ,
4. if r creates l then cl (l) > rl (r) .
(3) Nondeletion Layer Conditions
-----------------------------------------
If rule layer k is a nondeletion layer, then
1. r is nondeleting, i.e. r : L -> R is total and injective,
2. r has NAC n : L -> N with n' : N -> R injective s.t. n' o n = r ,
3. if x with type(x) = l occurs in L then cl (l) <= rl (r) ,
4. if r creates an item of type l then cl (l) > rl (r) .The termination criteria (2) and (3) are defined for typed graph transformation with injective rules, injective matches and injective negative application conditions (NACs).
The deletion layer conditions (2) ensure that the last creation of an element of a certain type should precede the first deletion of an element of the same type.
On the other hand, nondeletion layer conditions (3) ensure that if an element of a certain type occurs in the LHS of a rule then all elements of the same type were already created in this or a previous layer.A layered graph grammar with deletion and nondeletion layers terminates, if it is finite and if for each layer the deletion or nondeletion layer conditions defined above are satisfied.
In AGG, the rule layer can be set or generated. The creation and deletion type layer will be generated automatically. For each layer one set of layer conditions will be proved.