Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 215) +++ /reasoner/consTranslation.tex (revision 216) @@ -123,5 +123,5 @@ \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundEval} \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundAssign} - \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } \constraintWith{c}{v.s}\IVML{;}}{\varSubstitution{\constraintWith{c}{v.s}}{\variableMapping}}{forCompoundAssign} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } \constraintWith{c}{v.s}\IVML{;}}{\varSubstitution{\constraintWith{c}{v.s}}{\variableMapping}}{forCompoundConstraint} } @@ -138,5 +138,5 @@ \item \emph{Annotation assignments: } Akin to eval blocks, constraints in a nested assign block are evaluated in the containing compound scope as indicated by Pattern \ref{forCompoundAssign}. However, annotation assignments require specific handling of default values to avoid accidental re-assignment of default values as we will discuss in Section \ref{sectAnnotationDefaults}. - \item \emph{Top-level constraint defined over a compound variable $v$:} Due to the mandatory use of qualified slot access expressions in top-level constraints, no specific translation is needed. Pattern \ref{forCompoundAssign} is listed here to discuss all possible kinds of compound constraints. Such constraints treated in Algorithm \ref{algTranslateConstraints} line \ref{algTranslateConstraintsTopLevelConstraints}. + \item \emph{Top-level constraint defined over a compound variable $v$:} Due to the mandatory use of qualified slot access expressions in top-level constraints, no specific translation is needed. Pattern \ref{forCompoundConstraint} is listed here to discuss all possible kinds of compound constraints. Such constraints treated in Algorithm \ref{algTranslateConstraints} line \ref{algTranslateConstraintsTopLevelConstraints}. \end{itemize} @@ -150,5 +150,5 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$, compound $mode$} + \KwIn{declaration $d$, variable $v$, accessor expression $ca$, default value type $t$, compound $mode$} \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} @@ -224,7 +224,4 @@ $$slots^-(u) = \setWith{s}{s \in slots(u) \wedge \neg isTypeExcluded(\variableMapping, type(parent(s)))} $$ % -In lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}, Algorithm \ref{algTranslateCompoundContent} performs the translation of the default value expressions of all slots in $slots^-$. Here, we must distinguish two cases, namely whether the configuration variable $v$ is available or not\footref{fnVariableNull}. If $v$ is available (lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsMid}), $slots^-(v)$ returns all slots in terms of nested (refined) variables, which are applied to Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV}. If $v$ is not available (lines \ref{algTranslateCompoundDeclarationTranslateSlotsMid}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}), we use the type hierarchy as fallback, i.e., we translate constraints without knowledge about the actual type of the variables. In line \ref{algTranslateCompoundDeclarationTranslateSlotsT}, we call Algorithm \ref{algTranslateDeclaration} for a type-based transformation of the slot declaration $d$, i.e., without slot variable but with accessor expression for $s$ recorded in $\variableMapping$. - -Then we translate then the default values specified by nested annotation assignments in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. Akin to Algorithm \ref{algTranslateDeclaration}, translating these default values is not needed in incremental reasoning mode. \begin{algorithm}[H] @@ -259,4 +256,8 @@ \end{algorithm} +In lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}, Algorithm \ref{algTranslateCompoundContent} performs the translation of the default value expressions of all slots in $slots^-$. Here, we must distinguish two cases, namely whether the configuration variable $v$ is available or not\footref{fnVariableNull}. If $v$ is available (lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsMid}), $slots^-(v)$ returns all slots in terms of nested (refined) variables, which are applied to Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV}. If $v$ is not available (lines \ref{algTranslateCompoundDeclarationTranslateSlotsMid}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}), we use the type hierarchy as fallback, i.e., we translate constraints without knowledge about the actual type of the variables. In line \ref{algTranslateCompoundDeclarationTranslateSlotsT}, we call Algorithm \ref{algTranslateDeclaration} for a type-based transformation of the slot declaration $d$, i.e., without slot variable but with accessor expression for $s$ recorded in $\variableMapping$. + +Then we translate then the default values specified by nested annotation assignments in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. Akin to Algorithm \ref{algTranslateDeclaration}, translating these default values is not needed in incremental reasoning mode. + As preparation for subsequent variable substitutions, we determine in line \ref{algTranslateCompoundDeclarationSelf} the expression $f$ for \IVMLself{}, which is either the access expression $ca$ if given or the declaration $d$. The remaining translations are performed on $t_r$, the set of refined but not excluded types determined in line \ref{algTranslateCompoundRefinedNotExcluded}. Let % @@ -273,6 +274,4 @@ 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, which in extreme case requires nested quantification rather than unrolling of (nested) containers. \grayPara{ @@ -281,4 +280,6 @@ \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop} } + +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. 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. @@ -461,7 +462,13 @@ Annotation assignment blocks are specific syntactic sugar to ease the declaration of annotations and their default values. An assignment block specifies the default value (given in the parentheses between \IVML{assign} and \IVML{to} in Pattern \ref{fAnnotAssngBlock}) for all variables declared within the assignment block. Thus, an assignment block represents a mass-declaration of annotation default values. For more complex situations, annotation assignment blocks can be nested to enable assignment of default values to multiple annotations. To avoid accidental re-assignments, only the innermost nested value(s) shall ultimately be assigned to the listed variables and annotations~\cite{IVML-LS}. As indicated by Pattern \ref{fAnnotAssngBlock}, we translate annotation assignment blocks through the creation of a series of annotation assignment constraints, i.e., for all assigned annotations and all variables declared in the block (and nested blocks)\footnote{As we do not have a 'name' for the assignment block in Pattern \ref{fAnnotAssngBlock}, the '$\ldots$' on the right side indicate the creation of similar constraints for all variables declared in the block and all nested blocks with their respective default expressions.}. -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$} +We will detail the translation of annotation default value expressions in Section \ref{sectAnnDeclDeflts} and the translation of assignment blocks in Section \ref{sectAnnAssngBlocks}. + +\subsubsection{Translating Annotation Declarations and Defaults}\label{sectAnnDeclDeflts} + +Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration $d$ of the variable $v$ for which all declared annotations shall be processed as well as an optional access expression $ca$ in case that $d$ is a compound slot. The idea for Algorithm \ref{algTranslateAnnotationDeclarations} is to iterate over all annotations, either in terms of decision variables or declarations\footref{fnVariableNull}, and to process each annotation as if it is an ordinary variable, i.e., by calling Algorithm \ref{algTranslateDeclaration} with a respective access expression. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, accessor expression $ca$} \KwData{variable mapping $\variableMapping$} @@ -484,7 +491,5 @@ \end{algorithm} -Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration $d$ of the variable $v$ that shall be processed as well as an optional access expression $ca$ in case that $d$ is a compound slot. The idea for Algorithm \ref{algTranslateAnnotationDeclarations} is to iterate over all annotations, either in terms of decision variables or declarations\footref{fnVariableNull}, and to process each annotation as if it was an ordinary variable, i.e., by calling Algorithm \ref{algTranslateDeclaration} with a respective access expression. - -First, Algorithm \ref{algTranslateAnnotationDeclarations} determines in line \ref{algTranslateAnnotationDeclarationsCa} the actual base access expression as either $ca$ (e.g., as $d$ is a compound slot) if given or $d$. Annotations are translated based on nested variables of $v$ and their actual values, if $v$ is given (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}). Alternatively, e.g., for configuration initialization, the translation of annotations is done based on nested declarations of $d$ (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). In both cases, Algorithm \ref{algTranslateDeclaration} is called on the respective declaration, variable (if available) and accessor expression. The accessor expression is created by: +First, Algorithm \ref{algTranslateAnnotationDeclarations} determines in line \ref{algTranslateAnnotationDeclarationsCa} the accessor expression, i.e., either $ca$ if given (e.g., as $d$ is nested such as a compound slot) or $d$. The further translation depends on whether variable $v$ including actual value / type is available (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}) or we have to resort to a type-only translation\footref{fnVariableNull} based on nested declarations of $d$ (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). In both cases, Algorithm \ref{algTranslateDeclaration} is called on the respective annotation declaration, annotation variable (if available) and accessor expression. The accessor expression is created by: % \begin{align*} @@ -492,5 +497,7 @@ \end{align*} % -The function $annAcc$ creates an specific annotation accessor in case that we are translating a nested annotation assignment (the content stack contains here more than one frame) or the underlying variable holding the annotation is of a compound type and must be qualified explicitly. +The function $annAcc$ creates a specific annotation accessor in case that we are translating a nested annotation assignment (the stack in $\variableMapping$ contains then more than one frame) or the underlying variable holding the annotation is of a compound type and must be qualified explicitly. + +\subsubsection{Translating Annotation Assignment Blocks}\label{sectAnnAssngBlocks} We turn now to the second pattern, the translation of annotation assignments. The idea of Algorithm \ref{algTranslateAnnotationAssignments} is to incrementally create the set of effective assignments for the actual annotation assignment in order to ensure that only the innermost assignment data is applied. More technically, we build a mapping based on the names of the annotations and override inherited assignments with by those specified by the annotation assignment to be processed. @@ -500,5 +507,5 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{annotation assignment $a$, variable $v$, effective assignment data $ea$, compound access $ca$} + \KwIn{annotation assignment $a$, variable $v$, effective assignment data $ea$, accessor expression $ca$} \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$}