4.3.6. Choose Rule

4.3.6. Choose Rule
Prev	4.3. Compound ASM Rules	Next

	Description
	The choose rule binds its variables to non-deterministically selected elements from the model space (or from an ASM function) fulfilling a condition (existential condition), and then executes its body with those variable bindings.

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

Syntax

ChooseRuleAST ::= choose ConstrainedVariablesOptAST with ConditionAST do AsmRuleAST
ConditionAST ::= LogicalTermAST
               | GTRuleCallAST

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

Quantified variables of the choose 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 choose rule tries to find one substitution of variables defined in its head, which satisfies a boolean condition, and then the body rule is executed. If more variable substitutions satisfy the condition, then one is chosen non-deterministically. If there are no such substitutions then the choose rule fails. The body ASM rule may use the head variables of the choose construct. For a combination of values in the variables that make the formula true, the rule is executed. The location in the containment hierarchy of each variable in the constrained variable list can be narrowed to a specific container entity, or to a specific subtree of the model space. With the use of the `in` clause users can specify the direct parent which the values of the variables can be taken from. The `below` clause means that the values of the corresponding variable have to be taken from the model subtree below the given container. If the choose 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 choose 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 choose rule, and passed to pattern matching with an undef value (either in a GT rule call or in a graph pattern call) are always existentially quantified implicitly.

The choose rule tries to find one substitution of variables defined in its head, which satisfies a boolean condition, and then the body rule is executed. If more variable substitutions satisfy the condition, then one is chosen non-deterministically. If there are no such substitutions then the choose rule fails. The body ASM rule may use the head variables of the choose construct.

For a combination of values in the variables that make the formula true, the rule is executed.

The location in the containment hierarchy of each variable in the constrained variable list can be narrowed to a specific container entity, or to a specific subtree of the model space. With the use of the in clause users can specify the direct parent which the values of the variables can be taken from. The below clause means that the values of the corresponding variable have to be taken from the model subtree below the given container.

If the choose 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 choose 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 choose rule, and passed to pattern matching with an undef value (either in a GT rule call or in a graph pattern call) are always existentially quantified implicitly.

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

	Warning
	The choose rule is evaluated efficiently when the condition (with clause) is either a graph pattern call, or a GT rule call. Evaluating complex logical expressions with ASM function invocations can be highly inefficient. The intended use is to include attribute and other arithmetic constraints as part of a check condition of a graph pattern, where it is evaluated more efficiently.

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.4. Different invocations of a choose rule

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

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

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

Example 2.5. Quantification of variables passed to a choose rule

let X=uml.mymodel in 
choose Y with find myPatt(X,Y) do ...

In this case, X is an input variable.

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

causes a run-time exception as X is unbound.

Defined In: compound rule

See Also: forall rule

Prev	Up	Next
4.3.5. Let Rule	Home	4.3.7. Forall Rule