Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 95) +++ /reasoner/reasoner.tex (revision 96) @@ -384,4 +384,5 @@ \begin{itemize} \item $setRegisterContexts(\variableMapping, bool)$ enabling automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. + \item $isContextsRegistering(\variableMapping)$ returns whether context registering is currently active. \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, the new frame will be registered with the parent frame for $var$ (unless $var=\undef$) Further, $r$ indicates whether already processed types shall be recorded by this context, which is important for handling recursive types. \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating a quantified constraint, namely the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}. @@ -783,5 +784,9 @@ In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those ortogonal variables, the reasoner must create constraints to perform the evaluation and assignment of the default values before all other constraints are considered for reasoning. It is important to recall that IVML annotations are not recursive~\cite{IVML-LS}, although the reasoner algorithms could support this. Moreover, we must translate assignment-blocks, i.e., blocks assigning specific values to all variables declared within that block. In this section, we discuss first the translation of annotations, then the translation of annotation blocks. -Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration of the actual variable and a potential compound access expression $ca$ to $d$ if the algorithm is called for slots of a compound value. For all annotations of $v$ (as for $v$ here all inherited annotations are available), the algorithm creates the respective constraints through calling Algorithm \ref{algTranslateDeclaration}. Plase note that no specific variable accessors are handled for such top-level annotation assignments through a specific constraint syntax tree node, which is created through \IVMLMeta{acc()} in Algorithm \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateAnnotationAccess}. +Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration of the actual variable and a potential compound access expression $ca$ to $d$ if the algorithm is called for slots of a compound value. The actual access expression is either $ca$ if given or $d$ if $ca$ is not given (line \ref{algTranslateAnnotationDeclarationsCa}). Annotations are translated based on $v$ if given (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}), for configuration initialization also based on $d$ if $v$ is not given (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). + +For all annotations of $v$ +%(as for $v$ here all inherited annotations are available) +, the algorithm creates the respective constraints by creating a specific access expression (only if we are not actually translating annotation blocks implying context registering) through calling Algorithm \ref{algTranslateDeclaration}. For top-level annotation assignments , no specific access expressions except for the one created in line \ref{algTranslateAnnotationDeclarationsCa} are needed, as they are created in Algorithm \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateAnnotationAccess}. \begin{algorithm}[H] @@ -790,7 +795,19 @@ \KwData{constraints $\otherConstraints$} - \ForEach{$a\in annotations(v)$}{ - $translateDeclaration(decl(a), a, ca)$\;\label{algTranslateAnnotationDeclarationsTranslateDecl} - } + $ca\assng \closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}$\;\label{algTranslateAnnotationDeclarationsCa} + \uIf{$v \neq \undef$}{\label{algTranslateAnnotationDeclarationsTranslateVStart} + \ForEach{$a\in annotations(v)$}{ + $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } ca \neq \undef \wedge \neg isContextRegistering(\variableMapping)\\ ca, &\text{else}}$\; + $translateDeclaration(decl(a), a, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclV} + } + }\Else{\label{algTranslateAnnotationDeclarationsTranslateVEnd}\label{algTranslateAnnotationDeclarationsTranslateDStart} + \ForEach{$a\in annotations(d)$}{ + $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } ca \neq \undef \wedge \neg isContextRegistering(\variableMapping)\\ ca, &\text{else}}$\; + $translateDeclaration(a, \undef, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD} + } + }\label{algTranslateAnnotationDeclarationsTranslateDEnd} + +%isContextsRegistering(\variableMapping) + \caption{Translating annotation defaults (\IVML{translateAnnotationDeclarations}).}\label{algTranslateAnnotationDeclarations} \end{algorithm} @@ -943,5 +960,5 @@ Constraint variable & 3.1.10 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} \TBD{change} & Cs1, Cs2 \\ -Annotation & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}\tabAlgFollow\tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDecl}\tabAlgFollow Table \ref{tab:completenessAnnotations} & A1, A2, A3\\ +Annotation & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}\tabAlgFollow\tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclV} or \tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclD} \tabAlgFollow Table \ref{tab:completenessAnnotations} & A1, A2, A3\\ Assignment block & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelAnnotationAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnAI1 \\ @@ -1066,7 +1083,5 @@ Constraint type & 3.1.10 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationConstraintContainer}\TBD{change} & CnCt1, CnCt2 \\ -Derived constraint type & 3.1.10 & \TBD{??} & \TBD{tests} \\ - -Annotation & 2.2.2 & top-level only, see Table \ref{tab:completenessTopLevelTypes} & \TBD{tests}\\ +Annotation & 2.2.2 & top-level only, see Table \ref{tab:completenessTopLevelTypes} & TFCnCtCsA1 \\ Assignment blocks & - & - & - \\ @@ -1092,20 +1107,20 @@ \textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation Path} & \textbf{Test as annotation} & \textbf{Test anotate to}\\ \hline - \multicolumn{5}{|c|}{Annotations (starting with \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}\tabAlgFollow\tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDecl} cf. see Table \ref{tab:completenessTopLevelTypes})}\\ -\hline - -Integer type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & CnAI1 & CnAI1 \\ - -Real type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} & \TBD{tests} \\ - -Boolean type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} & \TBD{tests} \\ - -String type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} & \TBD{tests}\\ - -Enum type & 2.1.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} & \TBD{tests}\\ + \multicolumn{5}{|c|}{Annotations (starting with \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}\tabAlgFollow\tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclV} or \tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclD} cf. see Table \ref{tab:completenessTopLevelTypes})}\\ +\hline + +Integer type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & CnAI1, AI1 & CnAI1, A*1 \\ + +Real type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & AR1 & A*1 \\ + +Boolean type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & AB1 & A*1 \\ + +String type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & AS1 & A*1\\ + +Enum type & 2.1.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & AE1 & A*1\\ Derived type & 2.1.3.4 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & \TBD{tests} & \TBD{tests} \\ -Compound type & 2.1.3.5 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateCompound}\tabAlgFollow\tabAlg{algTranslateCompoundDeclaration}\tabAlgFollow\tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingAnnotationMapping}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess} & \TBD{tests} & CnAI1 \\ +Compound type & 2.1.3.5 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateCompound}\tabAlgFollow\tabAlg{algTranslateCompoundDeclaration}\tabAlgFollow\tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingAnnotationMapping}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess} & ACn1 & CnAI1, A*1 \\ Container type & 2.1.3.3 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateContainer}\tabAlgFollow\tabAlg{algTranslateContainerDeclaration}\MISSING{processed where?} & \TBD{tests} & \TBD{tests} \\ @@ -1123,5 +1138,5 @@ \hline \end{tabular} -\caption{Translation of annotations} +\caption{Translation of annotations starting with \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}} %\end{adjustbox} \label{tab:completenessAnnotations} @@ -1229,4 +1244,5 @@ B3 & \class{boolean/BooleanImpliesTest.ivml}\\ BF1 & \class{boolean/BooleanRefAssignTest.ivml\protect\footnotemark}\\ +AB1 & \class{boolean/BooleanAnnotationTest.ivml}\\ BCo1 & \class{boolean/BooleanInCompoundAssignTest.ivml}\\ BCo3 & \class{boolean/BooleanInCompoundDefaultsTest.ivml}\\ @@ -1236,4 +1252,5 @@ I1 & \class{integer/IntegerDefaultsTest.ivml}\\ I2 & \class{integer/IntegerAssignTest.ivml}\\ +AI1 & \class{integer/IntegerAnnotationTest.ivml}\\ IT1 & \class{operations/typedef.ivml}\\ IT2 & \class{operations/typedefOfTypedefValid.ivml}\\ @@ -1244,4 +1261,5 @@ R1 & \class{real/RealDefaultsTest.ivml}\\ R2 & \class{real/RealAssignTest.ivml}\\ +AR1 & \class{real/RealAnnotationTest.ivml}\\ RCo1 & \class{real/RealInCompoundDefaultsTest.ivml}\\ RCo2 & \class{real/RealInCompoundAssignTest.ivml}\\ @@ -1250,4 +1268,5 @@ S1 & \class{string/StringDefaultsTest.ivml}\\ S2 & \class{string/StringAssignTest.ivml}\\ +AS1 & \class{string/StringAnnotationTest.ivml}\\ SCo1 & \class{string/StringInCompoundDefaultsTest.ivml}\\ SCo2 & \class{string/StringInCompoundAssignTest.ivml}\\ @@ -1256,4 +1275,5 @@ E1 & \class{enums/EnumDefaultsTest.ivml}\\ E2 & \class{enums/EnumAssignTest.ivml}\\ +AE1 & \class{enums/EnumAnnotationTest.ivml}\\ EF1 & \class{enums/EnumRefAssignTest.ivml}\\ ECo1 & \class{enums/EnumInCompoundDefaultsTest.ivml}\\ @@ -1280,7 +1300,9 @@ CnCt3 & \class{compounds/CompoundContainerTest1.ivml}\\ CnCt4 & \class{compounds/CompoundContainerTest2.ivml}\protect\footnotemark\\ +ACn1 & \class{compounds/CompoundAnnotationTest.ivml}\\ CnTCt1 & \class{collectionConstraints/constraintSetDerivedCompound.ivml}\\ CnTCt2 & \class{collectionConstraints/constraintSetSetDerivedCompound.ivml}\\ -CtTCt1 & \class{collectionConstraints/setDerivedSet.ivml}\\ +CtTCt1 & \class{collectionConstraints/setDerivedSet.ivml}\\ +TFCnCtCsA1 & \class{collectionConstraints/QM.ivml}\\ ITCn1 & \class{operations/typedefNestedInCompoundValid.ivml}\\ ITCnCt1 & \class{operations/typedefCompoundNestedInSequenceValid1.ivml}\\