Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 135) +++ /reasoner/reasoner.tex (revision 136) @@ -74,9 +74,9 @@ 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). +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). The \emph{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system inspired by object-orientation, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (e.g., for binding times), quantification constraints, or user-defined constraint functions. The core idea of IVML is to represent a variability, i.e., a configuration option, as a typed variable. IVML even allows for modeling topological variability, i.e., configuring and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. -In this document, we discuss the approach and the design of the reasoning mechanism for IVML as well as its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}, an Open Source product line toolset implementing IVML. At its core, the reasoner 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. On the one hand side, this allows for performing typical validation and propagation tasks, but, on the other hand side, this currently does not support advanced reasoning functionality such as configuration completion. This document is mainly intended to summarize the actual state, the ideas behind individual steps of the reasoning process and the decisions made for realizing the reasoning. Besides the pure technical documentation, our specific constributions are: +In this document, we discuss the approach and the design of the reasoning mechanism for IVML as well as its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}, an Open Source product line toolset implementing IVML. At its core, the reasoner 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. On the one hand side, this allows for performing typical validation and propagation tasks, but, on the other hand side, this currently does not support advanced reasoning functionality such as configuration completion. This document is mainly intended to summarize the actual state, the ideas behind individual steps of the reasoning process and the decisions made for realizing the reasoning. Besides the pure technical documentation, our specific contributions are: \begin{itemize} @@ -84,8 +84,8 @@ \item Support for IVML type refinements, which can cause implicit effects on the application of constraints. IVML allows defining a type hierarchy, and so the potential types for a configuration option, i.e., a typed variable, can change along the type hierarchy. As types can introduce constraints, the actual constraint base considered during reasoning can change, i.e., constraints must be added or removed as an effect of a value type change. \item Support for IVML constraint variables, i.e., variables that hold constraints (including sets or sequences) and be changed by the configuration. Through constraint variables, IVML explicitly allows introducing, adding, removing and disabling constraints. Consequently, such changes can affect the constraint base considered during reasoning. - \item Instantiation of type-based constraints to variable-based constraints as a basis for a subsequent reasoning chain. For such subsequent reasoners, the IVML reasoner provides a solid basis, detailed error messages including the failed instantiated constraints so that a chained reasoner can directly continue with these constraints. We envision for future work, that further reasoning steps may add complementing reasoning functionalities such as identifying a value from narrowing constraints. + \item Instantiation of type-based constraints to variable-based constraints as a basis for a subsequent reasoning chain. For such subsequent reasoners, the IVML reasoner provides a solid basis, detailed error messages including the failed instantiated constraints so that a chained reasoner can directly continue with these constraints. We envision for future work, that further reasoning steps may add complementing reasoning functions such as identifying a value from narrowing constraints. \end{itemize} -This document is structured as follows: Section \ref{sectApproach} provides an overview to our approach. Section \ref{sectNotation} introduces the notation that we use throughout this document to specify the algorithms, i.e., we introduce notations for sets, sequences, substitutions as well as relevant parts of the IVML object model realizing the various IVML concepts, here in terms of notations for accessing (derived) properties of the IVML model. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints and reasoning. In Section \ref{sectTranslation}, we detail the translation of constraints for all IVML modeling concepts. The result is a set of instantiated constraints that can be used for reasoning. Section \ref{sectTranslation} includes also the mechanism for re-scheduling constraints when value types or constraint variables change, as this mechanism heavily relies on the constraint translations discussed before. In Section \ref{sectCompleteness}, we analyze the translations in order to assess their completeness with respect to IVML concepts and indicate the state of the validiation, i.e., regression test cases checking that the constraint translations are applied correctly for specific modeling situations. In Section \ref{sectEvaluation}, we present an evaluation of the actual performance of the reasoning approach for different kinds of IVML models. In Section \ref{sectPerformance}, we summarize performance issues, findings and resolutions we made while revising the reasoner, in particular to avoid that future modifications violate already resolved performance anti-patterns. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook on future work. +This document is structured as follows: Section \ref{sectApproach} provides an overview to our approach. Section \ref{sectNotation} introduces the notation that we use throughout this document to specify the algorithms, i.e., we introduce notations for sets, sequences, substitutions as well as relevant parts of the IVML object model realizing the various IVML concepts, here in terms of notations for accessing (derived) properties of the IVML model. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints and reasoning. In Section \ref{sectTranslation}, we detail the translation of constraints for all IVML modeling concepts. The result is a set of instantiated constraints that can be used for reasoning. Section \ref{sectTranslation} includes also the mechanism for re-scheduling constraints when value types or constraint variables change, as this mechanism heavily relies on the constraint translations discussed before. In Section \ref{sectCompleteness}, we analyze the translations in order to assess their completeness with respect to IVML concepts and indicate the state of the validation, i.e., regression test cases checking that the constraint translations are applied correctly for specific modeling situations. In Section \ref{sectEvaluation}, we present an evaluation of the actual performance of the reasoning approach for different kinds of IVML models. In Section \ref{sectPerformance}, we summarize performance issues, findings and resolutions we made while revising the reasoner, in particular to avoid that future modifications violate already resolved performance anti-patterns. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook on future work. %----------------------------------------------------------------------------------------------------------------- @@ -136,5 +136,5 @@ In this section, we discuss the IVML elements and types that are relevant for IVML reasoning. 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 that are 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 assigned values. For temporary/local variables, we typically use a name close by, e.g., $w$ for an iterator variable (instead of $v$) etc. 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. +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 consisting of decision variables and their assigned values. For temporary/local variables, we typically use a name close by, e.g., $w$ for an iterator variable (instead of $v$) etc. 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 all IVML elements introduced in the following subsections, we denote the set of constraints\footnote{Duplicates do not matter in this document as constraints are usually rather unique structures. The only effects of duplicates could be unintended re-evaluations or unintended multiple error messages for the duplicated constraints.} defined for element $e$ by $constraints(e)$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. Further, for a model element $e$, $parent(e)$ denotes the model element $e$ is nested within, typically, a compound or a project. @@ -241,7 +241,7 @@ Moreover, \IVML{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint stored as a value of a constraint variable is extracted and then evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the old constraint must be discarded or even replaced by the new constraint value and considered in the subsequent reasoning process. $isConstraint(t)$ indicates whether type $t$ is a constraint type. %$isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to unconditionally change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} the constraint \IVML{x = 25;} in IVML notation is an assignment Constraint. -During the constraint instantiation, variables must be substituted by other variables or expressions. Let $c$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{y}. For example, if the constraint $c$ was before the substitution \IVML{x = 25}, it will be \IVML{y = 25} after the substitution. The right side of a substition can be a variable or, more generally, an expression. Substitutions are transitive, i.e., in $\varSubstitution{c}{x=y,y=z}$ $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. Substitutions can also be expressed in terms of a mapping to express multiple substitutions or to create up / reuse the substitution specification for several constraints. Let $\variableMapping=\set{\mapEntry{x}{e}}$ be a mapping, then $x$ is the variable to be replaced, $e$ the replacing variable/expression and $\varSubstitutionVarMapping{c}$ denotes the respective substitution. Both notations can be combined, e.g., to $\varSubstitutionOtherVarMapping{c}{x = y}$. - -During the constraint instantation, also new constraints must be created. For this purpose, we use a specific notation to indicate constraint creation and the construction of sub-expressions. This notation combines algorithm elements, e.g., variables, carrying actual values/elements (written in mathematical notation) and IVML expression constructors (stated in teletype). For example, for creating the IVML constraint \IVML{x = 25;} we write $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the creation of the expression making up the constraint. Here, \IVML{assng} is the constructor for the assign operation defined by IVML (actually implementing the assignment in \IVML{x = 25}) returning a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may generically denote $\createConstraint{\IVML{assign}(x, 25)}$, with $x$ being determined by the algorithm. +During the constraint instantiation, variables must be substituted by other variables or expressions. Let $c$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{y}. For example, if the constraint $c$ was before the substitution \IVML{x = 25}, it will be \IVML{y = 25} after the substitution. The right side of a substitution can be a variable or, more generally, an expression. Substitutions are transitive, i.e., in $\varSubstitution{c}{x=y,y=z}$ $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. Substitutions can also be expressed in terms of a mapping to express multiple substitutions or to create up / reuse the substitution specification for several constraints. Let $\variableMapping=\set{\mapEntry{x}{e}}$ be a mapping, then $x$ is the variable to be replaced, $e$ the replacing variable/expression and $\varSubstitutionVarMapping{c}$ denotes the respective substitution. Both notations can be combined, e.g., to $\varSubstitutionOtherVarMapping{c}{x = y}$. + +During the constraint instantiation, also new constraints must be created. For this purpose, we use a specific notation to indicate constraint creation and the construction of sub-expressions. This notation combines algorithm elements, e.g., variables, carrying actual values/elements (written in mathematical notation) and IVML expression constructors (stated in teletype). For example, for creating the IVML constraint \IVML{x = 25;} we write $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the creation of the expression making up the constraint. Here, \IVML{assng} is the constructor for the assign operation defined by IVML (actually implementing the assignment in \IVML{x = 25}) returning a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may generically denote $\createConstraint{\IVML{assign}(x, 25)}$, with $x$ being determined by the algorithm. @@ -257,5 +257,5 @@ A \emph{compound} is an IVML type, which consists of nested variable declarations, called slots. Let $t$ be a compound type, then $isCompound(t)$ returns $true$ and $false$ for all other types. The declared slots of a compound $t$ can be accessed through $slots(t)$. Akin to a variable declaration, for slot $s$ $name(s)$, $default(s)$ and $type(s)$ are defined. -Compounds can form an inheritance hierarchy. $refines(t)$ represents the set of compound types directly refined by compound $t$ through multii-inheritance, returning an empty set if there are no such compounds or if $t$ is not a compound type. Individual slots from parent compounds can thereby shadowed / redefined by slots of the same or more specific type. We define +Compounds can form an inheritance hierarchy. $refines(t)$ represents the set of compound types directly refined by compound $t$ through multi-inheritance, returning an empty set if there are no such compounds or if $t$ is not a compound type. Individual slots from parent compounds can thereby shadowed / redefined by slots of the same or more specific type. We define % $$allRefines(t) = @@ -329,5 +329,5 @@ \subsubsection{Containers}\label{sectNotationContainers} -An IVML \emph{container} is a parameterized type representing a structure that holds an arbitrary number of variables / values. IVML defines two default container types, namely \emph{sequence} (duplicates allowed, order important) and \emph{set} (no duplicates allowed, order irrelevant). The type parameters of a container are not relevant for reasoning, as we can assume that the static type compliance is checked by the IVML object model or the IVML parser before reasoning. +An IVML \emph{container} is a parametrized type representing a structure that holds an arbitrary number of variables / values. IVML defines two default container types, namely \emph{sequence} (duplicates allowed, order important) and \emph{set} (no duplicates allowed, order irrelevant). The type parameters of a container are not relevant for reasoning, as we can assume that the static type compliance is checked by the IVML object model or the IVML parser before reasoning. Let $c$ be a container, then $elements(c)$ denotes the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$. Further, $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} in IVML notation, $contained(t)$ returns \IVML{setOf(Integer)}. @@ -483,39 +483,39 @@ \subsubsection{Variable Mapping}\label{sectVarMapping} -During the constraint translation, top-level constraints can directly be applied to the involved top-level variables. As mentioned above, constraints defined on compound slots or indirectly through use of compound instances in containers must be treated differently. The particular issue here is that these constraints can be defined on types rather than top-level variables, which is possible but valid only for individual top-level variables, and for evaluating the related constraints, the must be rewritten to utilize through accessors based on top-level variables. To manage the various lots and access expressions, the translation utilizes a stack-based data structure, onto which we push/pop a stack (context) frame for each IVML project and each contained compound type, container type or combinations of both used in variables of a project. A context frame linkes all currently relevant variables to the respective accessor expressions, which are created before the respective translation. - -However, a simple stack is not sufficient, as IVML projects may contain assignment-blocks. An assignment-block implicitly defines constraints for its contained variable declarations including containers or compounds. If we translate first the variable declarations and then the constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, leading to wrong constraint translations and erroneous reasoner failures. While changing the translation sequence would be one option, it would also intermingle compund/container translation with annotation-block translation. Thus, we opted to extend the notion of a context stack, allowing to register a declaration with its context frame, to store this registration in the parent context frame and to activate/deactivate such a frame upon translating the implicit assignment-block constraints for a given variable declaration. Registered stack frames are removed from the stack structure when the parent context frame is popped from the stack. - -The variable mapping stack structure $\variableMapping$ of the IVML reasoner provides the following operations: +During the constraint translation, top-level constraints can directly be evaluated over involved top-level variables. As already mentioned in Section \ref{sectNotationConstraints}, constraints defined on compound slots or indirectly through use of compound instances in containers must be translated before evaluation. The particular issue here is that these constraints can be defined in an IVML model over types (for which no values can be assigned in a configuration) rather than over top-level variables. A solution is to rewrite these constraints by substituting type-local variables by appropriate accessors starting at top-level variables. To manage the various lots and access expressions, the translation utilizes a stack-based data structure, onto which we push/pop a context frame for each IVML project and each contained compound type, container type or combinations of both used in variables of a project. A context frame links all currently relevant variables to the correct accessor expressions, which are created before the respective variable substitutions are applied. + +However, a simple stack is not sufficient for two reasons, namely nested complex types, excluded types and assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames can store the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. The constraint rescheduling re-uses the constraint transformation. However, performing a complete transformation of all types related to certain value change is typically not needed, so that excluding types from the translation speeds up the re-scheduling operations. Moreover, IVML projects and compounds can contain nested assignment blocks. An assignment block implicitly defines assignment constraints for its contained variable declarations including containers or compounds. If we translate first variable declarations and then the related constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, i.e., wrong constraints would be added to the constraint bae. Intermingling compund/container translation with annotation-block translation would be a potential solution, which increases the algorithm / code complexity. Thus, we opted to register a declaration with its context frame (which is then implicitly registered with its parent frame for proper cleanup) and to activate/deactivate such a frame, although it is not on top of the stack, when translating the implicit assignment constraints in an assignment block. Such stack frames are also removed from the stack when popping the respective parent context frame. + +In summary, the variable mapping stack structure $\variableMapping$ of the IVML reasoner provides the following operations: \begin{itemize} \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. \item $isContextsRegistering(\variableMapping)$ returns whether context registering is currently active. - \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, the new frame will be registered with the parent frame for $var$ (unless $var=\undef$) Further, $r$ indicates whether already processed types shall be recorded by this context, which is important for handling recursive types. - \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating a quantified constraint, namely the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}. - \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the containing IVML project, is not removed by this operation. - \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variabe declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$. - \item $getMapping(\variableMapping, d)=\variableMapping[d]$ returns the mapping for $d$. If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. - \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If $isCompound(t)$, this function performs a registration for $allRefined^+(t)$. - \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered in one of the enclosing contexts. - \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ from the current context frame. As long as the current context frame exists, this operation can be called over and over. If no context frame is registered for $d$, the stack is not modified. - \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists. + \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, $r$ indicates whether the new frame shall be registered with the parent frame and whether already processed types (for handling nested complex types) shall be recorded by this context. + \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating an all-quantified constraint prefix for all constraints added to the constraint base as long this frame is on the stack. The information includes the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}. + \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the enclosing IVML project, is not removed by this operation. + \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variable declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$. + \item $getMapping(\variableMapping, d)$ returns the mapping for $d$. If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. + \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If \linebreak[4] $isCompound(t)$, this function registers $allRefined^+(t)$. + \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the enclosing context frames. + \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ taken from the current context frame. As long as the current context frame exists, this operation can be called again and again. If no context frame is registered for $d$, the stack is not modified. + \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists on the stack. \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}. - \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type rather and avoids applying them some nested type. - \item $currentType(\variableMapping)$ returns the type $t$ stored in the current contect by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happend on the current context. - \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is excluded in the current context and $excludedTypes(\variableMapping)$ returns all excluded types for the current context or an empty set. - \item $size(\variableMapping)$ the number of contexts on the stack. There is at least always one context on the stack representing the containing project. + \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type and avoids applying them some nested type. + \item $currentType(\variableMapping)$ returns the type $t$ stored in the current context by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happened for the current context. + \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is excluded in the current context. $excludedTypes(\variableMapping)$ returns all excluded types for the current context or an empty set. + \item $size(\variableMapping)$ the number of contexts on the stack. There is always at least one context on the stack representing the enclosing project. \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project. \end{itemize} -From a black-box perspective, $\variableMapping$ can be considered as a usual map as discussed in Section \ref{sectGeneralNotation}. Thus, we just use $\variableMapping$ in the variable substitution notation as introduced in Section \ref{sectNotationConstraints}, e.g., let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ with definition $d$ by $\variableMapping[d]$, respectively. - -For translating containers, context frames can store additional information. We will provide details along with the translation of containers in Section \ref{sectContainerDefaults}. +From a black-box perspective, $\variableMapping$ can be considered as a usual map as discussed in Section \ref{sectGeneralNotation}, but performing some stack-based lookup operations. Thus, we just use $\variableMapping$ in the variable substitution notation as introduced in Section \ref{sectNotationConstraints}, e.g., let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ having a mapping (through the $getMapping$ operation) in at least on context frame of $\variableMapping$. + +%For translating containers, context frames can store additional information. We will provide details along with the translation of containers in Section \ref{sectContainerDefaults}. \subsubsection{Scope Assignments}\label{sectScopeAssignments} -Due to the potentially nested nature of IVML projects, the knowledge about when an assignment to a variable has been made cannot be maintained by a flat mapping, rather than a data structure which stores information about assignments per project (scope). This information is important to detect invalid variable re-assignments, i.e., a variable is not allowed to be assigned more than once per scope \cite{IVML-LS}. - -The scope assignments structure of the IVML reasoner (usually named $\scopeAssignments$) provides the following operations: +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: \begin{itemize} @@ -523,10 +523,10 @@ \item $addAssignment(\scopeAssignments, v)$ indicates that variable $v$ was changed through an assignment within the actual scope. \item $wasAssigned(\scopeAssignments, v)$ returns whether variable $v$ was assigned in the actual scope. This operation is used to validate an assignment before it is performed out by the expression evaluator. - \item $clearAssignments$ clears all assignments in all scopes. + \item $clearAssignments()$ clears all assignments in all scopes. \end{itemize} \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. On top level, there are IVML variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions become relevant when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated from type constraints to variable constraints. +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\footnote{These elements can technically be identified through a model visitor.} 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. \begin{algorithm}[H]