Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 94) +++ /reasoner/reasoner.tex (revision 95) @@ -384,8 +384,11 @@ \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 $pushContext(\variableMapping, d)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration is enabled, the new frame will be registered with the parent frame for $var$ (unless $var=\undef$). + \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}. \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the containing IVML project, is not removed by this operation. \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variabe declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$. - \item $getMapping(\variableMapping, d)=\variableMapping[d]$ returns the mapping for $d$. If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping was registered at all, the result is $\undef$. + \item $getMapping(\variableMapping, d)=\variableMapping[d]$ returns the mapping for $d$. If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. + \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If $isCompound(t)$, this function performs a registration for $allRefined^+(t)$. + \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered in one of the enclosing contexts. \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ from the current context frame. As long as the current context frame exists, this operation can be called over and over. If no context frame is registered for $d$, the stack is not modified. \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists. @@ -592,5 +595,7 @@ A compound can define constraints in several places, namely through types and defaults of its slots and annotations (including constraint variables as well as refined slots and annotations), as constraints listed directly within a compound, within assignment-blocks or within eval-blocks. For slots and annotations we can resort to Algorithm \ref{algTranslateDeclaration}, i.e., compound types, derived types, constraint variables and collections, while for the remaining constraints, we must visit these structures, instantiate and collect the respective constraints. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. In particular, if the IVML keyword \IVMLself{} is used within a constraint, it must be substituted by the actual variable of the respective compound type. Moreover, it is important to recall that a variable $v$ of type $type(v)$ can contain instances of any refined type $allRefines^+(t)$, and in this case the translation must consider the default values of the potentially larger slot, additional constraints and nested structures. -Algorithm \ref{algTranslateCompoundDeclaration} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} creates a context frame and pushes it onto the variable mapping stack $\variableMapping$. The main two steps are detailed in Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithms \ref{algRegisterCompoundMapping} registers all compound slots and annotations in the variable mapping, using $ca$ or $d$ as basis for access expressions for slots and annotations and casts to the type of the actual value in $v$ if available (else $\undef$ is passed in as argument). Now Algorithm \ref{algTranslateCompoundContent} can translate the entire compound content including slots, annotations, constraints, annotation-blocks and eval-blocks. Finally, Algorithm \ref{algTranslateCompoundDeclaration} pops the context frame for this compound from $\variableMapping$. +Algorithm \ref{algTranslateCompoundDeclaration} collects and translates the constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). No translation happens if type $t$ was already processed, e.g., in case of recursive compound types. The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} creates a context frame and pushes it onto the variable mapping stack $\variableMapping$. Used types are registered only if there is no variable $v$ given, e.g., we process constraints according to a potentially recursive type structure. In contrast, if a variable $v$ is given, the nested variables are initialized correctly, in particular recursively nested variables terminate correctly based on configured values, i.e., we do not have to take care of recursion in this case. + +The main two steps are detailed in Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithms \ref{algRegisterCompoundMapping} registers all compound slots and annotations in the variable mapping, using $ca$ or $d$ as basis for access expressions for slots and annotations and casts to the type of the actual value in $v$ if available (else $\undef$ is passed in as argument). Now Algorithm \ref{algTranslateCompoundContent} can translate the entire compound content including slots, annotations, constraints, annotation-blocks and eval-blocks. Finally, Algorithm \ref{algTranslateCompoundDeclaration} pops the context frame for this compound from $\variableMapping$. \begin{algorithm}[H] @@ -599,10 +604,12 @@ \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} - $pushContext(\variableMapping, d)$\; - $e \assng \createExpression{d}$\; - $registerCompoundMapping(t, ca, e, type(value(v)))$\; - $translateCompoundContent(d, v, t, ca)$\; - $popContext(\variableMapping)$; - + \If{$\neg alreadyProcessed(\variableMapping, t)$} { + $recordProcessed(\variableMapping, t)$\; + $pushContext(\variableMapping, d, v \neq \undef)$\; + $e \assng \createExpression{d}$\; + $registerCompoundMapping(t, ca, e, type(value(v)))$\; + $translateCompoundContent(d, v, t, ca)$\; + $popContext(\variableMapping)$; + } \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} \end{algorithm} @@ -670,4 +677,5 @@ \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$} + $pushContext(\variableMapping, false)$\; $t_n \assng nested(t); t_b \assng base(t_n); used\assng\emptySet$\; $val\assng relevantValue(d, v, inc)$\; @@ -693,4 +701,5 @@ $translateDerivedDatatypeConstraints(t_n, d)$\; \label{algTranslateContainerDeclarationDerivedTypes} } + $popContext(\variableMapping)$\; \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration} \end{algorithm} @@ -706,5 +715,7 @@ Thus, the core idea of this algorithm is to consider all elements over all used types. If no value is available, we resort to the static type of the declaration of the containser variable. We create all-quantized constraints for all used types and distinguish between constraint containers, where the values directly turn into constraints, compound containers, where slots, constraints and annotations lead to further constraints, and derived types. -Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). First, we determine the innermost nested type $t_n$ and its base type $t_b$ (i.e., ignoring intermediate derived types) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the used types. If there is a value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault} and prune more general refined types in line \ref{algTranslateContainerDeclarationUsedTypesPrune}, as the following algorithm must anyway iterate over the refinement hierarchy. If there is no value, the only used type is the innermost nested base type $t_b$, actually a compound (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). The, we iterate over all (pruned) used types and apply Algorithm \ref{algTranslateCompoundContainer}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}. +Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). However, if $isCompound(t)$ and $t$ is also recursively used as slot type, Algorithm \ref{algTranslateContainerDeclaration} may cause an endless recursion. Thus, we translate constraints for $t$ only if $t$ was not already processed as flattening of the container elements used below requires considering each used type exactly once. + +For translating constraints, we first determine the innermost nested type $t_n$ and its base type $t_b$ (i.e., ignoring intermediate derived types) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the used types. If there is a value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault} and prune more general refined types in line \ref{algTranslateContainerDeclarationUsedTypesPrune}, as the following algorithm must anyway iterate over the refinement hierarchy. If there is no value, the only used type is the innermost nested base type $t_b$, actually a compound (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). The, we iterate over all (pruned) used types and apply Algorithm \ref{algTranslateCompoundContainer}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}. Algorithm \ref{algTranslateCompoundContainer} creates constraints for compound values utilized in compounds, e.g., through a container initialize, in IVML like \IVML{seq = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{seq} is a sequence of compounds, which have an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no default value constraints, nested constraints, annotation assignments etc. are scheduled to the constraint base, i.e., these compounds would remain uninitialized and their constraints not considered. @@ -714,7 +725,11 @@ \KwIn{declaration $d$, (specific) type $t$, declared type $u$, access $ca$} \KwData{deferred default constraints $\deferredDefaultConstraints$} - $l\assng \createExpression{\IVMLMeta{var}(t)}$\; - - $e\assng\closedCases{ca, & \text{if } ca \neq \undef\\\createExpression{d}, &\text{else}}$\; \label{algTranslateDefaultsCompoundContainerInitE} + + \If{$\neg alreadyProcessed(\variableMapping, t)$}{ + $recordProcessed(\variableMapping, t)$\; + + $l\assng \createExpression{\IVMLMeta{var}(t)}$\; + + $e\assng\closedCases{ca, & \text{if } ca \neq \undef\\\createExpression{d}, &\text{else}}$\; \label{algTranslateDefaultsCompoundContainerInitE} \uIf{$isNested(type(d))$} { $e\assng\createExpression{\IVML{flatten}(d)}$\; \label{algTranslateDefaultsCompoundContainerFlatten} @@ -723,8 +738,10 @@ $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateDefaultsCompoundContainerCast} } - $pushContext(\variableMapping, \undef, e, l)$\; - $registerCompoundMapping(t, l, d, t)$\; \label{algTranslateDefaultsCompoundContainerMapping} - $translateCompoundContent(l, \undef, t, ca)$\; \label{algTranslateDefaultsCompoundContainerContent} - $popContext()$\; + + $pushContext(\variableMapping, \undef, e, l, true)$\; + $registerCompoundMapping(t, l, d, t)$\; \label{algTranslateDefaultsCompoundContainerMapping} + $translateCompoundContent(l, \undef, t, ca)$\; \label{algTranslateDefaultsCompoundContainerContent} + $popContext()$\; + } \caption{Translating constraints for compound containers (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} \end{algorithm} @@ -924,9 +941,9 @@ Constraint & 2, 3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelConstraints} & B2, ...\\ -Constraint variable & 3.1.10 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} & \MISSING{!} \\ +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\\ -Assignment block & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelAnnotationAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnA1, CnA2, CnA3 \\ +Assignment block & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelAnnotationAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnAI1 \\ Partial evaluation & 2.2.5.3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelEvals} & Ev1, Ev2 \MISSING{prio?}\\ @@ -946,5 +963,5 @@ Enum type & 2.1.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & E1, E2\\ -Reference type & 2.2.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & BR1, ER1\\ +Reference type & 2.2.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & BF1, EF1\\ Derived type & 2.1.3.4 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} @@ -987,19 +1004,19 @@ Derived type & 2.1.3.4 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CnTCt1, CnTCt2 \\ -Compound type & 2.1.3.5 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateCompound}\tabAlgFollow\tabAlg{algTranslateCompoundDeclaration} $\ldots$ & \TBD{tests} \\ - -Container type & 2.1.3.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateContainer}\tabAlgFollow Table \ref{tab:completenessContainers} & \TBD{tests} \\ - -Reference type & 2.2.3.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & RCn1, \TBD{tests} \\ +Compound type & 2.1.3.5 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateCompound}\tabAlgFollow\tabAlg{algTranslateCompoundDeclaration} $\ldots$ & Cn2, Cn3 \\ + +Container type & 2.1.3.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateContainer}\tabAlgFollow Table \ref{tab:completenessContainers} & CnCt3, CnCt4 \\ + +Reference type & 2.2.3.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & FCn1, FCn2, FCn3 \\ Constraint type & 3.10.1 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} & CsCn1, CsCn2 \\ -Constraints & & \tabAlgLines{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd}&\TBD{tests}\\ - -Annotation & 2.2.2 & top-level see Table \ref{tab:completenessTopLevelTypes}, nested usage \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & \TBD{tests}\\ - -Assignment blocks & 2.2.2 & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationCompoundAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & \TBD{tests} \\ - -Partial evaluation & 2.2.5.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationEvalStart}{algTranslateCompoundDeclarationEvalEnd} & \TBD{tests} \\ +Constraints & & \tabAlgLines{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd}& Cn1 \\ + +Annotation & 2.2.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$, cf. Table \ref{tab:completenessTopLevelTypes} & CnA3\\ + +Assignment blocks & 2.2.2 & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationCompoundAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnAI2, CnAI3 \\ + +Partial evaluation & 2.2.5.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationEvalStart}{algTranslateCompoundDeclarationEvalEnd} & \TBD{missing tests} \\ \hline @@ -1037,19 +1054,17 @@ 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$ & \TBD{tests} \\ - -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$ & \TBD{tests} \\ - -Derived Container Type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & \TBD{tests} \\ - -Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & \TBD{tests} \\ - -Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers} \TBD{constraint value} & \TBD{tests}\\ - -Constraint Container& 3.1.10 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationConstraintContainer}\TBD{??} & \TBD{CnCt1, CnCt2} \\ - -Derived Constraint Container& 3.1.10 & \TBD{??} & \TBD{tests} \\ +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 \\ + +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, CnTCt2 \\ + +Derived container type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CtTCt1 \\ + +Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & CnFCt1 \\ + +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}\\ @@ -1073,40 +1088,40 @@ %\begin{adjustbox}{angle=90} \centering -\begin{tabular}{|p{4cm}|r||p{6cm}|p{3cm}|} -\hline -\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation Path} & \textbf{Test}\\ -\hline - \multicolumn{4}{|c|}{Annotations}\\ -\hline - -Integer type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} \\ - -Real type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} \\ - -Boolean type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} \\ - -String type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests} \\ - -Enum type & 2.1.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateAnnotationAccess}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \TBD{tests}\\ - -Derived type & 2.1.3.4 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & \TBD{tests} \\ - -Compound type & 2.1.3.5 & \TBD{??} & \TBD{tests} \\ - -Container type & 2.1.3.3 & \TBD{??} & \TBD{tests} \\ - -Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & \TBD{tests} \\ - -Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers}& \TBD{tests} \\ - -Annotation & - & - & - \\ - -Assignment blocks & - & - & - \\ - -Partial evaluation & - & - & - \\ +\begin{tabular}{|p{4cm}|r||p{4cm}|p{2.5cm}|p{2.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}{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}\\ + +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 \\ + +Container type & 2.1.3.3 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateContainer}\tabAlgFollow\tabAlg{algTranslateContainerDeclaration}\MISSING{processed where?} & \TBD{tests} & \TBD{tests} \\ + +Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & \TBD{tests} & \TBD{tests} \\ + +Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers}& \TBD{tests} & \TBD{tests} \\ + +Annotation & - & - & - & -\\ + +Assignment blocks & - & - & - &- \\ + +Partial evaluation & - & - & - &- \\ \hline \end{tabular} -\caption{Translation of annotations, starting top-level in Table \ref{tab:completenessTopLevelTypes}} +\caption{Translation of annotations} %\end{adjustbox} \label{tab:completenessAnnotations} @@ -1192,5 +1207,5 @@ E & Enum\protect\footnotemark\\ T & Typedef\\ -R & Refreence\\ +F & Reference\\ \hline \end{tabular} @@ -1213,5 +1228,5 @@ B2 & \class{boolean/BooleanAssignTest.ivml}\\ B3 & \class{boolean/BooleanImpliesTest.ivml}\\ -BR1 & \class{boolean/BooleanRefAssignTest.ivml\footnote{A similar test is defined for all basic types.}}\\ +BF1 & \class{boolean/BooleanRefAssignTest.ivml\protect\footnotemark}\\ BCo1 & \class{boolean/BooleanInCompoundAssignTest.ivml}\\ BCo3 & \class{boolean/BooleanInCompoundDefaultsTest.ivml}\\ @@ -1241,5 +1256,5 @@ E1 & \class{enums/EnumDefaultsTest.ivml}\\ E2 & \class{enums/EnumAssignTest.ivml}\\ -ER1 & \class{enums/EnumRefAssignTest.ivml}\\ +EF1 & \class{enums/EnumRefAssignTest.ivml}\\ ECo1 & \class{enums/EnumInCompoundDefaultsTest.ivml}\\ ECo2 & \class{enums/EnumInCompoundAssignTest.ivml}\\ @@ -1252,4 +1267,5 @@ %\end{adjustbox} \end{table*} +\footnotetext{A similar test is defined for all basic types.} \begin{table*}[h] @@ -1262,6 +1278,9 @@ CnCt1 & \class{collectionConstraints/constraintSetDefault.ivml}\\ CnCt2 & \class{collectionConstraints/constraintSetSetDefault.ivml}\\ +CnCt3 & \class{compounds/CompoundContainerTest1.ivml}\\ +CnCt4 & \class{compounds/CompoundContainerTest2.ivml}\protect\footnotemark\\ CnTCt1 & \class{collectionConstraints/constraintSetDerivedCompound.ivml}\\ -CnTCt1 & \class{collectionConstraints/constraintSetSetDerivedCompound.ivml}\\ +CnTCt2 & \class{collectionConstraints/constraintSetSetDerivedCompound.ivml}\\ +CtTCt1 & \class{collectionConstraints/setDerivedSet.ivml}\\ ITCn1 & \class{operations/typedefNestedInCompoundValid.ivml}\\ ITCnCt1 & \class{operations/typedefCompoundNestedInSequenceValid1.ivml}\\ @@ -1269,15 +1288,22 @@ ITCt1 & \class{operations/typedefNestedInSequenceValid.ivml}\\ ITCt2 & \class{operations/typedefNestedInSetValid.ivml}\\ -CnA1 & \class{attributes/BlockAssign.ivml}\\ -CnA2 & \class{attributes/BlockAssignNested.ivml}\\ -CnA3 & \class{attributes/BlockAssignNestedConstraint.ivml}\\ -RCn1 & \class{compounds/CompoundRefAssignTest1.ivml}\\ +CnAI1 & \class{attributes/BlockAssign.ivml}\\ +CnAI2 & \class{attributes/BlockAssignNested.ivml}\\ +CnAI3 & \class{attributes/BlockAssignNestedConstraint.ivml}\\ +FCn1 & \class{compounds/CompoundRefAssignTest1.ivml}\\ +FCn2 & \class{compounds/CompoundRefAssignTest2.ivml}\\ +FCn3 & \class{compounds/CompoundRefAssignTest3.ivml}\\ +Cn1 & \class{compounds/CompoundConstraintTest}\\ +Cn2 & \class{compounds/CompoundCompoundTest1.ivml}\\ +Cn3 & \class{compounds/CompoundCompoundTest2.ivml}\protect\footnotemark\\ A1 & \class{attributes/DefaultAssign.ivml}\\ A2 & \class{attributes/IndividualAssign.ivml}\\ A3 & \class{attributes/IndividualAssignNested.ivml}\\ +CnA3 & \class{attributes/CompoundIndividualAssign.ivml}\\ Cs1 & \class{constraintVariables/constraintAssigned.ivml}\\ Cs2 & \class{constraintVariables/constraintDefault.ivml}\\ CsCn1 & \class{constraintVariables/constraintCompoundAssigned.ivml}\\ CsCn2 & \class{constraintVariables/constraintCompoundDefault.ivml}\\ +CnFCt1 & \class{constraintVariables/QM\_constraintOrder.ivml}\\ Ev1 & \class{evals/SimpleEval.ivml}\\ Ev2 & \class{evals/NestedEval.ivml}\\ @@ -1288,4 +1314,7 @@ %\end{adjustbox} \end{table*} +\addtocounter{footnote}{-1} +\footnotetext{This test aims at recursive compound types.}\stepcounter{footnote} +\footnotetext{This test aims at recursive compound types.} \end{appendices}