4.3.7. Forall Rule

4.3.7. Forall Rule
Prev	4.3. Compound ASM Rules	Next

	Description
	The forall rule collects all variable bindings fulfilling a condition (universal condition) by selecting elements from the model space (or from an ASM function), and then executes its body (one by one) for each of these variable bindings.

	Syntax
ForalleRuleAST ::= forall ConstrainedVariablesOptAST with ConditionAST do AsmRuleAST ConditionAST ::= LogicalTermAST \| GTRuleCallAST The forall rule consists of (scoped) variable declarations, a condition part (with clause), and an ASM rule invocation as body. Quantified variables of the forall rule may only appear in the condition part in a graph pattern call, a GT rule call or an ASM function location.

Syntax

ForalleRuleAST ::= forall ConstrainedVariablesOptAST with ConditionAST do AsmRuleAST
ConditionAST ::= LogicalTermAST
               | GTRuleCallAST

The forall rule consists of (scoped) variable declarations, a condition part (with clause), and an ASM rule invocation as body.

Quantified variables of the forall rule may only appear in the condition part in a graph pattern call, a GT rule call or an ASM function location.

Semantics

	Semantics
The forall rule finds all substitution of variables defined in its head which satisfies a boolean condition, and then executes the body rule for each substitution separately. Note that the execution semantics of a forall rule is not fully parallel. In the first phase, each variable binding is calculated (typically, by pattern matching). As the next step, the body of the rule is executed for each binding, but side effects can be accumulated for external variables (see Example 2.7, “Counting with a forall rule”). If no variable substitutions satisfy the condition, then the forall rule is still successful and the execution continues, but nothing is changed. In contrast to the iterate rule, termination is normally not a critical issue when using the forall rule, which first collects all available matchings, and then applies the rule for all of them in a single (most frequently determinstic) step. However, if different matchings of a GT rule are overlapping, parallel rule application may result in conflicts when conflicting operations are issued on a model element (e.g. delete vs. preserve). currently does not provide support for detecting such conflicts, thus it is the role of the transformation designer to assure that a GT rule applied in forall rule is not conflicting with itself. A forall rule can be used in three ways: In the first form, the body ASM rule is executed for all matches of a given graph pattern serving as the condition. In the second one, a graph transformation rule is executed for all possible matches of its precondition pattern and the body ASM rule is then executed. In the third form, body ASM rule is executed for all (combination of) variable substitutions that satisfy the condition logical term. In such a case, only those variables are substituted which are used as locations to access ASM functions. Naturally, only those locations are enumerated which stores a value other than undef. An example for this third case is given in Example 2.9, “Forall rule used in the context of ASM functions”. The location in the containment hierarchy of each variable in the constrained variable list can be restricted to a specific container entity, or to a specific part of the model space. With the use of the `in`clause users can specify a container whereof the values of the variables can be taken from. Similarly, the `below` clause means that the values of the variables must be taken from the model tree below the given container. If the forall rule is used with GT rule call then the quantified variables have to be output parameters of the GT rule, and input parameters of its precondition pattern, Variables not quantified explicitly by the forall rule, and passed to the pattern matcher with a specific value (either in a GT rule call or in a graph pattern call) are input parameters for the pattern matcher. Variables not quantified explicitly by the forall rule, and passed to pattern matching with an undef value (either in a GT rule call or in a graph pattern call) cause a run-time exception. When a forall rule is executed

The forall rule finds all substitution of variables defined in its head which satisfies a boolean condition, and then executes the body rule for each substitution separately. Note that the execution semantics of a forall rule is not fully parallel.

In the first phase, each variable binding is calculated (typically, by pattern matching).
As the next step, the body of the rule is executed for each binding, but side effects can be accumulated for external variables (see Example 2.7, “Counting with a forall rule”).

If no variable substitutions satisfy the condition, then the forall rule is still successful and the execution continues, but nothing is changed.

In contrast to the iterate rule, termination is normally not a critical issue when using the forall rule, which first collects all available matchings, and then applies the rule for all of them in a single (most frequently determinstic) step.

However, if different matchings of a GT rule are overlapping, parallel rule application may result in conflicts when conflicting operations are issued on a model element (e.g. delete vs. preserve). currently does not provide support for detecting such conflicts, thus it is the role of the transformation designer to assure that a GT rule applied in forall rule is not conflicting with itself.

A forall rule can be used in three ways:

In the first form, the body ASM rule is executed for all matches of a given graph pattern serving as the condition.
In the second one, a graph transformation rule is executed for all possible matches of its precondition pattern and the body ASM rule is then executed.
In the third form, body ASM rule is executed for all (combination of) variable substitutions that satisfy the condition logical term. In such a case, only those variables are substituted which are used as locations to access ASM functions. Naturally, only those locations are enumerated which stores a value other than undef. An example for this third case is given in Example 2.9, “Forall rule used in the context of ASM functions”.

The location in the containment hierarchy of each variable in the constrained variable list can be restricted to a specific container entity, or to a specific part of the model space. With the use of the inclause users can specify a container whereof the values of the variables can be taken from. Similarly, the below clause means that the values of the variables must be taken from the model tree below the given container.

If the forall rule is used with GT rule call then the quantified variables have to be

output parameters of the GT rule, and
input parameters of its precondition pattern,

Variables not quantified explicitly by the forall rule, and passed to the pattern matcher with a specific value (either in a GT rule call or in a graph pattern call) are input parameters for the pattern matcher.

Variables not quantified explicitly by the forall rule, and passed to pattern matching with an undef value (either in a GT rule call or in a graph pattern call) cause a run-time exception.

When a forall rule is executed

	Constraints
	In the constrained variable list only entities can be constrained. If a containment constraint is applied to a relation, it causes a runtime error.

	Warning
	The evaluation of forall rules for variables ranging over the indices of ASM functions is not optimized, and it can be very slow for complex expressions like in Example 2.9, “Forall rule used in the context of ASM functions”.

Remark. Note that in a typical model transformation, the forall rule and the choose rule will drive the execution of elementary graph transformation rules. In this respect, wherever a Boolean condition is expected, we may use a graph pattern as condition, and wherever an ASM rule is executed, we may apply a GT rule.

Example 2.6. Different invocations of a forall rule

// Invoking a graph pattern
pattern myPattern(X) = { ... }
forall Y with find myPatt(Y) do println(fqn(Y));

// Invoking a graph transformation rule
gtrule myGtRule(out X) = { ... }
forall Y with find myGtRule(Y) do println(fqn(Y));

// Invoking a logical term with an ASM function (INEFFICIENT) 
asmfunction myAsmFun/1 = { ... }
forall Y with myAsmFun(Y) > 2 do println(Y);

Example 2.7. Counting with a forall rule

let N=0 in seq {
  forall Y with find myPatt(Y) do 
    update N = N+1;
  println("Number of matches: " + N);
}

Example 2.8. Quantification of unbound variables passed to a forall rule

The following example

let X=undef in 
forall Y with find myPatt(X,Y) do ...

causes a run-time exception since X is not an input parameter.

Example 2.9. Forall rule used in the context of ASM functions

asmfunction adderFun / 2 = { (1,2) = 3; (0,1) = 1; (2,3) = 5;  }
forall X,Y with adderFun(adderFun(X, Y), Z) > 2 do print(X + Y + Z);

This enumerates all triples X, Y, Z, where adderFun is defined for X, Y, and adderFun is also defined for the result of adderFun(X,Y) and Z. In our example, this retrieves: X = 0, Y = 1, Z = 2.

Defined In: compound rule

See Also: choose rule, iterate rule

Prev	Up	Next
4.3.6. Choose Rule	Home	4.3.8. Iterate Rule