Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 213) +++ /reasoner/consTranslation.tex (revision 214) @@ -274,5 +274,5 @@ As a generic type, an IVML container variable can declare the contained element type. Moreover, a container differs from other IVML types, as a container can hold an arbitrary number of elements. The element values can be defined through a default value expression, an assignment constraint or respective container operations. However, there is no direct opportunity to define constraints for a container type. Of course, constraints can defined for container variables, but also through a derived type, the contained element type, or the actual type of the individual elements. The actual element type is important, in particular for elements of a container type, as due to type refinement an individual container element may have a more specific type than the element type defined for the container. For the element type, a reference type appears to be transparent, i.e., constraints are imposed by the target type of the reference and basic types do not impose further constraints as no constraints can be defined on them (cf. Section \ref{sectNotationOthers}). -As containers can hold an arbitrary number of elements, specifying a constraint over a container (not an individual element) often involves all-quantification. However, a change of a single element leads to a re-evaluation of quantfied container constraints. As a performance optimization strategy, the constraint translation might internally unroll a container for reasoning over quantified constraints, i.e., create constraints for the individual elements and take care of the changes of the individual element variables. Although potentially more efficient in some cases, unrolling is not possible for all IVML container types, e.g., \IVML{Set}-types do not offer index-based access to the individual elements, i.e., may require transformations into corresponding \IVML{Sequence}-types. So far, to achieve a uniform translation patterns, we apply quantification rather than unrolling. +As containers can hold an arbitrary number of elements, specifying a constraint over a container (not an individual element) often involves all-quantification. However, a change of a single element leads to a re-evaluation of quantfied container constraints. As a performance optimization strategy, the constraint translation might internally unroll a container for reasoning over quantified constraints, i.e., create constraints for the individual elements and take care of the changes of the individual element variables. Although potentially more efficient in some cases, unrolling is not possible for all IVML container types, e.g., \IVML{Set}-types do not offer index-based access to the individual elements, i.e., may require transformations into corresponding \IVML{Sequence}-types. So far, to achieve a uniform translation patterns, which in extreme case requires nested quantification rather than unrolling of (nested) containers. \grayPara{ @@ -284,28 +284,37 @@ There are three basic translation patterns for containers: Pattern \ref{forContainerQuant} considers all used element types in $v$, Pattern \ref{forConstraintContainer} handles containers containing constraints and Pattern \ref{forContainerTop} illustrates the transformation for top-level container variables. \begin{itemize} -\item For each constraint defined for the element types used in the actual value of container $v$, Pattern \ref{forContainerQuant} creates an all-quantified constraint over $v$. Let $t$ be a used element type in $v$. Then we can apply the constraints defined for $t$ by a quantification over all container elements (of type $t$). Let $c(x)$ be a constraint defined for type $t$, i.e., the constraint is expressed over variable $x$ of type $t$. If we want to apply $c(x)$ to all container elements of type $t$, we all-quantify the container and express $c(x)$ over the iterator variable $i$ of type $t$, i.e., substitute in particular $x$ and \IVMLself{} by $i$. However, if $v$ is a nested container, we may have to flatten $v$, i.e., remove all nested containers, to apply the constraint to the individual elements. Further, if $\subTypeOf{t}{T}$, accessing specific compound slots requires type casting / selection on the element values. Whether we need these additional container operations depends on the actual types of $v$ and $t$. We generically represent these operations in Pattern \ref{forContainerQuant} by $f(v, t)$. Although individual quantified constraints may appear superfluous, i.e., we might aim at creating joined quantified expressions for individual types, the individual constraints are needed to provide detailed reasoning error messages. - -\item Constraint containers are containers containing of constraints. The particular transformation required here is to extract all element values, to turn them into constraints and to add them to the constraint base as indicated by Pattern \ref{forConstraintContainer}. If the values in the constraint container change, the constraint re-scheduling must change the constraint base accordingly. As no further constraints can be attached to the constraint type (cf. Section \ref{sectNotationOthers}), Pattern \ref{forContainerQuant} and Pattern \ref{forConstraintContainer} do not need to be combined. - -\item Pattern \ref{forContainerTop} defines the usual translation for top-level constraints over collection variables, i.e., the potential need to substitute top-level variables by the actual access expressions collected in $\variableMapping$. In fact, Pattern \ref{forContainerTop} can be combined with Pattern \ref{forConstraintContainer} or Pattern \ref{forContainerQuant}. +\item Constraints may be defined on the element type of a collection and, thus, implicitly apply to all elements. For each constraint defined for the element types used in the actual value of container $v$, Pattern \ref{forContainerQuant} creates an all-quantified constraint over $v$. Let $t$ be a used element type in $v$. Then we can apply the constraints defined for $t$ by a quantification over all container elements (of type $t$). Let $c(x)$ be a constraint defined for type $t$, i.e., the constraint is expressed over variable $x$ of type $t$. If we want to apply $c(x)$ to all container elements of type $t$, we all-quantify the container and express $c(x)$ over the iterator variable $i$ of type $t$, i.e., substitute in particular $x$ and \IVMLself{} by $i$. However, if $v$ is a nested container, we may have to flatten $v$, i.e., remove all nested containers, to apply the constraint to the individual elements. Further, if $\subTypeOf{t}{T}$, accessing specific compound slots requires type casting / selection on the element values. Whether we need these additional container operations depends on the actual types of $v$ and $t$. We generically represent these operations in Pattern \ref{forContainerQuant} by $f(v, t)$. Although individual quantified constraints may appear superfluous, i.e., we might aim at creating joined quantified expressions for individual types, the individual constraints are needed to provide detailed reasoning error messages. + +\item Constraint containers are containers containing of constraints. The particular transformation required here is to extract all element values, to turn them into constraints and to add them to the constraint base as indicated by Pattern \ref{forConstraintContainer}. If the values in the constraint container change, the constraint re-scheduling must change the constraint base accordingly. + +\item Pattern \ref{forContainerTop} defines the translation for constraints on the container itself, e.g., a size restriction or already quantified constraints over collection variables, e.g., top-level constraints. For these expressions, we just need to consider the actual access expressions in $\variableMapping$. \end{itemize} -We will focus here on Pattern \ref{forContainerQuant}, as Pattern \ref{forContainerTop} is implicitly handled by the translation of top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. First, we detail $f(v,t)$ in Section \ref{sectAdjContainer}. Then, we discuss Algorithm \ref{algTranslateContainerDeclaration} in Section \ref{sectTranslContainer} as well as subsequent algorithms, namely the translation of compound containers in Section \ref{sectCompoundContainer} and the incremental container quantification in Section \ref{sectContainerQuantification}. +We will focus here on Pattern \ref{forContainerQuant}, as Pattern \ref{forContainerTop} is implicitly handled by the translation of top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. First, we detail $f(v,t)$ in Section \ref{sectAdjContainer}. Then, we discuss Algorithm \ref{algTranslateContainerDeclaration} as the main entry point for the translation of containers in Section \ref{sectTranslContainer}, the incremental quantification of nested containers in Section \ref{sectTranslContainer} as well as a subsequent algorithm for translating compound containers in Section \ref{sectCompoundContainer}. \subsubsection{Adjusting Containers}\label{sectAdjContainer} -In summary, $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}. - -If $ca$ is a nested container (and $t$ is not a container type), we apply the IVML \IVML{flatten} operation to extract all element values from all nested containers into a single joint container. As a side effect, we enable access even to deeply nested container elements. - -If $t$ is a subtype of the element type of the container, we apply the \IVML{selectByKind} operation, as otherwise slots defined on the specific type $t$ are not accessible. - -$f(v, t)$ composes both optional operations as shown in Schema \ref{fSimpleContainerQuantorPrefix}. Pattern \ref{forContainerQuant} uses $f(v, t)$ to create quantified constraints, i.e., appends the all-quantor with a respective iterator variable and constraint. +In summary, $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{asSet}, \IVML{flatten} and \IVML{selectByKind}. + +\begin{itemize} +\item If $t$ is a \IVML{Sequence}, we apply the \IVML{asSet} operation to avoid checking the same constraints on duplicated collection entries. This also avoids receiving the same reasoning error message multiple times. + +\item If $t$ indicates a nested container (and $t$ is not a container type), we apply the IVML \IVML{flatten} operation to extract all element values from all nested containers into a single joint container. As a side effect, we enable access even to deeply nested container elements. + +\item If $t$ is a subtype of the element type of the container, we apply the \IVML{selectByKind} operation, as otherwise slots defined on the specific type $t$ are not accessible. +\end{itemize} + +$f(v, t)$ composes the three optional IVML operations as shown in Schema \ref{fSimpleContainerQuantorPrefix}. Pattern \ref{forContainerQuant} uses $f(v, t)$ to create quantified constraints, i.e., appends the all-quantor with a respective iterator variable and constraint. % \begin{equation} -\IVMLforall{v\IVMLcarrow \underbrace{\IVML{flatten()}\IVMLcarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}}_{\text{if } \subTypeOf{t}{nested^*(e)}}}{i}{\constraintWith{c}{i}} +\IVMLforall{v + \underbrace{\IVMLcarrow \IVML{asSet()}}_{\text{if}~isSequence(v)} + \underbrace{\IVMLcarrow\IVML{flatten()}}_{\text{if}~isNested(v)} + \underbrace{\IVMLcarrow\IVML{selectByKind(}t\IVML{)}}_{\text{if } \subTypeOf{t}{nested^*(v)}}} + {i}{\constraintWith{c}{i}} \label{fSimpleContainerQuantorPrefix} \end{equation} % + \subsubsection{Translating Containers}\label{sectTranslContainer} @@ -313,4 +322,8 @@ Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable $v$ of declaration $d$, if nested with given access expression $ca$ and actual type $t$. + +In line \ref{algTranslateContainerDeclarationPushContext}, we create a new variable mapping context in $\variableMapping$ in order to keep accessor expressions and processed types local to the actual container translation. In line \ref{algTranslateContainerDeclarationInitTypes}, we determine the innermost nested type $t_n$, its base type $t_b$ (ignoring intermediate derived types) as well as the relevant value $val$ (cf. Section \ref{sectNotationValues}). + +If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we apply Pattern \ref{forConstraintContainer}. We translate all (flattened) element values to individual container constraints applying a respective substitution and add the resulting constraints to the other constraints sequence $\otherConstraints$ (line \ref{algTranslateContainerDeclarationConstraintContainer}). \begin{algorithm}[H] @@ -347,69 +360,28 @@ \end{algorithm} -In line \ref{algTranslateContainerDeclarationPushContext}, we create a new variable mapping context in $\variableMapping$ in order to keep accessor expressions and processed types local to the actual container translation. In line \ref{algTranslateContainerDeclarationInitTypes}, we determine the innermost nested type $t_n$, its base type $t_b$ (ignoring intermediate derived types) as well as the relevant value $val$ (cf. Section \ref{sectNotationValues}). - -If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we apply Pattern \ref{forConstraintContainer}. We translate all (flattened) element values to individual container constraints applying a respective substitution and add the resulting constraints to the other constraints sequence $\otherConstraints$ (line \ref{algTranslateContainerDeclarationConstraintContainer}). - -If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the (actual) types used in the container. As nested containers are handled through $f(v, t)$, we apply here Pattern \ref{forContainerQuant} except for basic IVML types that cannot have constraints (cf. Section \ref{sectNotationOthers}). If there is a container value in $v$, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. As the translation algorithm will traverse the refinement hierarchy for each type in $used$, we can focus on the most specific types, i.e., skip less specific types in the respective refinement hierarchy (line \ref{algTranslateContainerDeclarationUsedTypesPrune}). If there is no value for $v$, we use the innermost nested base (compound) type $t_b$ as fallback, i.e., the only (known) used type in the container (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). Then, we iterate over all (most specific) used types and apply Algorithm \ref{algTranslateCompoundContainer}. - -Independently whether $v$ is a constraint or a compound container, the element type may be a (chained) derived type. To handle the implied constraints, we translate and collect all constraints stemming from $t_n$ in line \ref{algTranslateContainerDeclaration}. It is important to recall here that Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which is called here, handles container quantification. Finally, we pop the context frame created at the beginning of the algorithm in line \ref{algTranslateContainerDeclarationDerivedTypes}. - -\subsubsection{Translating Compound Containers}\label{sectCompoundContainer} - -Algorithm \ref{algTranslateCompoundContainer} translates a compound container declaration $d$ with access expression $ca$ based on a given actual element type $t$ and the declared elemnt type $t_d$. The idea of Algorithm \ref{algTranslateCompoundContainer} is to $f(v, t)$ in order to quantify the constraints in $t$ over all container elements in $d$ and to translate the individual constraints using the compound translation algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}. As several constraints may need to be translated for $t$, Algorithm \ref{algTranslateCompoundContainer} creates the quantification prefix expression including $f(v, t)$ once and applies it for all constraints defined by $t$. As containers and compounds may be nested, Algorithm \ref{algTranslateCompoundContainer} stores the relevant information for the quantification prefix in the actual context frame of $\variableMapping$ and composes the complete quantification prefix when adding a translated constraint to the constraint base. Adding constraints happens by calling Algorithm \ref{algTranslateCompoundContent}, i.e., dependent on the type structure, this may cause a recursion involving also the general translation of declarations in Algorithm \ref{algTranslateDeclaration}. - -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 - \KwIn{declaration $d$, actual element type $t$, declared element type $t_d$, container access $ca$} - \KwData{variable mapping $\variableMapping$} - - \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{algTranslateCompoundContainerAsSet} - } - \uIf{$isNested(type(d))$} { - $e\assng\createExpression{\IVML{flatten}(e)}$\; \label{algTranslateCompoundContainerFlatten} - } - \uIf{$t \neq t_d$} { - $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateCompoundContainerCast} - } - - $pushContext(\variableMapping, \undef, e, l, true)$\; \label{algTranslateCompoundPushContext} - $registerCompoundMapping(t, l, d)$\; \label{algTranslateCompoundContainerMapping} - - $translateCompoundContent(l, \undef, t, l)$\; \label{algTranslateCompoundContainerContent} - $popContext()$\; \label{algTranslateCompoundContainerPopContext} - } - \caption{Translating constraints for compound containers (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} -\end{algorithm} - -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. +If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the (actual) types used in the container. As nested containers are handled through $f(v, t)$, we apply here Pattern \ref{forContainerQuant} except for basic IVML types that cannot have constraints (cf. Section \ref{sectNotationOthers}). If $v$ contains a container value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. As the translation algorithm will traverse the refinement hierarchy for each type in $used$, we can focus on the most specific types, i.e., skip less specific types in the respective refinement hierarchy (line \ref{algTranslateContainerDeclarationUsedTypesPrune}). If $v$ does not have a value, we use the innermost nested base (compound) type $t_b$ as fallback, i.e., the only (known) used type in the container (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). Then, we iterate over all (most specific) used types and apply Algorithm \ref{algTranslateCompoundContainer} (cf. Section \ref{sectCompoundContainer}). + +Independently whether $v$ is a constraint or a compound container, the element type may be a (chained) derived type. To handle the implied constraints, we translate and collect all constraints stemming from $t_n$ in line \ref{algTranslateContainerDeclaration}. It is important to recall that Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which is called here, handles container quantification. Finally, we pop the context frame created at the beginning of the algorithm in line \ref{algTranslateContainerDeclarationDerivedTypes}. \subsubsection{Incremental Container Quantification}\label{sectContainerQuantification} -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. +While $f(v, t)$ allows processing a container variable $v$, it is just one part in the translation of nested containers. In this section we discuss the quantification of constraints for nested container structures. As we collect the information for the quantification across various algorithms, we call this approach \textbf{incremental container quantification}. The actual quantification happens when adding constraints to the constraint base, i.e., in the $add$ function (cf. Algorithm \ref{algAddConstraint} in Section \ref{sectContainerBase}). + +The basic idea of Pattern \ref{forContainerQuant} is that constraints defined on (used) element types must be lifted to the container level by all-quantification. However, containers may be nested, i.e., require nested quantification. While directly nested containers are handled by $f(v, t)$, nesting containers via compounds requires special care. + +Let \IVML{C} and \IVML{D} be compound types defining some constraints on their slots. Let slot \IVML{s} of \IVML{C} be of type \IVML{setOf(D)}, then \IVML{setOf(C)} is a nested compound container type. The required quantification expression for constraints defined on \IVML{D} is illustrated below in Schema \ref{fNestedContainerQuantorPrefix}. % \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}:\constraintWith{c}{l_2})) +\underbrace{\underbrace{ca}_{1: acc}\IVMLcarrow{} fvt}_{1: cont}\IVMLcarrow{}\IVML{forall}(\underbrace{l}_{1: iter}:\underbrace{\underbrace{l.s}_{2: acc}\IVMLcarrow{}fvt}_{2: cont}\IVMLcarrow{}\IVML{forall}(\underbrace{l_2}_{2: iter}:\constraintWith{c}{l_2})) \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. +Let $ca$ be an access expression pointing to a container variable of type \IVML{setOf(C)}. Further, let $fvt$ stand for the result of $f(v, t)$ in the respective context. Due to the nesting, the container translation is executed in recursive manner starting at some container variable (more generically accessor $ca$). Thus, the quantification must be performed incrementally as part of the recursion. We indicate in Schema \ref{fNestedContainerQuantorPrefix} the call levels as well as the function of the respective sub-expression with respect to the translation/quantification, i.e., \textit{acc}essor, \textit{cont}ainer expression or \textit{iter}ator. + +The container translation starts at some container variable in terms of the accessor expression $ca$ given as argument. On the first call level, $ca$ is the accessor ('$1:acc$') representing the container. The translation algorithm builds the full container expression ('$1:cont$') by applying $ca$ to $f(v, t)$. For composing the quantification, the algorithm creates an iterator variable $l$ of the element type of the container ('$1:iter$'). This information would be sufficient to quantify the constraints for all container elements of type \IVML{C}. However, as \IVML{C} may contain further containers, in our example slot \IVML{s}, we must provide information about the quantification to the recursive container translation that will be applied to \IVML{s}. Therefore, we store the iterator variable $l$ and the full container expression in a new context frame on $\variableMapping$ and pass $l$ on as accessor expression for the translation of \IVML{C}. When adding the constraints for the other (non-container) slots of \IVML{C} to the constraint base, the quantification information in the container stack frame will be used by the $add$ function to complete the constraints. Therefore, the $add$ function applies a variable substitution involving $l$ and creates a quantification expression for the constraint as shown for Pattern \ref{forContainerQuant} . + +When translating slot \IVML{s}, $l$ is provided as accessor argument, leading to the composed accessor expression $l.s$ for \IVML{s} in Algorithm \ref{algRegisterCompoundMapping}. As \IVML{s} is a compound container of type \IVML{setOf(D)}, we execute the container translation recursively and pass in $l.s$ as accessor ('$2:acc$'). To compose the full container expression '$2:cont$', the algorithm executes now $f(l.s, t)$ and creates the iterator variable $l_2$ ('$2:iter$)'. Now this quantification information is stored in a new context frame on $\variableMapping$. When adding the constraints of \IVML{D} to the constraint base, the $add$ function considers the quantification information in both stack frames to perform the variable substitution and to compose the quantification expression shown in Schema \ref{fNestedContainerQuantorPrefix}. + +Algorithm \ref{algComposeExpression} composes the complete quantification expression for a given constraint $c$ and acts as a helper function for $add$. Algorithm \ref{algComposeExpression} traverses the stack in top-down manner, form the perspective of $c$ starting with the innermost nested context frame, and, thus, processes the containing frames incrementally. 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 for $c$ a constraint of the form shown in Schema \ref{fNestedContainerQuantorPrefix} in inside out fashion. In Algorithm \ref{algComposeExpression}, $c$ changes incrementally for each processed stack frame requiring quantification, i.e., providing quantification information. For each such stack frame, the algorithm surrounds 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] @@ -428,5 +400,51 @@ \end{algorithm} -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. + +Along with the translation, also assignment constraints for default values of compound slots are created by Algorithm \ref{algTranslateDeclaration} and quantized through the $add$ function. Relying on quantor constraints here implies that default initializations, which remain unevaluated as some dependent variables have not been determined, cause a re-evaluation for all elements of the container (re-assignments are handled by the constraint evaluator). Here, unfolding the loop of a quantor may be more efficient, as then only so far undefined constraints are evaluated. However, 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 quantized constraints even for default values assignments. + +\subsubsection{Translating Compound Containers}\label{sectCompoundContainer} + +Algorithm \ref{algTranslateCompoundContainer} translates a compound container declaration $d$ with access expression $ca$ based on a given actual element type $t$ and the declared elemnt type $t_d$. The idea of Algorithm \ref{algTranslateCompoundContainer} is to realize $f(v, t)$, to provide quantification information for the incremental constraint quantification and to translate the individual constraints using Algorithm \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}. +%As several constraints may need to be translated for $t$, Algorithm \ref{algTranslateCompoundContainer} creates the quantification prefix expression including $f(v, t)$ once and applies it for all constraints defined by $t$. + +%The quantification according to Pattern \ref{forContainerQuant} is not directly realized in Algorithm \ref{algTranslateCompoundContainer}. As explained in Section \ref{sectContainerQuantification}, the $add$ function uses information from the context frames in $\variableMapping$ to compose a quantified constraint (if needed) when adding a translated constraint to the constraint base. Therefore, Algorithm \ref{algTranslateCompoundContainer} just stores the relevant information for the incremental quantification in the actual context frame of $\variableMapping$. The actual constraint translation happens then by calling Algorithm \ref{algTranslateCompoundContent}, i.e., dependent on the type structure, this may cause a recursion involving also the general translation of declarations in Algorithm \ref{algTranslateDeclaration}. + +Algorithm \ref{algTranslateCompoundContainer} 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. Moreover, checking whether $t$ has already been processed in the same container also prevents endless recursion that may occur if $t$ is also used as a slot type of a nested compound / as an element type in a nested container (through a call sequence of Algorithms \ref{algTranslateCompoundContainer}, \ref{algTranslateContainerDeclaration}, \ref{algTranslateCompoundContent} and \ref{algTranslateDeclaration}). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, actual element type $t$, declared element type $t_d$, container access $ca$} + \KwData{variable mapping $\variableMapping$} + + \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{algTranslateCompoundContainerAsSet} + } + \uIf{$isNested(type(d))$} { + $e\assng\createExpression{\IVML{flatten}(e)}$\; \label{algTranslateCompoundContainerFlatten} + } + \uIf{$t \neq t_d$} { + $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateCompoundContainerCast} + } + + $pushContext(\variableMapping, \undef, e, l, true)$\; \label{algTranslateCompoundPushContext} + $registerCompoundMapping(t, l, d)$\; \label{algTranslateCompoundContainerMapping} + + $translateCompoundContent(l, \undef, t, l)$\; \label{algTranslateCompoundContainerContent} + $popContext()$\; \label{algTranslateCompoundContainerPopContext} + } + \caption{Translating constraints for compound containers (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} +\end{algorithm} + +If type $t$ has not already been processed in the current context frame, line \ref{algTranslateCompoundContainerMarkProcessed} marks the type as processed. For enabling the incremental quantification, Algorithm \ref{algTranslateCompoundContainer} creates in line \ref{algTranslateCompoundContainerIterator} a local variable $l$ as iterator for the incremental quantification. Then, the algorithm derives the collection accessor expression in line \ref{algTranslateCompoundContainerInitE}, either using $ca$ if given (for nested containers) or the container variable declaration $d$ (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 in Section \ref{sectAdjContainer}. If the actual element type $t$ is not the same as the declared element type $t_d$, we must apply type selection for conversion in line \ref{algTranslateCompoundContainerCast} to make slots defined on specific types accessible. + +Then the algorithm creates in line \ref{algTranslateCompoundPushContext} a context frame (always linked to the parent container frame) for the following compound transformation. The algorithm uses this context frame to store the information for incremental quantification, i.e., the iterator variable $l$ and the container expression $e$. As for compounds, the algorithm creates in line \ref{algTranslateCompoundContainerMapping} the accessor expressions by calling Algorithm \ref{algRegisterCompoundMapping} using the iterator variable $l$ as accessor and $t$ as the actual type to avoid unnecessary type casts. Then, the algorithm calls Algorithm \ref{algTranslateCompoundContent} to translate the compound constraints that will implicitly be quantified when calling the $add$ function. Finally, the algorithm pops in line \ref{algTranslateCompoundContainerPopContext} the context frame created in line \ref{algTranslateCompoundPushContext}. \subsection{Annotations}\label{sectAnnotationDefaults} Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 213) +++ /reasoner/mainAlgorithms.tex (revision 214) @@ -160,5 +160,5 @@ Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. The algorithm receives a project $p$ as input and, as a side effect, identifies and translates\footnote{In the implementation, the translation steps in this algorithm are realized in terms of an IVML model visitor implicitly identifying and handling the types without iterating multiple times over the project as the notation here might suggest.} the constraints in $p$. The constraint sequences are filled as side effects of the calls in lines \ref{algTranslateConstraintsTranslationStart}-\ref{algTranslateConstraintsTranslationEnd}, where the algorithm iterates over the top-level constraint types, i.e., variable declarations, constraints, annotation assignments and eval blocks directly contained in project $p$. -It is important to note that adding constraints to such a constraint sequence involves activities such as completing constraints by quantification, handling constraint variables, filtering out unneeded constraints according to the reasoning mode as well as relating constraints and their used variables (cf. $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). These activities are realized in the $add$ function (e.g., used in line \ref{algTranslateConstraintsAdd}), which we will detail in Section \ref{sectContainerBase}. For short, the $add$ function receives the target constraint sequence, the constraint(s) to add, a flag whether checking for constraint values is needed and an optional configuration variable to which new constraints shall be related to (for building up $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). The $add$ function also considers the global $inEvals$ flag\footnote{For documentation purposes, we follow here the style of the implementation, where the visitor is a class communicating such information via instance variables.}, which raises the priority for all (eval) constraints passed in. +It is important to note that adding constraints to such a constraint sequence involves activities such as completing constraints by incremental quantification, handling constraint variables, filtering out unneeded constraints according to the reasoning mode as well as relating constraints and their used variables (cf. $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). These activities are realized in the $add$ function (e.g., used in line \ref{algTranslateConstraintsAdd}), which we will detail in Section \ref{sectContainerBase}. For short, the $add$ function receives the target constraint sequence, the constraint(s) to add, a flag whether checking for constraint values is needed and an optional configuration variable to which new constraints shall be related to (for building up $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). The $add$ function also considers the global $inEvals$ flag\footnote{For documentation purposes, we follow here the style of the implementation, where the visitor is a class communicating such information via instance variables.}, which raises the priority for all (eval) constraints passed in. According to the priority of the constraint sequences $\defaultConstraints$, $\deferredDefaultConstraints$, $\topLevelConstraints$ and $\otherConstraints$, Algorithm \ref{algTranslateConstraints} composes in line \ref{algTranslateConstraintsCompose} the constraint base (keeping remaining constraints from prior projects). Then, Algorithm \ref{algTranslateConstraints} clears $\defaultConstraints$, $\deferredDefaultConstraints$, $\topLevelConstraints$ and $\otherConstraints$ in lines \ref{algTranslateConstraintsClearSetsStart}-\ref{algTranslateConstraintsClearSetsEnd} and copies the constraint $base$ to prepare the incremental reasoning mode in its first run. Finally, in line \ref{algTranslateConstraintsClearMapping}, Algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$ so that it can be re-used for translating the next IVML project.