Omit Negative Application Conditions

This is an optimisation pattern.

Summary

Redundant tests for negative application conditions of a rule are omitted in order to optimise the rule implementation.

Application conditions

If it can be statically deduced that the succedent (rule actions/postcondition) of a rule is inconsistent with the antecedent (rule condition/assumption), omit checks in the rule implementation for the truth of the succedent. Such checks can constitute a substantial part of the execution time of the transformation rule for complex succedents.

Solution

Before applying a rule

for s : Si satisfying SCond
do Succ

to source model elements, model transformation implementations usually test to check if the succedent Succ is already true (if SCond holds): if Succ does already hold, then the rule is not applied. However, if it is known that Succ logically implies not(SCond) then the test of Succ is unnecessary and can be omitted.

Benefits

The executable code of the rule is simplified and its execution cost is reduced.

Applications and examples

The pattern is applicable to all categories of transformation, but it is particularly relevant for update-in-place transformations such as refactorings. The pattern is an inbuilt implementation technique in UML-RSDS.

An example of applying the pattern is the derivation of the root class of an Entity, where rootClass is a *..0..1 auxiliary association from Entity to Entity:

for e : Entity satisfying e.parent->size() = 0
do e.rootClass = Set{ e }

This rule sets the root class of each class e without superclasses to be e itself.

for e : Entity
satisfying e.parent->size() > 0 and
e.rootClass->size() = 0 and
e.parent.rootClass->size() > 0
do e.rootClass = e.parent.rootClass

This rule sets the root class of a class e with superclasses to be the root class(es) of all its direct superclasses, if e's root has not already been set and if its parent does have a set root class. In the second rule, the succedent contradicts the antecedent, so the test for the succedent can be omitted from the rule implementation.

This example also illustrates a case of Sequential Composition where two rules write disjoint sets of objects, and the second reads data written by the first. The first rule here has a bounded iteration implementation, but the second needs a fixed-point implementation.

Related patterns

The Replace Fixed-point by Bounded Iteration optimisation is an alternative optimisation of such rules.