Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 43) +++ /reasoner/reasoner.tex (revision 44) @@ -20,7 +20,9 @@ \newcommand\emptySet[0]{\{\}} \newcommand\set[1]{\{#1\}} +\newcommand\setEmpty[0]{\set{}} % or \emptyset \newcommand\setWith[2]{\{#1:#2\}} \newcommand\setSepText[0]{colon } \newcommand\seq[1]{[#1]} +\newcommand\seqEmpty[0]{\set{\text{}}} \newcommand\seqWith[2]{[#1:#2]} \newcommand\createConstraint[1]{\langle #1 \rangle} @@ -39,4 +41,5 @@ \date{} \maketitle +\LinesNumbered Analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language. In this document, we provide an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML), a variability and configuration modeling language that contains several complex concepts. We discuss the approach to reasoning for IVML, in particular, the implementing constraint translation and reasoning algorithms. @@ -62,8 +65,8 @@ Due to these experiences, we decided to realize a \emph{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 \emph{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 \cite{IVML-LS} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniquely 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-block 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 \emph{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 \emph{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. More specifically, we distinguish between incremental reasoning +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 \emph{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 \emph{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. For these cases, we introduce two main \emph{reasoning modes}, namely full reasoning and incremental reasoning, while the latter can be achieved through the following two techniques. \begin{itemize} - \item with \emph{creation of a partial constraint base}. In this incremental mode, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mode can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration. - \item \emph{re-using a previously build constraint base}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning fronted). + \item \emph{Creation of a partial constraint base:} Using this technique, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mechanism can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration. + \item \emph{Re-using a previously build constraint base:}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning fronted) and it can be combined with the mechanisms for creating a partial constraint base, i.e., skipping default constraints or constraints if all dependent variables are frozen. \end{itemize} @@ -78,11 +81,11 @@ \subsection{General notation} -As usual, we denote a set of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \set{} as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter). - -For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need sequences, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seq{\text{ }} as the empty sequence. Akin to sets, 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_1$, 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 a sequence concatenation that omits duplicates. +As usual, we denote a set of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \setEmpty as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter). + +For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need sequences, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty as the empty sequence. Akin to sets, 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_1$, 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 a sequence concatenation that omits duplicates. Further, we denote the undefined value by $\undef$. If not indicated otherwise, all operations introduced below that are bound to a certain type, e.g., an IVML compound, return $\undef$ if the operation is used with another type, e.g., an IVML basic type. -For individual algorithms, we indicate and use the actual name as used in the implementation to ease mapping from code to algorithms and back. For ease of reading, we ignore here that elements or results of functions in the actual implementation may be a null pointer implying respective checks. Thus, we simply assume here that unless stated otherwise functions either return $\undef$ or, in case of set or sets or sequences $\set{}$ or $\seq{\text{ }}$, respectively. +For individual algorithms, we indicate and use the actual name as used in the implementation to ease mapping from code to algorithms and back. Further, we use parameters and return values in the fashion the implementation does and indicate access to class or instance attributes in the`data' section of the algorithm descriptions. For ease of reading, we ignore here that elements or results of functions in the actual implementation may be a null pointer implying respective checks. Thus, we simply assume here that unless stated otherwise functions either return $\undef$ or, in case of set or sets or sequences $\setEmpty$ or $\seqEmpty$, respectively. \subsection{IVML elements} @@ -91,21 +94,21 @@ As a convention to ease reading the algorithms presented later, we use $d$ for variable declarations, $v$ for configuration variables, $t$ for types, $val$ for a values, $c$ for constraints and $cfg$ for configurations consting of decision variables and their associated values. For temporary/local variables, we typically use a name close by, e.g., $w$ for an iterator variable (instead of $v$) etc. -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}$. +For all \emph{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}$. \subsubsection{Variable Declarations} -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$. +An IVML \emph{variable declaration} $d$ specifies a 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$. +An IVML \emph{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 +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)=\setEmpty$ 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 \\ + \setEmpty, & \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} @@ -113,9 +116,11 @@ \begin{multline} allParents(v) = \begin{cases} - \set{}, & \text{if } \neg isVariable(parent(v)) \\ + \setEmpty, & \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). + +Variables can be \emph{local}, e.g., as specified in the IVML model used as parameters of a user-defined constraint function, within let-expression or as collection iterator. Such variables have the same properties as usual configuration variables and can be identified using $isLocal(v)$, which then returns $true$. 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: @@ -132,9 +137,9 @@ 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. +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$, \setEmpty 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)$ 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)$. +A \emph{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. @@ -142,7 +147,7 @@ \subsubsection{Constraints}\label{sectNotationConstraints} -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. +A \emph{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, \emph{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;}. @@ -152,9 +157,9 @@ 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$. +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$. For a variable $v$ created by \IVMLMeta{var} holds $isLocal(v) = true$. \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$, 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 +A \emph{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 @@ -196,9 +201,11 @@ 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})}$. +\emph{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})}$. + +The value of a compound variable defined, e.g., as a default value expression or as an assignment constraint, using complex value expressions, so called \emph{compound initializers}, essentially a name-value mapping. As slots can be of a complex type, e.g., a compound, a compound initializer can also contain complex values, e.g., further compound initializers. \subsubsection{Containers} -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). +A \emph{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 the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$. Further, $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \linebreak \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and @@ -216,7 +223,9 @@ 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. For example, \IVML{seq[1]} accesses an indexed element of the sequence \IVML{seq} and the accessor to \IVML{slot} on \IVML{seq[1]} is then the combined expression \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. +Akin to compounds, containers can be initialized by complex values, so called \emph{container initializers}, here as a listing of possible complex values. If the container is a sequence, the given order of values in the container initializer used as (initial) order of the sequence elements. + \subsubsection{Derived types} -In IVML, a derived type creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given. +In IVML, a \emph{derived type} creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given. For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. @@ -226,9 +235,9 @@ $$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}$$ -\subsection{Miscellaneous} - -No specific functions are required for translating constraints for / reasoning on \textit{basic types} (Boolean, Integer, Real String). The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning. - -In IVML, a \textit{configuration reference} points to a variable defined in the same or another project (if made available through imports). As the actual IVML specification \cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume 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 translated for / evaluated on the referenced variable. +\subsection{Other IVML Elements} + +No specific functions are required for translating constraints for / reasoning on \emph{basic types} (Boolean, Integer, Real String). The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning. + +In IVML, a \emph{configuration reference} points to a variable defined in the same or another project (if made available through imports). As the actual IVML specification \cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume 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 translated for / evaluated on the referenced variable. %----------------------------------------------------------------------------------------------------------------- @@ -243,5 +252,5 @@ \newcommand\relevantConstraints[0]{r_t} -The reasoner performs forward reasoning, i.e., it identifies all constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. +The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. For IVML, the reasoner must take the structure of IVML models into account, i.e., in particular IVML projects. An IVML projects constitutes a reasoning scopes, i.e., no duplicated variable assignment must occur within a project. Moreover, a project acts as search space for dynamic dispatch of user-defined operations. The main reasoning loop over the involved IVML projects for a given configuration $cfg$ is shown in Algorithm \ref{algMainLoop}. @@ -346,5 +355,5 @@ \KwData{constraint $base$ , variable mapping $\variableMapping$} - $\variableMapping \assng \set{}$\; % clear + $\variableMapping \assng \setEmpty$\; % clear %>ConstraintTranslationVisitor \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults @@ -357,8 +366,8 @@ %