Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 185) +++ /reasoner/mainAlgorithms.tex (revision 186) @@ -160,5 +160,5 @@ $add(\topLevelConstraints, constraints(p), true, \undef)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints} \ForAll{$a \iterAssng assignments(p)$}{ - $add(\topLevelConstraints, allAssignmentConstraints(a), true, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} + $add(\topLevelConstraints, allConstraints(a), true, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} $translateAnnotationAssignments(a, \undef, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments} } \label{algTranslateConstraintsTranslationEnd} Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 185) +++ /reasoner/notation.tex (revision 186) @@ -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. $decls(p)$ denotes the set of all variable declarations introduced in project $p$. $isProject(p)$ returns $true$ for a 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 project $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. @@ -107,35 +107,35 @@ In IVML, an \emph{annotation assignment} is a kind of block, which allows assigning annotation values to the variables declared within the block, i.e., the specified annotation values shall be applied to all contained variable declarations. The declared variables shall behave as if they are defined in the innermost containing element that is not an annotation assignment. For convenience, also constraints relating to the contained variable declarations can be stated within an annotation assignment. To indicate orthogonal combinations of annotation assignments in IVML models, annotation assignment blocks can be nested. For convenience, only the innermost annotation value assignment shall be applied in nested assignment blocks in order to avoid accidental multiple assignments to the same annotation within the same project scope~\cite{IVML-LS}. -$assignments(p)$ is the set of (potentially nested) annotation assignments of project $p$. If $a\in assignments(p)$ then $decls(a)$ returns the variables declared in $a$ and $constraints(a)$ the constraints declared within $a$. Further, $assignments(a)$ returns the annotation assignments nested within $a$. All three results may be empty. Further, $assignmentData(a)$ provides access to the intended value assignment, i.e., if $f \in assignmentData(a)$ then $name(f)$ is the name of the affected attribute and $default(f)$ the intended default value expression that shall be assigned to all attributes with name $name(f)$ for all declarations within the containing attribute assignment. $isAnnotationAssng(a)$ returns whether $e$ is an annotation assignment. - -Using these functions, $allAssignmentConstraints(a)$ determines all assignment constraints within an assignment $a$ considering potentially further nested annotation assignments: +$assignments(p)$ is the set of annotation assignments of project $p$. The function $isAnnotationAssng(a)$ returns whether $a$ is an annotation assignment. For an annotation assignment $a$, $decls(a)$ returns the variables declared in $a$ and $constraints(a)$ the constraints defined in $a$. $assignments(a)$ returns the annotation assignments nested within $a$. $assignmentData(a)$ provides access to the value assignment, i.e., if $f \in assignmentData(a)$ then $name(f)$ is the name of the affected attribute and $default(f)$ the default value expression to be assigned to all attributes with name $name(f)$ for all declarations declared in the attribute assignment. + +Using these functions, $allConstraints(a)$ determines all constraints defined within an annotation assignment $a$ potentially including constraints in nested annotation assignments: % \begin{align*} -all&AssignmentConstraints(a) = \\ - &constraints(a) \cup \setWith{allAssignmentConstraints(b)}{b \in assignments(a)} +all&Constraints(a) = \\ + &constraints(a) \cup \setWith{allConstraints(b)}{b \in assignments(a)} \end{align*} % -In some algorithms we need to determine an attribute attribute declaration with name $n$ that is directly attributed to variable $v$ or one of the containing scopes of $v$. While for nested variables, we can just take the parent variables into account, this ends with the containing project. For ease of access, we (internally) represent a project as a (pseudo-)variable $variable(p)$ containing all variables declared by the project as nested variable. Then +In some algorithms we need to determine an annotation declaration by name, i.e., the declaration of an annotation with name $n$ that is directly attributed to variable $v$ or to one of the scopes containing $v$. For nested variables, we can just take the parent variables into account, but this ends with the containing project. Then % \begin{multline*} -findAnnotation(v, n) = \\ \ \ \begin{cases} - annotation(v, n) &\text{if } annotation(v, n) \neq \undef\\ - findAnnotation(parent(v), n) &\text{if } isVariable(parent(v))\\ - findAnnotation(variable(parent(v)), n) &\text{if } isProject(parent(v))\\ +findAnnotation(e, n) = \\ \ \ \begin{cases} + annotation(e, n) &\text{if } annotation(e, n) \neq \undef\\ + findAnnotation(parent(e), n) &\text{if } parent(e) \neq \undef\\ + %findAnnotation(parent(e), n) &\text{if } isProject(parent(e))\\ %implied in notation above through annotations(p) \undef & \text{else} \\ \end{cases} \end{multline*} % -returns the innermost annotation for variable $v$ with name $n$. - -A configuration $cfg$ as introduced in Section \ref{sectNotationConfigVars} always contains the decision variables for an underlying defining $project(cfg)$. +returns for model element $e$ and containing scopes the innermost annotation declaration with name $n$. + +Following Section \ref{sectNotationConfigVars}, a configuration $cfg$ and its defining project $p$ are related by $p = project(cfg)$. Please note that multiple (different) configurations for the same project can exist, while in terms of IVML a configuration is typically defined through at least one own project scope. % \subsubsection{Constraints}\label{sectNotationConstraints} -In IVML, a \emph{constraint} is a Boolean expression that must always evaluate to $true$. Otherwise, reasoning shall either fail. After a change of at least one of the values of the variables involved in the constraint, the constraint may be re-evaluated successfully, causing a cleanup of previous reasoning errors for that constraint. - -Technically, a constraint is an expression, which may consist of several (sub-)expressions, such as constants, variable uses, or function calls. An expression $e$ evaluates to a value of some IVML type, i.e., $type(e)$ returns the static value type of an expression. In particular, let $c$ be a constraint then $type(c) = \IVML{Boolean}$. Expressions are used to determine the default value of variables. Let $v$ be a variable then we denote by $e(v)$ that expression $e$ is using variable $v$ and by $var(e)$ the set of variables used in $e$. Moreover, if $c$ is an assignment constraint representing $x = y$, the $rightSide(c) = y$ returns the right side expression $y$, else $\undef$. If $e$ represents a constant, $const(e)$ returns the constant value, else $\undef$. - -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. +In IVML, a \emph{constraint} is a Boolean expression that must always evaluate to $true$. Otherwise, reasoning shall fail and details about the failing constraints shall be recorded. After a change of at least one of the values of the variables involved in the constraint, the constraint may be re-evaluated successfully, causing a cleanup of previous reasoning errors for that constraint. + +Technically, a constraint is an expression, which may consist of several (sub-)expressions, such as constants, variable uses, or function calls. An expression $e$ evaluates to a value of some IVML type, i.e., $type(e)$ returns the static value type of an expression. In particular, let $c$ be a constraint then $type(c) = \IVML{Boolean}$. Expressions are used to determine the default value of variables. Let $v$ be a variable then we denote by $e(v)$ that expression $e$ is using variable $v$ and by $var(e)$ the set of variables used in $e$. Moreover, if $c$ is an assignment constraint representing $x = y$, then $rightSide(c) = y$ returns the right side expression $y$, else $\undef$. If an expression $e$ represents a constant, $const(e)$ returns the constant value, else $\undef$. + +\IVML{Constraint} is an IVML type, indicating that a variable actually holds a constraint. $isConstraint(t)$ indicates whether type $t$ is a constraint type, From the reasoning point of view, a constraint stored in a constraint variable is extracted and evaluated as any other constraint. The value in such a variable may, as for all other variables, be undefined, re-defined (once per project scope), set to \IVMLnull{} or frozen, implying that the old constraint must be discarded, potentially replaced by the new constraint (value) and considered in the subsequent reasoning process. %$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 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}$. @@ -191,5 +191,5 @@ \begin{align*} all&CmpConstraints(t) = \\ - &\setWith{constraints(s) \cup allAssignmentConstraints(s)}{s \in allRefines^+(t)} + &\setWith{constraints(s) \cup allConstraints(s)}{s \in allRefines^+(t)} \end{align*} % Index: /reasoner/reasoner.bib =================================================================== --- /reasoner/reasoner.bib (revision 185) +++ /reasoner/reasoner.bib (revision 186) @@ -372,6 +372,6 @@ @techreport{IVML-LS, author = {H. Eichelberger and S. El-Sharkawy and C. Kr{\"o}her and K. Schmid}, - title = "INDENICA Variability Modeling Language: Language Specification, version 1.22", - year = 2014, + title = "INDENICA Variability Modeling Language: Language Specification, version 1.29", + year = 2018, note = {Available online at: http://projects.sse.uni-hildesheim.de/easy/docs/ivml\_spec.pdf}, }