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.
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.