Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 73) +++ /reasoner/reasoner.tex (revision 74) @@ -121,17 +121,17 @@ 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$ and $nested(v, n)$ the nested variable with name $n$ in $v$ ($nested(v, n)$ may be undefined). 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} +% +\begin{multline*} allNested(v) = \begin{cases} \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} - -\begin{multline} +\end{multline*} +% +\begin{multline*} allParents(v) = \begin{cases} \setEmpty, & \text{if } \neg isVariable(parent(v)) \\ \begin{aligned}\set{&parent(v)} \cup\\ &allParents(parent(v)),\end{aligned} & \text{else}\\ \end{cases} -\end{multline} - +\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). @@ -165,5 +165,5 @@ &constraints(e) \cup \setWith{allEvalConstraints(f)}{f \in evals(e)} \end{align*} - +% In IVML, an \emph{annotation assignment} is a kind of 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. @@ -174,5 +174,5 @@ &constraints(a) \cup \setWith{allAssignmentConstraints(b)}{b \in assignments(a)} \end{align*} - +% \subsubsection{Constraints}\label{sectNotationConstraints} @@ -185,5 +185,5 @@ 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 populate the constraint base. For this purpose, we use a specific notation indicating constraint creation combining algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (stated in teletype) used to build up the constraint expression. For example, for creating the IVML constraint \IVML{x = 25;}, we denote in algorithms $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the expression representing the constraint. Here, \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}), which returns 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 generically describe a constraint instantiation. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i|i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i|i>20)}}$. -As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a set of $\mapEntry{e_s, e_t}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. +As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a $\variableMapping=\set{\mapEntry{e_s, e_t}}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. 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)}$ @@ -194,7 +194,7 @@ 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 $t$, then $decision(v, s)$ returns the variable related to slot $s$ in the configuration $v$ is a member of. $slots(v)$ is definied similarly to $slots(t)$, but contains all slots of the variable, i.e., including those inherited from refined compounds and those declared within assignment-blocks nested within the declaration of the compound type $t$. 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 - +% Compounds can form an inheritance hierarchy through multiple inheritance. Individual slots from parent compounds can thereby shadowed / redefined by slots of the same or more specific type. $refines(t)$ represents the set of compound types directly refined by compound $t$, returning an empty set if there are no such compounds or if $t$ is not a compound type. We define % @@ -261,15 +261,15 @@ 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 - +% $$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ - +% to return 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 consists of constraints, i.e., - +% $$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$$. - +% In other situations, we need to know all types that are used in a container (value), 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. 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})}$. @@ -283,7 +283,7 @@ 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 is relevant. 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 - +% $$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{Other IVML Elements}\label{sectNotationOthers} @@ -345,5 +345,7 @@ \subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation} -Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. The variable mapping is a core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed. +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. + +The variable mapping is a global core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed and can safely be cleared. As $\variableMapping$ is global (also for performance reasons) and cleared only after processing an IVML project, it can temporarily contain outdated or superfluous entries, e.g., from the a previous compound of the same type being currently processed. However, the mapping is anyway correct as long as the IVML model was correctly created, e.g., through the IVML parser, as then all model elements and their types are properly resolved, no dangling references do exist and the relevant entires in $\variableMapping$ are overridden by the translation algorithm before use, i.e., the remaining superfluous entries are just ignored. From a technical point of view, the variability mapping consists of mapping entries relating a variable declaration with an access expression if needed. For directly accessible variables such as top-level variables directly defined within a project, no such mapping is needed ($\undef$). For variables used in constraints within compounds or containers, an appropriate accessor is needed, created and registered when starting to translate the respective type. The respective constraints for that type are then enumerated, copied and while copying the variables registered in the variable mapping are replaced by the accessor expressions in the mapping. It is important to ensure that the mapping for the respective type is complete before constraint translation, so that all variables including cross references within the same type can be replaced properly. References to other variables are already given as accessor expressions and do not need to be considered here. @@ -467,6 +469,4 @@ If there is finally a default value expression to be recorded in the constraint base, we have to distinguish whether the actual variable is a constraint variable or an usual variable. In the first case, we apply Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). In the second case, we turn the default value expression into an assignment expression. However, the accessor creation depends on whether $d$ is an annotation or an usual variable. Then, we substitute \IVML{self} and the actual variable mapping on the complete constraint expression and turn the result into a default constraint. We either either it to $\deferredDefaultConstraints$ if the constraint may override a complete value assignment (\IVML{self} is used referring to another variable in the same compound or $d$ is an overridden slot that may accidentally be overriden by a complex compound value) or in all other cases to the usual default constraints set $\defaultConstraints$. - -Adding constraints or sets of constraints to the constraint base involves constraint filtering in order to respect the incremental reasoning mode and in some cases collection of constraints that initialize compounds and containers \TBD{unclear}. We will discuss these operations in Section \ref{sectContainerBase} and just use the function $addConstraint(s, c, b)$, adding constraint $c$ to constraint set $s$, considering copound and container initialization if $b = true$. \begin{algorithm}[H] @@ -505,4 +505,5 @@ \end{algorithm} +Adding constraints or sets of constraints to the constraint base involves constraint filtering in order to respect the incremental reasoning mode as well as constraints that initialize compounds and containers through respective initializer expressions. This is done by a specific operation, which we will discuss in Section \ref{sectContainerBase}. Below, we ill just use the respective function $add(s, c, b)$, which adds constraint $c$ to constraint set $s$, considering compound and container initialization expressions if $b = true$. We allow disabling the checks for container and compound initiailizers for certain kinds of constraints, for which we are sure that the these expressions do not occur, to improve the performance of the reasoning. \subsection{Derived types}\label{sectDerivedTypes} @@ -542,6 +543,4 @@ In lines \ref{algTranslateCompoundDeclarationVarMappingStart}-\ref{algTranslateCompoundDeclarationVarMappingEnd}, Algorithm \ref{algTranslateCompoundDeclaration} creates accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. The first case creates a static accessor based on the declared type. The second case handles values of sub-types of $type(d)=type(v)$. Therefore, it creates a compound accessor for the most specific type given by $type(value(v))$. However, due to static type checking of the expression, we need a type cast to $type(value(v))$ as otherwise slots defined on the more specific type are not accessible. In fact, as an optimization, the type cast can be omitted if $t=type(value(v))$, but this is not shown in Algorithm \ref{algTranslateCompoundDeclaration}. Now, as the mapping is completed for $v$, the algorithm performs a transitive / recursive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlots}. Please note that $slots(v)$ also includes the actual annotations for $v$, i.e., at this point the variable mapping contains also accessors to annotations and processing their declarations through Algorithm \ref{algTranslateDeclaration} anyway considers annotations. - -Now, we can translate further nested values / structures or contained constraints involving the mapping. First, Algorithm \ref{algTranslateCompoundDeclaration} inspects all slots / attributes. 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 other constraints $\otherConstraints$. \begin{algorithm}[H] @@ -568,4 +567,6 @@ \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} \end{algorithm} + +Now, we can translate further nested values / structures or contained constraints involving the mapping. First, Algorithm \ref{algTranslateCompoundDeclaration} inspects all slots / attributes. 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 other constraints $\otherConstraints$. Finally, the algorithm translates the nested structures. Then it translates all annotation value assignments using Algorithm \ref{algTranslateAnnotationAssignments}. For the last two translations, we need the actual value of \IVMLself{}, to be determined for the recent compound, either based on the given accessor $ca$ or the declaration $d$. Then, to keep the priority of eval-blocks, it collects all constraints of all nested eval-blocks, replaces \IVMLself{} and variable mappings $\variableMapping$ and adds them to $\otherConstraints$. Finally, we take over and translate all constraints of all transitively declared constraints refined compounds and assignment constraints.