Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 131) +++ /reasoner/reasoner.tex (revision 132) @@ -35,6 +35,6 @@ \newcommand\seqEmpty[0]{\seq{\text{ }}} \newcommand\seqWith[2]{[#1:#2]} -\newcommand\subTypeOf[2]{t \succ s} -\newcommand\subTypeEqOf[2]{t \succeq s} +\newcommand\subTypeOf[2]{#1 \succ #2} +\newcommand\subTypeEqOf[2]{#1 \succeq #2} \newcommand\createConstraint[1]{\langle #1 \rangle} \newcommand\createDefaultConstraint[1]{\langle #1 \rangle_d} @@ -165,5 +165,5 @@ Let $v$ be a (top-level) configuration variable of variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$ and $parent(v)=cfg$. 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$ and $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$, in particular if $type(v)$ is a refined type through inheritance (cf.~\cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy). +$value(v)$ denotes the actual value of $v$ and $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$, in particular if $type(v)$ is a refined type through inheritance (cf.~\cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy). We will detail some relevant properties of values below in Section \ref{sectNotationValues}. As some IVML types allow 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))$. For a variable $v$, $\forall_{w\in nested(v)}\text{ } parent(w)=v$ must hold. Moreover, let $nested(v, n)$ be the nested variable in $v$ with name $n$, while $nested(v, n)=\undef$ if no such variable is defined. For convenience, we also define @@ -335,11 +335,11 @@ We define $isNested(t) = isContainer(contained(t))$ and % -$$nested(t)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ -% -returning the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. If $isNested(c)$ is $true$ for a container $c$, $elements(c)$ contains values of the nested type. In some situations, the flattened container is needed, i.e., for nested collections preferrably with the same innermost nested type only the innermost contained values are relevant. For this purpose, $allElements(c)$ returns the transitively flattened elements of the respective container, i.e., set or sequence, i.e., all leaf elements of a depth-first traversal of the containment tree. +$$nested^*(t)=\begin{cases}nested^*(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ +% +returning the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested^*(t)$ returns \IVML{Integer}. If $isNested(c)$ is $true$ for a container $c$, $elements(c)$ contains values of the nested type. In some situations, the flattened container is needed, i.e., for nested collections preferrably with the same innermost nested type only the innermost contained values are relevant. For this purpose, $allElements(c)$ returns the transitively flattened elements of the respective container, i.e., set or sequence, i.e., all leaf elements of a depth-first traversal of the containment tree. During the constraint translation, we must identify whether a container consists of constraints, i.e., % -$$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$$ +$$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested^*(t))$$ % In other situations, we need to know all actual innermost nested types that are used in a container, i.e., the set @@ -347,5 +347,5 @@ $$usedTypes(c) = \setWith{contained(type(e))}{e\in allElements(c)}$$ % -This is in particular important if $isCompound(nested(type(c)))$ holds for a container $c$, as then also values of refined types of $nested(type(c))$ may occur in $usedTypes(c)$. +This is in particular important if $isCompound(nested^*(type(c)))$ holds for a container $c$, as then also values of refined types of $nested^*(type(c))$ may occur in $usedTypes(c)$. For containers, \emph{access expressions} usually occur either in quantorized expressions utilizing the iterator variable or if the collection is a sequence (typically of compounds). Then accessing an element by an index happens through the IVML index access function for sequences. For example, let \IVML{seq} be a sequence of compounds, all having a common slot \IVML{slot}. Then \IVML{seq[1]} accesses the second element in the container\footnote{In contrast to OCL, IVML indexes are 0-based.} and accessing \IVML{slot} on the first element happens through \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. @@ -355,43 +355,47 @@ \subsubsection{Derived types}\label{sectNotationDerivedTypes} -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)$ returns the type $t$ is derived from. - -For specifying constraints, a derived type $t$ implicitly declares a variable $decl(t)$ of type $base(t)$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type $base^*(t)$ is relevant. +In IVML, a \emph{derived type} denotes a new type based on an existing type. A derived type can restrict the base type by specifiying constraints. Further, without constraints, a derived type can act as an alias of a type, e.g., a complex container type. + +For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ returns the type $t$ is derived from. For specifying constraints, a derived type $t$ implicitly declares a variable $decl(t)$ of type $base(t)$. Constraint expressions may use $decl(t)$, which must be substituted by a concrete variable during constraint instantiation, as well as any other variable accessible in the actual scope. + +In particular, derived types can be defined based on already existing derived types. In this case, a chain of dependent base types is created, whereby for reasoning typically the most basic type $base^*(t)$ is relevant. % $$base^*(t) = \begin{cases}base(t), & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ base^*(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t)) \\ \undef, & \text{else}\\ \end{cases}$$ % -For constraint translation in reasoning it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define +For the constraint translation it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define % $$allBase(t) = \begin{cases}\set{base(t)}, & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ \set{base(t)} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ \emptySet, & \text{else}\\ \end{cases}$$ % -\subsection{Other IVML Types}\label{sectNotationOthers} - -No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real String), the constraint type as well as for enums as IVML does not support modifying these types or does not allow attaching constraints directly to these types. Constraints can be attached indirectly through variable declarations / compound slots or derived types. 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). A reference is a type $t$ defined for a base type $base(t)$ the reference points to. If $t$ is a reference, $isReference(t)$ returns true. In some cases, we must dereference a set $s$ of reference types through -% -$$deref(t)=\begin{cases} deref(base(t)), & \text{if } isDerived(t) \wedge \neg isDerived(base(base(t)))\\ deref(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ t, & \text{else}\\\end{cases}$$ -% -and +\subsubsection{Other IVML Types}\label{sectNotationOthers} + +No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real, String), the constraint type introduced in Section \ref{sectNotationConstraints} as well as for enums, because IVML does not support directly attaching constraints to these types. Constraints for these types can only be defined indirectly as global constraints for variable declarations, as nested compound constraints for compound slots or via derived types as introduced in Section \ref{sectNotationDerivedTypes}. Thus, no specific functions for these types must be discussed here. The available IVML functions and operations for these types, such as adding two integer values, are subject of the creation of expressions / the IVML model, e.g., through the IVML parser as well as of the IVML expression evaluation mechanism, rather than the reasoning algorithms discussed in this document. + +However, IVML \emph{configuration references} require a specific treatment in some situations. In IVML, a configuration reference points to a variable defined in the same or another imported project. A configuration reference is a generic type $t$ defined for the base type $base(t)$ of the variable the reference points to. If $t$ is a reference, $isReference(t)$ returns true. + +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. For this purpose, we must be able to (sliently) dereference a type $t$ +% +$$deref(t)=\begin{cases} base(t), & \text{if } isDerived(t) \wedge \neg isDerived(base(t))\\ deref(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ t, & \text{else}\\\end{cases}$$ +% +and in some cases even a set $s$ of types through % $$deref(s)=\setWith{s\in t}{deref(t)}$$ % -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. - -\subsubsection{Values}\label{sectNotationValues} - -IVML types have corresponding values in the IVML object model, in particular as complex structured types such as compounds and containers may be nested. As the expression evaluator is dealing with values, applying operations to them and storing them in the configuration, we can largely ignore the specific properties of vales. However, some specific properties must be taken into account for reasoning. Basically, a value $val$ always carries its type $type(val)$. One specific value is \IVML{null}, which is certainly different from the undefined value $\undef$. As introduced in Section \ref{sectNotationConstraints}, a constrant expression holds a value, which can be obtained from an expression using $const(e)$ (returns $\undef$ for any expression that is not a constant expression). Further, complex values can consist of nested values, which are accessible through $elements(val)$, without nesting as flattened set or sequence through $allElements(val)$, respectively. For non-complex values, these two functions just return $\set{val}$. To ease some notation, we assume that $elements(\undef)=\emptySet$, similarly for $allElements(\undef)$. - -In some situations we must either rely on the actual value of a variable or its default value. The latter is particularly important for initializing a configuration. Thus, having available a variable $v$ and its declaration $d=decl(v)$, we define + +\subsubsection{IVML Values}\label{sectNotationValues} + +In the IVML object model, IVML types have corresponding typed values, in particular to correctly represent potentially nested complex structured types such as compounds and containers. As the IVML expression evaluator is operating on values, in particular by retrieving them from a configuration, applying IVML operations and storing them back to a configuration, we can mostly neglect the specific properties of IVML values. However, some specific properties must be taken into account for reasoning, which we introduce in this section. + +A value $val$ is typed and, thus, always provides access to its type $type(val)$. In case of a compound variable $v$, the value determines the actual type of $v$, as $\subTypeEqOf{type(value(v))}{type(v)}$. One specific value is \IVML{null}, which is compliant with all types, i.e., can be assigned to any variable to indicate that a variable is (explicitly) not configured. \IVML{null} is certainly different from the undefined value $\undef$: $\undef$ indicates in this context that so far no value has been assigned to a variable and the variable shall have either assignment state \IVML{UNDEFINED} or \IVML{FROZEN}. \IVML{null} wipes out a previously assigned, replaces $\undef$ and the assignment state of a variable with value \IVML{null} shall not be \IVML{UNDEFINED}. + +As introduced in Section \ref{sectNotationConstraints}, a constraint expression may just represent a constant value. This constant value can be obtained from an expression $e$ using $const(e)$, which returns $\undef$ for any expression that is not a constant expression. Further, complex values can consist of nested values, which are accessible through $elements(val)$. In case of a collection value, $allElements(val)$ returns the values of the flattened collection, respectively. To ease the notation of some algorithms, we just assume here that for a non-complex value $val$, $elements(val)=\set{val}$ and, in case of a collection value, $allElements(val)=\set{val}$ else $\set{}$. Further, we assume that $elements(\undef)=\emptySet$ and $allElements(\undef)=\emptySet$. + +In some situations we must either rely on the actual value of a variable (if available) or the default value of the variable, the latter in particular for initializing a configuration through the reasoner. Thus, for a variable $v$ and its declaration $d=decl(v)$, we define\footnote{We follow the style of the implementation for documentation purposes. There, $d$ is typically available via a parameter or a local variable to avoid repeated method calls.} % $$ -relevantValue(v, d, inc) = \begin{cases}value(v), & \text{if } value(v) \neq\undef\\ const(default(d)), & \text{if} default(d) \neq\undef \wedge \neg inc\\ \undef, & \text{else}\end{cases} +relevantValue(v, d, inc) = \begin{cases}value(v), & \text{if } value(v) \neq\undef\\ const(default(d)), & \text{if } default(d) \neq\undef \wedge \neg inc\\ \undef, & \text{else}\end{cases} $$ % -i.e., the relevant value of a variable is either its assigned value or its constant default value, the latter only if we are not in incremental reasoning mode $inc$. -% -Please note that we could also write $relevantValue(v, inc)=relevantValue(v, decl(v), inc)$, but many algorithms below will explicitly require a variable $v$ and its declaration $d$. This is due to historical reasons in the development of the reasoner aiming to avoid frequently calling $decl(v)$. +returning the relevant value of variable $f$ either in terms of its assigned value or its default value, the latter only if we are not in incremental reasoning mode $inc$. +% %----------------------------------------------------------------------------------------------------------------- @@ -853,5 +857,5 @@ $pushContext(\variableMapping, false)$\; - $t_n \assng nested(t); t_b \assng base^*(t_n); used\assng\emptySet$\; + $t_n \assng nested^*(t); t_b \assng base^*(t_n); used\assng\emptySet$\; $val\assng relevantValue(d, v, inc)$\; \uIf{$isConstraint(t_b)$} { @@ -883,5 +887,5 @@ % \begin{displaymath} -d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested(c)}}\IVML{forAll}(l:c(l)) +d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(c)}}\IVML{forAll}(l:c(l)) \end{displaymath} % @@ -1029,5 +1033,5 @@ }$\; \If{$v \neq \undef$}{ - $w \assng nested(v, name(d))$\; + $w \assng nested^*(v, name(d))$\; \uIf{$n \neq \undef \wedge\text{ } value(w) \neq \undef$} { $t \assng type(value(w))$\;