Replace Fixed-point by Bounded Iteration

This is an optimisation pattern.

Summary

Use a single bounded iteration over a source domain Si, instead of a fixed-point iteration, to implement rules based on Si which also create, modify or delete Si elements, if each application strictly reduces the set of Si elements that satisfy the application conditions of the rule.

Application conditions

A rule

for s : Si satisfying SCond
do Succ

can be implemented by a single iteration over Si provided that each application of Succ reduces the set of Si instances that match the application conditions of the rule.

Solution

For such a rule, if the above conditions hold, then a bounded iteration over the original set of Si instances that satisfy SCond is sufficient to ensure that the rule is established, because no other instances can satisfy the application condition.

One test for this situation is that for any s' : Si created/modified in Succ, the initialised/modified data of s' does not satisfy SCond.

Benefits

The execution time of the optimised rule implementation depends only upon the original number of elements of Si, not upon the maximum number that could exist. There is no need for proof of termination of the implementation, e.g., using a variant function.

Applications and examples

The pattern is applicable to all categories of transformation, but is particularly relevant for update-in-place transformations.

An example is the `repotting geraniums' example of (Rensink et al, 2009):

for p : Pot; v satisfying
p.broken = true and
v = p.plants->select( flowering = true ) and v /= Set{}
create p1 : Pot satisfying p1.plants = v

For every broken pot p that contains some flowering plant, a new (unbroken) pot p' is created and the flowering plants of the broken pot are transferred to the new pot.

Even though new pots are created by applications of the rule, the number of pots satisfying the application condition (the antecedent of the rule) is reduced by each application. p1.broken = false follows from the succedent.

In UML-RSDS the pattern is an inbuilt implementation facility. Rules can be marked for optimisation by this pattern by using pre-state versions of the entities and features involved on the LHS of the rule, e.g.:

for p : Pot@pre; v satisfying
p.broken@pre = true and
v = p.plants@pre->select( flowering = true ) and v /= Set{ }
create p1 : Pot satisfying p1.plants = v

for the above example, where f@pre is the value of the entity type or feature f at the start of execution of the transformation rule. This indicates that the rule does not write any data that it also reads (Pot, plants and broken are written, but only the pre-state versions of these features are read), so that a bounded iteration can be automatically selected for implementation of the rule.

(Rensink et al., 2009) A. Rensink, J-H. Kuperus, Repotting the Geraniums: on nested graph transformation rules, proceedings of GT-VMT 2009, Electronic communications of the EASST vol 18, 2009, http://dblp.uni-trier.de/db/journals/eceasst/eceasst18.html#RensinkK09.