Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 188) +++ /reasoner/notation.tex (revision 189) @@ -96,5 +96,5 @@ A \emph{project} is a named scope, which can contain variable declarations, type declarations, annotation assignment blocks and \IVML{eval}-blocks. $isProject(p)$ returns $true$ for a project $p$. $decls(p)$ denotes the set of all variable declarations and $annotations(p)$ all annotation declarations introduced in $p$. -A project constitutes the evaluation scope for all contained constraints, i.e., during the evaluation of a project, a variable must not be assigned more than once~\cite{IVML-LS}. As stated above, local variables are evaluated within their containing local scope and can be re-assigned. +A project constitutes an evaluation scope for all contained constraints. During reasoning, a variable must not be assigned more than once within the same project scope~\cite{IVML-LS}. IVML interfaces can affect the project scope by defining visibilities and access restrictions for imported projects. Project interfaces represent static structural properties that are handled while creating an IVML project, i.e., project interfaces are transparent to the reasoner and do not need to be considered during reasoning. In contrast, local variables are evaluated within their containing local scope and can be re-assigned. $evals(p)$ is the set of (potentially nested) \emph{eval-blocks} in project $p$. If $e\in evals(p)$ then $constraints(e)$ returns the constraints listed in $e$, whereby $constraints(e)$ may be empty, in particular if $e$ is an arbitrary model element. Similarly, $evals(e)$ returns the nested eval-blocks. Subsequently, the function $allEvalConstraints(e)$ returns all constraints in eval-block $e$ including all nested eval-blocks: @@ -239,18 +239,21 @@ \subsubsection{Containers}\label{sectNotationContainers} -An IVML \emph{container} is a parametrized type representing a structure that holds an arbitrary number of variables / values. IVML defines two default container types, namely \emph{sequence} (duplicates allowed, order important) and \emph{set} (no duplicates allowed, order irrelevant). The type parameters of a container are not relevant for reasoning, as we can assume that the static type compliance is checked by the IVML object model or the IVML parser before reasoning. +An IVML \emph{container} is data structure that is parameterized over the types of its elements and holds an arbitrary number of variables / values. IVML defines two container types, namely the \emph{sequence type} (duplicates allowed, order important) and the \emph{set type} (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))} in IVML notation, $contained(t)$ returns \IVML{setOf(Integer)}. -We define $isNested(t) = isContainer(contained(t))$ and +We define $isNested(t) = isContainer(contained(t))$. If $isNested(c)$ is $true$ for a container $c$, $elements(c)$ contains values of the nested type. Moreover, + % $$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))$$ -% +returning the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested^*(t)$ returns \IVML{Integer}. + +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 created from all leafs of a depth-first traversal of the elements containment trees. +% +%During constraint translation, we must identify whether a container consists of constraints, i.e., +%% +%$$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 % @@ -259,5 +262,5 @@ 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})}$. +For containers, element \emph{access expressions} frequently occur in terms of the iterator variable of container operations, e.g., quantors, or through index access to sequence elements. For example, let \IVML{seq} be a sequence of compounds, all having a common slot \IVML{slot}. Then $\IVML{seq->forAll(e|}c(\IVML{e.slot})\IVML{)}$ is a quantorized expression based on the iterator variable \IVML{e}. As \IVML{seq[1]} is an index-based access for the second element in the container\footnote{In contrast to OCL, IVML indexes are 0-based.}, accessing \IVML{slot} on the second 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})}$. 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. @@ -265,9 +268,9 @@ \subsubsection{Derived types}\label{sectNotationDerivedTypes} -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. +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 introduce an alias of a type, e.g., a speaking or simplifying name for 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 $base(t)$. Constraint expressions may use $decl(t)$, which must be substituted during constraint translation by the concrete variable declared for the derived type. + +In particular, derived types can be defined based on already existing derived types. In this case, a chain of dependent base types is created. 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}$$ @@ -275,29 +278,33 @@ 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}$$ +$$allBase(t) = \begin{cases} + \set{base(t)}, & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ + \set{base(t)} & \\ + \text{ } \cup allBase(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ + \emptySet, & \text{else}\\ \end{cases}$$ % \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$ +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 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 introduced 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. + +In IVML, a \emph{configuration reference} points to a variable defined in the same or another imported project. IVML configuration references require specific treatment during constraint translation. Therefore we introduce the following specific functions. 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. 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 dereference a configuration reference 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)}$$ -% -IVML project interfaces impose variable visibilities and access restrictions among imported projects. Thus, project interfaces represent static structural properties that must be handled while creating the IVML project, i.e., project interfaces are transparent to the reasoner and do not need to be considered during reasoning. +and in some cases even a set\footnote{As introduced in Section \ref{sectGeneralNotation} rather than an IVML collection of set type.} $s$ of types through +% +$$deref(s)=\setWith{t \in s}{deref(t)}$$ +% \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$. +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 neglect here most of the specific properties of IVML values. We introduce the relevant properties for reasoning in this section. + +A value $val$ is typed and, thus, always 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 that so far no value has been assigned to a variable and the variable may have either \IVML{UNDEFINED} or \IVML{FROZEN} as assignment state. \IVML{null} wipes out a previously assigned and can replace $\undef$. The assignment state of a variable with value \IVML{null} shall not be \IVML{UNDEFINED}. + +As introduced in Section \ref{sectNotationConstraints}, an expression may be a constant value in the most simple case. This constant value can be obtained from an expression $e$ using $const(e)$, which returns $\undef$ for any expression that is not a constant. 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 algorithms, we define 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 define 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.} @@ -307,4 +314,4 @@ $$ % -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$. -% +returning the relevant value of variable $v$ either as its assigned value or its default value, the latter only if reasoning is not done incrementally ($inc$). +%