Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 39)
+++ /reasoner/reasoner.tex	(revision 40)
@@ -21,5 +21,5 @@
 \newcommand\set[1]{\{#1\}}
 \newcommand\setWith[2]{\{#1:#2\}}
-\newcommand\setSepText[0]{colon}
+\newcommand\setSepText[0]{colon }
 \newcommand\seq[1]{[#1]}
 \newcommand\seqWith[2]{[#1:#2]}
@@ -37,5 +37,5 @@
 \maketitle
 
-Analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language. In this document, we provide an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML), a variability and configuration modelling language that contains several complex concepts. We discuss the approach to reasoning for IVML, in particular, the implementing constraint translation and reasoning algorithms.
+Analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language. In this document, we provide an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML), a variability and configuration modeling language that contains several complex concepts. We discuss the approach to reasoning for IVML, in particular, the implementing constraint translation and reasoning algorithms.
 
 \section{Introduction}
@@ -43,26 +43,29 @@
 In Product Line Engineering, a \textbf{variability model} defines the options to customize a software system, while a \textbf{configuration} specifies the choices made for a specific instance of the software system. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another option. Such dependencies are typically expressed using different forms of \textbf{constraints}. For instantiating a software system, a configuration must be valid, i.e., all (relevant) constraints must be fulfilled. To analyze a configuration for validity, for figuring out the number of remaining configuration options or for propagating derivable values, various forms of \textbf{reasoning mechanisms} are utilized. Several reasoning mechanisms are available, such as SAT-solving or SMT-reasoners \TBD{cites}. However, expressiveness of the modeling concepts and supported constraints affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, also the applicable reasoning mechanism.
 
-Besides traditional variability modeling approaches, such as feature modeling~\cite{CzarneckiHelsenEisenecker05, KangCohenHess+90} or decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}, in recent time several approaches to textual variability modeling have been proposed~\cite{EichelbergerSchmid15a}. Moreover, there seems to be a trend that more recent variability modeling support more powerful modeling conceepts~\cite{EichelbergerSchmid15a}, which then require more powerful analysis and reasoning mechanisms. As stated above, typically these mechanisms then imply limitations of the analysis capabilities, e.g., non-Boolean decisions typically prevent determining the actual number of possible configurations (of course not the number of configuration options that remain to be configured to achieve a complete configuration).
-
-The \textbf{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}. Currently, the reasoning mechanism focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propoagation as much as possible. So far, this allows performing typical validation and propagation tasks. However, we are aware of the fact that more advanced tasks like configuration completion are not supported by the current approach. This is subject to future work, for which this document shall provide a solid foundation.
-
-This document is structured as follows: Section \ref{sectApproach} introduces the overall approach to reasoning for IVML. Section \ref{sectNotation} introduces the notation that we use to describe the reasoning algorithm, in particular the notation to access (derived) properties of the various IVML concepts. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints, reasoning and reacting to value changes / propagation. In Section \ref{sectTranslation}, we detail the instantiation and translation of constraints for individual configuration settings. In Section \ref{sectCompleteness}, we summarize the translations in order to assess the actual state for completeness with respect to IVML concepts. \TBD{So far no evaluation} In Section \ref{sectConclusion} we conclude and provide an outlook to future work.
+Besides traditional variability modeling approaches, such as feature modeling~\cite{CzarneckiHelsenEisenecker05, KangCohenHess+90} or decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}, in recent time several approaches to textual variability modeling have been proposed~\cite{EichelbergerSchmid15a}. Moreover, there seems to be a trend that more recent variability modeling support more powerful modeling concepts~\cite{EichelbergerSchmid15a}, which then require more powerful analysis and reasoning mechanisms. As stated above, typically these mechanisms then imply limitations of the analysis capabilities, e.g., non-Boolean decisions typically prevent determining the actual number of possible configurations (of course not the number of configuration options that remain to be configured to achieve a complete configuration).
+
+The \textbf{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}. Currently, the reasoning mechanism focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propagation as much as possible. So far, this allows performing typical validation and propagation tasks. However, we are aware of the fact that more advanced tasks like configuration completion are not supported by the current approach. This is subject to future work, for which this document shall provide a solid foundation.
+
+This document is structured as follows: Section \ref{sectApproach} introduces the overall approach to reasoning for IVML. Section \ref{sectNotation} introduces the notation that we use to describe the reasoning algorithm, in particular the notation to access (derived) properties of the various IVML concepts. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints, reasoning and reacting to value changes / propagation. In Section \ref{sectTranslation}, we detail the instantiation and translation of constraints for individual configuration settings. In Section \ref{sectCompleteness}, we analyze the effect translations in order to assess the actual state for completeness with respect to IVML concepts. In Section \ref{}, we summarize the findings made during the revision of the reasoner with regard to performance, in particular that further modifications don't apply modify the implementation against already known performance anti-patterns. In Section \ref{sectEvaluation}, we present an evaluation of the actual evaluation with respect to performance incuding different kinds of IVML models. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook to future work.
+
+%-----------------------------------------------------------------------------------------------------------------
 
 \section{Approach}\label{sectApproach}
 
-IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \cite{IVML-LS} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \textbf{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), container types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in constrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged~\cite{CzarneckiHelsenEisenecker05a} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points.
+IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \cite{IVML-LS} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \textbf{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), container types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in contrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged~\cite{CzarneckiHelsenEisenecker05a} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points.
 
 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 \textbf{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 \textbf{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 uniqualy 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 squence 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). Based on our experience (and the specific requirements of default-value logic, project scopes, eval scopes), the reasoning mechanism shall directly operate on an IVML model instead of performing a model transformation first. However, as constraints in IVML can be attached to types (to increase consistency and to avoid repeated constraints), first a constraint transformation is needed, which instantiates constraints towards variables and their respective types. Then, forward-chaining is executed on this constraint base. Extending approaches may continue on a the result of a failed reasoning through forward-execution.
+Due to these experiences, we decided to realize a \textbf{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 \textbf{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 squence 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). Based on our experience (and the specific requirements of default-value logic, project scopes, eval-block scopes), the reasoning mechanism shall directly operate on an IVML model instead of performing a model transformation first. However, as constraints in IVML can be attached to types (to increase consistency and to avoid repeated constraints), first a constraint transformation is needed, which instantiates constraints towards variables and their respective types. Then, forward-chaining is executed on this constraint base. Extending approaches may continue on a the result of a failed reasoning through forward-execution.
 
 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 \textbf{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 \textbf{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. More specifically, we distinguish between incremental reasoning
 \begin{itemize}
   \item with \textbf{creation of a partial constraint base}. In this incremental mode, 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 mode can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration.
-  \item \textbf{re-using a previously build constraint base}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning frontend).
+  \item \textbf{re-using a previously build constraint base}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning fronted).
 \end{itemize}
 
 To implement the IVML reasoner, we designed and realized first an \textbf{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. This includes constraint expressions (expressions evaluating to a Boolean value) and as special case default value expressions (evaluating to a value that can be assigned to the respective variable). We do not detail the constraint evaluation mechanism further here, rather than focusing on the IVML reasoning mechanism, which relies on the expression evaluation mechanism for evaluating constraints.
 
+%-----------------------------------------------------------------------------------------------------------------
 
 \section{Notation and Terminology}\label{sectNotation}
@@ -72,16 +75,18 @@
 \subsection{General notation}
 
-As usual, we denote a set of elements by $s=\set{1, 2, ...}$ with no duplicates allowed. We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., the part after the \setSepText  indicates the set to take the elements from (possibly including a condition), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, whereby $s_2$ contains no duplicates (and the sequence of elements does not matter).
-
-For some parts of the reasoning algorithm, we need sequences, i.e., a structure that contains elements in a given sequence, but potentially containing duplicates. Similar to sets, we denote a sequence by $q=\seq{2, 1, ...}$ and the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_d$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as the sequence concatenation as described before but without duplicates.
-
-Further, we denote the undefined value by $\undef$. If not indicated otherwise, all operations introduced below that are bound to a certain type return $\undef$ if the operation is used with another type.
-
-For individual algorithms, we use the actual name of the implementation (to ease mapping code to algorithms and back) and indicate the name in the caption of the algorithm. For simplicity, we ignore that elements or results of functions in the actual implementation may be a null pointer and respective checks are needed in the actual implementation. In the algorithm descriptions in this document, we simply assume that function return either $\undef$ or (in case of set or sequences) $\set{}$, 
+As usual, we denote a set of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \set{} as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText  to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter).
+
+For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need sequences, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seq{\text{ }} as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates.
+
+Further, we denote the undefined value by $\undef$. If not indicated otherwise, all operations introduced below that are bound to a certain type, e.g., an IVML compound, return $\undef$ if the operation is used with another type, e.g., an IVML basic type.
+
+For individual algorithms, we indicate and use the actual name as used in the implementation to ease mapping from code to algorithms and back. For ease of reading, we ignore here that elements or results of functions in the actual implementation may be a null pointer implying respective checks. Thus, we simply assume here that unless stated otherwise functions either return $\undef$ or, in case of set or sets or sequences $\set{}$ or $\seq{\text{ }}$, respectively. 
 
 \subsection{IVML elements}
-In this section, we discuss the IVML elements and types that are relevant to the reasoning. For these elements and types we introduce functions to access their respective properties. We focus on functions that are used for specifying the reasoning algorithm rather than all functions defined by the IVML object model. As convention, we use als parameter names $d$ for a variable declaration, $v$ for a configuration variable, $t$ for a type, $val$ for a value and $cfg$ for a configuration consting of decision variables. For temporary/local variables, we use names close by, e.g., $s$ for an iterator variable used for a set of types.
-
-For all IVML elements, we denote $constraints(e)$ as the set of constraints defined for element $e$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. No specific functions are required here for \textit{basic types} (Boolean, Integer, Real String). In IVML, a \textit{configuration reference} points to a variable in the same project or elsewhere. A configuration reference is indicated through the generic reference type, e.g., \IVML{refTo(SomeCompound)}. As the actual IVML specification \TBD{IVML-spec} does not define specific properties or operations for reference types, we assume here 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 evaluated on the referenced variable.
+In this section, we recapitulate the IVML elements and types that are relevant to reasoning for IVML. For these elements and types we introduce functions to access their respective properties. We focus here on functions that are used for specifying the reasoning algorithm rather than all functions defined in the IVML object model. 
+
+As a convention to ease reading the algorithms presented later, we use $d$ for variable declarations, $v$ for configuration variables, $t$ for types, $val$ for a values, $c$ for constraints and $cfg$ for configurations consting of decision variables and their associated values. For temporary/local variables, we typically use a name close by, e.g., $w$ for an iterator variable (instead of $v$) etc.
+
+For all IVML elements, we denote $constraints(e)$ as the set of constraints defined for element $e$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. 
 
 \subsubsection{Variable Declarations}
@@ -161,4 +166,12 @@
 
 $$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{Miscellaneous}
+
+No specific functions are required for translating constraints for / reasoning on \textit{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 model and, therefore, if specified, already part of constraint expressions before reasoning.
+
+In IVML, a \textit{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.
+
+%-----------------------------------------------------------------------------------------------------------------
 
 \section{Reasoning algorithm}\label{sectReasoning}
@@ -252,4 +265,6 @@
  \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange}
 \end{algorithm}
+
+%-----------------------------------------------------------------------------------------------------------------
 
 \section{Constraint translation}\label{sectTranslation}
@@ -606,5 +621,5 @@
 \end{algorithm}
 
-\section{Completeness}\label{sectCompleteness}
+\section{IVML-Completeness}\label{sectCompleteness}
 
 \begin{table*}[h]
@@ -636,9 +651,42 @@
 \end{table*}
 
-
+%-----------------------------------------------------------------------------------------------------------------
+
+\section{Performance Considerations}\label{sectPerformance}
+
+In this section, we briefly collect some observations seen/refactored/solved/left over during the improvement of the reasoner. \TBD{The individual texts may be pretty short, and are currently just intended for remembering/recording the obstacles.}
+
+\begin{itemize}
+    \item For lists of unknown size and for the expected capacity of IVML models, use \textbf{linked lists} instead of array lists. Main operations are adding, iterating over all, and removing elements to clean up memory incrementally, i.e., linked lists can avoid performance-impacting resizing effects. Index-based access is not needed, constraints are just added and one iteration is needed to build up the constraint base or to perform reasoning. Pre-calculation of the expectied size of the data structures per model seems to be unfeasible as this requires a second run over all model elements.
+    \item Process the \textbf{constraint base} iteratively and remove processed constraints directly after processing. This again requires a linked list as otherwise incremental resizing effects can affect the performance. In summary, building the constraint base and reasoning causes peak memory effects that are better from a performance point of view than (re-)allocating big array memory blocks.
+    \item Avoid having too many unneeded \textbf{partitions of the constraint base} being stored during the translation in different lists, that are finally added to the constraint base. Try to directly add constraints where possible to the constraint base, e.g., for default constraints to avoid iterating over the complete constraint base before reasoning. However, due to the prioritization of the constraint types and their required sequence, this is not always possible. One alternative, a numeric prioritization of the individual constraints would require sorting the constraint base, at the new parts not the left-over constraints to be re-evaluated from a previous reasoning steps. However, implicit sorting on insertion according to priorities could help here.
+    \item Create/translate a \textbf{constraint in one step}, if required in compounds split into filling the variability mapping and then creating the constraints based on the actual mapping. 
+    \item Try to figure out whether a certain \textbf{constraint (type) is actually needed} for reasoning and avoid its translation/creation wherever feasible. \TBD{Can we move the decision about keeping a constraint from adding it to the constraint base before constraint creation. However, this requires changes/additional alternatives for different code parts.}. Thus, don't re-process or filter certain constraint types at the end (done in the initial version for default and derived type constraints), as this implies iterating multiple times over the (partial) constraint base and re-creating/throwing away constraint instances in memory.
+    \item \TBD{Avoid storing constraints that can be \textbf{processed immediately}, e.g., default constraints. However, if a default constraint fails, it must be added to the constraint basis for later possible re-evaluation if dependent values become available/right.}
+    \item For identifying whether constraints are already in the constraint base, use a \textbf{fast look-up structure} instead of an iteration over the constraint base. Although the initial implementation utilized here reference equality (faster than the equals method), the current lookup structure is significantly faster than the original approach trading off execution speed for (peek) memory. Here a lookup structure based on reference equality could further speed up reasoning, which, however, may in the end be slower than the built in collections due to JIT compilation and JVM optimization effects.
+    \item Incremental reasoning using a \textbf{stored constraint base} may speed up reasoning but only achieves this through large memory allocations. Ensure initializing the model through default constraints so that the actual stored constraint base only contains really needed constraint types, i.e., no default constraints and, if possible, no constraints for which all depending variables are already frozen.
+    \item \textbf{Reuse visitor instances} if applied more than once, in particular reasoners with more complex internal data structures such as maps or lists. This required some refactoring of the IVML model implementation.
+    \item \textbf{Avoid} iterators, temporary constraint creation, temporary data structures wherever possible.
+\end{itemize}
+
+\section{Evaluation}\label{sectEvaluation}
+
+\TBD{Keep or remove that section. However, some basic performance evaluations should not be so difficult. All executions need multiple runs, in particular to even out JIT compilation. It seems that this is done during/after the second reasoning run. Potential topics:
+
+\begin{itemize}
+    \item Artificial models of some size/variable/constraint ratio. Christian had a generator for that and Roman typically did some evaluations using these models. Compare to known results where available.
+    \item QualiMaster full, incremental, runtime reasoning (full, no defaults, no frozen, reuse constraint base). Runtime vs. full reasoning seems to behave rather linearly, at around 23 constraints evaluated per ms. Compare to known results where available.
+    \item All test cases involving reasoning as an overview map.
+\end{itemize}
+
+}
+
+%-----------------------------------------------------------------------------------------------------------------
 
 \section{Conclusion}\label{sectConclusion}
 
-\TBD{End here if we do not turn this into a TR or more. Else, evaluate, e.g., along the different test versions of EASy, the synthetic cases of Roman, etc.}
+\TBD{We are better than before, we are now more IVML-complete, but not reasoning-complete. Future, integrate with SMT or other solvers for left-over reasoning problems or configuration completion/instance creation (potential student work).}
+
+%-----------------------------------------------------------------------------------------------------------------
 
 \section*{Acknowledgements}
