Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 129) +++ /reasoner/reasoner.tex (revision 130) @@ -39,5 +39,6 @@ \newcommand\createConstraint[1]{\langle #1 \rangle} \newcommand\createDefaultConstraint[1]{\langle #1 \rangle_d} -\newcommand\isDefaultConstraint[1]{isDefault(#1)} +\newcommand\isDefaultConstraintName[0]{isDefault} +\newcommand\isDefaultConstraint[1]{\isDefaultConstraintName(#1)} \newcommand\createConstraintConstraint[1]{\langle #1 \rangle_c} \newcommand\isConstraintConstraint[1]{isVariableConstraint(#1)} @@ -197,5 +198,5 @@ %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} +\subsubsection{Project}\label{sectNotationProject} A \emph{project} is a named scope, which can contain variable declarations, type declarations, assignment-blocks and eval-blocks. $decls(p)$ denotes the set of all variable declarations introduced in project $p$. $isProject(p)$ returns $true$ for a project $p$. @@ -234,28 +235,27 @@ \subsubsection{Constraints}\label{sectNotationConstraints} -In IVML, 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 variables involved in the constraint, 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, \IVML{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;} - -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{assng} 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. Moreover, to indicate some generic use of constraints, e.g., in transformation patterns, we denote a constraint $c$ using a certain variable $v$ by $c(v)$. - -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}$. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. As we use the '$|$' symbol for variable substitutions, using the same symbol in some transformations in IVML quantor expressions would be confusing. Thus, we use in this document the respective syntax parts ':' as introduced for sets in Section \ref{sectGeneralNotation} instead of the syntactically correct '$|$', e.g., \IVML{forall(x:c(x))} instead of the correct IVML notation \IVML{forall(x|c(x))}. 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)}}$. - -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, e.g., for creating a default constraint, we denote $b \assng \createDefaultConstraint{\IVML{assign}(x, 25)}$ for which $\isDefaultConstraint{b} = true$ holds. In case of an assignment constraint $x = y$, i.e., $c=\createDefaultConstraint{\IVML{assign(}x, y\IVML{)}}$, $rightSide(c) = x$ else $\undef$. Further, we allow attaching additional information to a constraint, e.g., the type it was created for. Let $c = attach(c, t)$ be an operation that attaches $t$ to constraint $c$ (and returns $c$) as well as $t = attached(c)$ return the respective attachment. +In IVML, a \emph{constraint} is a Boolean expression that must always evaluate to $true$. Otherwise, reasoning shall either fail. After a change of at least one of the values of the variables involved in the constraint, the constraint may be re-evaluated successfully, causing a cleanup of previous reasoning errors for that constraint. + +Technically, a constraint can consist of sub-expressions, that can evaluate to values of some type supported by IVML, in particular of Boolean type. Such expressions can be used to determine the default value of variables and, of course, sub-expressions may make use of / refer to variables. Let $v$ be a constraint, then we indicate, e.g., in transformation patterns, by $c(v)$ that constraint $c$ is using variable $v$. Moreover, if $c$ is an assignment constraint representing $x = y$, the operation $rightSide(c)$ returns $y$ else $\undef$. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. + +Moreover, \IVML{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 of a constraint variable is extracted and then 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 in the subsequent reasoning process. $isConstraint(t)$ indicates whether type $t$ is a constraint type. %$isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to unconditionally change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} the constraint \IVML{x = 25;} in IVML notation is an assignment Constraint. + +During the constraint instantiation, variables must be substituted by other variables or expressions. Let $c$ 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{y}. For example, if the constraint $c$ was before the substitution \IVML{x = 25}, it will be \IVML{y = 25} after the substitution. The right side of a substition can be a variable or, more generally, an expression. Substitutions are transitive, i.e., in $\varSubstitution{c}{x=y,y=z}$ $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}$. Substitutions can also be expressed in terms of a mapping to express multiple substitutions or to create up / reuse the substitution specification for several constraints. Let $\variableMapping=\set{\mapEntry{x}{e}}$ be a mapping, then $x$ is the variable to be replaced, $e$ the replacing variable/expression and $\varSubstitutionVarMapping{c}$ denotes the respective substitution. Both notations can be combined, e.g., to $\varSubstitutionOtherVarMapping{c}{x = y}$. + +During the constraint instantation, also new constraints must be created. For this purpose, we use a specific notation to indicate constraint creation and the construction of sub-expressions. This notation combines algorithm elements, e.g., variables, carrying actual values/elements (written in mathematical notation) and IVML expression constructors (stated in teletype). For example, for creating the IVML constraint \IVML{x = 25;} we write $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the creation of the expression making up the constraint. Here, \IVML{assng} is the constructor for the assign operation defined by IVML (actually implementing the assignment in \IVML{x = 25}) returning a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may generically denote $\createConstraint{\IVML{assign}(x, 25)}$, with $x$ being determined by the algorithm. + + +As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. However, as we use the '$|$' symbol for variable substitutions, also using the same symbol in IVML quantor expressions may be confusing. Thus, we use in this document ':' instead of '$|$', e.g., we denote \IVML{forall(x:$c(x)$)} to indicate the construction of an all-quantized expression over a constraint using the quantor iterator variable $x$ instead of \IVML{forall(x|$c(x)$)}. In summary, let \IVML{o} be an IVML collection of Integers, then \IVML{o->forall(i:i>20);} requires that all values in $o$ must be greater than 20. To create such a constraint with $o$ being an algorithm variable, we denote $\createConstraint{o\IVML{->forall(i:i>20)}}$. + +To perform specific instantiations, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate default value constraints by `$d$' in the constraint creation notation. For example, for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ for which the operation $\isDefaultConstraintName$ returns $true$. Further, we allow attaching additional information to a constraint, e.g., the type it was created for. Let $c$ be a constraint, then $attach(c, t)$ is an operation that attaches $t$ to constraint $c$ and returns $c$. The operation $attached(c)$ return the respective attachment. %Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds. -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. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. When creating expressions, sometimes a temporary (local) variable is needed, e.g., for an IVML let-expression or a container iterator. We state this by $\IVMLMeta{var}(t)$, i.e., create the temporary variable of type $t$ (we don't care for the name of the variable here). For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. +In some cases, constraints cannot be created in terms of a single step, i.e., sub-expressions are created iteratively. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating expressions, in particular in an incremental fashion, sometimes a temporary (local) IVML variable is needed, e.g., for an IVML let-expression or a container iterator. We state the creation of such a variable by $\IVMLMeta{var}(t)$, i.e., request the creation of a temporary variable\footnote{We don't care for the variable name in this document.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. \subsubsection{Compounds}\label{sectNotationCompounds} -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 define own nested constraints, i.e., the constaints of compound type $t$ are then $constraints(t)$. - -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 +A \emph{compound} is an IVML type, which consists of nested variable declarations, called slots. Let $t$ be a compound type, then $isCompound(t)$ returns $true$ and $false$ for all other types. The declared 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. + +Compounds can form an inheritance hierarchy. $refines(t)$ represents the set of compound types directly refined by compound $t$ through multii-inheritance, returning an empty set if there are no such compounds or if $t$ is not a compound type. Individual slots from parent compounds can thereby shadowed / redefined by slots of the same or more specific type. We define % $$allRefines(t) = @@ -266,5 +266,5 @@ $$ % -as the set of all refined compounds along the compound refinement / inheritance hierarchy of $t$ and +as the set of all refined compounds along the compound refinement hierarchy of $t$ and % $$allRefines^+(t) = @@ -274,11 +274,11 @@ \end{cases}$$ % -as the set of all refined compounds along the compound refinement / inheritance hierarchy of $t$ including $t$. We denote for $t$ and $s$ compounds $\subTypeOf{t}{s}$ if $t\in allRefines(s)$, i.e., $s$ is a subtype of $t$. Similarly, $\subTypeEqOf{t}{s}$ if $t\in allRefines^+(s)$. - -Based on the functions above, the set of all slots for compound type $t$ can be derived by +as the set of all refined compounds along the compound refinement hierarchy of $t$ including $t$ itself. Let $t$ and $s$ be compound types. Then we denote $\subTypeOf{t}{s}$ if $t\in allRefines(s)$, i.e., $s$ is a subtype of $t$. Similarly, $\subTypeEqOf{t}{s}$ if $t\in allRefines^+(s)$. Based on these functions, the set of all slots for compound type $t$ can be obtained by % $$slots^+(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ -% -All declared compound constraints\footnote{The implementation unifies $allCompoundConstraints(t)$ with $allVariableConstraints(t)$ distinguished by a boolean parameter. We differentiate them here to indicate the sets to be transformed more clearly.} for compound type $t$ are + +A compound $t$ can define own nested assignment blocks $assignments(t)$ (related functions are defined for compounds akin to Section \ref{sectNotationProject}) and constraints $constraints(t)$. All declared compound constraints +%\footnote{The implementation unifies $allCompoundConstraints(t)$ with $allVariableConstraints(t)$ distinguished by a boolean parameter. We differentiate them here to indicate the sets to be transformed more clearly.} +for compound type $t$ are % \begin{align*} @@ -287,11 +287,21 @@ \end{align*} % -and all constraints stemming from constraint variables for $t$ -% -\begin{align*} -all&VariableConstraints(t) = \setWith{\createConstraint{s}}{s\in slots^+(t) \wedge isConstraint(type(s))}\text{ } -\end{align*} -% -In some constraint transformations it is important to determine, whether a variable declaration, i.e., in particular for a compound slot is overridden. Let $d$ be a declaration, in particular $d\in slots(t) \wedge isCompund(t)$, then the parent compound of $d$ is +%and all constraints stemming from constraint variables for $t$ +%% +%\begin{align*} +%all&VariableConstraints(t) = \setWith{\createConstraint{s}}{s\in slots^+(t) \wedge isConstraint(type(s))}\text{ } +%\end{align*} +%% + +Let $v$ be a compound variable, i.e., a variable of a compound type $t$. Then $decision(v, s)$ returns the configuration variable representing slot $s$ in the compound variable $v$. As in the implementation, $slots(v)$ returns also all slots inherited from refined compounds including those defined in nested assignment blocks. +% +%For convenience, we introduce a function returning all default slots of a variable $v$ +%% +%$$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 +%% + + +% +In some constraint transformations it is important to determine, whether a compound slot is overridden. Let $d$ be a declaration, in particular $d\in slots(t) \wedge isCompund(t)$, then the parent compound of $d$ skipping potentially enclosing nested assignment blocks is % \begin{align*} @@ -304,9 +314,9 @@ \end{align*} -and we can determine whether $d$ is overridden by +and we can determine whether $d$ is overridden / also defined by a refined compound by % $$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ -Akin to projects, $assignments(t)$ is defined for a compound type $t$ and returns the annotation assignment-blocks and $evals(t)$ all eval-blocks nested in $t$. Further, for $t$, constraints for all nested eval-blocks can be obtained using +Akin to projects in Section \ref{sectNotationProject}, $evals(t)$ is defined for a compound type $t$ and returns all eval-blocks nested in $t$. Further, all constraints defined by all nested eval-blocks of $t$ can be obtained using % \begin{equation*} @@ -314,15 +324,15 @@ \end{equation*} % -\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. +\emph{Accessors} to compound variables define a path to access a certain slot within a compound variable, i.e., an accessor specifies the variable and the slot / nested slot path to access. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} defined in \IVML{cmp} 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 in the constraint translation, we use the IVML access constructor \IVML{acc}. Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor 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 can be defined, e.g., as a default value expression or as an assignment constraint, using a complex value expression, a so called \emph{compound initializer}, essentially a name-value mapping. As slots can be in turn of a complex type, e.g., of a compound type, a compound initializer can also contain nested complex values, e.g., nested compound initializers. \subsubsection{Containers}\label{sectNotationContainers} -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). +An IVML \emph{container} is a parameterized 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 at least the static type compliance is checked by the IVML parser before reasoning. 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}$$ +$$nested(t)=\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}. If a container $isNested(c)$ for a container $c$, $elements(c)$ contains container values of the nested type. Here, $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.