Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 187) +++ /reasoner/consTranslation.tex (revision 188) @@ -172,5 +172,5 @@ If constraints shall be translated, Algorithm \ref{algTranslateCompoundDeclaration} calls Algorithm \ref{algTranslateCompoundContent}, pops the previously created context, records $t$ as processed and returns that no further compound translation ($NONE$) is needed for $t$. -We detail now the variable mapping for compounds. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t$ and creates for each slot a respective accessor. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$). +We detail now the variable mapping for compounds. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots defined for the given compound type $t$ including shadowed ones along the refinement hierarchy starting at $t$. If a slot already has a local access expression mapping (line \ref{algRegisterCompoundMappingExMapping}), it is shadowed and we just use the already registered more specific expression. If no mapping exists, Algorithm \ref{algRegisterCompoundMapping} a respective accessor for slot $s$. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$). Given a complete mapping for compound type $t$, we can transform the constraints, i.e., apply Algorithm \ref{algTranslateCompoundContent}. As mentioned above, the algorithm first translates all default value expressions of slots, then the default values from annotation assignments, and, finally, the constraints in eval blocks with higher evaluation priority as well as the remaining nested constraints. When translating the default value expression for slots, Algorithm \ref{algTranslateCompoundContent} calls Algorithm \ref{algTranslateDeclaration}, and, thus, triggers a potentially recursive translation along the respective slot types, in particular in case of compound or container slots. @@ -181,6 +181,9 @@ \KwData{variable mapping $\variableMapping$} - \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca, s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} + \ForAll{$s \iterAssng slots^+(t)$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots + $x \assng getLocalMapping(\variableMapping, name(s))$\; \label{algRegisterCompoundMappingExMapping} + \If{$x = \undef$} { + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca, s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} + } $registerMapping(\variableMapping, s, x)$\; \ForAll{$a \iterAssng annotations(s)$}{ Index: /reasoner/introduction.tex =================================================================== --- /reasoner/introduction.tex (revision 187) +++ /reasoner/introduction.tex (revision 188) @@ -12,4 +12,5 @@ \item An IVML-complete reasoning mechanism, i.e., translation and reasoning for a complex, rich and typed variability modeling language. \item Support for IVML type refinements, which can cause imply changes to the set of active constraints during reasoning. For short, IVML allows defining a hierarchy of types, and so the potential types for a configuration option can change along the type hierarchy. As types can introduce different constraints, the actual constraint set considered during reasoning can change, i.e., constraints must be added or removed as an effect of a value (type) change. + \item Support for shadowed / redefined IVML compound slots, i.e., properly applying constraints for shadowed slots to the most specific slot in a compound hierarchy. \item Support for IVML constraint variables. IVML supports variables that hold a constraint, i.e., a configuration can explicitly define, add, remove or disable constraints, i.e., actively change the constraint set during reasoning. \item Although the current reasoning approach is not reasoning complete, it is designed to act as the first step in a chained reasoning approach. 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 working with these constraints. Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 187) +++ /reasoner/mainAlgorithms.tex (revision 188) @@ -97,4 +97,5 @@ \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$ (for short $\variableMapping[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 $getLocalMapping(\variableMapping, n)$ returns the mapping for variable / slot name $n$ within the actual context frame. If there is no registration, 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. Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 187) +++ /reasoner/notation.tex (revision 188) @@ -94,5 +94,5 @@ \subsubsection{Project}\label{sectNotationProject} -A \emph{project} is a named scope, which can contain variable declarations, type declarations, annotation assignment blocks and \IVML{eval}-blocks. $isProject(p)$ returns $true$ for a project $p$. $decls(p)$ denotes the set of all variable declarations and $annotations(p)$ all annotation declarations introduced in project $p$. +A \emph{project} is a named scope, which can contain variable declarations, type declarations, annotation assignment blocks and \IVML{eval}-blocks. $isProject(p)$ returns $true$ for a project $p$. $decls(p)$ denotes the set of all variable declarations and $annotations(p)$ all annotation declarations introduced in $p$. A project constitutes the evaluation scope for all contained constraints, i.e., during the evaluation of a project, a variable must not be assigned more than once~\cite{IVML-LS}. As stated above, local variables are evaluated within their containing local scope and can be re-assigned. @@ -154,5 +154,5 @@ Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To provide an overview of the transformations performed by an algorithm, we use constraint transformation patterns. The algorithm then applies constraint and expression creations as well as variable substitutions to realize the respective transformations. -A \emph{constraint transformation pattern} indicates how a certain IVML model fragment is instantiated to a corresponding constraint given in IVML constraint notation rather than the algorithm notation for creating constraints introduced in this section. The model fragment acting as prerequisite is given on the left side of the derivation symbol $\patternDerivationSymbol$, the corresponding constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are given in italics to indicate the information flow between both sides. Constant parts are given in normal font, IVML syntax in \IVML{teletype}. One or more transformation patterns are displayed in a gray box. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$. +A \emph{constraint transformation pattern} indicated by a gray background box summarizes how one or more IVML model fragments are transformed for reasoning. The model fragment acting as prerequisite is given on the left side of the derivation symbol $\patternDerivationSymbol$, the resulting constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are denoted in italics to indicate. Variable parts used on both sides indicate the information flow between prerequisite and transformation result. Constant parts are given in normal font or in case of IVML language elements in \IVML{teletype}. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$. \grayPara{ @@ -165,12 +165,12 @@ \subsubsection{Compounds}\label{sectNotationCompounds} -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 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 +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. Within the context of a compound value, \IVMLself{} represents the actual instance of the compound and ca be used in expressions, in particular as argument for (user-defined) functions. + +Compounds can form an inheritance hierarchy. $refines(t)$ represents the set of compound types directly refined by compound $t$, returning an empty set if there are no such compounds or if $t$ is not a compound type. Individual slots from parent compounds can be shadowed / redefined by slots of the same or more specific type. We define % $$allRefines(t) = \begin{cases} \emptySet, & \text{if } refines(t) = \emptySet \\ - \begin{aligned}all&Refines(t)~\cup\\ &\bigcup_{u\in refines(t)} allRefines(u),\end{aligned} & \text{else} + \begin{aligned}&refines(t)~\cup\\ &\bigcup_{u\in refines(t)} allRefines(u),\end{aligned} & \text{else} \end{cases} $$ @@ -184,9 +184,24 @@ \end{cases}$$ % -as the set of all refined compounds along the compound refinement hierarchy of $t$ including $t$ itself. Let $t$ and $s$ be compound types. Then we denote $\subTypeOf{t}{s}$ if $t\in allRefines(s)$, i.e., $s$ is a subtype of $t$. Similarly, $\subTypeEqOf{t}{s}$ if $t\in allRefines^+(s)$. Based on these functions, the set of all slots for compound type $t$ can be obtained by -% -$$slots^+(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ - -A compound $t$ can define own nested assignment blocks $assignments(t)$ (related functions are defined for compounds akin to Section \ref{sectNotationProject}) and constraints $constraints(t)$. All declared compound constraints +as the set of all refined compounds along the compound refinement hierarchy of $t$ including $t$ itself. Let $t$ and $s$ be compound types. Then we denote $\subTypeOf{t}{s}$ if $t\in allRefines(s)$, i.e., $s$ is a subtype of $t$. Similarly, $\subTypeEqOf{t}{s}$ if $t\in allRefines^+(s)$. All slots for compound type $t$ (including shadowed ones in sequence of the refinement hierarchy) can be obtained by +% +$$slots^+(t) = \seq{slots(t)}~\addSeq \bigoplus_{u\in refines(t)} slots^+(u)$$ +% +%In some constraint transformations it is important to determine, whether a compound slot is shadowed / overridden. Let $d$ be a (slot) declaration, in particular $d\in %slots(t)$, then the parent compound of $d$ skipping potentially enclosing nested assignment blocks is +%% +%\begin{align*} +%parent&Compound(d) = \\ +% &\begin{cases} +% parent(d), & \begin{aligned}\text{if }& parent(d) \neq \undef \wedge{}\\ &isCompound(parent(d)) \end{aligned}\\ +% parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ +% \undef, & \text{else} +% \end{cases} +%\end{align*} +% +%and we can determine whether $d$ is overridden by +%% +%$$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ + +A compound $t$ can define own nested assignment blocks denoted by $assignments(t)$ and constraints $constraints(t)$. Related functions are defined for compound assignment blocks akin to Section \ref{sectNotationProject}. All declared compound constraints %\footnote{The implementation unifies $allCompoundConstraints(t)$ with $allVariableConstraints(t)$ distinguished by a boolean parameter. We differentiate them here to indicate the sets to be transformed more clearly.} for compound type $t$ are @@ -204,38 +219,21 @@ %% -Let $v$ be a compound variable, i.e., a variable of a compound type $t$. Then $decision(v, s)$ returns the configuration variable representing slot $s$ in the compound variable $v$. As in the implementation, $slots(v)$ returns also all slots inherited from refined compounds including those defined in nested assignment blocks. -% -%For convenience, we introduce a function returning all default slots of a variable $v$ -%% -%$$dfltSlots(v) = \setWith{s}{s\in slots(v) \wedge default(s) \neq \undef}$$ %, compound slots of $v$ having default value expressions, empty for all non-compound types -%% - -% -In some constraint transformations it is important to determine, whether a compound slot is overridden. Let $d$ be a declaration, in particular $d\in slots(t) \wedge isCompund(t)$, then the parent compound of $d$ skipping potentially enclosing nested assignment blocks is -% -\begin{align*} -parent&Compound(d) = \\ - &\begin{cases} - parent(d), & \begin{aligned}\text{if }& parent(d) \neq \undef \wedge{}\\ &isCompound(parent(d)) \end{aligned}\\ - parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ - \undef, & \text{else} - \end{cases} -\end{align*} - -and we can determine whether $d$ is overridden / also defined by a refined compound by -% -$$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ - -Akin to projects in Section \ref{sectNotationProject}, $evals(t)$ is defined for a compound type $t$ and returns all eval-blocks nested in $t$. Further, all constraints defined by all nested eval-blocks of $t$ can be obtained using +Akin to a project in Section \ref{sectNotationProject}, $evals(t)$ is defined for a compound type $t$ and returns all eval-blocks directly nested in $t$. Further, all constraints defined by all nested eval-blocks of $t$ can be obtained using % \begin{equation*} allEvalConstraints(t) = \bigcup_{e\in evals(t)}{allEvalConstraints(e)} \end{equation*} -% -\emph{Accessors} to compound variables define a path to access a certain slot within a compound variable, i.e., an accessor specifies the variable and the slot / nested slot path to access. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} defined in \IVML{cmp} looks in IVML notation like \IVML{cmp.slot}. If \IVML{slot} is in turn of compound type, also nested accessors may occur, e.g., \IVML{cmp.slot1.slot2}. For creating such expressions in the constraint translation, we use the IVML access constructor \IVML{acc}. Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor expression can be expressed by $\createExpression{\IVMLMeta{acc}\IVML{(cmp, slot)}}$, while for the second accessor we use $\createExpression{\IVMLMeta{acc}(\IVMLMeta{acc}(\IVML{cmp}, \IVML{slot}),\IVML{slot2})}$. Let $ce$ be an accessor expression, then $compound(e)$ returns the part referring to the compound if $e$ is a compound accessor, $\undef$ else. - -The value of a compound variable can be defined using a complex value expression, a so called \emph{compound initializer}, essentially a name-value mapping. As slots can be, in turn, of a complex type, e.g., of a compound type, a compound initializer can also contain nested complex values, e.g., nested compound initializers. - -Within a compound type, \IVMLself{} is a specific pre-defined value, which represents the actual instance of the compound. Thus, \IVMLself{} is only defined in the context of concrete compound values. As a compound initializer represents a compound value, \IVMLself{} can be used in expressions within a compound initializer, sometimes without direct relation to the underlying compound variable. \IVMLself{} can be evaluated in two different ways: 1) The reasoner tells the expression evaluator for each constraint the actual value of \IVMLself{} or 2) the constraint translation substitutes \IVMLself{} with a respective compound accessor. Typically, we rely on the constraint translation as this avoids managing a context for each constraint. However, when evaluating a (nested) compound initializer, defining a substitution is not obvious, also as the top-level (compound) variable is not always directly available, e.g., as it is determined as part of an expression. In this situation, the expression evaluator can track the actual access path more easily, i.e., while in general, the SSE reasoner relies on constraint translation, in specific situations we delegate the evaluation of \IVMLself{} to underlying mechanisms such as the constraint evaluation. + +Let $v$ be a compound variable, i.e., a configuration variable of a compound type $t$. Then $decision(v, s)$ returns the \emph{slot configuration variable} representing $s$ in the compound decision variable $v$. As in the implementation, $slots(v)$ returns also all (non-shadowed) slots inherited from refined compounds including those defined in nested assignment blocks. +% +%For convenience, we introduce a function returning all default slots of a variable $v$ +%% +%$$dfltSlots(v) = \setWith{s}{s\in slots(v) \wedge default(s) \neq \undef}$$ %, compound slots of $v$ having default value expressions, empty for all non-compound types +%% + +% +\emph{Accessors} to compound variables define a path to access a certain slot within a compound variable, i.e., an accessor specifies the compound variable and the (nested) slots to access in sequence. Let \IVML{cmp} be an IVML variable of a compound type, then an accessor to slot \IVML{slot} defined in \IVML{cmp} looks in IVML notation like \IVML{cmp.slot}. If \IVML{slot} is in turn of compound type, also more complex accessors can occur, e.g., \IVML{cmp.slot1.slot2}. For creating such expressions in the constraint translation, we use the IVML access constructor \IVML{acc}. Following the expression creation notation introduced in Section \ref{sectNotationConstraints}, creating the first accessor expression mentioned above is expressed by $\createExpression{\IVMLMeta{acc}\IVML{(cmp, slot)}}$ and the second by $\createExpression{\IVMLMeta{acc}(\IVMLMeta{acc}(\IVML{cmp}, \IVML{slot}),\IVML{slot2})}$. Let $e$ be an accessor expression, then $compound(e)$ returns the part referring to the outermost compound (value) if $e$ is a compound accessor, $\undef$ else. + +The value of a compound variable can be defined using a complex value expression, a so called \emph{compound initializer}, essentially a name-value mapping. As slots can be, in turn, of a complex type, e.g., of a compound type, a compound initializer can also contain nested complex values. Within the context of a compound initializer, \IVMLself{} represents the actual compound the initializer is defining. However, evaluating \IVMLself{} here is a bit tricky as it changes in nested compound initializers. Technically, the evaluation can be realized in two different ways: 1) The reasoner tells the expression evaluator for each expression the correct value of \IVMLself{} or 2) the constraint translation substitutes even nested occurrences of \IVMLself{} with the correct compound accessor. Typically, we rely in the following algorithms on the second alternative, i.e., constraint translation, as this avoids managing a context for each expression. However, when evaluating a (nested) compound initializer, defining a correct substitution is not trivial and involves creating long nested accessor expressions. In this situation, tracking the actual value of \IVMLself{} within the expression evaluator can be realized more easily. In summary, for most occurrences of \IVMLself{} the SSE reasoner applies constraint translation, while in specific situations we delegate the evaluation of \IVMLself{} to underlying mechanisms such as the constraint evaluation. \subsubsection{Containers}\label{sectNotationContainers}