Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 36) +++ /reasoner/reasoner.tex (revision 37) @@ -9,5 +9,5 @@ \newcommand\IVML[1]{\texttt{#1}} \newcommand\IVMLself[0]{\texttt{self}} -\newcommand\IVMLMeta[1]{\texttt{\underline{#1}}} +\newcommand\IVMLMeta[1]{\texttt{#1}} %\underline{} \newcommand\addSet[0]{\cup} \newcommand\addSeq[0]{\oplus} @@ -26,5 +26,5 @@ \newcommand\createConstraint[1]{\langle #1 \rangle} \newcommand\createDefaultConstraint[1]{\langle_d\text{ } #1 \rangle} -\newcommand\createInternalConstraint[1]{\langle_i\text{ } #1 \rangle} +%\newcommand\createInternalConstraint[1]{\langle_i\text{ } #1 \rangle} \newcommand\createExpression[1]{\langle\langle #1 \rangle\rangle} \newcommand\closedCases[1]{\left.\begin{cases}#1\end{cases}\right\}} @@ -45,5 +45,5 @@ Besides traditional variability modeling approaches, such as feature modeling \TBD{cite} or decision modeling \TBD{cite}, in recent time several approaches to textual variability modeling have been proposed \TBD{cite-STTT}. Moreover, there seems to be a trend that more recent variability modeling support more powerful modeling conceepts \TBD{cite-STTT}, which then require more powerful analysis and reasoning mechanisms. As stated above, typically these mechanisms then imply limitations of the analysis capabilities, e.g., non-Boolean decisions typically prevent determining the actual number of possible configurations (of course not the number of configuration options that remain to be configured to achieve a complete configuration). -The \textbf{Integrated Variability Modeling Language (IVML)} \TBD{cite IVML} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, collection types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures \TBD{cite IVML-topo}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer \TBD{cite}. Currently, the reasoning mechanism focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propoagation as much as possible. So far, this allows performing typical validation and propagation tasks +The \textbf{Integrated Variability Modeling Language (IVML)} \TBD{cite IVML} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures \TBD{cite IVML-topo}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer \TBD{cite}. Currently, the reasoning mechanism focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propoagation as much as possible. So far, this allows performing typical validation and propagation tasks \TBD{structure}. However, we are aware of the fact that more advanced tasks like configuration completion are not supported by the current approach. This is subject to future work, for which this document shall provide a solid foundation. @@ -52,9 +52,9 @@ \section{Approach}\label{sectApproach} -IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \TBD{cite} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \textbf{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), collection types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in constrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged \TBD{cite} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points. - -Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines \TBD{cite}. Although these mechanisms are powerful in their own respect and typically available as implementation, using them for IVML requires translating an IVML model and its constraints into the model of the respective mechanism and executing that mechanism on the translated model. While traditional reasoners allow for completing the model through feasible ground instances, they typically also perform a kind of constrained state space evaluation. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables), just applying a traditional reasoner to usual IVML models is an inefficient approach. Other related mechanisms such as rule engines can be applied to some degree, however, according to our experience \TBD{cite} lead to a significant and infeasible runtime overhead. Moreover, these both kinds of approaches are limited as they typically do not directly support the breadth of OCL operations, in particular collection iterators, quantifiers and user-defined constraint operations. In contrast, specific reasoning approaches, e.g., for OWL partially support quantification, but are similarly limited. Moreover, relying on OCL reasoning mechanisms could be a feasible approach, but would require significant extension to enable value propagation and IVML-specific operations. - -Due to these experiences, we decided to realize a \textbf{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach.. The basis is \textbf{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. Based on our experience, the reasoning mechanism shall directly operate on an IVML model instead of performing a model transformation first. However, as constraints in IVML can be attached to types (to increase consistency and to avoid repeated constraints), first a constraint transformation is needed, which instantiates constraints towards variables and their respective types. Then, forward-chaining is executed on this constraint base. Extending approaches may continue on a the result of a failed reasoning through forward-execution. +IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \TBD{cite} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \textbf{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), container types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in constrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged \TBD{cite} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points. + +Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines \TBD{cite}. Although these mechanisms are powerful in their own respect and typically available as implementation, using them for IVML requires translating an IVML model and its constraints into the model of the respective mechanism and executing that mechanism on the translated model. While traditional reasoners allow for completing the model through feasible ground instances, they typically also perform a kind of constrained state space evaluation. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables), just applying a traditional reasoner to usual IVML models is an inefficient approach. Other related mechanisms such as rule engines can be applied to some degree, however, according to our experience \TBD{cite} lead to a significant and infeasible runtime overhead. Moreover, these both kinds of approaches are limited as they typically do not directly support the breadth of OCL operations, in particular container iterators, quantifiers and user-defined constraint operations. In contrast, specific reasoning approaches, e.g., for OWL partially support quantification, but are similarly limited. Moreover, relying on OCL reasoning mechanisms could be a feasible approach, but would require significant extension to enable value propagation and IVML-specific operations. + +Due to these experiences, we decided to realize a \textbf{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis is \textbf{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. It is important to notice that IVML \TBD{IVML-spec} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniqualy determined, IVML allows changing the value of a constraint only once within a project scope, otherwise requiring that a reasoning mechanism issues an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in certain cases, some form of squence of the constraints can be indicated through eval-blocks within a project, i.e., (nested) blocks containing constraints. Here the rule is that a project is considered as the outermost eval-scope, then eval blocks are evaluated in their nesting sequence (whereby eval blocks on the same nesting level do not imply any sequence). Based on our experience (and the specific requirements of default-value logic, project scopes, eval scopes), the reasoning mechanism shall directly operate on an IVML model instead of performing a model transformation first. However, as constraints in IVML can be attached to types (to increase consistency and to avoid repeated constraints), first a constraint transformation is needed, which instantiates constraints towards variables and their respective types. Then, forward-chaining is executed on this constraint base. Extending approaches may continue on a the result of a failed reasoning through forward-execution. Typically, reasoning over all variables of a project including all constraints is needed. However, in some use cases considering all constraints is not needed and even not efficient with respect to reasoning time. The first case is \textbf{incremental reasoning}, i.e., starting with a given (valid) configuration and just analyzing the changes made by the user. The idea is to provide nearly immediate results, so that reasoning even on complex and large models can happen on every change made by the user. The second case is \textbf{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \TBD{cite}. More specifically, we distinguish between incremental reasoning @@ -77,14 +77,18 @@ For some parts of the reasoning algorithm, we need sequences, i.e., a structure that contains elements in a given sequence, but potentially containing duplicates. Similar to sets, we denote a sequence by $q=\seq{2, 1, ...}$ and the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_d$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as the sequence concatenation as described before but without duplicates. -Further, we denote the undefined value by $\undef$. +Further, we denote the undefined value by $\undef$. If not indicated otherwise, all operations introduced below that are bound to a certain type return $\undef$ if the operation is used with another type. \subsection{IVML elements} In this section, we briefly discuss the various IVML elements and introduce functions to access their respective properties. We focus on functions that are used for specifying the reasoning algorithm rather than all functions defined by the IVML object model. As convention, we use als parameter names $d$ for a variable declaration, $v$ for a configuration variable, $t$ for a type, $val$ for a value and $cfg$ for a configuration consting of decision variables. For temporary/local variables, we use names close by, e.g., $s$ for an iterator variable used for a set of types. -For all \textbf{IVML elements}, we denote $constraints(e)$ as the set of constraints defined for element $e$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. - -An IVML\textbf{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 \textbf{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 collections). Further, we define two derived functions +For all IVML elements, we denote $constraints(e)$ as the set of constraints defined for element $e$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. No specific functions are required here for \textit{basic types} (Boolean, Integer, Real String). In IVML, a \textit{configuration reference} points to a variable in the same project or elsewhere. A configuration reference is indicated through the generic reference type, e.g., \IVML{refTo(SomeCompound)}. As the actual IVML specification \TBD{IVML-spec} does not define specific properties or operations for reference types, we assume here that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are evaluated on the referenced variable. + +\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. + +\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}$$ @@ -92,7 +96,23 @@ $$allParents(v) = \begin{cases}\set{}, & \text{if } \neg isVariable(parent(v)) \\ \set{parent(v)} \cup allParents(parent(v)), & \text{else}\\ \end{cases}$$ -A \textbf{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)$. - -A \textbf{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 +\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)$. + +\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$. + +\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 $$inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ @@ -108,20 +128,19 @@ $$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ - -\textbf{collections}... - - -An access expression specifies slots (within a compound variable or through references) or elements (within a collection) to be accessed. In IVML, an accessor looks like: \IVML{cmp.slot}, \IVML{cmp.slot1.slot2}, \IVML{coll[1]}, \IVML{coll[1].slot}. +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})}$. + +\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 + +$$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ + +returns the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. In some situations, we must identify whether a container contains constraints, i.e., $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$. More generally, we also define a function that returns the set of all (contained) types used in a container, i.e., $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$. + +For containers, access expressions usually occur only if the collection has a compound as nested type and if the collection is a sequence. Then accessing an element by an index happens through the IVML index access function for sequences \IVML{seq[1]} and the accessor to \IVML{slot} would then be the combined expression \IVML{seq[1].slot}, for creating an expression $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. + +\subsubsection{Derived types} \begin{itemize} - \item collections - \begin{itemize} - \item $isContainer(t)$, $isConstraint(t)$, $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nestedType(t))$ - \item $elements(c)$ is the set of all element values in a collection - \item $isNested(c)$ whether a collection is a nested collection and $nestedType(c)$ is the (innermost) nested type - \item $contained(t)$ the type contained in $t$ if $isCollection(t)$ or $t$ - \item $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$ the set of (contained) types used in collection $c$ - \end{itemize} - \item reference \item derived \begin{itemize} @@ -129,9 +148,4 @@ \item $isDerived(t)$ whether $t$ is a derived type. In this case, $basis(t)$ is the basis type $t$ is derived from, else $basis(t) =\undef$. $decl(d)$ is the specific variable of a derived type used to define restricting constraints. \item $allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge base(t) = \undef \\ \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$ - \end{itemize} - \item constraints - \begin{itemize} - \item A constraint is a boolean expression that requires to be evaluated to \IVML{true}. Creating a constraint through OCL function call notation in angle brackets, e.g., $\createConstraint{\IVML{assign}(x, 25)}$ represents the IVML constraint \IVML{x = 25;} (knowing that the assignment IVML assignment operation returns a boolean value indicating its success). If the constraint is marked as a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$, if it is an internal \TBD{clarify semantics }constraint for reasoning we use $\createInternalConstraint{\IVML{assign}(x, 25)}$. We indicate IVML operations in teletype font. We denote a partial expression for incrementally building a constraint by $createExpression{expr}$ and indicate IVML meta operations for creating expression parts as follows: $\createExpression{\IVMLMeta{var}(i, t)}$ creates a temporary variable $i$ of type $t$. $\createExpression{\IVMLMeta{acc}(c, s)}$ creates an accessor $c.s$, e.g., to access slot $s$ on compound $c$ (implicitly requiring $isCompound(c) \wedge s\in slots(c)$). - \item $isAssignmentConstraint(c)$ whether constraint $c$ is of form \IVML{assign(v, e)} with $v$ variable and $e$ expression \end{itemize} \end{itemize} @@ -171,5 +185,5 @@ \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$ but before the other usual constraints in $\topLevelConstraints$ and $\otherConstraints$. \item Top level constraints and derived type constraints $\topLevelConstraints$ - \item Remaining usual constraints including compound types used in collections, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints, default annotation constraints and assigned annotation constraints $\otherConstraints$. + \item Remaining usual constraints including compound types used in containers, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints, default annotation constraints and assigned annotation constraints $\otherConstraints$. \end{enumerate} Further, the algorithm maintains a global variable mapping $\variableMapping$, a map of already processed variables to accessors so that later processed complex expressions can be substituted with the correct accessors. @@ -227,5 +241,5 @@ \end{algorithm} -When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a collection operation nor a local variable defined in a let-expression, the change is registered within the actual scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value changes}) for both, parent and client variables of $v$ are identified. Both, parents and children must be considered, as value in compounds may have impact on both kinds of siblings. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint base. +When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the change is registered within the actual scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value changes}) for both, parent and client variables of $v$ are identified. Both, parents and children must be considered, as value in compounds may have impact on both kinds of siblings. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint base. \begin{algorithm}[H] @@ -287,8 +301,8 @@ \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\otherConstraints$ \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm substitutes all occurrences of \IVMLself{} by the actual declaration as well as all mapped variables from $m$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified. - \item Collects all transformed collection compounds based on the actual used types if $d$ is a collection. If $d$ is a collection over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_collections}). + \item Collects all transformed container compounds based on the actual used types if $d$ is a container. If $d$ is a container over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_containers}). \item Translates remaining (slot) default value expression by replacing potential \IVMLself{} usages with the compound access. In case that \IVMLself{} is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($\deferredDefaultConstraints$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. - \item Translates usual collection compound constraints independent of any default value expression and stores them into $\otherConstraints$. \TBD{check} - \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\otherConstraints$. \TBD{check, also section ref} + \item Translates usual container compound constraints independent of any default value expression and stores them into $\otherConstraints$. \TBD{check} + \item Translates container constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\otherConstraints$. \TBD{check, also section ref} \end{itemize} Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $\otherConstraints$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $\defaultConstraints$ or $\deferredDefaultConstraints$ as determined before. @@ -312,5 +326,5 @@ \ForAll{$u \iterAssng usedTypes(dflt)$}{ \MISSING{derived types: coCompoundConstraints, translateCollIntConstraints here?} - $translateDefaultsCompoundsCollection(d, u)$\; + $translateDefaultsCompoundsContainer(d, u)$\; } }\ElseIf{$ca \neq \undef$}{ @@ -319,7 +333,7 @@ } } \uElse{$ dflt \assng \undef $\;} - $add(\otherConstraints, translateCollectionCompoundConstraints(d, v, \undef), true)$\; + $add(\otherConstraints, translateContainerCompoundConstraints(d, v, \undef), true)$\; \If{$isContainer(t) \wedge isDerived(contained(t))$}{ - $translateCollectionDerivedDatatypeConstraints(d, \undef)$\; + $translateContainerDerivedDatatypeConstraints(d, \undef)$\; } \If{$ deflt \neq \undef $}{ @@ -346,9 +360,9 @@ $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\; - $add(\topLevelConstraints, \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\; + $add(\topLevelConstraints, \setWith{\createConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\; \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} \end{algorithm} -The translation of derived datatypes for collections can be done similarly, but must consider the nested values/variables of a collection. As accessor to the collection, Algorithm \ref{algTranslateCollectionDerivedDatatypeConstraints} uses either the declaration $d$ or, if given, the accesor $ca$. In contrast to Algorithm \ref{algTranslateDerivedDatatypeConstraints}, Algorithm \ref{algTranslateCollectionDerivedDatatypeConstraints} introduces an all-quantor and substitutes the specific variable of a derived datatype definition by the actual declaration $d$ to be processed. +The translation of derived datatypes for containers can be done similarly, but must consider the nested values/variables of a container. As accessor to the container, Algorithm \ref{algTranslateContainerDerivedDatatypeConstraints} uses either the declaration $d$ or, if given, the accesor $ca$. In contrast to Algorithm \ref{algTranslateDerivedDatatypeConstraints}, Algorithm \ref{algTranslateContainerDerivedDatatypeConstraints} introduces an all-quantor and substitutes the specific variable of a derived datatype definition by the actual declaration $d$ to be processed. \begin{algorithm}[H] @@ -359,5 +373,5 @@ $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\; $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\; - \caption{Translating constraints for derived collection types (\IVML{translateCollectionDerivedDatatypeConstraints}).}\label{algTranslateCollectionDerivedDatatypeConstraints} + \caption{Translating constraints for derived container types (\IVML{translateContainerDerivedDatatypeConstraints}).}\label{algTranslateContainerDerivedDatatypeConstraints} \end{algorithm} @@ -418,5 +432,5 @@ First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclarationDefaults}. -Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\otherConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound collection, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateCollectionCompoundConstraints}. +Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\otherConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound container, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateContainerCompoundConstraints}. Finally, the algorithm translates all attribute assignments using Algorithm \ref{algTranslateAnnotationAssignments}, all direct compound constraints (substituting \IVMLself{} and registered variables), and translates and collects all eval constraints (\TBD{no self??}). @@ -441,5 +455,5 @@ $add(\otherConstraints, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\; } - $add(\otherConstraints, translateCollectionCompoundConstraints(s, v, \variableMapping[s]), true)$\; + $add(\otherConstraints, translateContainerCompoundConstraints(s, v, \variableMapping[s]), true)$\; } \If{$\neg inc$} { @@ -499,7 +513,7 @@ -\subsection{Collection default constraints}\label{deflt_collections} - -Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundCollection} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested collection). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the collection using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$. +\subsection{Container default constraints}\label{deflt_containers} + +Constraints defined on types that are implicitly instantiated within a container must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundContainer} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested container). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the container using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$. \begin{algorithm}[H] @@ -511,9 +525,9 @@ } - \caption{Translating defaults in compound collections (\IVML{translateDefaultsCompoundCollection}).}\label{algTranslateDefaultsCompoundCollection} -\end{algorithm} - -If $d$ is a container, we must translate and apply all constraints of compounds within that collection \TBD{nested collections follow?} to $d$. As Algorithm \ref{algTranslateCollectionCompoundConstraints} is used within different algorithms, we return the collected constraints here. -The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateCollectionCompoundConstraints2}). + \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer} +\end{algorithm} + +If $d$ is a container, we must translate and apply all constraints of compounds within that container \TBD{nested containers follow?} to $d$. As Algorithm \ref{algTranslateContainerCompoundConstraints} is used within different algorithms, we return the collected constraints here. +The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateContainerCompoundConstraints2}). \begin{algorithm}[H] @@ -522,14 +536,14 @@ \KwOut{resulting constraints $c$} - \If{$isCollection(type(d)$ \TBD{check: move up}} { + \If{$isContainer(type(d)$ \TBD{check: move up}} { $c \assng \set$\; $tc \assng contained(type(d))$\; \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in elements(v)}$}{ \If{$isCompound(t)$}{ - $c \assng c \cup translateCollectionCompoundConstraints(t, tc, d, ca)$\; + $c \assng c \cup translateContainerCompoundConstraints(t, tc, d, ca)$\; } } } - \caption{Translating compound constraints from a collection (\IVML{translateCollectionCompoundConstraints}).}\label{algTranslateCollectionCompoundConstraints} + \caption{Translating compound constraints from a container (\IVML{translateContainerCompoundConstraints}).}\label{algTranslateContainerCompoundConstraints} \end{algorithm} @@ -551,5 +565,5 @@ } - \caption{Translating compound constraints from a collection (\IVML{translateCollectionCompoundConstraints}).}\label{algTranslateCollectionCompoundConstraints2} + \caption{Translating compound constraints from a container (\IVML{translateContainerCompoundConstraints}).}\label{algTranslateContainerCompoundConstraints2} \end{algorithm} @@ -575,5 +589,5 @@ %\begin{align*} -%retrieve&CollectionConstraints(c, m) =\\ +%retrieve&ContainerConstraints(c, m) =\\ % &\closedCases{checkContainerInitializer(c, \undef), & \text{if } isContainerInitializer(c) \\ checkCompoundInitializer(c, m) &\text{if } isCompoundInitializer(c)\\ \set{}, & \text{else}} %\end{align*} @@ -586,5 +600,5 @@ \end{align*} -\TBD{Just here, as algorithm descriptions often utilize collection notation.} +\TBD{Just here, as algorithm descriptions often utilize container notation.} \begin{algorithm}[H] \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$} @@ -610,5 +624,5 @@ Enum variable & & & \\ Compound variable & & & \\ -Container variable & & & \ref{deflt_collections} \\ +Container variable & & & \ref{deflt_containers} \\ Reference variable & & & \\ Constraint variable & & & \\