Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 52) +++ /reasoner/reasoner.tex (revision 53) @@ -64,5 +64,5 @@ Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines \cite{QMD42}. Although these mechanisms are powerful in their own respect and typically available as implementation, using them for IVML requires translating an IVML model and its constraints into the model of the respective mechanism and executing that mechanism on the translated model. While traditional reasoners allow for completing the model through feasible ground instances, they typically also perform a kind of constrained state space evaluation. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables), just applying a traditional reasoner to usual IVML models is an inefficient approach. Other related mechanisms such as rule engines can be applied to some degree, however, according to our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} lead to a significant and infeasible runtime overhead. Moreover, these both kinds of approaches are limited as they typically do not directly support the breadth of OCL operations, in particular container iterators, quantifiers and user-defined constraint operations. In contrast, specific reasoning approaches, e.g., for OWL partially support quantification, but are similarly limited. Moreover, relying on OCL reasoning mechanisms could be a feasible approach, but would require significant extension to enable value propagation and IVML-specific operations. -Due to these experiences, we decided to realize a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis is \emph{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. It is important to notice that IVML \cite{IVML-LS} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniquely determined, IVML allows changing the value of a constraint only once within a project scope, otherwise requiring that a reasoning mechanism issues an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in certain cases, some form of sequence of the constraints can be indicated through eval-blocks within a project, i.e., (nested) blocks containing constraints. Here the rule is that a project is considered as the outermost eval-scope, then eval-blocks are evaluated in their nesting sequence (whereby eval-blocks on the same nesting level do not imply any sequence). +Due to these experiences, we decided to realize a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis is \emph{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. It is important to notice that IVML \cite{IVML-LS} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniquely determined, IVML allows changing the value of a constraint only once within a project scope, otherwise requiring that a reasoning mechanism issues an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in certain cases, some form of sequence of the constraints can be indicated through partial evaluations, i.e., eval-blocks within a project or a compound. An eval-block consists of constraints or nested eval-blocks. IVML \cite{IVML-LS} considers project as outermost (implicit) eval-scope, then eval-blocks are evaluated in their nesting sequence (whereby eval-blocks on the same nesting level do not imply any sequence). However, not all IVML constraints can be directly used for reasoning. This is in particular true for constraints defined directly on compound types, or indirectly, through types used within collections. Specifying IVML constraints on types, such as compounds, rather than variables (where applicable) simplifies the model (for a compound such constraints are automatically valid for all instances without explicit quantification), supports consistency and helps reduces the model size and complexity. Such constraints typically utilize local variables defined within the compound including the special pre-defined variable \IVML{self} pointing to the actual compound instance. Cross-references to other types are required to be specified through an explicit accessor, i.e., an expression mentioning the variable and the respective nested variable(s). During reasoning, constraints over types cannot be evaluated, as the actual values are not available. Thus, we perform first a \emph{constraint translation step} to instantiate the constraints for configuration variables based on the actual type of the variable or its value. An alternative here could be reasoning over the type constraints and modifying the mapping on demand before evaluation. This could save memory and runtime (for constraint translation / creation), but, however, increases complexity in managing the actual constraints to be evaluated. So we opted for instantiating the constraints and keeping only the new, failed or recently affected ones in the constraint base. @@ -244,5 +244,5 @@ \subsection{Other IVML Elements}\label{sectNotationOthers} -No specific functions are required for translating constraints for / reasoning on \emph{basic types} (Boolean, Integer, Real String). 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. +No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real String) as well as for enums as IVML does not support 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. @@ -307,6 +307,6 @@ $\variableMapping \assng \setEmpty$\; \label{algTranslateConstraintsClearMapping} \tcp{start of model visitor}%>ConstraintTranslationVisitor - \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart} %translateDeclarationDefaults - $translateDeclarationDefaults(d, decision(cfg, d), \undef)$\; \label{algTranslateConstraintsTranslationDeclarationDefaults} + \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart} + $translateDeclaration(d, decision(cfg, d), \undef)$\; \label{algTranslateConstraintsTranslationDeclaration} } $add(\topLevelConstraints, constraints(p), true)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints} @@ -410,7 +410,7 @@ We start with the algorithm for translating declaration types and defaults in Section \ref{sectTranslationDeclarationTypesDefaults}. Then we will discuss more specific algorithms used within the translatation of declaration types and defaults, including 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}, and, finally, container defaults in Section \ref{sectContainerDefaults}. -\subsection{Translate Declaration Types and Default Values}\label{sectTranslationDeclarationTypesDefaults} - -Algorithm \ref{algTranslateDeclarationDefaults} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm +\subsection{Translate Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} + +Algorithm \ref{algTranslateDeclaration} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm \begin{itemize} \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\topLevelConstraints$. @@ -429,5 +429,5 @@ \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$} - $translateDerivedDatatypeConstraints(d)$\; + $translateDerivedDatatypeConstraints(d)$\; \label{algTranslateDeclarationDerivedDatatype} \If{$\neg inc$} { $translateAnnotationDefaults(cfg, d, \undef)$\; @@ -462,5 +462,5 @@ } } - \caption{Translating default value expressions to constraints (\IVML{translateDeclarationDefaults}).}\label{algTranslateDeclarationDefaults} + \caption{Translating default value expressions to constraints (\IVML{translateDeclaration}).}\label{algTranslateDeclaration} \end{algorithm} @@ -546,5 +546,5 @@ Algorithm \ref{algTranslateCompoundDefaults} 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)$. -First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclarationDefaults}. +First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration}. Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\otherConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound container, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateContainerCompoundConstraints}. @@ -562,5 +562,5 @@ } \ForAll{s \iterAssng slots(v)} { %actual slots - $translateDeclarationDefaults(s, decision(v, s), c)$\; + $translateDeclaration(s, decision(v, s), c)$\; } \ForAll{s \iterAssng slots(v)} { %actual slots @@ -730,49 +730,48 @@ \begin{table*}[h] \centering -\begin{tabular}{|l|c||l|p{3cm}|} +\begin{tabular}{|l|c||p{8cm}|} \hline -\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} & \textbf{Comments}\\ +\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} \\ \hline - \multicolumn{4}{|c|}{Top-level}\\ +Decision variable & 2.1.4 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTranslationDeclaration} $\rightarrow$ Alg. \ref{algTranslateDeclaration} \TBD{check} \\ +Constraint & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelConstraints} \\ +Annotation assignment & 2.2.2 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments} $\rightarrow$ Alg. \ref{algTranslateAnnotationAssignments} \\ +Partial evaluation & 2.2.5.3 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals} \\ \hline -Decision variable & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTranslationDeclarationDefaults} $\rightarrow$ Alg. \ref{algTranslateDeclarationDefaults} & \TBD{check} \\ -Constraint & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelConstraints} & \\ -Annotation assignment & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments} $\rightarrow$ Alg. \ref{algTranslateAnnotationAssignments} & \\ -Eval-block & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals} & \\ + \multicolumn{3}{|c|}{Types}\\ \hline - \multicolumn{4}{|c|}{Types}\\ -\hline -Basic types & & - & No translation, cf. Section \ref{sectNotationOthers}\\ -Derived types & & & \\ -Enum types & & & \\ -Compound types & & & \\ -+ Basic types & & & \\ -+ Derived variable & & & \\ -+ Enum variable & & & \\ -+ Compound variable & & & \\ -+ Container variable & & & \\ -+ Reference variable & & & \\ -+ Constraint variable & & & \\ -Container variable & & & \\ -+ Basic variable & & & \\ -+ Derived variable & & & \\ -+ Enum variable & & & \\ -+ Compound variable & & & \\ -+ Container variable & & & \\ -+ Reference variable & & & \\ -+ Constraint variable & & & \\ -+ Assignment Block & & & \\ -+ Constraint & & & \\ -Annotation & & & \\ -+ Basic variable & & & \\ -+ Derived variable & & & \\ -+ Enum variable & & & \\ -+ Compound variable & & & \\ -+ Container variable & & & \\ -+ Reference variable & & & \\ -+ Constraint variable & & & \\ -+ Constraint & & & \\ -Reference variable & & & \\ -Constraint variable & & & \\ +Basic types & 2.1.3.1 & No translation, cf. Section \ref{sectNotationOthers} \\ +Enum types & 2.1.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ +Derived types & 2.1.3.4 & Alg. \ref{algTranslateDeclaration}, line \ref{algTranslateDeclarationDerivedDatatype} $\rightarrow$ Alg. \ref{algTranslateDerivedDatatypeConstraints} \\ +Compound types & 2.1.3.5 & \\ ++ Basic types & 2.1.3.1 & No translation, cf. Section \ref{sectNotationOthers} \\ ++ Enum variable & 2.1.3.2 & \\ ++ Derived variable & 2.1.3.4 & \\ ++ Compound variable & 2.1.3.5 & \\ ++ Container variable & 2.1.3.3 & \\ ++ Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ ++ Constraint variable & 3.10.1 & \\ ++ Constraint & 2.1.3.5 & \\ ++ Refined compounds & 2.2.3.1 & \\ ++ Partial evaluation & 2.2.5.3 & \\ +Container variable & 2.1.3.3 & \\ ++ Basic variable & 2.1.3.1 & \\ ++ Enum variable & 2.1.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ ++ Derived type variable & 2.1.3.4 & \\ ++ Compound variable & 2.1.3.5 & \\ ++ Container variable & 2.1.3.3 & \\ ++ Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ ++ Constraint variable & 3.10.1 & \\ ++ Assignment Block & 2.2.2 & \\ +Annotation & 2.2.2 & \\ ++ Basic variable & 2.1.3.1 & \\ ++ Enum variable & 2.1.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ ++ Derived type variable & 2.1.3.4 & \\ ++ Compound variable & 2.1.3.5& \\ ++ Container variable & 2.1.3.3 & \\ ++ Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ ++ Constraint variable & 3.10.1 & \\ +Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ +Constraint variable & 3.10.1 & \\ \hline \end{tabular}