Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 74) +++ /reasoner/reasoner.tex (revision 75) @@ -77,5 +77,5 @@ Based on our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} and taking into account the specific requirements of default-value logic, project scopes, eval-block scopes), the reasoning mechanism shall directly operate on an IVML model. In particular, model transformations such as the constraint translation shall happen only if required to reduce overhead on the reasoning time. In particular no complete model transformations as we did in previous approaches to maximize reuse of existing reasoning mechanisms is infeasible. After the required constraint translation, constraint evaluation and forward-chaining is executed on this constraint base. As this approach is not reasoning complete (while through construction IVML complete), we can imagine that specific reasoning engines such as SMT could complement the described approach. Therefore, translating the failed constraints into a model that is suitable for sophisticated reasoning approaches could enable advanced capabilities, such as value determination, instance creation or configuration completion / repair. -Typically, reasoning over all variables of a project including all constraints is needed. However, in some use cases considering all constraints is not needed and even not efficient with respect to reasoning time. The first case is \emph{incremental reasoning}, i.e., starting with a given (valid) configuration and just analyzing the changes made by the user. The idea is to provide nearly immediate results, so that reasoning even on complex and large models can happen on every change made by the user. The second case is \emph{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. For these cases, we introduce two main \emph{reasoning modes}, namely full reasoning and incremental reasoning, while the latter can be achieved through the following two techniques. +Typically, reasoning over all variables of a project including all constraints is needed. This may differ for initializing a model through the reasoner (assign first default values in a first round, perform a reasoning round in a second round) as well as in use cases where considering all constraints is explicitly not needed and even not efficient with respect to reasoning time. The first case is \emph{incremental reasoning}, i.e., starting with a given (valid) configuration and just analyzing the changes made by the user. The idea is to provide nearly immediate results, so that reasoning even on complex and large models can happen on every change made by the user. The second case is \emph{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. For these cases, we introduce two main \emph{reasoning modes}, namely full reasoning and incremental reasoning, while the latter can be achieved through the following two techniques. \begin{itemize} \item \emph{Creation of a partial constraint base:} Using this technique, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mechanism can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration. @@ -189,5 +189,5 @@ For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, i.e., for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ -In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We state this by $\IVMLMeta{var}(i, t)$, i.e., create the temporary variable $i$ of type $t$. For a variable $v$ created by \IVMLMeta{var} holds $isLocal(v) = true$. +In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We state this by $\IVMLMeta{var}(i, t)$, i.e., create the temporary variable $i$ of type $t$. For a variable $v$ created by \IVMLMeta{var} holds $isLocal(v) = true$. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. \subsubsection{Compounds}\label{sectNotationCompounds} @@ -264,11 +264,13 @@ $$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ % -to return the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. In some situations, we must identify whether a container consists of constraints, i.e., +to return the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. If a container $isNested(c)$ for a container $c$, $elements(c)$ contains container values of the nested type. Here, $allElements(c)$ returns the transitively flattened elements of the respective container, i.e., set or sequence, i.e., all leaf elements of a depth-first traversal of the containment tree. + +In some situations, we must identify whether a container consists of constraints, i.e., % $$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$$. % -In other situations, we need to know all types that are used in a container (value), i.e., -% -$$usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$$ +In other situations, we need to know all types that are used in a container (value), i.e., the set +% +$$usedTypes(c) = \setWith{contained(type(e))}{e\in allElements(c)}$$ % For containers, access expressions usually occur only if the collection has a compound as nested type and if the collection is a sequence. Then accessing an element by an index happens through the IVML index access function for sequences. For example, \IVML{seq[1]} accesses an indexed element of the sequence \IVML{seq} and the accessor to \IVML{slot} on \IVML{seq[1]} is then the combined expression \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. @@ -286,9 +288,23 @@ $$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}$$ % -\subsection{Other IVML Elements}\label{sectNotationOthers} +\subsection{Other IVML Types}\label{sectNotationOthers} No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real String), the constraint type as well as for enums as IVML does not support modifying these types or does not allow attaching constraints directly to these types. Constraints can be attached indirectly through variable declarations / compound slots or derived types. The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning. In IVML, a \emph{configuration reference} points to a variable defined in the same or another project (if made available through imports). As the actual IVML specification \cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are translated for / evaluated on the referenced variable. + +\subsubsection{Values}\label{sectNotationValues} + +IVML types have corresponding values in the IVML object model, in particular as complex structured types such as compounds and containers may be nested. As the expression evaluator is dealing with values, applying operations to them and storing them in the configuration, we can largely ignore the specific properties of vales. However, some specific properties must be taken into account for reasoning. Basically, a value $val$ always carries its type $type(val)$. One specific value is \IVML{null}, which is certainly different from the undefined value $\undef$. As introduced in Section \ref{sectNotationConstraints}, a constrant expression holds a value, which can be obtained from an expression using $const(e)$ (returns $\undef$ for any expression that is not a constant expression). Further, complex values can consist of nested values, which are accessible through $elements(val)$, without nesting as flattened set or sequence through $allElements(val)$, respectively. For non-complex values, these two functions just return $\set{val}$. To ease some notation, we assume that $elements(\undef)=\emptySet$, similarly for $allElements(\undef)$. + +In some situations we must either rely on the actual value of a variable or its default value. The latter is particularly important for initializing a configuration. Thus, having available a variable $v$ and its declaration $d=decl(v)$, we define +% +$$ +relevantValue(v, d, inc) = \begin{cases}value(v), & \text{if } value(v) \neq\undef\\ const(default(d)), & \text{if} default(d) \neq\undef \wedge \neg inc\\ \undef, & \text{else}\end{cases} +$$ +% +i.e., the relevant value of a variable is either its assigned value or its constant default value, the latter only if we are not in incremental reasoning mode $inc$. +% +Please note that we could also write $relevantValue(v, inc)=relevantValue(v, decl(v), inc)$, but many algorithms below will explicitly require a variable $v$ and its declaration $d$. This is due to historical reasons in the development of the reasoner aiming to avoid frequently calling $decl(v)$. %----------------------------------------------------------------------------------------------------------------- @@ -345,9 +361,9 @@ \subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation} -Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. - -The variable mapping is a global core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed and can safely be cleared. As $\variableMapping$ is global (also for performance reasons) and cleared only after processing an IVML project, it can temporarily contain outdated or superfluous entries, e.g., from the a previous compound of the same type being currently processed. However, the mapping is anyway correct as long as the IVML model was correctly created, e.g., through the IVML parser, as then all model elements and their types are properly resolved, no dangling references do exist and the relevant entires in $\variableMapping$ are overridden by the translation algorithm before use, i.e., the remaining superfluous entries are just ignored. - -From a technical point of view, the variability mapping consists of mapping entries relating a variable declaration with an access expression if needed. For directly accessible variables such as top-level variables directly defined within a project, no such mapping is needed ($\undef$). For variables used in constraints within compounds or containers, an appropriate accessor is needed, created and registered when starting to translate the respective type. The respective constraints for that type are then enumerated, copied and while copying the variables registered in the variable mapping are replaced by the accessor expressions in the mapping. It is important to ensure that the mapping for the respective type is complete before constraint translation, so that all variables including cross references within the same type can be replaced properly. References to other variables are already given as accessor expressions and do not need to be considered here. +The core idea of the constraint translation is to collect the constraints following the structure of an IVML model. On top level, there are IVML variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions become relevant when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated from type constraints to variable constraints. + +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. + +In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$, i.e., a dictionary linking each actually relevant variable, compound slot or annotation to its access expression based on a top-level IVML variable. The variable mapping is a global core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed and can safely be cleared. As $\variableMapping$ is global (also for performance reasons) and cleared only after processing an IVML project, it can temporarily contain outdated or superfluous entries, e.g., from the a previous compound of the same type being currently processed. However, the mapping is anyway correct as long as the IVML model was correctly created, e.g., through the IVML parser, as then all model elements and their types are properly resolved, no dangling references do exist and the relevant entires in $\variableMapping$ are overridden by the translation algorithm before use, i.e., the remaining superfluous entries are just ignored. \begin{algorithm}[H] @@ -382,4 +398,6 @@ \end{algorithm} +From a technical point of view, the variability mapping consists of mapping entries relating a variable declaration with an access expression if needed. For directly accessible variables such as top-level variables directly defined within a project, no such mapping is needed ($\undef$). For variables used in constraints within compounds or containers, an appropriate accessor is needed, created and registered when starting to translate the respective type. The respective constraints for that type are then enumerated, copied and while copying the variables registered in the variable mapping are replaced by the accessor expressions in the mapping. It is important to ensure that the mapping for the respective type is complete before constraint translation, so that all variables including cross references within the same type can be replaced properly. References to other variables are already given as accessor expressions and do not need to be considered here. + Then, the algorithm identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are populated independently during the constraint translation and, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets @@ -392,4 +410,6 @@ These constraint sets are filled through the top-level calls in line \ref{algTranslateConstraintsTranslationStart}-\ref{algTranslateConstraintsTranslationEnd} including subsequent calls, prioritizing eval-blocks \cite{IVML-LS}. Please note that adding constraints to a constraint set (currently) requires filtering out unneeded constraints as well as indexing used variables. This is done by the $add$ function (e.g., in line \ref{algTranslateConstraintsAdd}), which we will detail below in Section \ref{sectTranslation}. This algorithm also takes into account the $inEval$ flag prioritizing eval-block contents. According to the priority of the constraint sets introduced above, Algorithm \ref{algTranslateConstraints} composes the constraint base (keeping remaining constraints from prior project evaluations of the same configuration) in line \ref{algTranslateConstraintsCompose}. Finally, Algorithm \ref{algTranslateConstraints} clears the temporary constraint sets in lines \ref{algTranslateConstraintsClearSetsStart}-\ref{algTranslateConstraintsClearSetsEnd} and copies the constraint $base$ in the first run of the incremental reasoning mode with re-used constraint base. + +Adding constraints or sets of constraints to the constraint base involves constraint filtering in order to respect the incremental reasoning mode as well as constraints that initialize compounds and containers through respective initializer expressions. This is done by a specific operation, which we will discuss in Section \ref{sectContainerBase}. During algorithm discussion, we ill just use the respective function $add(s, c, b)$, which adds constraint $c$ to constraint set $s$, considering compound and container initialization expressions if $b = true$. Compound and container initialization expressions are a specific and relevant case here, as they represent complex compound or container values containing (interrelating) expressions that can only be evaluated during reasoning in contrast to constant values, which are already resolved by the IVML parser (or by a simple configuration initialization mechanism). These expressions are particularly important to correctly consider constraints stemming from constraint variables. While most translation algorithms rely on default values or actual values (e.g., through the $relevantValue$ function defined in Section \ref{sectNotationValues}, compound and container initializers can only be obtained from assignment constraints, i.e., completed and instantiated constraints, which are only available when adding constraints to a constraint set or the constraint base. Thus, We will skip container and compound initializers in the translation algorithms, focus on actual or constant default values, and finally consider these specific cases in Section \ref{sectContainerBase}. \subsection{Top-level Constraints Evaluation}\label{sectTopLevelConstraintsEvaluation} @@ -452,15 +472,17 @@ \section{Constraint translation}\label{sectTranslation} -The constraint translation analyzes constraints defined for a given IVML model, identifies those ones that must be instantiated, i.e., turned from constraints on types to constraints on variables, and performs this translation to fill the constraint base. Therefore, we consider three main types of constraints: +The constraint translation analyzes constraints defined for a given IVML model, identifies those ones that must be instantiated, i.e., turned from constraints on types to constraints on variables, and performs this translation to fill the constraint base. We distinguish three main types of constraints: \begin{enumerate} \item Explicit \emph{top-level constraints} written by the domain expert, which are already using qualified variables. This group of constraints includes also constraints in top-level (nested) eval blocks as well as constraints in top-level annotation assignment-blocks. Top-level constraints, eval-block constraints and annotation assignment constraints are ready for reasoning, do not need further translation and can directly be taken over into the constraint base (Algorithm \ref{algTranslateConstraints}, lines \ref{algTranslateConstraintsAdd} - \ref{algTranslateConstraintsTopLevelEvals}). As annotation assignments typically also include variable declarations, we enumerate them through a specific algorithm, which is also used for translating annotation assignments in compound types. However, we pass here parameters that focus on enumerating and adding rather than translating the related constraints. - \item \emph{Constraints introduced through variable types}, e.g., compound types. These constraints must be instantiated through translation, i.e., use of type level variables and slots must be rewritten to use actual variables and slots. Here, we start from top-level variable variables and perform a transitive instantiation based on the respective type of the variable. Where possible, it is important to consider the actual type of the value of the individual variables, as through type compatibility of refined types, the actual value type may be more specific that the declared type of the variable. This is initiated in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. + \item \emph{Constraints introduced through variable types}, e.g., compound types, typedefs with constraints or, transitively, collections. These constraints must be instantiated through translation, i.e., use of type level variables and slots must be rewritten to use actual variables and slots. Here, we start from top-level variable variables and perform a transitive instantiation based on the respective type of the variable. Where possible, it is important to consider the actual type of the value of the individual variables, as through type compatibility of refined types, the actual value type may be more specific that the declared type of the variable. This is initiated in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. \item \emph{Constraints for default values}. To achieve uniformity of the constraint evaluation and variable update process (cf. Section \ref{sectReasoning}), we (currently) translate default value assignments to assignment constraints. In more detail, the IVML declaration \IVML{Type v = ex;} must be translated into a constraint $\createConstraint{v = ex}$. We add these assignment constraints to the constraint base with higher priority than other constraints to ensure that default values are assigned first. Here, we must consider that default value assignments can change the actual value type implying that a refined set of constraints must be evaluated on the respective variable. Moreover, default value expressions for complex values shall have more priorities than default values for individual slots, as otherwise the default value for the individual slot (e.g., given as default value within a compound or a refined slot) may be overridden by a complex value from a containing scope, e.g., a top-level variable declaration. This is also initiated in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. \end{enumerate} -We start with the main algorithm, Algorithm \ref{algTranslateDeclaration}, for translating variable declarations and related default value expressions in Section \ref{sectTranslationDeclarationTypesDefaults}. Algorithm \ref{algTranslateDeclaration} decides about the translations needed in detail and delegates the translation to further algorithms. Thus, we structure the further sections along the structure of Algorithm \ref{algTranslateDeclaration} and detail the translatation of derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound defaults in Section \ref{sectCompoundDefaults}, container defaults in Section \ref{sectContainerDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}. - -\subsection{Translate Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} +The main entry point to the constraint translation are variable declarations. A variable declaration consists of a type, a name, and, if given, a default value. As mentioned above, some types can define constraints that must be instantiated, in particular derived types (typedefs), compounds, containers (through their used types) and contraint variables. Algorithm \ref{algTranslateDeclaration} (in Section \ref{sectTranslationDeclarationTypesDefaults}) performs the translation of variable declarations, related default value expressions and, following the call graph in Figure \ref{figStructure} dispatches further translations according to the type of the variable. Please note that Algorithm \ref{algTranslateDeclaration} is (indirectly) subject to recursion if further variable declarations, in particular compound slots and annotations must be processed. + +We start in Section \ref{sectTranslationDeclarationTypesDefaults} with the translation of variable declarations structure the remainder of this section according to the algorithms called while processing a variable declaration, i.e., the translation of default values in Section \ref{sectTranslationDeclarationTypesDefaults}, derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound types in Section \ref{sectCompoundDefaults}, container types in Section \ref{sectContainerDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}. A section about algorithms for building the constraint base in Section \ref{sectContainerBase} completes the constraint translation. + +\subsection{Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and respective variable $v$ through their actual type. Basically, the algorithm considers for the given variable, depending on the actual type, derived type constraints, annotation defaults, compound constraints, container constraints, and constraints of overridden slots leading to a deferred default initialization through the global constraints set $\deferredDefaultConstraints$. @@ -480,5 +502,5 @@ $translateAnnotationDeclarations(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault} } - \lIf{$dflt \neq \undef$}{$t \assng type(d)$} + \lIf{$dflt \neq \undef$}{$t \assng type(d)$ \MISSING{relevantValue}} \uIf{$isCompound(t)$}{ $s \assng d$\; @@ -505,11 +527,11 @@ \end{algorithm} -Adding constraints or sets of constraints to the constraint base involves constraint filtering in order to respect the incremental reasoning mode as well as constraints that initialize compounds and containers through respective initializer expressions. This is done by a specific operation, which we will discuss in Section \ref{sectContainerBase}. Below, we ill just use the respective function $add(s, c, b)$, which adds constraint $c$ to constraint set $s$, considering compound and container initialization expressions if $b = true$. We allow disabling the checks for container and compound initiailizers for certain kinds of constraints, for which we are sure that the these expressions do not occur, to improve the performance of the reasoning. - \subsection{Derived types}\label{sectDerivedTypes} -As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined based on base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines restricting constraints over $base(t)$ through the local variable $decl(t)$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. - -If a variable $v$ is declared as of a derived type $t$, all constraints defined for $t$ over $base(t)$ and, transitively all constraints over all base types $allBase(t)$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. For a given variable $v$ (in terms of declaration $d$ and specific type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraint.} all constraints defined for $allBase(t)$ as constraints of $d$. Thereby, we must consider whether we perform this instantiation for a container variable. If it is a container variable, we create an all-quantifying constraint over all container values, whereby the iterator variable substitutes $decl(t)$. If it is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$. % shall not make a difference for nested variables as they are already initialized +As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined through its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines restricting constraints over $base(t)$ through the local variable $decl(t)$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. + +If a variable $v$ is declared as of a derived type $t$, all constraints defined for $t$ over $base(t)$ and, transitively all constraints over all base types $allBase(t)$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. The constraint translation follows this nested type structure and instantiates all constraints defined along the nesting. + +For a given variable $v$ (in terms of declaration $d$ and specific type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraint.} all constraints defined for $allBase(t)$ as constraints of $d$. Thereby, we must consider whether we perform this instantiation for a container variable. If it is a container variable, we create an all-quantifying constraint over all container values, whereby the iterator variable substitutes $decl(t)$. If it is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$. % shall not make a difference for nested variables as they are already initialized \begin{algorithm}[H] @@ -530,5 +552,5 @@ \subsection{Compound constraints}\label{sectCompoundDefaults} -Translating a compound into all its constraints requires considering all slots including inherited slots, all constraints defined within a compound including inherited ones, as well as all nested structures, such as eval blocks or attribute value assignment-blocks. In particular, if the IVML keyword \IVMLself{} is used, it must be replaced 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. +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} consists of three parts: @@ -572,10 +594,7 @@ Finally, the algorithm translates the nested structures. Then it translates all annotation value assignments using Algorithm \ref{algTranslateAnnotationAssignments}. For the last two translations, we need the actual value of \IVMLself{}, to be determined for the recent compound, either based on the given accessor $ca$ or the declaration $d$. Then, to keep the priority of eval-blocks, it collects all constraints of all nested eval-blocks, replaces \IVMLself{} and variable mappings $\variableMapping$ and adds them to $\otherConstraints$. Finally, we take over and translate all constraints of all transitively declared constraints refined compounds and assignment constraints. -%----------------------------------------------------------------------------------------------------------------- - \subsection{Container constraints}\label{sectContainerDefaults} -Constraints defined on types that are implicitly instantiated within a container must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundContainer} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested container). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the container using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$. -If the slot is a constraint container, it translates all contained constraints performing the usual variable substutions. +Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. \begin{algorithm}[H] @@ -584,19 +603,29 @@ \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$} - \uIf{$ dflt \neq \undef \wedge \neg inc $}{ - \ForAll{$u \iterAssng usedTypes(default(d))$}{ - \MISSING{derived types?} + $t_n \assng nested(t); t_b \assng base(t_n); used\assng\emptySet$\; + $val\assng relevantValue(d, v, inc)$\; + \uIf{$isConstraint(t_b)$} { + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{e}{ca}}}{e \in allElements(val)}, true)$\; \label{algTranslateContainerDeclarationConstraintContainer} + } \ElseIf{$isCompound(t_b)$} { + $used \assng \setWith{base(u)}{u \in usedTypes(val) \wedge isContainer(base(u))}$\; \label{algTranslateContainerDeclarationUsedTypesDefault} + \ForAll{$u \iterAssng used$}{\label{algTranslateContainerDeclarationCompoundContainerDefaultsStart} $translateDefaultsCompoundsContainer(d, u)$\; - } - } - $add(\otherConstraints, translateCompoundContainer(d, v, ca), true)$\; - \uIf{$isContainer(t) \wedge isDerived(contained(t))$}{ - $translateDerivedDatatypeConstraints(contained(t), d)$\; + }\label{algTranslateContainerDeclarationCompoundContainerDefaultsEnd} + \ForAll{$u \iterAssng used \setminus \setWith{allRefines(u)}{u \in used}$} {\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart} + $add(\otherConstraints, translateCompoundContainer(u, t_n, d, ca), true)$\; + }\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd} + $add(\otherConstraints, translateCompoundContainer(d, v, ca, used), true)$\;\label{algTranslateContainerDeclarationCompoundContainerCompounds} } - \uIf{$isConstraintContainer(type(s))$} { - $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{value(v)}{ca}}}{e \in elements(value(s))}, true)$\; + \uIf{$isDerived(t_n)$}{ + $translateDerivedDatatypeConstraints(t_n, d)$\; \label{algTranslateContainerDeclarationDerivedTypes} } \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration} \end{algorithm} + +However, containers are different than usual variables as the may contain an arbitrary number of elements. Thus, for specifying a constraint over a container, we must apply all-quantification (the IVML \IVML{forAll} operation) for all constraints defined on contained types. Moreover, for nested collections we must apply the IMVL \IVML{flatten} operation to gain access to the individual elements, and for refined types even explicit IVML type casts using the \IVML{asType} operation to have access to specific operations, slots or annotations. + +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$ (taking derived types into account) 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 try to derive as many relevant constraints as possible. Therefore, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. For all these types, we determine all default value constraints using Algorithm \ref{algTranslateDefaultsCompoundContainer} in lines \ref{algTranslateContainerDeclarationCompoundContainerDefaultsStart}-\ref{algTranslateContainerDeclarationCompoundContainerDefaultsEnd}. Moreover, for all used most specific compound types, we collect and instantiate all compound-related constraints using Algorithm \ref{algTranslateCompoundContainer2} in lines \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}-\ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd}. As Algorithm \ref{algTranslateCompoundContainer2} takes all refined compounds into account, we leave out the refined types from the used containers in line \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}. For the remaining, not already translated compound types, we also apply Algorithm \ref{algTranslateCompoundContainer2}, here through Algorithm \ref{algTranslateCompoundContainer} (based on the configured value) in line \ref{algTranslateContainerDeclarationCompoundContainerCompounds}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}. + +%----------------------------------------------------------------------------------------------------------------- @@ -617,11 +646,12 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$} + \KwIn{declaration $d$, variable $v$, compound access $ca$, compound set $done$} \KwOut{resulting constraints $c$} $c \assng \set$\; $tc \assng contained(type(d))$\; - \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in elements(v)}$}{ - \If{$isCompound(t)$}{ + \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in allElements(v)}$}{ + \lIf{$isDerived(t)$}{$t \assng base(t)$} + \uIf{$isCompound(t) \wedge (done = \undef \vee done[t]=\undef)$}{ $c \assng c \cup translateCompoundContainer(t, tc, d, ca)$\; } @@ -638,5 +668,5 @@ $c \assng \set$\; - $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$ + $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$\; \ForAll{s \iterAssng slots(t)} { $\variableMapping \assng \variableMapping \addMap \mapEntry{s}{\createExpression{\IVMLMeta{acc}(v,s)}}$\; @@ -644,4 +674,5 @@ \ForAll{$e \iterAssng allCompoundConstraints(t) \cup allVariableConstraints(t)$} { $coll \assng\createExpression{\closedCases{ca, & \text{if } ca = \undef \\ d, &\text{else}}}$\; + \lIf{$nested(d)$}{$coll \assng\createExpression{\IVML{flatten}(coll)}$} $coll \assng\createExpression{coll.\closedCases{\IVML{selectByKind}(a, t), & \text{if } t \neq dt \\ &\text{else}}}$\; $c\assng c \cup \createConstraint{coll\rightarrow\IVML{forAll}(i|\text{ }\varSubstitutionVarMapping{e})}$\; @@ -770,4 +801,5 @@ \end{algorithm} +For constraint variables and constraint variable containers: %\begin{align*} %retrieve&ContainerConstraints(c, m) =\\ @@ -775,5 +807,5 @@ %\end{align*} \begin{align*} -checkContainerInitializer(c, \variableMapping) = \seqWith{\closedCases{\varSubstitutionVarMapping{e}, & \text{if } \variableMapping \ne \undef \\ e &\text{else}}}{e\in expr(c)} +check&ContainerInitializer(c, \variableMapping) =\\ &\seqWith{\closedCases{checkContainerInitializer(e), & \text{if } isContainerInitializer(e) \\ \createConstraint{\varSubstitutionVarMapping{e}}, &\text{else}}}{e\in expr(c)} \end{align*} \begin{align*} @@ -820,4 +852,6 @@ + Compound type & 2.1.3.5 & Alg. \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateCompound} $\rightarrow$ Alg.\ref{algTranslateCompoundDeclaration} \\ + Container type & 2.1.3.3 & \\ ++ Derived Compound Type & & \\ ++ Derived Container Type & & \\ + Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} \\ + Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers}, constraint value in \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationConstraintVariableConstraint} via compound access line \ref{algTranslateDeclarationTranslateInCompound} \\ @@ -832,4 +866,6 @@ + Compound type & 2.1.3.5 & \\ + Container type & 2.1.3.3 & \\ ++ Derived Compound Type & & \\ ++ Derived Container Type & & \\ + Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} \\ + Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers} \TBD{constraint value} \\