| <html><head><META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"><title>4.3.7. Forall Rule</title><link href="style.css" rel="stylesheet" type="text/css"><meta content="DocBook XSL Stylesheets V1.72.0" name="generator"><link rel="start" href="index.html" title="The VIATRA2 Model Transformation Framework"><link rel="up" href="sec_ASMCompoundRules.html" title="4.3. Compound ASM Rules"><link rel="prev" href="def_ChooseRule.html" title="4.3.6. Choose Rule"><link rel="next" href="def_IterateRule.html" title="4.3.8. Iterate Rule"></head><body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF"><div class="navheader"><table summary="Navigation header" width="100%"><tr><th align="center" colspan="3">4.3.7. Forall Rule</th></tr><tr><td align="left" width="20%"><a accesskey="p" href="def_ChooseRule.html">Prev</a> </td><th align="center" width="60%">4.3. Compound ASM Rules</th><td align="right" width="20%"> <a accesskey="n" href="def_IterateRule.html">Next</a></td></tr></table><hr></div><div class="sect3" lang="en"><div class="titlepage"><div><div><h4 class="title"><a name="def_ForallRule"></a>4.3.7. Forall Rule</h4></div></div></div><div class="tip" style="margin-left: 0.5in; margin-right: 0.5in;"><table border="0" summary="Tip: Description"><tr><td valign="top" align="center" rowspan="2" width="25"><img alt="[Tip]" src="images/tip.png"></td><th align="left"><a name="def_ForallRule_Description"></a>Description</th></tr><tr><td valign="top" align="left"><p> | |
| The <span class="strong"><strong>forall rule</strong></span><a name="N11814" class="indexterm"></a> | |
| 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. | |
| </p></td></tr></table></div><div class="important" style="margin-left: 0.5in; margin-right: 0.5in;"><table border="0" summary="Important: Syntax"><tr><td valign="top" align="center" rowspan="2" width="25"><img alt="[Important]" src="images/important.png"></td><th align="left"><a name="def_ForallRule_Syntax"></a>Syntax</th></tr><tr><td valign="top" align="left"><pre class="programlisting"> | |
| ForalleRuleAST ::= <span class="token">forall</span> <a href="def_ConstrainedVariableList.html" title="5.8.4. Constrained Variable List">ConstrainedVariablesOptAST</a> <span class="token">with</span> ConditionAST <span class="token">do</span> <a href="def_AsmRuleInvoc.html" title="4.1.2. ASM Rule Invocation">AsmRuleAST</a> | |
| ConditionAST ::= <a href="def_LogicalTerm.html" title="5.2.1. Logical Term">LogicalTermAST</a> | |
| | <a href="def_GTRuleCall.html" title="3.4.1. GTRule Call">GTRuleCallAST</a> | |
| </pre><p> | |
| The <span class="strong"><strong>forall rule</strong></span> consists of (scoped) variable | |
| declarations, a condition part (<span class="emphasis"><em>with </em></span>clause), and an <a href="def_AsmRuleInvoc.html" title="4.1.2. ASM Rule Invocation">ASM rule invocation</a> as body. | |
| </p><p> | |
| Quantified variables of the <span class="strong"><strong>forall rule</strong></span> may only appear in the condition part in | |
| a <a href="def_GraphPatternCall.html" title="2.1.4. Graph Pattern Call">graph pattern call</a>, a <a href="def_GTRuleCall.html" title="3.4.1. GTRule Call">GT rule call</a> or | |
| an <a href="def_AsmFunctionLocation.html" title="5.5.3. ASM Function Location">ASM function location</a>. | |
| </p></td></tr></table></div><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><table border="0" summary="Note: Semantics"><tr><td valign="top" align="center" rowspan="2" width="25"><img alt="[Note]" src="images/note.png"></td><th align="left"><a name="def_ForallRule_Semantics"></a>Semantics</th></tr><tr><td valign="top" align="left"><p> | |
| The <span class="strong"><strong>forall rule</strong></span> 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 <span class="strong"><strong>forall rule</strong></span> | |
| is not fully parallel. | |
| <div class="itemizedlist"><ul type="disc"><li><p> | |
| In the first phase, each variable binding is calculated (typically, by pattern matching). | |
| </p></li><li><p> | |
| As the next step, the body of the rule is executed for each binding, but side effects can be accumulated for external variables | |
| (see <a href="def_ForallRule.html#def_ForallRule_Example2" title="Example 2.7. Counting with a forall rule">Example 2.7, “Counting with a forall rule”</a>). | |
| </p></li></ul></div> | |
| </p><p> | |
| If no variable substitutions satisfy the condition, then the | |
| <span class="strong"><strong>forall rule</strong></span> is still successful and the execution continues, | |
| but nothing is changed. | |
| </p><p> | |
| In contrast to the <a href="def_IterateRule.html" title="4.3.8. Iterate Rule">iterate rule</a>, termination is normally | |
| not a critical issue when using the <span class="strong"><strong>forall rule</strong></span>, which first | |
| collects all available matchings, and then applies the rule for all of them | |
| in a single (most frequently determinstic) step. | |
| </p><p> | |
| 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 | |
| <span class="strong"><strong>forall rule</strong></span> is not conflicting with itself. | |
| </p><p> | |
| A <span class="strong"><strong>forall rule</strong></span> can be used in three ways: | |
| <div class="itemizedlist"><ul type="disc"><li><p> | |
| In the first form, the body <a href="def_AsmRuleInvoc.html" title="4.1.2. ASM Rule Invocation">ASM rule</a> is executed for | |
| all matches of a given <a href="def_GraphPatternCall.html" title="2.1.4. Graph Pattern Call">graph pattern</a> serving as the condition. | |
| </p></li><li><p> | |
| In the second one, a <a href="def_GTRuleCall.html" title="3.4.1. GTRule Call">graph transformation rule</a> is | |
| executed for all possible matches of its precondition pattern and the body | |
| <a href="def_AsmRuleInvoc.html" title="4.1.2. ASM Rule Invocation">ASM rule</a> is then executed. | |
| </p></li><li><p> | |
| In the third form, body <a href="def_AsmRuleInvoc.html" title="4.1.2. ASM Rule Invocation">ASM rule</a> is executed for all (combination of) variable | |
| substitutions that satisfy the condition <a href="def_LogicalTerm.html" title="5.2.1. Logical Term">logical term</a>. In such a case, | |
| only those variables are substituted which are used as locations to | |
| access <a href="def_AsmFunctionLocation.html" title="5.5.3. ASM Function Location">ASM functions</a>. Naturally, | |
| only those locations are enumerated which stores a value other than <a href="">undef</a>. | |
| An example for this third case is given in <a href="def_ForallRule.html#def_ForallRule_Example4" title="Example 2.9. Forall rule used in the context of ASM functions">Example 2.9, “Forall rule used in the context of ASM functions”</a>. | |
| </p></li></ul></div> | |
| </p><p> | |
| The location in the containment hierarchy of each variable in the | |
| <a href="def_ConstrainedVariableList.html" title="5.8.4. Constrained Variable List">constrained variable list</a> can be restricted to a specific | |
| <span class="emphasis"><em>container entity</em></span>, or to a specific part of the model space. With the | |
| use of the <code class="computeroutput">in</code>clause users can specify a container whereof the | |
| values of the variables can be taken from. Similarly, the <code class="computeroutput">below</code> | |
| clause means that the values of the variables must be taken from the model | |
| tree below the given container. | |
| </p><p> | |
| If the <span class="strong"><strong>forall rule</strong></span> is used with <a href="def_GTRuleCall.html" title="3.4.1. GTRule Call">GT rule call</a> | |
| then the quantified variables have to be | |
| <div class="itemizedlist"><ul type="disc"><li><p>output parameters of the <a href="def_GTRuleDef.html" title="3.1.1. Graph Transformation Rule Definition">GT rule</a>, and | |
| </p></li><li><p>input parameters of its <span class="emphasis"><em>precondition </em></span> <a href="def_GraphPatternDef.html" title="2.1.1. Graph Pattern Definition">pattern</a>, | |
| </p></li></ul></div> | |
| </p><p> | |
| Variables not quantified explicitly by the <span class="strong"><strong>forall rule</strong></span>, and | |
| passed to the pattern matcher with a specific value (either in a | |
| <a href="def_GTRuleCall.html" title="3.4.1. GTRule Call">GT rule call</a> or in a <a href="def_GraphPatternCall.html" title="2.1.4. Graph Pattern Call">graph pattern call</a>) are | |
| input parameters for the pattern matcher. | |
| </p><p> | |
| Variables not quantified explicitly by the <span class="strong"><strong>forall rule</strong></span>, and | |
| passed to pattern matching with an <span class="strong"><strong>undef</strong></span> value (either in a | |
| <a href="def_GTRuleCall.html" title="3.4.1. GTRule Call">GT rule call</a> or in a <a href="def_GraphPatternCall.html" title="2.1.4. Graph Pattern Call">graph pattern call</a>) | |
| cause a run-time exception. | |
| </p><p> | |
| When a <span class="strong"><strong>forall rule</strong></span> is executed | |
| </p></td></tr></table></div><div class="caution" style="margin-left: 0.5in; margin-right: 0.5in;"><table border="0" summary="Caution: Constraints"><tr><td valign="top" align="center" rowspan="2" width="25"><img alt="[Caution]" src="images/caution.png"></td><th align="left"><a name="def_ForallRule_Constraints"></a>Constraints</th></tr><tr><td valign="top" align="left"><p> | |
| In the <a href="def_ConstrainedVariableList.html" title="5.8.4. Constrained Variable List">constrained variable list</a> only entities can be constrained. | |
| If a containment constraint is applied to a relation, it causes a runtime error. | |
| </p></td></tr></table></div><div class="warning" style="margin-left: 0.5in; margin-right: 0.5in;"><table border="0" summary="Warning: Warning"><tr><td valign="top" align="center" rowspan="2" width="25"><img alt="[Warning]" src="images/warning.png"></td><th align="left"><a name="def_ForallRule_Warning"></a>Warning</th></tr><tr><td valign="top" align="left"><p> | |
| The evaluation of <span class="strong"><strong>forall rules</strong></span> for variables | |
| ranging over the indices of ASM functions is not optimized, and it can be | |
| very slow for complex expressions like in <a href="def_ForallRule.html#def_ForallRule_Example4" title="Example 2.9. Forall rule used in the context of ASM functions">Example 2.9, “Forall rule used in the context of ASM functions”</a>. | |
| </p></td></tr></table></div><div class="highlights"><a name="def_ForallRule_Remark"></a><p><b>Remark. </b> | |
| Note that in a typical model transformation, the <span class="strong"><strong>forall rule</strong></span> | |
| and the <a href="def_ChooseRule.html" title="4.3.6. Choose Rule">choose rule</a> 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. | |
| </p></div><div class="example"><a name="def_ForallRule_Example1"></a><p class="title"><b>Example 2.6. Different invocations of a forall rule</b></p><div class="example-contents"><pre class="programlisting"> | |
| // 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); | |
| </pre></div><p></p></div><br class="example-break"><div class="example"><a name="def_ForallRule_Example2"></a><p class="title"><b>Example 2.7. Counting with a forall rule</b></p><div class="example-contents"><pre class="programlisting"> | |
| let N=0 in seq { | |
| forall Y with find myPatt(Y) do | |
| update N = N+1; | |
| println("Number of matches: " + N); | |
| } | |
| </pre></div><p></p></div><br class="example-break"><div class="example"><a name="def_ForallRule_Example3"></a><p class="title"><b>Example 2.8. Quantification of unbound variables passed to a forall rule</b></p><div class="example-contents"><p> | |
| The following example | |
| </p><pre class="programlisting"> | |
| let X=undef in | |
| forall Y with find myPatt(X,Y) do ... | |
| </pre><p> | |
| causes a run-time exception since X is not an input parameter. | |
| </p></div><p></p></div><br class="example-break"><div class="example"><a name="def_ForallRule_Example4"></a><p class="title"><b>Example 2.9. Forall rule used in the context of ASM functions</b></p><div class="example-contents"><pre class="programlisting"> | |
| 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); | |
| </pre><p> | |
| This enumerates all triples <code class="computeroutput">X, Y, Z</code>, | |
| where <code class="computeroutput">adderFun</code> is defined for <code class="computeroutput">X, Y</code>, | |
| and <code class="computeroutput">adderFun</code> is also defined for the result of | |
| <code class="computeroutput">adderFun(X,Y)</code> and <code class="computeroutput">Z</code>. | |
| In our example, this retrieves: <code class="computeroutput">X = 0</code>, | |
| <code class="computeroutput">Y = 1</code>, <code class="computeroutput">Z = 2</code>. | |
| </p></div><p></p></div><br class="example-break"><div class="highlights"><a name="def_ForallRule_DefinedIn"></a><p><b>Defined In: </b> | |
| <a href="def_CompoundRule.html" title="4.3.1. Compound Rule">compound rule</a> | |
| </p></div><div class="highlights"><a name="def_ForallRule_SeeAlso"></a><p><b>See Also: </b> | |
| <a href="def_ChooseRule.html" title="4.3.6. Choose Rule">choose rule</a>, <a href="def_IterateRule.html" title="4.3.8. Iterate Rule">iterate rule</a> | |
| </p></div></div><div class="navfooter"><hr><table summary="Navigation footer" width="100%"><tr><td align="left" width="40%"><a accesskey="p" href="def_ChooseRule.html">Prev</a> </td><td align="center" width="20%"><a accesskey="u" href="sec_ASMCompoundRules.html">Up</a></td><td align="right" width="40%"> <a accesskey="n" href="def_IterateRule.html">Next</a></td></tr><tr><td valign="top" align="left" width="40%">4.3.6. Choose Rule </td><td align="center" width="20%"><a accesskey="h" href="index.html">Home</a></td><td valign="top" align="right" width="40%"> 4.3.8. Iterate Rule</td></tr></table></div></body></html> |