Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 165) +++ /reasoner/consRescheduling.tex (revision 166) @@ -44,13 +44,13 @@ $t_n \assng type(value(v)))$\; - \uIf{$isConstraint(t_n)$} {\label{algRescheduleContainerValueConsStart} - $rescheduleConstraintValue(v_p, v, clear)$\; \label{algRescheduleContainerValueConsEnd} - } \uElseIf{$isCompound(t_n)$}{ \label{algRescheduleContainerValueCompStart} + \uIf{$isConstraint(t_n)$} {\label{algRescheduleValueChangeConsStart} + $rescheduleConstraintValue(v_p, v, clear)$\; \label{algRescheduleValueChangeConsEnd}\label{algRescheduleValueChangeCons} + } \uElseIf{$isCompound(t_n)$}{ \label{algRescheduleValueChangeCompStart} \ForAll{$s\iterAssng slots(value(v))$}{ \If{$value(s) \neq \undef$}{ $rescheduleValueChange(v, s, value(s), true)$\; } - } \label{algRescheduleContainerValueCompEnd} - } \uElseIf{$isContainer(t_n) \wedge isContainer(type(val_o))$}{\label{algRescheduleContainerValueContStart} + } \label{algRescheduleValueChangeCompEnd} + } \uElseIf{$isContainer(t_n) \wedge isContainer(type(val_o))$}{\label{algRescheduleValueChangeContStart} $first \assng true$\; \ForAll{$c \iterAssng elements(val_n), o \iterAssng elements(val_o)$} { @@ -58,12 +58,12 @@ $first \assng false$\; } - }\label{algRescheduleContainerValueContEnd} - - \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleContainerValue} -\end{algorithm} - -Algorithm \ref{algRescheduleContainerValue} is responsible for re-scheduling constraint values from a given IVML value. The idea is to follow nested value structures recursively, to extract constraint values and to add them after variable substitution to the constraint base. Upon the first changed constraint value for the given variable, existing constraints shall be cleared from the reasoning data structures. - -For this purpose, Algorithm \ref{algRescheduleContainerValue} receives the changed variable $v$, its optional parent variable $v_p$ (if $v$ is nested into $p$), the old value $val_o$ and a flag that indicates whether existing constraints shall be cleared within this call. If $val_n$ is a constraint, the algorithm calls Algorithm \ref{algRescheduleConstraintValue} (lines \ref{algRescheduleContainerValueConsStart}-\ref{algRescheduleContainerValueConsEnd}). If $val_n$ is a compound, the algorithm calls itself recursively for all slots that have a value assigned (lines \ref{algRescheduleContainerValueCompStart}-\ref{algRescheduleContainerValueCompEnd}). Finally, if $val_n$ is a container, the algorithm iterates over the elements in the new and the old value (assuming that at least all elements in $val_n$ are considered, eventually $val_o$ is $\undef$ then) and calls itself recursively for each pair (lines \ref{algRescheduleContainerValueContStart}-\ref{algRescheduleContainerValueContEnd}). Existing constraints are cleared only for the first element pair ($first$). + }\label{algRescheduleValueChangeContEnd} + + \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleValueChange} +\end{algorithm} + +Algorithm \ref{algRescheduleValueChange} is responsible for re-scheduling constraint values from a given IVML value. The idea is to follow nested value structures recursively, to extract constraint values and to add them after variable substitution to the constraint base. Upon the first changed constraint value for the given variable, existing constraints shall be cleared from the reasoning data structures. + +For this purpose, Algorithm \ref{algRescheduleValueChange} receives the changed variable $v$, its optional parent variable $v_p$ (if $v$ is nested into $p$), the old value $val_o$ and a flag that indicates whether existing constraints shall be cleared within this call. If $val_n$ is a constraint, the algorithm calls Algorithm \ref{algRescheduleConstraintValue} (lines \ref{algRescheduleValueChangeConsStart}-\ref{algRescheduleValueChangeConsEnd}). If $val_n$ is a compound, the algorithm calls itself recursively for all slots that have a value assigned (lines \ref{algRescheduleValueChangeCompStart}-\ref{algRescheduleValueChangeCompEnd}). Finally, if $val_n$ is a container, the algorithm iterates over the elements in the new and the old value (assuming that at least all elements in $val_n$ are considered, eventually $val_o$ is $\undef$ then) and calls itself recursively for each pair (lines \ref{algRescheduleValueChangeContStart}-\ref{algRescheduleValueChangeContEnd}). Existing constraints are cleared only for the first element pair ($first$). Algorithm \ref{algRescheduleConstraintValue} targets re-scheduling a constraint value. This involves replacing existing constraints for a given variable $v$ by a new constraint instantiated using variable substitution. In more details, Algorithm \ref{algRescheduleConstraintValue} receives the changed variable $v$, its optional parent variable $v_p$ and a flag whether existing constraints shall be cleared (if this function is called repeatedly on the same $v_p$, e.g., for all slots of a compound). Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 165) +++ /reasoner/consTranslation.tex (revision 166) @@ -528,5 +528,5 @@ } -When assigning a value to a variable, the right side may be a complex initializer expression determining the actual value of a collection or a compound. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer expressions. Instead of defining a specific translation algorithm that must be called from different algorithms, we opted for integrating the translation with the central functionality of adding constraints to the constraint base. The first translation pattern targets containers and the second one compounds. In both patterns, constraint values may occur as (deeply nested) contained values. The translation applied in Algorithm \ref{algAddConstraint} extracts these constraints, performs a respective variable substitution (\IVMLself{} is currently not supported here) and adds the result to the constraint base. +When assigning a value to a variable, the right side may be a complex initializer expression determining the actual value of a collection or a compound. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer expressions. Instead of defining a specific translation algorithm that must be called from different algorithms, we opted for integrating the translation with the central functionality of adding constraints to the constraint base. The first translation pattern targets containers and the second one compounds. In both patterns, constraint values may occur as (deeply nested) contained values. The translation applied in Algorithm \ref{algAddConstraint} extracts these constraints, performs a respective variable substitution (\IVMLself{} is handled by the expression evaluator here) and adds the result to the constraint base. Algorithm \ref{algAddConstraint} receives a target constraint sequence $s$, a constraint $c$ that shall be added to $s$, a flag which enables checking for constraint values and an optional variable $v$ the constraint shall be related to. For convenience, in some algorithms we also passed a set of constraints for adding instead of a single constraint. We just assume that then all given constraints are forwarded iteratively to Algorithm \ref{algAddConstraint}. Index: /reasoner/ivmlCompleteness.tex =================================================================== --- /reasoner/ivmlCompleteness.tex (revision 165) +++ /reasoner/ivmlCompleteness.tex (revision 166) @@ -1,5 +1,18 @@ \section{IVML-Completeness}\label{sectCompleteness} -In this section, we discuss the completeness of the reasoner with respect to IVML concepts. Reasoning completeness, e.g., involving advanced reasoning capabilities such as narrowing down value instances by limiting constraints or instance creation, is not topic of this section and may be targeted by future work. +In this section, we discuss the completeness of the reasoner with respect to IVML concepts defined in \cite{IVML-LS}. Reasoning completeness, e.g., involving advanced reasoning capabilities such as narrowing down value instances by limiting constraints or instance creation, is currently not supported by the approach and may be subject to future work. + +To assess the IVML completeness, we enumerate all IVML concepts relevant to reasoning, their defining section in the IVML specification~\cite{IVML-LS}, the transformation path along the algorithms presented in this document and the test cases validating the transformation and the reasoning results. The referenced test cases are detailed in Appendix \ref{appendixTestCases}. A '*' in a test id indicates a wildcard, e.g., A*1 means all annotation-related tests. Test cases are referenced by ids in order to indicate that all relevant combinations are subject to regression testing in the continuous build process of EASy-Producer. + +We present the argumentation in four parts grouped according to IVML concepts, namely 1) top-level concepts / basic types (Table \ref{tab:completenessTopLevelTypes}), compound types (Table \ref{tab:completenessCompounds}), container types (Table \ref{tab:completenessContainers}) and annotations (Table \ref{tab:completenessAnnotations}). + +Table \ref{tab:completenessTopLevelTypes} summarizes the translations for top-level concepts, changes of variables and basic types. Some variable change properties are common such as validating variable re-assignments or handling variable change by forward reasoning are listed here and apply to all further concepts. Handing constraint variable changes depends on the context of the variable - here top-level variables only. + +Table \ref{tab:completenessCompounds} provides an overview on the possible combinations and transformations for compound types, here in particular including nested constraints, nested annotation assignments, eval blocks, but also changes of constraint slots and changing the actual type of a compound variable. + +Table \ref{tab:completenessContainers} summarizes the transformations and tests for containers, in particular also regarding the specific handling of containers consisting of compounds as well as containers consisting of constraints. + +Finally, Table \ref{tab:completenessAnnotations} indicates the transformation paths for annotations. Here, the possible combinations are limited as annotations cannot be recursive, cannot have nested annotation assignments or eval-blocks. + \begin{table*}[!h] @@ -13,9 +26,9 @@ \hline -Decision variable & 2.1.4 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \textit{all} \\ +Decision variable & 2.1.4 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \textit{*} \\ Constraint & 2, 3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelConstraints} & B2, ...\\ -Constraint variable & 3.1.10 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd}, change \tabAlg{algVarChange}\TBD{addLine} & Cs1, Cs2, CsCtCn1 \\ +Constraint variable & 3.1.10 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} & Cs1, Cs2, CsCtCn1 \\ 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\\ @@ -26,7 +39,13 @@ Partial evaluation & 2.2.5.3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelEvals} & Ev1\\ -Interfaces & 2.2.4.3 & no specific support needed & If1, If2\\ - -re-assignment & 2.1.4, 3.1.4 & \tabAlgLine{algVarChange}{algVarChangeScope}, \tabAlgLines{algEvalLoop}{algEvalLoopClearScope}{algEvalLoopSetScope} & Sc1, Sc2, Sc3\\ +Interfaces & 2.2.4.3 & no support needed & If1, If2\\ + +\hline + +Re-assignment & 2.1.4, 3.1.4 & \tabAlgLine{algVarChange}{algVarChangeScope}, \tabAlgLines{algEvalLoop}{algEvalLoopClearScope}{algEvalLoopSetScope} & Sc1, Sc2, Sc3\\ + +Variable change & - & \tabAlgLines{algVarChange}{algVarChangeRescheduleParents}{algVarChangeRescheduleNested} & \MISSING{prop} \\ + +Constraint variable change & 3.1.10 & \tabAlgLine{algVarChange}{algVarChangeRescheduleConstraintVariables}\tabAlgFollow\tabAlgLines{algRescheduleValueChange}{algRescheduleValueChangeConsStart}{algRescheduleValueChangeConsEnd}\tabAlgFollow\tabAlg{algRescheduleConstraintValue} & \MISSING{Cs1, Cs2, CsCtCn1} \\ \hline @@ -58,11 +77,6 @@ \end{table*} - -To indicate the IVML completeness, we enumerate all relevant IVML concepts, their definition in the IVML specification~\cite{IVML-LS}, the transformation path along the algorithms presented in this document and the test cases validating the transformation and the reasoning results. We separate the argumentation into four parts and present for each path the relation of specification entry, transformation path and test cases in terms of a summarizing table. The four parts are 1) top-level concepts / basic types (Table \ref{tab:completenessTopLevelTypes}), compound types (Table \ref{tab:completenessCompounds}), container types (Table \ref{tab:completenessContainers}) and annotations (Table \ref{tab:completenessAnnotations}). Test cases are referenced by ids in order to indicate that all relevant combinations are subject to regression testing in the continuous build process of EASy-Producer. The referenced test cases are detailed in Appendix \ref{appendixTestCases}. - \pagebreak -\TBD{Check quantized instance constraints.} - \begin{table*}[!h] %\begin{adjustbox}{angle=90} @@ -94,7 +108,7 @@ Container type & 2.1.3.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateContainer}\tabAlgFollow Table \ref{tab:completenessContainers} & CnCt3, CnCt4 \\ -Constraint type & 3.10.1 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd}, change \tabAlg{algVarChange}\TBD{addLine} & CsCn1, CsCn2, CsCtCn1 \\ - -Constraints & & \tabAlgLines{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd}& Cn1, CnCs1 \\ +Constraint type & 3.10.1 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} & CsCn1, CsCn2, CsCtCn1 \\ + +Nested constraints & & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationAll}& Cn1, CnCs1 \\ \IVML{self} & 3.1.6 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf1}, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf2}, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf3} & CnA3 \\ @@ -103,7 +117,13 @@ Assignment blocks & 2.2.2 & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationCompoundAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnAI2, CnAI3 \\ -$\triangleright$ constraints & 2.2.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd} & CnA4 \\ - -Partial evaluation & 2.2.5.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationEvalStart}{algTranslateCompoundDeclarationEvalEnd} & CnEv1 \\ +$\triangleright$ constraints & 2.2.2 & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationAll} & CnA4 \\ + +Partial evaluation & 2.2.5.3 & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationEval} & CnEv1 \\ + +\hline + +Constraint type change & 3.10.1 & \tabAlgLine{algVarChange}{algVarChangeRescheduleConstraintVariables}\tabAlgFollow\tabAlgLines{algRescheduleValueChange}{algRescheduleValueChangeCompStart}{algRescheduleValueChangeCompEnd}\tabAlgFollow\ldots\tabAlgFollow\tabAlgLines{algRescheduleValueChange}{algRescheduleValueChangeConsStart}{algRescheduleValueChangeConsEnd}\tabAlg{algRescheduleConstraintValue} & \MISSING{CsCn1, CsCn2, CsCtCn1} \\ + +Compound type change & - & \tabAlgLine{algVarChange}{algVarChangeRescheduleConstraintVariables}\tabAlgFollow\tabAlgLine{algRescheduleValueChange}{algVarChangeRescheduleValueTypeChange}\tabAlgFollow\tabAlg{algTranslateValueTypeChange}\tabAlgFollow\ldots & \MISSING{!} \\ \hline @@ -116,16 +136,14 @@ \pagebreak -\TBD{No annotation, assignment blocks and partial evaluation possible from IVML syntax. Accessor-based access handled by \tabAlg{algTranslateDeclaration}.} - -\begin{table*}[!h] -%\begin{adjustbox}{angle=90} -\centering -\begin{tabular}{|p{3cm}|r||p{6cm}|p{3cm}|} +\begin{table*}[!h] +%\begin{adjustbox}{angle=90} +\centering +\begin{tabular}{|p{3cm}|r||p{4cm}|p{3cm}|} \hline \textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation Path} & \textbf{Test}\\ \hline -% \multicolumn{4}{|c|}{Compound types}\\ % disabled due to page break/moving tables to the end -%\hline + \multicolumn{4}{|c|}{Container types}\\ % disabled due to page break/moving tables to the end +\hline Integer type & 2.1.3.1 & no action in \tabAlg{algTranslateContainerDeclaration}, cf. Sect. \ref{sectNotationOthers} & ICt1, ICt2\\ @@ -141,9 +159,9 @@ Derived type & 2.1.3.4 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes}\tabAlgFollow\tabAlg{algTranslateDeclaration} & ITCt1, ITCt2 \\ -Compound type & 2.1.3.5 & \tabAlgLines{algTranslateContainerDeclaration}{algTranslateContainerDeclarationCompoundContainerStart}{algTranslateContainerDeclarationCompoundContainerEnd}\tabAlgFollow\tabAlgLines{algTranslateCompoundContainer}{algTranslateDefaultsCompoundContainerMapping}{algTranslateDefaultsCompoundContainerContent}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & CnCt3, CnCt4 \\ +Compound type & 2.1.3.5 & \tabAlgLines{algTranslateContainerDeclaration}{algTranslateContainerDeclarationCompoundContainerStart}{algTranslateContainerDeclarationCompoundContainerEnd}\tabAlgFollow\tabAlgLines{algTranslateCompoundContainer}{algTranslateCompoundContainerMapping}{algTranslateCompoundContainerContent}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & CnCt3, CnCt4 \\ Derived compound type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes} \tabAlgFollow \tabAlg{algTranslateDerivedDatatypeConstraints} & ITCnCt1, ITCnCt2 \\ -Container type & 2.1.3.3 & \tabAlgLines{algTranslateContainerDeclaration}{algTranslateContainerDeclarationCompoundContainerStart}{algTranslateContainerDeclarationCompoundContainerEnd}\tabAlgFollow\tabAlgLines{algTranslateCompoundContainer}{algTranslateDefaultsCompoundContainerMapping}{algTranslateDefaultsCompoundContainerContent}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & CnCt2, CtTF1 \\ +Container type & 2.1.3.3 & \tabAlgLines{algTranslateContainerDeclaration}{algTranslateContainerDeclarationCompoundContainerStart}{algTranslateContainerDeclarationCompoundContainerEnd}\tabAlgFollow\tabAlgLines{algTranslateCompoundContainer}{algTranslateCompoundContainerMapping}{algTranslateCompoundContainerContent}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & CnCt2, CtTF1 \\ Derived container type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CtTCt1, CtTF1 \\ @@ -151,5 +169,5 @@ Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & CnFCt1, CnTFCt1 \\ -Constraint type & 3.1.10 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationConstraintContainer}, change \tabAlg{algVarChange}\TBD{addLine} & CnCt1, CnCt2, CsCtCn1 \\ +Constraint type & 3.1.10 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationConstraintContainer} & CnCt1, CnCt2, CsCtCn1 \\ Annotation & 2.2.2 & top-level only, see Table \ref{tab:completenessTopLevelTypes} & TFCnCtCsA1 \\ @@ -158,4 +176,8 @@ Partial evaluation & - & - & - \\ + +\hline + +Constraint type change & 3.1.10 & change \tabAlgLine{algVarChange}{algVarChangeRescheduleConstraintVariables}\tabAlgFollow\tabAlgLines{algRescheduleValueChange}{algRescheduleValueChangeCompStart}{algRescheduleValueChangeCompEnd}\tabAlgFollow\ldots\tabAlgFollow\tabAlgLines{algRescheduleValueChange}{algRescheduleValueChangeContStart}{algRescheduleValueChangeContEnd}\tabAlg{algRescheduleConstraintValue} & \MISSING{CnCt1, CnCt2, CsCtCn1} \\ \hline @@ -168,14 +190,12 @@ \pagebreak -\TBD{Recursive annotations are not supported by IVML, add section number below. A*1 means all annotation-related tests, which focus on one specifc type used in the annotation, e.g., ACn1 for a compound used in an annotation, but always applied to all relvant types.} - -\begin{table*}[!h] -%\begin{adjustbox}{angle=90} -\centering -\begin{tabular}{|p{2.5cm}|r||p{4cm}|p{2cm}|p{2cm}|} +\begin{table*}[!h] +%\begin{adjustbox}{angle=90} +\centering +\begin{tabular}{|p{2.5cm}|r||p{4cm}|p{1,5cm}|p{1,5cm}|} \hline \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}{algTranslateAnnotationDeclarationsTranslateDeclV} or \tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclD} cf. see Table \ref{tab:completenessTopLevelTypes})}\\ + \multicolumn{5}{|c|}{Annotations}\\ \hline @@ -208,10 +228,8 @@ \hline \end{tabular} -\caption{Translation of annotations starting with \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}} +\caption{Translation of annotations starting with \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationAnnotationDefault}\tabAlgFollow\tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclV} or \tabAlgLine{algTranslateAnnotationDeclarations}{algTranslateAnnotationDeclarationsTranslateDeclD}} %\end{adjustbox} \label{tab:completenessAnnotations} \end{table*} -\TBD{annotation on typedef-ref, ref-typedef, variable on typedef-ref, ref-typedef} - -\pagebreak +\clearpage Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 165) +++ /reasoner/notation.tex (revision 166) @@ -272,4 +272,5 @@ $$deref(s)=\setWith{s\in t}{deref(t)}$$ % +IVML project interfaces impose variable visibilities and access restrictions among imported projects. Thus, project interfaces represent static structural properties that must be handled while creating the IVML project, i.e., project interfaces are transparent to the reasoner and do not need to be considered during reasoning. \subsubsection{IVML Values}\label{sectNotationValues}