Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 137) +++ /reasoner/reasoner.tex (revision 138) @@ -26,12 +26,13 @@ \newcommand\undef[0]{\perp} \newcommand\mapEntry[2]{(#1, #2)} -\newcommand\emptySet[0]{\{\}} \newcommand\set[1]{\{#1\}} -\newcommand\setEmpty[0]{\set{}} % or \emptyset +\newcommand\emptySet[0]{\set{}} % or \emptyset +\newcommand\emptyMap[0]{\set{}} % or \emptyset +%\newcommand\setEmpty[0]{\set{}} % or \emptyset \newcommand\setWith[2]{\{#1:#2\}} \newcommand\setWithFlat[2]{\bigcup_{#2}\text{} #1} \newcommand\setSepText[0]{colon } \newcommand\seq[1]{[#1]} -\newcommand\seqEmpty[0]{\seq{\text{ }}} +\newcommand\emptySeq[0]{\seq{\text{ }}} \newcommand\seqWith[2]{[#1:#2]} \newcommand\subTypeOf[2]{#1 \succ #2} @@ -72,5 +73,5 @@ \section{Introduction} -In Product Line Engineering, a \emph{variability model} defines the options to customize a software system, while a \emph{configuration} specifies the choices made for a specific instance / product of the product line. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another customization option. Such dependencies are typically expressed using different forms of \emph{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 \emph{reasoning mechanisms} are utilized, such as SAT-solvers in \cite{BakDiskinAntkiewicz+16, BenavidesTrinidadRuiz-Cortes05, MendoncaBrancoCowan09} or SMT-reasoners in \cite{BakDiskinAntkiewicz+16}. For some models, specific forms of reasoning were even shown to be efficient, e.g., SAT-solving on feature models \cite{MendoncaWasowskiCzarnecki09}. However, the expressiveness of the modeling concepts affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, limit also the feasibility of applying (existing) reasoning mechanisms. +In Product Line Engineering, a \emph{variability model} defines the options to customize a software system, while a \emph{configuration} specifies the choices made for a specific instance / product of the product line. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another customization option. Such dependencies are typically expressed using different forms of \emph{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 \emph{reasoning mechanisms} are utilized, such as SAT-solvers in~\cite{BakDiskinAntkiewicz+16, BenavidesTrinidadRuiz-Cortes05, MendoncaBrancoCowan09} or SMT-reasoners in~\cite{BakDiskinAntkiewicz+16}. For some models, specific forms of reasoning were even shown to be efficient, e.g., SAT-solving on feature models~\cite{MendoncaWasowskiCzarnecki09}. However, the expressiveness of the modeling concepts affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, limit also the feasibility of applying (existing) reasoning mechanisms. 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 with more powerful modeling concepts have been proposed, e.g., supporting non-Boolean variability, sets of variabilities or advanced types of constraints, e.g., first-order logic. One rather popular form of approaches is textual variability modeling, as analyzed in more details in~\cite{EichelbergerSchmid15a}. Such more powerful modeling approaches require also adequate reasoning mechanisms, while the expressiveness of modeling concepts trades off with analyzability~\cite{EichelbergerKroeherSchmid13}. For short, typically more powerful modeling concepts imply limitations of the analysis capabilities, e.g., non-Boolean configuration options typically prevent determining the actual number of possible configurations (in contrast to the number of configuration options that remain to be configured to achieve a complete configuration). @@ -95,7 +96,7 @@ 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 and can be used to express the (meta-)model of a configuration as well as individual configurations. The main concept of IVML is the \emph{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, can be subject to 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 by and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by concepts (and notation) of the Object Constraint Language (OCL)~\cite{OCL24}, 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 so called \IVML{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 reasoning mechanism and executing that mechanism on the translated model. In the past, we identified in particular this transformation as performance bottleneck as well as an obstacle to achieve IVML-completeness, i.e., we were often not able to express all IVML concepts in the respective reasoner model. While traditional reasoners allow for completing a model through feasible ground instances, they typically also perform a kind of constrained state space exploration. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables \cite{EichelbergerQinSizonenko+16, EichelbergerQinSchmid17a}), we experienced that 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, traditional reasoners as well as rule engines are limited as they typically do not support the range of OCL operations required for IVML, in particular container iterators, quantifiers and user-defined constraint operations. Further, also specific reasoning approaches, e.g., for the Object Web Language (OWL) \cite{KahnPorres15, KolliaGlimmHorrocks11} might be an option as they partially support quantification, but they are similarly limited regarding the range of OCL operations. Moreover, OCL-based approaches such as \cite{DemuthLoecherZschaler04, ClavelEgea06} typically also focus on forward-chaining, but would require deep extensions, as OCL does not allow for side-effects or value propagation as required by IVML. - -Due to these experiences, we decided to pursue 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. In our case, the basis for a mixed approach is \emph{forward-chaining}, i.e., evaluation of a given constraint base as long as no constraints are left over, while re-scheduling constraints that depend on a variable changed during reasoning. The SSE IVML reasoner as described in this document realizes this basis, while the actual mixed approach is part of future work. Other work also combine multiple reasoning approaches to achieve advanced reasoning capabilities, e.g., evolutionary algorithms with SAT-solving to realize many-objective optimization for feature modeling \cite{XiangZhouZheng+2018}. +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 reasoning mechanism and executing that mechanism on the translated model. In the past, we identified in particular this transformation as performance bottleneck as well as an obstacle to achieve IVML-completeness, i.e., we were often not able to express all IVML concepts in the respective reasoner model. While traditional reasoners allow for completing a model through feasible ground instances, they typically also perform a kind of constrained state space exploration. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables~\cite{EichelbergerQinSizonenko+16, EichelbergerQinSchmid17a}), we experienced that 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, traditional reasoners as well as rule engines are limited as they typically do not support the range of OCL operations required for IVML, in particular container iterators, quantifiers and user-defined constraint operations. Further, also specific reasoning approaches, e.g., for the Object Web Language (OWL)~\cite{KahnPorres15, KolliaGlimmHorrocks11} might be an option as they partially support quantification, but they are similarly limited regarding the range of OCL operations. Moreover, OCL-based approaches such as~\cite{DemuthLoecherZschaler04, ClavelEgea06} typically also focus on forward-chaining, but would require deep extensions, as OCL does not allow for side-effects or value propagation as required by IVML. + +Due to these experiences, we decided to pursue 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. In our case, the basis for a mixed approach is \emph{forward-chaining}, i.e., evaluation of a given constraint base as long as no constraints are left over, while re-scheduling constraints that depend on a variable changed during reasoning. The SSE IVML reasoner as described in this document realizes this basis, while the actual mixed approach is part of future work. Other work also combine multiple reasoning approaches to achieve advanced reasoning capabilities, e.g., evolutionary algorithms with SAT-solving to realize many-objective optimization for feature modeling~\cite{XiangZhouZheng+2018}. It is important to notice that IVML~\cite{IVML-LS} supports declarative specification of constraints, i.e., modeling concepts and constraints can be specified regardless of their actual evaluation sequence. To ensure that values for variables are uniquely determined, in particular in presence of default values, IVML allows changing the value of a variable only once within a project scope. Otherwise the reasoning mechanism must issue an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in specific situations, some form of sequence of the constraints can be indicated through the concept of partial evaluations, i.e., eval-blocks stated within a project or a compound. An eval-block consists of constraints or nested eval-blocks, while nested eval-blocks implicitly define an evaluation sequence. In other words, a project is the outermost (implicit) eval-block and nested eval-blocks shall be evaluated in their nesting sequence, while eval-blocks on the same nesting level do not imply any evaluation sequence. @@ -105,7 +106,7 @@ As a consequence, the reasoning mechanism must relate type-based constraints to the correct underlying configuration variables. In our approach, we perform first a \emph{constraint translation} to instantiate the constraints for configuration variables based on the actual type of the variable or its value. An alternative could be reasoning over type constraints and modifying the mapping to the variables on demand before evaluation. This may save memory and runtime (required for constraint translation / creation), but, however, also increases the complexity of managing the actual constraints to be evaluated. -Based on our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} and taking into account the specific requirements of the default values, project scopes, eval-block scopes, we are convinced that (at least the first step in a mixed reasoning approach) shall directly operate on an IVML model, also to achieve a high runtime performance. In particular, model transformations such as the constraint translation shall happen only if required to reduce overhead on the reasoning time. After the required constraint translation, constraint evaluation and forward-chaining is executed on the collected constraint base. Besides the resulting configuration, \emph{detained reasoning output} is required, so that subsequent reasoners in a reasoning chain can continue on the results. For this purpose, reasoning error messages shall not only contain the failed constraint, but also additional information such as failing sub-expressions. Based on such output, we can imagine that more advanced reasoning engines such as SMT-reasoners could complement the described approach. Translating the information about 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. However, such chained reasoning is out of the scope of this document. - -Basically, reasoning over all variables of a project including all constraints is needed. This may differ for certain use cases where considering all constraints neither required nor efficient in terms of reasoning time. The first use case is \emph{incremental reasoning}, i.e., starting with a given configuration and just analyzing the changes made by the user. The idea is to provide immediate reasoning results, so that reasoning even on complex and large models can happen upon every change made by the user. The second use case is \emph{runtime reasoning}, e.g., reasoning for validity of a configuration at runtime of a system to identify validations and to trigger re-configuration or adaptation \cite{Eichelberger16}. In this case, we may assume that the underlying IVML model is not changed, so that initially translated constraints can be re-used. This assumption may does not hold in the incremental reasoning case. For supporting these two cases, we introduce two main \emph{reasoning modes}, namely complete (full) reasoning and incremental reasoning, while incremental reasoning can be achieved through the following two techniques. +Based on our experience~\cite{EichelbergerQinSizonenko+16, QMD42, QMD43} and taking into account the specific requirements of the default values, project scopes, eval-block scopes, we are convinced that (at least the first step in a mixed reasoning approach) shall directly operate on an IVML model, also to achieve a high runtime performance. In particular, model transformations such as the constraint translation shall happen only if required to reduce overhead on the reasoning time. After the required constraint translation, constraint evaluation and forward-chaining is executed on the collected constraint base. Besides the resulting configuration, \emph{detained reasoning output} is required, so that subsequent reasoners in a reasoning chain can continue on the results. For this purpose, reasoning error messages shall not only contain the failed constraint, but also additional information such as failing sub-expressions. Based on such output, we can imagine that more advanced reasoning engines such as SMT-reasoners could complement the described approach. Translating the information about 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. However, such chained reasoning is out of the scope of this document. + +Basically, reasoning over all variables of a project including all constraints is needed. This may differ for certain use cases where considering all constraints neither required nor efficient in terms of reasoning time. The first use case is \emph{incremental reasoning}, i.e., starting with a given configuration and just analyzing the changes made by the user. The idea is to provide immediate reasoning results, so that reasoning even on complex and large models can happen upon every change made by the user. The second use case is \emph{runtime reasoning}, e.g., reasoning for validity of a configuration at runtime of a system to identify validations and to trigger re-configuration or adaptation~\cite{Eichelberger16}. In this case, we may assume that the underlying IVML model is not changed, so that initially translated constraints can be re-used. This assumption may does not hold in the incremental reasoning case. For supporting these two cases, we introduce two main \emph{reasoning modes}, namely complete (full) reasoning and incremental reasoning, while incremental reasoning can be achieved through the following two techniques. \begin{itemize} \item \emph{Creation of a partial constraint base:} Constraints assigning already processed default values or constraints over variables that cannot change anymore (frozen variables) are not added to the constraint base. The remaining configuration variables are assumed to be properly initialized or shall be instantiated by the reasoner if possible. Thus, reasoning focuses on non-frozen variables\footnote{In EASy-Producer, this technique can be enabled through the reasoner configuration.}, in particular changed variables. In our experiments, this mechanism can save up to 65\% reasoning time. @@ -125,11 +126,11 @@ In general, we use $\undef$ to denote an \emph{undefined result/value}. Unless stated otherwise, we assume, that operations return a meaningful result even if $\undef$ is passed in as parameter. -As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed. \setEmpty{} is the empty set. We denote the derivation of set $s_1$ from another set $s$ by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over and determining a new value for all elements $i$ in $s$, here through $i+1$. In this notation, conditions / projections may apply to the source set $s_1$. Further, $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. For convenience, we assume for a set $s_3$ that $s_3\text{ } \cup \undef = s_3$. - -For some parts of the reasoning algorithm, in particular to prioritize the evaluation of different constraint types and eval-blocks, we need \emph{sequences}, i.e., structures that hold elements in a given sequence as well as potentially duplicates of the elements. The the order is defined when adding / inserting elements to a sequence. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty{} as the empty sequence. Akin to sets, we denote the derivation of a sequence $q_1$ from another sequence $q$ preserving the order of elements in $q$ by $q_1=\seqWith{i+1}{i \in q}$. Accessing the $i$-th element in sequence $q$ is expressed by $q[i]$. Further, we denote the sequence concatenation by $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements (including duplicates) from $q$ and $q_1$, first the elements from $q$ in the sequence of $q$, then the elements from $q_1$ in their sequence of $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ to denote a sequence concatenation of $q$ and $q_d$ omitting all occurring duplicates. +As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed. \emptySet{} is the empty set. We denote the derivation of set $s_1$ from another set $s$ by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over and determining a new value for all elements $i$ in $s$, here through $i+1$. In this notation, conditions / projections may apply to the source set $s_1$. Further, $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. For convenience, we assume for a set $s_3$ that $s_3\text{ } \cup \undef = s_3$. + +For some parts of the reasoning algorithm, in particular to prioritize the evaluation of different constraint types and eval-blocks, we need \emph{sequences}, i.e., structures that hold elements in a given sequence as well as potentially duplicates of the elements. The the order is defined when adding / inserting elements to a sequence. We denote a sequence by $q=\seq{2, 1, ...}$ and \emptySeq{} as the empty sequence. Akin to sets, we denote the derivation of a sequence $q_1$ from another sequence $q$ preserving the order of elements in $q$ by $q_1=\seqWith{i+1}{i \in q}$. Accessing the $i$-th element in sequence $q$ is expressed by $q[i]$. Further, we denote the sequence concatenation by $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements (including duplicates) from $q$ and $q_1$, first the elements from $q$ in the sequence of $q$, then the elements from $q_1$ in their sequence of $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ to denote a sequence concatenation of $q$ and $q_d$ omitting all occurring duplicates. In some cases, we also need to express a \emph{mapping} between key elements and associated value elements. We denote such a mapping as a set of pairs $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. Within a mapping, key-value pairs are unique with respect to the key. We denote adding a key-value pair to a map by $m \addMap \mapEntry{k}{v}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ is $\undef$. Iterating over a map means iterating over the entries of a map. -As this document is intended to detail the actual implementation and to ease mapping from code to algorithms and back, we use for the \emph{algorithms} (where feasible from the space / layout point of view) the actual name from the implementation. Further, we use parameters and return values as done in the implementation. If global, static or instance data is used, we indicate this in `data' section of the respective algorithm description. For simplifying the reading, we treat null values that may occur in the implementation either through $\undef$ or just omit null pointers and the respective checks needed in the code, i.e., unless stated otherwise, functions return then $\undef$ or, in case of set or sets or sequences $\setEmpty$ or $\seqEmpty$, respectively. +As this document is intended to detail the actual implementation and to ease mapping from code to algorithms and back, we use for the \emph{algorithms} (where feasible from the space / layout point of view) the actual name from the implementation. Further, we use parameters and return values as done in the implementation. If global, static or instance data is used, we indicate this in `data' section of the respective algorithm description. For simplifying the reading, we treat null values that may occur in the implementation either through $\undef$ or just omit null pointers and the respective checks needed in the code, i.e., unless stated otherwise, functions return then $\undef$ or, in case of set or sets or sequences $\emptySet$ or $\emptySeq$, respectively. \subsection{IVML elements} @@ -167,9 +168,9 @@ $value(v)$ denotes the actual value of $v$ and $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$, in particular if $type(v)$ is a refined type through inheritance (cf.~\cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy). We will detail some relevant properties of values below in Section \ref{sectNotationValues}. -As some IVML types allow a nesting of configuration variables, we generically define $nested(v)$ as the set of all variables nested in $v$. Of course, $nested(v)=\setEmpty$ if no nested variables are defined on $v$, $type(v)$ or $type(value(v))$. For a variable $v$, $\forall_{w\in nested(v)}\text{ } parent(w)=v$ must hold. Moreover, let $nested(v, n)$ be the nested variable in $v$ with name $n$, while $nested(v, n)=\undef$ if no such variable is defined. For convenience, we also define +As some IVML types allow a nesting of configuration variables, we generically define $nested(v)$ as the set of all variables nested in $v$. Of course, $nested(v)=\emptySet$ if no nested variables are defined on $v$, $type(v)$ or $type(value(v))$. For a variable $v$, $\forall_{w\in nested(v)}\text{ } parent(w)=v$ must hold. Moreover, let $nested(v, n)$ be the nested variable in $v$ with name $n$, while $nested(v, n)=\undef$ if no such variable is defined. For convenience, we also define % \begin{multline*} allNested(v) = \begin{cases} - \setEmpty, & \text{if } |nested(v)| = 0 \\ + \emptySet, & \text{if } |nested(v)| = 0 \\ \begin{aligned}\set{&nested(v)}~\cup\\ &\setWith{allNested(w)}{w\in nested(v)},\end{aligned} & \text{else}\\ \end{cases} \end{multline*} @@ -177,5 +178,5 @@ \begin{multline*} allParents(v) = \begin{cases} - \setEmpty, & \text{if } \neg isVariable(parent(v)) \\ + \emptySet, & \text{if } \neg isVariable(parent(v)) \\ \begin{aligned}\set{&parent(v)} \cup\\ &allParents(parent(v)),\end{aligned} & \text{else}\\ \end{cases} \end{multline*} @@ -196,5 +197,5 @@ Variables can be \emph{local}, e.g., as they are used in the IVML model as parameters of a user-defined constraint function, as variable in a let let-expression or as an iterator of a collection function. Such variables have the same properties as usual configuration variables, but they just hold a temporary value, may be re-assigned within a certain scope, e.g., iterator variables, typically have the state \IVML{ASSIGNED} and cannot be frozen. Local variables can be identified using $isLocal(v)$, which returns $true$ if $v$ is a local variable. -%For simplifying the descriptions of algorithms, we ignore here the fact that IVML variables can have the IVML value \IVML{null}, i.e., explicitly undefined (and different from a null pointer). While the underlying implementation must contain explicit checks, we just assume here that the functions lead to $\undef$, \setEmpty or \seq{\text{}}, respectively. +%For simplifying the descriptions of algorithms, we ignore here the fact that IVML variables can have the IVML value \IVML{null}, i.e., explicitly undefined (and different from a null pointer). While the underlying implementation must contain explicit checks, we just assume here that the functions lead to $\undef$, \emptySet or \seq{\text{}}, respectively. \subsubsection{Project}\label{sectNotationProject} @@ -407,8 +408,8 @@ \newcommand\otherConstraints[0]{c_{o}} \newcommand\topLevelConstraints[0]{c_{t}} -\newcommand\relevantConstraintsPerType[0]{r_t} +\newcommand\relevantConstraintsPerDeclaration[0]{r_d} \newcommand\relevantConstraintVariables[0]{r_c} \newcommand\scopeAssignments[0]{a} -\newcommand\usedVariables[0]{u} +%\newcommand\usedVariables[0]{u} \newcommand\problemRecords[0]{m} @@ -433,5 +434,5 @@ \SetAlgoLined \KwIn{configuration $c$} - \KwData{configuration $cfg$, expression evaluator $e$, scope assignments $\scopeAssignments$, start time $startTime$, $reuse$ flag, constraint base copy $base_c, base_{\relevantConstraintsPerType}, base_{\relevantConstraintVariables}$, $projects$ sequence, $hasTimeout$ and $stop$ flags, constraints relations $\relevantConstraintsPerType$ and $\relevantConstraintVariables$, problem records $\problemRecords$} + \KwData{configuration $cfg$, expression evaluator $e$, scope assignments $\scopeAssignments$, start time $startTime$, $reuse$ flag, constraint relations $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerDeclaration}, base_{\relevantConstraintVariables}$, $projects$ sequence, $hasTimeout$ and $stop$ flags}%, problem records $\problemRecords$ \KwResult{Reasoning result $r$} @@ -444,7 +445,7 @@ \uIf{$base_c = \undef$}{ \label{algMainLoopFullStart} \If{$reuse$}{ - $base_c = \seqEmpty{}$\; %sequence? - $base_{\relevantConstraintsPerType} = \setEmpty{}$\; %map? - $base_{\relevantConstraintVariables} = \setEmpty{}$\; %map? + $base_c = \emptySeq{}$\; %sequence? + $base_{\relevantConstraintsPerDeclaration} = \emptyMap{}$\; + $base_{\relevantConstraintVariables} = \emptySet{}$\; %map? } $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} @@ -455,5 +456,5 @@ } \label{algMainLoopEnd}\label{algMainLoopFullEnd} }\Else {\label{algMainLoopIncStart} - $\relevantConstraintsPerType \assng base_{\relevantConstraintsPerType}$\;\label{algMainLoopResetRelStart} + $\relevantConstraintsPerDeclaration \assng base_{\relevantConstraintsPerDeclaration}$\;\label{algMainLoopResetRelStart} $\relevantConstraintVariables \assng base_{\relevantConstraintVariables}$\;\label{algMainLoopResetRelEnd} \ForAll{$i \in \set{0, \ldots, |base_c|} \wedge \neg hasTimeout \wedge \neg stop$}{ @@ -469,9 +470,9 @@ First, Algorithm \ref{algMainLoop} sets up the global configuration variable $cfg$ and the expression evaluator\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These details are omitted here.} in lines \ref{algMainLoopSetupVar}-\ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. In line \ref{algMainLoopStartTime} it stores the start time to terminate potentially endless loops induced by ping-pong assignments among constraints within a given maximum time. The remainder of the algorithm is separated into two parts, the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part. -As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per type ($base_{\relevantConstraintsPerType}$) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$). Then, the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, which is determined by the top-level IVML project making up $cfg$ and a cycle-free traversal of the imports of the top-level project. $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns the processing sequence of all projects involved in $cfg$, i.e., the imported projects sorted in ascending manner according to their number of import dependencies. The main reasoning loop processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user requests a stop of the reasoning (global flag $stop$). - -For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ and populates the constraint base as a side effect of the constraint translation called in line \ref{algMainLoopTranslate} (detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled through $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerType}$ and $base_{\relevantConstraintVariables}$. Then the algorithm performs a forward-chaining evaluation of the constraint base in line \ref{algMainLoopEvaluate} (explained in Section \ref{sectTopLevelConstraintsEvaluation}). If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. - -In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to reset the constraint relations in lines \ref{algMainLoopResetRelStart}-\ref{algMainLoopResetRelEnd}, i.e., the relevant constraints per type $\relevantConstraintsPerType$ and the relevant constraint variables per decision variable $\relevantConstraintVariables$, to iterate over all stored projects in $base_c$. For each project, the algorithm takes over the respective constraints from $base_c$ into the actual constraint base, and, as before, evaluates the constraints and freezes the variables. +As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per declaration ($base_{\relevantConstraintsPerDeclaration}$, a mapping of declarations to using constraints) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$, bidirectional mapping between constraint values assigned to configured decision variables). Then, the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, which is determined by the top-level IVML project making up $cfg$ and a cycle-free traversal of the imports of the top-level project. $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns the processing sequence of all projects involved in $cfg$, i.e., the imported projects sorted in ascending manner according to their number of import dependencies. The loop processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user requests a stop of the reasoning (global flag $stop$). + +For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ and populates the constraint base as a side effect of the constraint translation called in line \ref{algMainLoopTranslate} (detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled through $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerDeclaration}$ and $base_{\relevantConstraintVariables}$. Then the algorithm performs a forward-chaining evaluation of the constraint base in line \ref{algMainLoopEvaluate} (explained in Section \ref{sectTopLevelConstraintsEvaluation}). If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. + +In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to reset the constraint relations in lines \ref{algMainLoopResetRelStart}-\ref{algMainLoopResetRelEnd}, i.e., the mapping of constraints per declaration $\relevantConstraintsPerDeclaration$ and the mapping between constraint variables and decision variables $\relevantConstraintVariables$, to iterate over all stored projects in $base_c$. For each project, the algorithm takes over the respective constraints from $base_c$ into the actual constraint base, and, as before, evaluates the constraints and freezes the variables. Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the algorithm composes\footnote{In the implementation, this is done in \class{Engine.java}, the actual reasoner instance, which creates and utilizes instances of \class{Resolver.java}.} in line \ref{algMainLoopResult} a detailed reasoning result based on recorded evaluation problems. This reasoning result also indicates a successful or failed execution, in particular whether a timeout occurred or a user-requested cancellation was requested. @@ -515,5 +516,5 @@ \subsubsection{Scope Assignments}\label{sectScopeAssignments} -Due to the potentially nested nature of IVML projects, the knowledge about when an assignment for a variable has been made cannot be maintained by a simple flat mapping. This requires a data structure, which stores information about assignments per project (scope). This structure is important to detect invalid variable re-assignments, i.e., to figure out whether a variable assigned more than once per scope \cite{IVML-LS}. +Due to the potentially nested nature of IVML projects, the knowledge about when an assignment for a variable has been made cannot be maintained by a simple flat mapping. This requires a data structure, which stores information about assignments per project (scope). This structure is important to detect invalid variable re-assignments, i.e., to figure out whether a variable assigned more than once per scope~\cite{IVML-LS}. The scope assignments structure of the IVML reasoner (usually named $\scopeAssignments$ for assignments) provides the following operations: @@ -528,5 +529,5 @@ \subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation} -The core idea of the constraint translation is to collect the constraints following the structure of an IVML model and to replace each type-related variable by the correct accessor expression for a global variable in the current scope. According to the IVML specification \cite{IVML-LS}, the relevant top-level elements are variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions are considered when when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated. +The core idea of the constraint translation is to collect the constraints following the structure of an IVML model and to replace each type-related variable by the correct accessor expression for a global variable in the current scope. According to the IVML specification~\cite{IVML-LS}, the relevant top-level elements are variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions are considered when when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated. Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. As a side effect, the constraint translation 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 prioritize the constraints correctly, the reasoner uses four global sets, which are populated during the constraint translation and, finally, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets @@ -558,8 +559,8 @@ \tcp{end of model visitor}% 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart} $c \assng pop(base)$\; \label{algEvalLoopPop} - $setAssignmenttScope(\scopeAssignments, c)$\; \label{algEvalLoopSetScope} - $\usedVariables \assng \setEmpty$\; \label{algEvalLoopClear} + $setAssignmentScope(\scopeAssignments, c)$\; \label{algEvalLoopSetScope} + %$\usedVariables \assng \emptySet$\; \label{algEvalLoopClear} $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} - $\problemRecords \assng \problemRecords \addSeq analyzeEvaluationResult(evaluate(e, c), \usedVariables)$\; \label{algEvalLoopAssngEval} + $\problemRecords analyzeEvaluationResult(\problemRecords, evaluate(e, c))$\; \label{algEvalLoopAssngEval} \If{$constraintFulfilled(e) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} - $\relevantConstraintsPerType \assng \relevantConstraintsPerType \cap \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cap \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; \MISSING{mapping to set!} }\label{algEvalLoopClearEnd} $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} @@ -603,19 +604,19 @@ \end{algorithm} -The main loop (lines \ref{algEvalLoopLoopStart}-\ref{algEvalLoopLoopEnd}) runs as long as there are constraints in the constraint $base$, assuming that the evaluation either terminates when all constraints are successfully evaluated (and value changes may add new constraints, cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) or constraints fail and do not induce further constraints. The main loop also stops if reasoning runs into a timeout or is canceled by the user through the $stop$ flag. - -In each iteration of the main loop, the algorithm pops a constraint for evaluation from $base$ (line \ref{algEvalLoopPop}) and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}). - -In order to assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} registers the actual assignment state for the current constraint $c$ (line \ref{algEvalLoopAssngState}).If $c$ is a default constraint, this causes that the subsequent value assignments during the evaluation of $c$ are done with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) through the constraint evaluator. If configuration variables are changed as part of the constraint evaluation, the variables are recorded in $\usedVariables$ (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created, e.g., due to duplicate variable assignments in the same project scope etc. Here, we distinguish three cases. +The main loop (lines \ref{algEvalLoopLoopStart}-\ref{algEvalLoopLoopEnd}) runs as long as there are constraints for evaluation in the constraint $base$, no timeout and no user cancellation request occurred. The (size of the) constraint base changes dynamically during reasoning as Algorithm \ref{algEvalLoop} removes processed constraints and value (type) changes may add constraints, e.g., those involving the changed variable (see Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling} for details). If no value assignment cycles occur, which ultimately lead to a timeout, the evaluation loop either terminates when all constraints are successfully evaluated or failing constraints do not induce the evaluation of further constraints. + +In each iteration of the main loop, the algorithm pops a constraint for evaluation from $base$ (line \ref{algEvalLoopPop}). % and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}). +To assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} registers the actual assignment state for the current constraint $c$ (line \ref{algEvalLoopAssngState}). If $c$ is a default constraint, all subsequent value assignments during the evaluation of $c$ happen with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) by passing it to the constraint evaluator. %If configuration variables are changed as part of the constraint evaluation, the variables are recorded (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). +Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created. We distinguish three cases: \begin{enumerate} - \item Constraint $c$ is evaluated successfully so that existing problem records for $c$ can be removed from $\problemRecords$. - \item Constraint $c$ is evaluated as undefined. As specified by IVML \cite{IVML-LS}, a constraint for which at least one variables or expressions is evaluated to undefined, is also considered undefined. This situation does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. - \item The constraint evaluation fails and a problem record is created including the used variables $\usedVariables$ for detailed error reporting or further (external) analysis. + \item Constraint $c$ is evaluated successfully so that either no problem record is created or potentially existing problem records for $c$ from previously failed evaluations can be removed from $\problemRecords$. + \item Constraint $c$ is evaluated as undefined. As specified by IVML~\cite{IVML-LS}, a constraint is also considered undefined, if at least one involved variable or expression is evaluated as undefined. This does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. + \item The constraint evaluation fails and a problem record for detailed error reporting or further (external) analysis is created. \end{enumerate} -Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them from the set of relevant constraints $\relevantConstraintsPerType$ in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. - -Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This information is particularly relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}. +Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. Please note that no modification of $\relevantConstraintVariables$, the mapping between decision variables and constraints, is needed, as no change of constraint variables or their values occurred here. + +Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This flag is also relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}. @@ -731,5 +732,5 @@ \subsection{Compound types}\label{sectCompoundDefaults} -A compound can define constraints in two differnt places, 1) nested within compound type definitions using qualified slot access expressions or unqualified slot names, and 2) as top-level as constraints with qualified slot access expressions. Both types of constraints imply all-quantification over all instances of the respective compound types \cite{IVML-LS}. We translate compound constraints using the following schema: +A compound can define constraints in two differnt places, 1) nested within compound type definitions using qualified slot access expressions or unqualified slot names, and 2) as top-level as constraints with qualified slot access expressions. Both types of constraints imply all-quantification over all instances of the respective compound types~\cite{IVML-LS}. We translate compound constraints using the following schema: \grayPara{ @@ -1016,5 +1017,5 @@ The translation of assignment-blocks on top-level is triggered by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. The translation of assignment-blocks within compounds is caused by Algorithm \ref{algTranslateCompoundDeclaration} in line \ref{algTranslateCompoundDeclarationCompoundAssignments} (variable mapping in Algorithm \ref{algRegisterCompoundMapping} line \ref{algRegisterCompoundMappingVarMapping} and slot translation in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT} in Algorithm \ref{algTranslateCompoundDeclaration} along with the decision variables of the compound value). In both cases, Algorithm \ref{algTranslateAnnotationAssignments} is called. -Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the set of effective assignments data $ea$ that is relevant for the actual assignment-block $a$ (initially $ea=\emptySet$ for a top-level assignment-block). However, only the innermost assignment is relevant in case of nested assignment blocks \cite{IVML-LS}, so that we build a mapping based on the annotation names overriding assignments inherited from the containing assignment blocks. +Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the set of effective assignments data $ea$ that is relevant for the actual assignment-block $a$ (initially $ea=\emptySet$ for a top-level assignment-block). However, only the innermost assignment is relevant in case of nested assignment blocks~\cite{IVML-LS}, so that we build a mapping based on the annotation names overriding assignments inherited from the containing assignment blocks. For a given assignment-block $a$, the algorithm performs then the transformation of each individual assignment and collects the created constraints in $\otherConstraints$. If the type of the slot (if available the dynamic type of the value) is a compound, the algorithm performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). It is important to note that we temporarily activate a context frame of $\variableMapping$ for each declaration $d$ if a context has been created/registered before during compound translation. This is required as the constraints are actually created after the translation of the types and otherwise we would still use the original variables specified in the model rather than the instantiated ones needed for reasoning. Finally, the algorithm recursively processes contained assignment-blocks. @@ -1122,5 +1123,5 @@ \begin{algorithm}[H] \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$, variable $v$} - \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerType$ , incremental flag $inc$, evals flag $inEvals$} + \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerDeclaration$ , incremental flag $inc$, evals flag $inEvals$} $c = composeExpression(\variableMapping, c)$\; \If{$check$}{ @@ -1138,5 +1139,5 @@ } \If{$\neg isSimpleConstraint(c)$}{ - $\relevantConstraintsPerType \assng \relevantConstraintsPerType \cup \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; % assignConstraintsToVariables + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cup \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; % assignConstraintsToVariables } } @@ -1192,5 +1193,5 @@ -If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the variable is relevant for re-scheduling. First, Algorithm \ref{algVarChange} registers in line \ref{algVarChangeScope} the change of $v$ within the actual project scope if the value of $v$ actually has been affected by reasoning. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then, if the value actually changed, we identify constraints that must be added to or removed from the constraint base. This may be due to nested constraint values (line \ref{algVarChangeRescheduleConstraintVariables}) in the new value as well as a type change of a compound value along the refinement hierarchy, which may require more or less constraints to be considered (line \ref{algVarChangeRescheduleValueTypeChange}). All these cases may affect the relevant constraints. When adding or removing constraints, new constraints are added to $\relevantConstraintVariables$ and $\relevantConstraintsPerType$, while now now irrelevant constraints are identified via $\relevantConstraintVariables$ and also removed from $\relevantConstraintVariables$ and $\relevantConstraintsPerType$. Finally , parent (line \ref{algVarChangeRescheduleParents}) and nested (line \ref{algVarChangeRescheduleNested}) constraints may need to be re-scheduled, too, if the related variables aside from constraint variables changed. This happens through a lookup to $\relevantConstraintsPerType$, implying that previously added / removed constraints due to value type changes are not re-scheduled. +If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the variable is relevant for re-scheduling. First, Algorithm \ref{algVarChange} registers in line \ref{algVarChangeScope} the change of $v$ within the actual project scope if the value of $v$ actually has been affected by reasoning. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then, if the value actually changed, we identify constraints that must be added to or removed from the constraint base. This may be due to nested constraint values (line \ref{algVarChangeRescheduleConstraintVariables}) in the new value as well as a type change of a compound value along the refinement hierarchy, which may require more or less constraints to be considered (line \ref{algVarChangeRescheduleValueTypeChange}). All these cases may affect the relevant constraints. When adding or removing constraints, new constraints are added to $\relevantConstraintVariables$ and $\relevantConstraintsPerDeclaration$, while now now irrelevant constraints are identified via $\relevantConstraintVariables$ and also removed from $\relevantConstraintVariables$ and $\relevantConstraintsPerDeclaration$. Finally , parent (line \ref{algVarChangeRescheduleParents}) and nested (line \ref{algVarChangeRescheduleNested}) constraints may need to be re-scheduled, too, if the related variables aside from constraint variables changed. This happens through a lookup to $\relevantConstraintsPerDeclaration$, implying that previously added / removed constraints due to value type changes are not re-scheduled. If the changed variable is local and there is a mapping in $\variableMapping$, e.g., as the variable is used as iterator in the evaluation of a quantor expression, we adjust the mapping\footnote{Technically, a local decision variable wraps either a value (if the evaluation runs over constants) or a decision variables. To allow for (call-by-reference) propagation on nested slots and attributes, changing the context registration actually refers to the actually wrapped decision variable, but this is not detailed here.}. @@ -1199,5 +1200,5 @@ \SetAlgoLined \KwIn{decision variable $v$, old value $val_o$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$} + \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} \If{$\neg isLocal(v)$}{ @@ -1210,6 +1211,6 @@ } } - $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerType[p]}{p\in allParents(v)}$\; \label{algVarChangeRescheduleParents}%constraintsForParent - $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerType[n]}{n\in allNested(v)}$\; \label{algVarChangeRescheduleNested}%constraintsForParent + $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerDeclaration[p]}{p\in allParents(v)}$\; \label{algVarChangeRescheduleParents}%constraintsForParent + $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerDeclaration[n]}{n\in allNested(v)}$\; \label{algVarChangeRescheduleNested}%constraintsForParent % $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}\relevantConstraints[c]$\; \label{algVarChangeRescheduleNested}%constraintsForChilds, nested geht für alle variablen }\ElseIf{$getMapping(\variableMapping, decl(v)) \neq \undef$}{ @@ -1239,5 +1240,5 @@ \SetAlgoLined \KwIn{parent variable $v_p$, decision variable $v$, clear flag $clear$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$} + \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} \If{$isConstraint(type(v)$} { @@ -1251,5 +1252,5 @@ $base \assng base \addSeq \otherConstraints$\; \ForAll{$p\iterAssng allParents(v)$}{ % variablesMap.addAll(variable, otherConstraints); - $\relevantConstraintsPerType \assng \relevantConstraintsPerType \addMap \mapEntry{p}{\relevantConstraintsPerType [v] \cup \otherConstraints}$\; + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \addMap \mapEntry{p}{\relevantConstraintsPerDeclaration [v] \cup \otherConstraints}$\; } $\otherConstraints \assng \emptySet$\; @@ -1262,5 +1263,5 @@ \SetAlgoLined \KwIn{decision variable $v$, old value $val_o$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$} + \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} \If{$isCompound(v)$}{ @@ -1277,5 +1278,5 @@ \SetAlgoLined \KwIn{decision variable $v$, old value $val_o$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$} + \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} $val_n \assng value(v))$\;