Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 40) +++ /reasoner/reasoner.tex (revision 41) @@ -92,64 +92,103 @@ \subsubsection{Variable Declarations} -An IVML variable declaration $d$ introduces a configuration variable with $name(d)$ and $type(d)$. $annotations(d)$ is the set of (orthogonal) IVML annotation (variable) declarations for a variable declaration $d$. $default(d)$ is an expression specifying the default value of $d$ ($default(d)$ must evaluate to a type compatible with $type(d)$). Moreover, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. +An IVML variable declaration $d$ introduces a configuration variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$. + +\subsubsection{Configuration Variables} + +An IVML configuration variable $v$ is an instance of a variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, for any other IVML element/type $false$. + +$value(v)$ denotes the actual value of $v$, with $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$ (cf. \cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy). + +As types like container or compound require a nesting of configuration variables, we generically define $nested(v)$ as the set of all variables nested in $v$. Of course, $nested(v)=\set{}$ if no nested variables are defined on $v$, $type(v)$ or $type(value(v))$. We define $parent(v)$ as the object $v$ is nested within, which is either the containing configuration if $v$ is a top-level variable or the parent variable, i.e., $\forall_{n\in nested(v)}:parent(n)=v$. For convenience, we also define + +\begin{multline} +allNested(v) = \begin{cases} + \set{}, & \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} + +\begin{multline} +allParents(v) = \begin{cases} + \set{}, & \text{if } \neg isVariable(parent(v)) \\ + \begin{aligned}\set{&parent(v)} \cup\\ &allParents(parent(v)),\end{aligned} & \text{else}\\ \end{cases} +\end{multline} + +Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and $\allowbreak{}annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations potentially inherited from containing project or variables (in case of compounds or containers). Due to the specific semantics of default or frozen variables, IVML variables have an internal state. The state of individual variables is actually changed (indirectly) by the expression evaluator as side effect of constraint evaluation. The following states are defined: \begin{itemize} - \item \IVML{UNDEFINED}: no value has been assigned so far or the value was cleared intentionally. - \item \IVML{DEFAULT}: a type compatible default value has been assigned by evaluating the default value expression of the underlying variable declaration. Default values can be changed unless frozen. Then the variable receives one of the following assignment states. - \item \IVML{ASSIGNED}: a type compatible value has been assigned (by the implementation), but the value is still changable. - \item \IVML{USER\_ASSIGNED}: a type compatible value has been assigned by the user and shall not be overriden by the impelmentation, e.g., the reasoner. - \item \IVML{DERIVED}: a type compatible value has been assigned as a consequence of evaluating constraints, e.g., through the reasoner. - \item \IVML{FROZEN}: the variable was frozen through the IVML \IVML{freeze} statement to avoid further changes of the actual value (including no value in state \IVML{UNDEFINED}). Further assignments are not allowed and cause an assignment error. + \item \IVML{UNDEFINED}: No value has been assigned so far or the value was cleared intentionally through \IVML{null}. + \item \IVML{DEFAULT}: A type compatible default value has been assigned by evaluating the default value expression of the underlying variable declaration. Default values can be changed unless frozen. + \item \IVML{ASSIGNED}: A type compatible value has been assigned (by some EASy component), but the value is still changeable. + \item \IVML{USER\_ASSIGNED}: A type compatible value has been assigned by the user and shall not be overridden by the implementation, e.g., the reasoner. + \item \IVML{DERIVED}: A type compatible value has been assigned as a consequence of reasoning and evaluating constraints. + \item \IVML{FROZEN}: The variable was frozen through the IVML \IVML{freeze} statement to avoid further changes of the actual value (including no value in state \IVML{UNDEFINED}). Further assignments are not allowed and cause an assignment error. \end{itemize} -\subsubsection{Configuration Variables} - -An IVML configuration variable $v$ is an instance of a variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, else $false$. Let $value(v)$ be the actual value of $v$, with $type(value(v))$ compliant with $type(v)$. As types like container or compound require a nesting of configuration variables, we define generically $nested(v)$ as the set of all variables nested in $v$ (may be empty). Similarly, we define $parent(v)$ as the object $v$ is nested within, which is either the containing configuration in case of a top-level variable or a variable, i.e., $\forall_{n\in nested(v)}:parent(n)=v$. Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and $annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations applied to the containing project or variables (in case of compounds or containers). Further, we define two derived functions - -$$allNested(v) = \begin{cases}\set{}, & \text{if } |nested(v)| = 0 \\ \set{nested(v)} \cup \setWith{allNested(w)}{w\in nested(v)}, & \text{else}\\ \end{cases}$$ - -$$allParents(v) = \begin{cases}\set{}, & \text{if } \neg isVariable(parent(v)) \\ \set{parent(v)} \cup allParents(parent(v)), & \text{else}\\ \end{cases}$$ +Please note, as already mentioned in Section \ref{sectApproach} that the value of a variable can be changed at maximum once within a project scope. + +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$, \set{} or \seq{\text{}}, respectively. \subsubsection{Project} -A project is a named scope, which can contain variable declarations, type declarations, assignment blocks and eval blocks. $varDeclarations(p)$ the set of all variable declarations in project $p$. $assignments(p)$ is the potentially nested set of annotation assignments of project $p$, i.e., if $e\in assignments(p)$ then $varDeclarations(e)$ as well as $constraints(e)$ is defined, but may be empty, similarly for $assignments(e)$. $f \in assignmentData(a)$ for an assignment $a$ provides access to the name of the attribute $name(f)$ and the default value expression $default(f)$ specifying the value to be assigned to the attribute with $name(f)$. Moreover, $evals(p)$ is the potentially nested set of eval-blocks in project $p$, i.e., if $e\in evals(p)$ then $constraints(e)$ is defined, but may be empty, similarly for $evals(e)$. - -For simplicity, we ignore in the algorithm descriptions that IVML variables can have the IVML value \IVML{null}, i.e., explicity undefined (and different from a null pointer). While the underyling implementation utilizes in specific cases explicit checks, we just assume here that the defined operations lead to $\undef$. +A project is a named scope, which can contain variable declarations, type declarations, assignment blocks and eval-blocks. $varDeclarations(p)$ denotes the set of all variable declarations introduced in project $p$. $evals(p)$ is the set of (potentially nested) eval-blocks in project $p$, i.e., if $e\in evals(p)$ then $constraints(e)$ is defined, but may be empty, similarly for $evals(e)$. + +An annotation assignment is a block, which specifies the values for given annotations that will be implicitly assigned to all contained variable declarations. To allow orthogonal combinations of annotation assignments, assignment blocks can be nested referring to different annotations. $assignments(p)$ is the set of (potentially nested) annotation assignments of project $p$. If $a\in assignments(p)$ then $varDeclarations(a)$ as well as $constraints(a)$ are defined, but may be empty, similarly for $assignments(a)$. $assignmentData(a)$ for an assignment $a$ provides access to the affected annotations and values, i.e., if $f \in assignmentData(a)$, $name(f)$ is the name of the affected attribute and $default(f)$ its the default value expression specifying the value to be assigned to all attributes with $name(f)$ for all declarations within the containing assignment block. \subsubsection{Constraints}\label{sectNotationConstraints} -As introduced above, a constraint is a Boolean expression that must always be evaluated to $true$. Otherwise, reasoning shall either fail or, after a change of the involved variables, the constraint shall be re-evaluated potentially whiping out a previous reasoning error. A constraint consists of expressions, that can evaluate to any type supported by IVML. These expressions can be used to determine the default value of variables. - -Moreover, \textit{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint within a constraint variable is 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 new constraint must also be re-evaluated. - -We define two basic functions, namely $isConstraint(t)$ indicating wether type $t$ is a constraint type and $isAssignmentConstraint(c)$ whether constraint $c$ changes the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}. - -As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to fill the constraint base. For this purpose, we use a specific constraint creation notation, which combines algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (displayed in teletype) used to build up the constraint expression. In more detail, for creating the IVML constraint \IVML{x = 25;}, we denote $\createConstraint{\IVML{assign(x, 25)}}$, i.e., angle brackets indicate a constraint creation, while \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}, returning a Boolean value indicating whether the execution of the operation succeeded). In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to instantiate the constraint. For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We attach this information to the constraint itself, i.e., for creating a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ - -In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We this as follows: $\createExpression{\IVMLMeta{var}(i, t)}$ creates a temporary variable $i$ of type $t$. +A constraint is a Boolean expression that must always evaluate to $true$. Otherwise, reasoning shall either fail or, after a change of at least one of the involved variables, the constraint shall be re-evaluated potentially wiping out previous reasoning errors for that constraint. A constraint consists of expressions, that can evaluate to values of some type supported by IVML. These expressions can be used to determine the default value of variables. + +Moreover, \textit{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 in a constraint variable is 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 by the reasoning process. + +We define two basic functions for constraints: $isConstraint(t)$ indicates whether type $t$ is a constraint type. $isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}. + +As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to populate the constraint base. For this purpose, we use a specific notation indicating constraint creation combining algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (stated in teletype) used to build up the constraint expression. For example, for creating the IVML constraint \IVML{x = 25;}, we denote in algorithms $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the expression representing the constraint. Here, \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}), which returns a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to generically describe a constraint instantiation. + +For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, i.e., for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ + +In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We state this by $\IVMLMeta{var}(i, t)$, i.e., create the temporary variable $i$ of type $t$. \subsubsection{Compounds} -A compound is an IVML type, which consists of variable declarations, called slots. Let $t$ be a compound type, then $isCompound(t)$ returns $true$. All slots of a compound $t$ can be accessed through $slots(t)$. Akin to a variable declaration, for a slot $s$ $name(s)$, $default(s)$ and $type(s)$ are defined. Moreover, let $v$ be a compound variable, i.e., a variable of a compound type, then $decision(v, s)$ returns the variable related to slot $s$. $refines(t)$ is the set of compound types directly refined by \TBD{refining?} compound $t$, returning an empty set if there are no such compounds or if $t$ is not a compound type. Assignments $assignments(t)$ is defined for a compound type akin to $assignments(p)$ for a project $p$. Further, we define the following derived functions +A compound is an IVML type, which consists of variable declarations, called slots. Let $t$ be a compound type, then $isCompound(t)$ returns $true$, else for all other types $false$. The 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. Moreover, let $v$ be a compound variable, i.e., a variable of a compound type, then $decision(v, s)$ returns the variable related to slot $s$ in the configuration $v$ is a member of. For convenience, we introduce + +$$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 + +Compounds can form an inheritance hierarchy through multiple inheritance. Individual slots from parent compounds can thereby shadowed / redefined by slots of the same or more specific type. $refines(t)$ represents the set of compound types directly refined by \TBD{refining?} compound $t$, returning an empty set if there are no such compounds or if $t$ is not a compound 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} + \end{cases} + $$ + +$$allRefines^+(t) = + \begin{cases} + allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ + \emptySet, & \text{else} + \end{cases}$$ $$inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ -$$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 - -$$allRefines(t) = \begin{cases}\emptySet, & \text{if } refines(t) = \emptySet \\ allRefines(t) \cup \bigcup_{u\in refines(t)} allRefines(u), & \text{else}\\ \end{cases}$$ - -$$allRefines^+(t) = \begin{cases}allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ \emptySet, & \text{else} \\ \end{cases}$$ - -$$parentCompound(d) = \begin{cases} parent(d), & \text{if } parent(d) \neq \undef \wedge{} isCompound(parent(d)) \\ parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ \undef, & \text{else}\end{cases}$$ +$$parentCompound(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}$$ $$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ -Accessors to compound variables aim at accessing a certain slot within that variable, i.e., an accessor must mention the variable and the slot. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} 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 an expression, we use the IVML operation \IVML{acc}\footnote{Actually, a constructor call to create an accessor expression tree node.} Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor within an IVML expression happens through $\createExpression{\IVMLMeta{acc}\IVML{(cmp, slot)}}$, while for the second accessor we use $\createExpression{\IVMLMeta{acc}(\IVMLMeta{acc}(\IVML{cmp}, \IVML{slot}),\IVML{slot2})}$. + +Akin to projects, $assignments(t)$ is defined for a compound type $t$ and returns the annotation assignment blocks. Similar functions apply to access the constraints, the variable declarations and the assignment data. + +Accessors to compound variables define a path to access a certain slot within that variable, i.e., an accessor must mention the variable and the slot to access. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} 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, we use the IVML operation \IVML{acc}\footnote{Actually, a constructor call to create an accessor expression tree node.}. Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor within an IVML 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})}$. \subsubsection{Containers} -A \textbf{container} is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). Let $c$ be a container, then $elements(c)$ denotes is the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$ and $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and +A container is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). Let $c$ be a container, then $elements(c)$ denotes is the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$ and $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and $$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$