Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 108) +++ /reasoner/reasoner.tex (revision 109) @@ -135,5 +135,7 @@ \subsubsection{Variable Declarations} -An IVML \emph{variable declaration} $d$ specifies a variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$ and $isAnnotation(d)$ returns whether a variable declaration is an annotation. For an arbitrary model element $e$ (including type definitions, projects and variable declarations), $parent(e)$ returns the parent model element and $isAssngBlock(e)$ returns whether $e$ is an assignment block. +An IVML \emph{variable declaration} $d$ specifies a variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. $isDeclaration(d)$ is true for a variable declaration $d$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$ and $isAnnotation(d)$ returns whether a variable declaration is an annotation. Let $annotation(d, n) = a$ if $a\in annotations(d) \wedge name(a)=m$, else $annotation(d, n) = \undef$. +% +For an arbitrary model element $e$ (including type definitions, projects and variable declarations), $parent(e)$ returns the parent model element and $isAssngBlock(e)$ returns whether $e$ is an assignment block. \subsubsection{Configuration Variables}\label{sectNotationConfigVars} @@ -157,5 +159,5 @@ \end{multline*} % -Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and $\allowbreak{}annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations potentially inherited from containing project or variables (in case of compounds or containers). +Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and $\allowbreak{}annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations potentially inherited from containing project or variables (in case of compounds or containers). Variables can be \emph{local}, e.g., as specified in the IVML model used as parameters of a user-defined constraint function, within let-expression or as collection iterator. Such variables have the same properties as usual configuration variables and can be identified using $isLocal(v)$, which then returns $true$. @@ -178,5 +180,5 @@ \subsubsection{Project} -A \emph{project} is a named scope, which can contain variable declarations, type declarations, assignment-blocks and eval-blocks. $varDeclarations(p)$ denotes the set of all variable declarations introduced in project $p$. +A \emph{project} is a named scope, which can contain variable declarations, type declarations, assignment-blocks and eval-blocks. $varDeclarations(p)$ denotes the set of all variable declarations introduced in project $p$. $isProject(p)$ returns $true$ for a project $p$. $evals(p)$ is the set of (potentially nested) \emph{eval-blocks} in project $p$, i.e., if $e\in evals(p)$ then $constraints(e)$ is defined, but may be empty, similarly for $evals(e)$. @@ -197,4 +199,17 @@ &constraints(a) \cup \setWith{allAssignmentConstraints(b)}{b \in assignments(a)} \end{align*} +% +Sometimes it is convenient to refer to a project as a pseudo-variable (of type \textit{Project}) with nested variables and annotations (declared for all contained variables). $variable(p)$ returns the declartion of this pseudo-variable for a given project $p$. Using this pseudo-variable, we can define how to find an attribute declaration with name $n$ that is directly attributed to variable $v$ or one of the containing scopes of $v$: +% +\begin{multline*} +findAnnotation(v, n) = \begin{cases} + annotation(v, n), &\text{if } annotation(v, n) \neq \undef\\ + findAnnotation(parent(v), n), &\text{if } isVariable(parent(v))\\ + findAnnotation(variable(parent(v)), n), &\text{if } isProject(parent(v))\\ + \undef, & \text{else} \\ + \end{cases} +\end{multline*} +% +returns the innermost annotation for $v$ with name $n$. % \subsubsection{Constraints}\label{sectNotationConstraints} @@ -311,7 +326,11 @@ For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ returns the type $t$ is derived from. -For specifying constraints, a derived type $t$ implicitly declares a variable $decl(t)$ of type $base(t)$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define -% -$$allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge base(t) = \undef \\ \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$$ +For specifying constraints, a derived type $t$ implicitly declares a variable $decl(t)$ of type $base(t)$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type $base^*(t)$ is relevant. +% +$$base^*(t) = \begin{cases}base(t), & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ base^*(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t)) \\ \undef, & \text{else}\\ \end{cases}$$ +% +For constraint translation in reasoning it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define +% +$$allBase(t) = \begin{cases}\set{base(t)}, & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ \set{base(t)} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ \emptySet, & \text{else}\\ \end{cases}$$ % \subsection{Other IVML Types}\label{sectNotationOthers} @@ -432,4 +451,8 @@ \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. + \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}. + \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type rather and avoids applying them some nested type. + \item $getCurrentType(\variableMapping)$ returns the type $t$ stored in the current contect by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happend on the current context. + \item $isTypeExcluded(t)$ returns whether $t$ is excluded in the current context. \item $size(\variableMapping)$ the number of contexts on the stack. There is at least always one context on the stack representing the containing project. \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project. @@ -648,6 +671,5 @@ 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} 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. 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. +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$\footnote{For optimizing constraint rescheduling (see Section \ref{sectTopLevelConstraintsRescheduling}), the algorithm applies type exclusions to the actual context by transferring them and storing the causing type $t$ in the current context}. Used types are registered only if there is no variable $v$ given, e.g., we process constraints according to a potentially recursive type structure. 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 Algorithm \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithm \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. As the context with the compound mapping is only valid during Algorithm \ref{algRegisterCompoundMapping}, default value expressions must be translated within the actual context, i.e., if $deflt$ has been passed in, lines \ref{algTranslateCompoundSubstStart}-\ref{algTranslateCompoundSubstEnd} perform the respective substitution, which will be returned as result of Algorithm \ref{algRegisterCompoundMapping}. Finally, Algorithm \ref{algTranslateCompoundDeclaration} removes the actual context frame for this compound from $\variableMapping$. @@ -661,4 +683,5 @@ $recordProcessed(\variableMapping, t)$\; $pushContext(\variableMapping, d, v \neq \undef)$\; + $transferTypeExcludes(\variableMapping, t)$\; $e \assng \createExpression{d}$\; $registerCompoundMapping(t, ca, e, type(value(v)))$\; @@ -675,5 +698,9 @@ Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The compound type $t_c$ indicates the type to be processed, i.e., where to take slot and annotation definitions from. The access expressions $ca$ is optional as usual and, if given, utilized as prefix to create access expressions for slots and annotations. Finally, a target type $t_t$ is given if the access via $ca_s$ or $ca_t$ requires a type cast so that specific slots of $t_t$ can be accessed. Type casts are required if if the actual value is of a refined type of $t_c$, as otherwise slots defined on the more specific type are not accessible and access is rejected by static type checking of IVML expressions. -Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t_c$ and creates for each slot a respective accessor. If a preceding compound access expression for the slots $ca_s$ is not given, it creates a static accessor based on $v$. If an accessor is given, we create an accessor based on $ca_s$ and include a type cast to $t_t$\footnote{The type cast can be omitted if $t=type(value(v))$. This is done by the implementation, but not detailed here as a type cast to the actual type does not have an effect.}. The created accessor is then registered with $\variableMapping$. Similarly, we iterate over all annotations for the current slot, create an accessor expression based on $ca_a$ and register the result with $\variableMapping$. +Let +% +$$slots^-(t) = \setWith{s \in slots(t)}{\neg isTypeExcluded(\variableMapping, type(parent(s)))} $$ +% +be the slots of $t$ for which the containing type is not excluded \footnote{Excluded types only occur as an optimization in constraint re-scheduling (cf. Section \ref{sectTopLevelConstraintsRescheduling}} in the actual context of $\variableMapping$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t_c$ and creates for each slot a respective accessor. If a preceding compound access expression for the slots $ca_s$ is not given, it creates a static accessor based on $v$. If an accessor is given, we create an accessor based on $ca_s$ and include a type cast to $t_t$\footnote{The type cast can be omitted if $t=type(value(v))$. This is done by the implementation, but not detailed here as a type cast to the actual type does not have an effect.}. The created accessor is then registered with $\variableMapping$. Similarly, we iterate over all annotations for the current slot, create an accessor expression based on $ca_a$ and register the result with $\variableMapping$. \begin{algorithm}[H] @@ -683,10 +710,10 @@ \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t_c)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} - $registerMapping(\variableMapping, s, x)$\; - \ForAll{$a \iterAssng annotations(s)$}{ - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t, a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping} - $registerMapping(\variableMapping, a, x)$\; - } + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} + $registerMapping(\variableMapping, s, x)$\; + \ForAll{$a \iterAssng annotations(s)$}{ + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t, a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping} + $registerMapping(\variableMapping, a, x)$\; + } }\label{algRegisterCompoundMappingVarMappingEnd} @@ -694,5 +721,5 @@ \end{algorithm} -Given a complete mapping for a compound type, we can apply Algorithm \ref{algTranslateCompoundContent}. The algorithm performs a transitive / recursive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} if $v$ is defined ($slots(v)$ also includes all slots for $v$) or all slots for type$t$. It is important to note that in both cases, the second occurs in container translations, we call Algorithm \ref{algTranslateDeclaration}, which dispatches for all types and also considers annotations. +Given a complete mapping for a compound type, we can apply Algorithm \ref{algTranslateCompoundContent}. The algorithm performs a transitive / recursive translation of the default values of all (not excluded) slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} if $v$ is defined ($slots(v)$ also includes all slots for $v$\footnote{This also holds for $slots^-(v)$ if the parent type of $v$ is not excluded.}) or all 8not excluded) slots for type$t$. It is important to note that in both cases, the second occurs in container translations, we call Algorithm \ref{algTranslateDeclaration}, which dispatches for all types and also considers annotations. In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression for self, i.e., the access expression $ca$ if given or the declaration $d$. Then, due to their specific priorities, we first translate all eval constraints defined along the type hierarchy for $t$ in lines \ref{algTranslateCompoundDeclarationEvalStart}-\ref{algTranslateCompoundDeclarationEvalEnd}. Afterwards, we include all remaining compound constraints, i.e., type constraints and annotation constraints in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd}. @@ -704,9 +731,9 @@ \uIf{$v\neq\undef$}{\label{algTranslateCompoundDeclarationTranslateSlotsStart} - \ForAll{$s \iterAssng slots(v)$ } { - $translateDeclaration(s, decision(v, s), \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsV} - } + \ForAll{$s \iterAssng slots^-(v)$} { + $translateDeclaration(s, decision(v, s), \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsV} + } } \Else { - \ForAll{$s \iterAssng \setWithFlat{slots(u)}{u\in allRefines^+(t)}$ } { + \ForAll{$s \iterAssng \setWithFlat{slots^-(u)}{u\in allRefines^+(t)}$ } { $translateDeclaration(s, \undef, \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsT} } @@ -749,5 +776,5 @@ $pushContext(\variableMapping, false)$\; - $t_n \assng nested(t); t_b \assng base(t_n); used\assng\emptySet$\; + $t_n \assng nested(t); t_b \assng base^*(t_n); used\assng\emptySet$\; $val\assng relevantValue(d, v, inc)$\; \uIf{$isConstraint(t_b)$} { @@ -855,5 +882,5 @@ In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those orthogonal 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. -The first transformation pattern for the direct translation of annotations is the second pattern from Section \ref{sectTranslationDeclarationTypesDefaults}. More specifically, Algorithm \ref{algTranslateDeclaration} from \ref{sectTranslationDeclarationTypesDefaults} calls the algorithms in this section, which in turn call Algorithm \ref{algTranslateDeclaration}, i.e., the algorithms here prepare the application of Algorithm \ref{algTranslateDeclaration} by composing specific accessor expressions. The second pattern relates to annotation blocks, i.e., specific assignment constraints (accessor expression $ca$ is determined by the top-level or compound context of the annotation block) is created for the variables declared in the assignment block for values mentioned in the assignment data (clause). It is important to note that annotation blocks may be nested in order to indicate orthogonal annotations, i.e., the constraint translation mist take this nesting and the respective precedence of the assignment data due to their nesting into account. +The first transformation pattern for the direct translation of annotations is the second pattern from Section \ref{sectTranslationDeclarationTypesDefaults}. More specifically, Algorithm \ref{algTranslateDeclaration} from \ref{sectTranslationDeclarationTypesDefaults} calls the algorithms in this section, which in turn call Algorithm \ref{algTranslateDeclaration}, i.e., the algorithms here prepare the application of Algorithm \ref{algTranslateDeclaration} by composing specific accessor expressions. The second pattern relates to annotation blocks, i.e., specific assignment constraints (accessor expression $ca$ is determined by the top-level or compound context of the annotation block) is created for the variables declared in the assignment block for values mentioned in the assignment data (clause). It is important to note that annotation blocks may be nested in order to indicate orthogonal annotations, i.e., the constraint translation must take this nesting and the respective precedence of the assignment data due to their nesting into account. \grayPara{ @@ -872,10 +899,10 @@ \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) \wedge size(\variableMapping) > 1\\ ca, &\text{else}}$\; + $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } qualifyAnnotation(v, a, ca)\\ 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) \wedge size(\variableMapping) > 1\\ ca, &\text{else}}$\; + $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } qualifyAnnotation(v, a, ca)\\ ca, &\text{else}}$\; $translateDeclaration(a, \undef, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD} } @@ -887,9 +914,17 @@ \end{algorithm} +with +% +\begin{align*} +qualifyAnnotation(v, a, & ca) = ca \neq \undef \wedge \neg isContextRegistering(\variableMapping) \wedge \\ &(size(\variableMapping) > 1 \vee isCompound(base^*(type(v)))) +\end{align*} +% +which requests creating an extended accessor expression if we are translating a nested annotation block (implying context registering) or if we are translating an annotation of a compound type. + 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 top-level 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}. +, the algorithm creates the respective constraints by creating a specific access expression according to $qualifyAnnotation(v, a, ca)$ 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}. We turn now to the translation of annotation assignment-blocks. In IVML, an assignment-block is used on top-level or within compounds to declare compound slots with an implicit assignment of a value to each declared annotation. Further, assignment-blocks can be nested and the assignments defined for the outer blocks must be applied also to the inner blocks. @@ -938,5 +973,5 @@ translate&AnnotationAssignment(a, d, ca) = \\ \createConstraint{\IVML{assign}&(\IVMLMeta{ann}(\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}, \\ - &annotation(d, name(a))), \varSubstitutionSelfVarMapping{default(a)}{ca})} + &findAnnotation(d, name(a))), \varSubstitutionSelfVarMapping{default(a)}{ca})} \end{align*} @@ -1093,4 +1128,6 @@ Partial evaluation & 2.2.5.3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelEvals} & Ev1\\ +Interfaces & 2.2.4.3 & no specific support needed & If1, If2\\ + \hline \multicolumn{4}{|c|}{Non-complex types (typed decision variable, starting in \tabAlg{algTranslateDeclaration})}\\ @@ -1360,4 +1397,5 @@ T & Typedef\\ F & Reference\\ +If & Interface\\ \hline \end{tabular} @@ -1411,4 +1449,19 @@ SCt1 & \class{string/StringInContainerAssignTest.ivml}\\ SCt2 & \class{string/StringInContainerDefaultsTest.ivml}\\ +\hline +\end{tabular} +\caption{Reasoner test cases for basic types combined with compounds or containers.} +\label{tab:reasonerTestCasesBasics} +%\end{adjustbox} +\end{table*} +\footnotetext{A similar test is defined for all basic types.} + +\begin{table*}[h] +%\begin{adjustbox}{angle=90} +\centering +\begin{tabular}{|l|p{12cm}|} +\hline +\textbf{Id} & \textbf{Test model}\\ +\hline E1 & \class{enums/EnumDefaultsTest.ivml}\\ E2 & \class{enums/EnumAssignTest.ivml}\\ @@ -1419,19 +1472,4 @@ ECt1 & \class{enums/EnumInContainerDefaultsTest.ivml}\\ ECt2 & \class{enums/EnumInContainerAssignTest.ivml}\\ -\hline -\end{tabular} -\caption{IVML reasoner test cases for basic types combined with compounds or containers.} -\label{tab:reasonerTestCasesBasics} -%\end{adjustbox} -\end{table*} -\footnotetext{A similar test is defined for all basic types.} - -\begin{table*}[h] -%\begin{adjustbox}{angle=90} -\centering -\begin{tabular}{|l|p{12cm}|} -\hline -\textbf{Id} & \textbf{Test model}\\ -\hline CnCt1 & \class{collectionConstraints/constraintSetDefault.ivml}\\ CnCt2 & \class{collectionConstraints/constraintSetSetDefault.ivml}\\ @@ -1464,4 +1502,21 @@ Cn3 & \class{compounds/CompoundCompoundTest2.ivml}\protect\footnotemark\\ CnTF1 & \class{collectionConstraints/RefernceDerivedCompoundTest.ivml}\\ +\hline +\end{tabular} +\caption{Reasoner test cases for advanced concepts and types (part 1).} +\label{tab:reasonerTestCasesAdvanced} +%\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.} + +\begin{table*}[h] +%\begin{adjustbox}{angle=90} +\centering +\begin{tabular}{|l|p{12cm}|} +\hline +\textbf{Id} & \textbf{Test model}\\ +\hline A1 & \class{attributes/DefaultAssign.ivml}\\ A2 & \class{attributes/IndividualAssign.ivml}\\ @@ -1477,13 +1532,13 @@ Ev1 & \class{evals/SimpleEval.ivml}\\ CnEv1 & \class{evals/CompoundEval.ivml}\\ +If1 & \class{interfaces/Frozen.ivml}\\ +If2 & \class{interfaces/Unfrozen.ivml}\\ \hline \end{tabular} -\caption{IVML reasoner test cases for advanced concepts and types.} -\label{tab:reasonerTestCasesAdvanced} +\caption{Reasoner test cases for advanced concepts and types (part 2).} +\label{tab:reasonerTestCasesAdvanced2} %\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}