Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 154) +++ /reasoner/consTranslation.tex (revision 155) @@ -260,9 +260,10 @@ For the first pattern, we consider all declared and used element types in the actual container value of the container variable $v$ and create for each constraint implied by these types an all-quantified constraint over $v$. In more details, let $t$ be a declared or used element type in $v$, then we can quantify all container elements (or at least a subset of type $t$) through a quantor iterator variable $x$ of type $t$ and apply all constraints for $t$ by instantiating the constraints for $x$, i.e., qualifying all used slots with respect to $x$ and replacing \IVML{self}. Although indivdual constraints may appear superfluous, they are needed to provide detailed error messages and also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, in IVML we must flatten the container, i.e., remove all nested containers, to apply the constraints to all individual elements. As mentioned above, if $\subTypeOf{t}{T}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by the function $f(v, t)$. -Basically, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects if needed to enable access to slots defined in refined compounds. Therefore, $f(v, t)$ uses the IMVL container operations \IVML{flatten} and \IVML{selectByKind}. Let $e$ be a container access expression, e.g., $e=\createExpression{decl(v)}$. If $e$ is of a nested container type, we apply the \IVML{flatten} operation to extract all element values from all nested containers into one top-level container, i.e., enable access even to deeply nested container elements. We apply the \IVML{selectByKind} operation if $t$ is a subtype of the element type of the container, as otherwise slots defined on the specific type $t$ are not accessible. Finally, as shown in the transformation pattern, we apply an all-quantor over the elements of the (projected) collection using the temporary iterator variable $x$ to the respective constraint $c$ after appropriate variable substitution, in particular to \IVMLself{} by $x$. -% -\begin{displaymath} -e\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(e)}}\IVML{forAll}(x:c(x)) -\end{displaymath} +Basically, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects if needed to enable access to slots defined in refined compounds. Therefore, $f(v, t)$ uses the IMVL container operations \IVML{flatten} and \IVML{selectByKind}. Let $ca$ be a container access expression, e.g., $ca=\createExpression{decl(v)}$. If $ca$ is of a nested container type, we apply the \IVML{flatten} operation to extract all element values from all nested containers into one top-level container, i.e., enable access even to deeply nested container elements. We apply the \IVML{selectByKind} operation if $t$ is a subtype of the element type of the container, as otherwise slots defined on the specific type $t$ are not accessible. Finally, as shown in the transformation pattern, we apply an all-quantor over the elements of the (projected) collection using the temporary iterator variable $x$ to the respective constraint $c$ after appropriate variable substitution, in particular to \IVMLself{} by $x$. +% +\begin{equation} +ca\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(e)}}\IVML{forAll}(x:c(x)) +\label{fSimpleContainerQuantorPrefix} +\end{equation} % Algorithm \ref{algTranslateContainerDeclaration} translates a container variable declaration. The core idea of this algorithm is to determine the used types for all container elements and for each type to instantiate the constraints as explained above. However, used types are only availabe if a container value has been assigned. If no container value is available, we resort to the static type of the declaration of the container variable. During constraint translation, we distinguish between constraint containers, for which we directly turn the values into constraints, and container types that may imply further constraints such as containers over compounds or containers over derived types. @@ -307,5 +308,4 @@ Algorithm \ref{algTranslateCompoundContainer} first checks in line \ref{algTranslateCompoundContainerAlreadyProcessed} whether type $t$ has already been translated within this container, i.e., in the scope of the actual context frame pushed in line \ref{algTranslateContainerDeclarationPushContext} of Algorithm \ref{algTranslateContainerDeclaration}. Translating the same type for the same container elements multiple times leads to a repeated evaluation of the constraints of that type, i.e., an increased reasoning time and, if the evaluation fails, to (accidentally) repeated error messages, e.g., for unintended variable re-assignments. Moreover, checking whether $t$ has already been processed in the same container also solves the problem that if $t$ is used as a slot type of a nested compound / as an element type in a nested container, processing it by a recursion of Algorithms \ref{algTranslateCompoundContainer}, \ref{algTranslateContainerDeclaration}, \ref{algTranslateCompoundContent} and \ref{algTranslateDeclaration} may cause an endless cycle. - \begin{algorithm}[H] \SetAlgoLined @@ -313,55 +313,59 @@ \KwData{variable mapping $\variableMapping$} - \If{$\neg alreadyProcessed(\variableMapping, t)$}{\label{algTranslateCompoundContainerAlreadyProcessed} - $recordProcessed(\variableMapping, t)$\; - - $l\assng \createExpression{\IVMLMeta{var}(t)}$\; - - $e\assng\closedCases{ca, & \text{if } ca \neq \undef\\\createExpression{d}, &\text{else}}$\; \label{algTranslateDefaultsCompoundContainerInitE} + \If{$\neg alreadyProcessed(\variableMapping, t)$}{ \label{algTranslateCompoundContainerAlreadyProcessed} + $recordProcessed(\variableMapping, t)$\; \label{algTranslateCompoundContainerMarkProcessed} + + $l\assng \createExpression{\IVMLMeta{var}(t)}$\; \label{algTranslateCompoundContainerIterator} + + $e\assng\closedCases{ca, & \text{if } ca \neq \undef\\\createExpression{d}, &\text{else}}$\; \label{algTranslateCompoundContainerInitE} \uIf{$isSequence(type(d))$} { - $e\assng\createExpression{\IVML{asSet}(e)}$\; \label{algTranslateDefaultsCompoundContainerAsSet} + $e\assng\createExpression{\IVML{asSet}(e)}$\; \label{algTranslateCompoundContainerAsSet} } \uIf{$isNested(type(d))$} { - $e\assng\createExpression{\IVML{flatten}(e)}$\; \label{algTranslateDefaultsCompoundContainerFlatten} + $e\assng\createExpression{\IVML{flatten}(e)}$\; \label{algTranslateCompoundContainerFlatten} } \uIf{$t \neq t_d$} { - $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateDefaultsCompoundContainerCast} + $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateCompoundContainerCast} } - $pushContext(\variableMapping, \undef, e, l, true)$\; - $registerCompoundMapping(t, l, d)$\; \label{algTranslateDefaultsCompoundContainerMapping} + $pushContext(\variableMapping, \undef, e, l, true)$\; \label{algTranslateCompoundPushContext} + $registerCompoundMapping(t, l, d)$\; \label{algTranslateCompoundContainerMapping} - $translateCompoundContent(l, \undef, t, \closedCases{\undef, & \text{if } ca = \undef\\l & \text{else}})$\; \label{algTranslateDefaultsCompoundContainerContent} - $popContext()$\; +% $translateCompoundContent(l, \undef, t, \closedCases{\undef, & \text{if } ca = \undef\\l & \text{else}})$\; \label{algTranslateCompoundContainerContent} + $translateCompoundContent(l, \undef, t, l)$\; \label{algTranslateCompoundContainerContent} + $popContext()$\; \label{algTranslateCompoundContainerPopContext} } \caption{Translating constraints for compound containers (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} \end{algorithm} -Initially, we a local variable $l$ as later iterator variable for the quantifier expressions. Then, we create a prefix expression $e$ of the quantor constraint expression, i.e., we determine in line \ref{algTranslateDefaultsCompoundContainerInitE} the access expression to the collection either using $ca$ or just holding the variable of the container $d$. If the container is a sequence that may contain duplicates, we first turn it into a set to avoid accidentally duplicated constraints (line \ref{algTranslateDefaultsCompoundContainerFlatten}). If the container is nested, we flatten it in line \ref{algTranslateDefaultsCompoundContainerFlatten} as constraints only need to be created for the elements (no specific constraints can be attached to a container type except for derived values, which are handled by Algorithm \ref{algTranslateDeclaration}). If the actual type $t$ is not the same as the type of the declaration $u)$, we must consider that the slot $s$ only exists for the specific refined type $t$. Then, the instantiation shall apply only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by projecting the container to all elements of type $t$ (and refined types). - -%from above - - -Now we create a context for the container on the stack of $\variableMapping$. In contrast to compound translations, we also register the prefix expression $e$ and the iterator variable $l$. This will be taken up by the $add$ operation, which completes the full constraint from the given information on the stack, i.e., the full creation of the constraint is prepared but not shown in Algorithm \ref{algRegisterCompoundMapping}. As for compounds, we create now the compound mapping using Algorithm \ref{algRegisterCompoundMapping}. Please note that slot access now happens via the iterator variable $l$, while annotation access happens through $ca$. Specifying $t$ also as target type avoids unnecessary type casts here. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots, implying translation of annotations as well as recursion over further compounds and containers. Thereby, we replace a given access expression by the iterator variable $l$ or leave the access undefined as it is implicity given in and used from the actual context. - -By storing constraint information on the stack of $\variableMapping$ and assembling the information in one place, we can even handle recursive compound containers, which leads to a recursive creation of constraints. The formula below indicates the constraint that we must create in case of a compound container nested into a compound container. -% -\begin{displaymath} +If type $t$ has not already been processed in the current context frame, line \ref{algTranslateCompoundContainerMarkProcessed} marks the type as processed. For incrementally building up the quantification prefix expression for the current context, Algorithm \ref{algTranslateCompoundContainer} creates a local variable $l$ as iterator for the all-quantifier in line \ref{algTranslateCompoundContainerIterator}. Then, the algorithm derives the collection accessor expression in line \ref{algTranslateCompoundContainerInitE}, either using $ca$ if given (in particular for nested containers) or the container variable declaration $d$ (in particular for top-level containers). + +For realizing $f(v, t)$, i.e., for deciding whether the container is nested or a sequence, the declared container type $type(d)$ is relevant. If the container is a sequence that may contain duplicates, we convert the container into a set to avoid accidentally duplicated constraints (line \ref{algTranslateCompoundContainerAsSet}). If the container is nested, we flatten it in line \ref{algTranslateCompoundContainerFlatten} to apply the constraints to the deepest container elements as explained above. If the actual element type $t$ is not the same as the declared element type $t_d$, we must apply type selection / conversion in line \ref{algTranslateCompoundContainerCast} to make slots defined on the specific type accessible. + +Akin to the translation of compounds in Algorithm \ref{algTranslateCompoundDeclaration}, the algorithm creates in line \ref{algTranslateCompoundPushContext} a context frame (always linked to the parent container frame) for the following compound transformation. As mentioned above, the algorithm stores in the new context frame the incrementally build-up quantification information, i.e., the iterator variable $l$ and the quantification prefix $e$ (without actual quantifier). This information is needed for creation of a potentially nested quantification for nested containers when adding individual constraints within this context frame. As for compounds, the algorithm creates in line \ref{algTranslateCompoundContainerMapping} the mapping using Algorithm \ref{algRegisterCompoundMapping}, the iterator variable $l$ as access expression and the actual type $t$ to avoid unnecessary type casts. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots also using the quantor iterator $l$ as access expression. As mentioned above, calling Algorithm \ref{algTranslateCompoundContent} implies a potential recursion over nested compounds and containers. Finally, the algorithm pops in line \ref{algTranslateCompoundContainerPopContext} the context frame created for the compound transformation. + +So far, we focused on the translation algorithm rather than the creation of the quantification prefix expressions also for nested container structures. Although the actual creation happens when adding constraints to the constaint base, i.e., in the $add$ function (cf. Algorithm \ref{algAddConstraint} in Section \ref{sectContainerBase}), we explain the approach and the required function for the variable mapping $\variableMapping$ in this section. The base case was already explained above in Formula \ref{fSimpleContainerQuantorPrefix} and requires after the creation of the prefix expression in Algorithm \ref{algTranslateCompoundContainer} just the addition of an all-quantor over $l$ and a constraint using $l$ as access expression. We derive the respective algorithm from the expression for a nested compound container such as \IVML{setOf(C)} over a compound type \IVML{C}, which, in turn, declares a slot \IVML{s} of some compound container. The derived quantification prefix is illustrated below by Formula \ref{fNestedContainerQuantorPrefix}. As the creation of a nested prefix expression happens in several recursive calls of Algorithm \ref{algTranslateCompoundContainer}, we indicate in Formula \ref{fNestedContainerQuantorPrefix} the recursion level and the respective parameter / variable from Algorithm \ref{algTranslateCompoundContainer} below the created partial expression. +% +\begin{equation} \underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}:\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}:c(l_2))) -\end{displaymath} -% -In the first iteration, we start with $ca$ (indicated by $1:ca$, may also be some $d$) and append flatten/typeSelect as needed to form $e$ (indicated by $1:e$, i.e., recursion level and parameter/variable name). In the first iteration, we also create a temporary variable $l$ as iterator variable. We store $l$ and $e$ on the stack of $\variableMapping$ and pass $l$ on as accessor to the translation of compound content in Algorithm \ref{algTranslateCompoundContent}. There, we create an accessor for a slot, let's say $s$, i.e. $l.s$, which is then passed on in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT}, respectively, to the translation of declarations in Algorithm \ref{algTranslateDeclaration}. As a further compound container is nested into the initial compound container, we end up again in Algorithm \ref{algTranslateCompoundContainer}. Now $l.s$ is considered as accessor (indicated by $2:ca$), flatten(typeSelect are added as needed to form $e$ (now $2:e$), which is stored along with the temporary iterator variable $l_2$ on the stack. In this context, we apply the constraint $c$ within an all-quantor (after appropriate variable substitution, in particular \IVMLself{} by $l_2$). The quantor expressions for completing the full constraint are created by the $add$ algorithm (details in Section \ref{sectContainerBase}). - -Let us assume that $stack(\variableMapping)$ returns the contex frames of the stack starting with the top frame, $container(s)$ returns the container expression assigned to context frame $s$ and $iterator(s)$ the iterator variable for $s$. The, Algorithm \ref{algComposeExpression} creates a constraint of the form shown above inside out, starting with $c$ after correct variable substation. For each stack element that has a container (we assume also an iterator variable) assigned, which is not the case for context frames created for compounds, we surround the actual $c$ by an all-quantor, running over $container(s)$ using $iterator(s)$ as iterator variable and $c$ as quantor expression. +\label{fNestedContainerQuantorPrefix} +\end{equation} +% + +In the first iteration, we start with a given collection access $ca$ (indicated as '$1:ca$', typically some declaration $d$). Algorithm \ref{algTranslateCompoundContainer} appends the required IVML operations for $f(v, t)$, i.e., \IVML{asSet}/\IVML{flatten}/\IVML{selectByKind} to form the prefix expression $e$ (indicated as '$1:e$', \IVML{flatten} is used as a representative of a potential combination of algorithms). In the first iteration, we also create a temporary variable $l$ as iterator variable indicated as '$1:l$'). We store $l$ and $e$ in a new context frame on $\variableMapping$ and pass $l$ on as accessor to the creation of the compound mapping in Algorithm \ref{algRegisterCompoundMapping}. + +In Algorithm \ref{algRegisterCompoundMapping}, we create an accessor expression for the compound container slot $s$, i.e., $l.s$, which is then passed on to the translation of declarations in Algorithm \ref{algTranslateCompoundContent} and \ref{algTranslateDeclaration}, respectively. As $s$ is a compound container, we execute Algorithm \ref{algTranslateCompoundContainer} recursively. Now $l.s$ is passed in as accessor (indicated as '$2:ca$'), IVML operations are added for $f(v, t)$ as needed to form $e$ (now '$2:e$'), which is stored in a new context frame along with the temporary iterator variable created in step '$2:l$' (named here $l_2$). In Algorithm \ref{algRegisterCompoundMapping} we create the respective compound mapping based on $l_2$ for the slots. In Algorithm \ref{algTranslateCompoundContainer} we translate some constraint $c$ for the actual type, i.e., we perform a variable substitution to replace the actual variable mapping and, in particular, \IVMLself{} by $l_2$. + +When adding $c$ to the constraint base, we must prefix the already translated $c$ (including the currently unbound iterator variable) with the whole quantification expression stored in the two containing (compound container) context frames. Algorithm \ref{algComposeExpression} composes this prefix expression and adds the respective quantification operations. Therefore, Algorithm \ref{algComposeExpression} traverses the stack in top-down manner, starting with the innermost nested context frame and incrementally processes then the outer frames. Let $stack(\variableMapping)$ return the sequence of context frames of the stack starting with the top frame. Further, let $container(f)$ return the container expression and $iterator(f)$ the iterator variable for context frame $f$. Then, Algorithm \ref{algComposeExpression} creates a constraint of the form shown in Formula \ref{fNestedContainerQuantorPrefix} in inside out fashion, starting with the given constraint $c$, which is supposed to be added to the constraint base. $c$ changes for each processed stack frame requiring quantiation. For each stack frame having a container (we assume then also an iterator variable) assigned, which is not the case for context frames created for compounds, we surround the actual constraint $c$ with an all-quantor over $container(f)$ using $iterator(f)$ as iterator variable and $c$ as quantized expression. \begin{algorithm}[H] \SetAlgoLined \KwIn{constraint $c$} - \KwOut{composed constraint $c$} + \KwOut{completed constraint $c$} \KwData{variable mapping $\variableMapping$} - \ForAll{$s \iterAssng stack(\variableMapping)$} { - \If{$container(s) \neq \undef$} { - $c \assng \createExpression{container(s)\rightarrow\IVML{forAll}(iterator(s):c)}$\; + \ForAll{$f \iterAssng stack(\variableMapping)$} { + \If{$container(f) \neq \undef$} { + $c \assng \createExpression{container(f)\rightarrow\IVML{forAll}(iterator(f):c)}$\; } } @@ -370,5 +374,5 @@ \end{algorithm} -Utilizing quantor constraints here implies that default initializations, which remain undefined if some dependent variables have not been determined so far, cause a re-evaluation for all elements of the container. Here, unfolding the implicit loop of such a quantor may be a solution, as then only individual constraints are triggered. However, this only works for sequences, as sets do not provide element-wise/index-based access and unfolding the constraint for a large container also may create a huge number of constraints. Currently, we stay with the compromise of creating a single quantized constraint for all slots with default values. +Along with the translation, also assignment constraints for default values of compound slots are created by recursions over Algorithm \ref{algTranslateDeclaration} and quantized. Relying on quantor constraints here implies that default initializations, which remain unevaluated as some dependent variables have not been determined so far, cause a re-evaluation for all elements of the container (still prohibiting in-consisting re-assignments in the same project scope). Here, unfolding the loop of a quantor may be more efficient, as then only so far undefined constraints are evaluated. However, this only would currently work only for sequences, as sets do not provide element-wise/index-based access. Moreover, unfolding constraints for a large container may create a huge number of constraints and increase the management effort for constraint re-scheduling upon value changes. Currently, we stay with the compromise of creating a single quantized constraint even for default values assignments. \subsection{Annotations}\label{sectAnnotationDefaults}