Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 11) +++ /reasoner/reasoner.tex (revision 12) @@ -5,12 +5,19 @@ \usepackage[ruled, vlined]{algorithm2e} -\newcommand\TBD[1]{{\color{red}TBD: #1}} -\newcommand\MISSING[1]{{\color{orange}MISSING: #1}} +\newcommand\TBD[1]{{\color{blue}TBD: #1}} +\newcommand\MISSING[1]{{\color{red}MISSING: #1}} \newcommand\IVML[1]{\texttt{#1}} -\newcommand\addSeq[0]{\uplus} +\newcommand\addSeq[0]{\oplus} +\newcommand\addSeqNoDupl[0]{\uplus} +\newcommand\assng[0]{\leftarrow} +\newcommand\iterAssng[0]{:} % <<- +\newcommand\undef[0]{\perp} +\newcommand\emptySet[0]{\{\}} +\newcommand\set[1]{\{#1\}} +\newcommand\setWith[2]{\{#1:#2\}} \begin{document} -\title{SSE reasoner} +\title{The SSE IVML reasoner} \date{} \maketitle @@ -18,18 +25,41 @@ This is a summary of the implemented reasoning algorithm of the SSE reasoner as a basis for checking completeness against the IVML specification and correctness of the reasoning. Changes to the implementation shall be reflected here and vice versa. +\TBD{structure} + + + \section{Notation/Terminology} \begin{itemize} + \item $\cup$ denotes the union of two sets (no duplicates in result, sequence does not matter), $\addSeq$ is adding elements to a sequence, $\addSeqNoDupl$ is adding elements to a sequence without duplicates (combination of $\cup$ and $\addSeq$) \item An access expression specifies slots (within compounds or behind references) or elements (within a collection) to be accessed. Examples: \IVML{cmp.slot}, \IVML{cmp.slot1.slot2}, \IVML{coll[1]}, \IVML{coll[1].slot}. - \item $\perp$ is the undefined constraint + \item An assignment state classifies the value in an IVML configuration variabe according to the configuration lifecycle. Relevant assignment states are: + \begin{itemize} + \item \IVML{UNDEFINED}: no value has been assigned so far or the value was cleared intentionally. + \item \IVML{DEFAULT}: a type compatible default value has been assigned by evaluating the default value expression of the underlying variable declaration. Default values can be changed unless frozen. Then the variable receives one of the following assignment states. + \item \IVML{ASSIGNED}: a type compatible value has been assigned (by the implementation), but the value is still changable. + \item \IVML{USER\_ASSIGNED}: a type compatible value has been assigned by the user and shall not be overriden by the impelmentation, e.g., the reasoner. + \item \IVML{DERIVED}: a type compatible value has been assigned as a consequence of evaluating constraints, e.g., through the reasoner. + \item \IVML{FROZEN}: the variable was frozen through the IVML \IVML{freeze} statement to avoid further changes of the actual value (including no value in state \IVML{UNDEFINED}). Further assignments are not allowed and cause an assignment error. + \end{itemize} + \item usually, if not used otherwise, $v$ is variable, $d$ is declaration, $t$ is type, $val$ is value + \item $\undef$ is the undefined value, e.g., an undfined constraint, type or declaration. \TBD{what is a constraint, how to denote a constraint creation in contrast to mathematical/algorithmic notation} + \item $declaration(v)$ the declaration of variable $v$ + \item $type(d)$ the type of the variable declaration $d$, similarly $type(v) = type(declaration(v))$ and $type(val)$ the (potentially sub-)type of the value $val$ + \item $varDeclarations(p)$ the set of all variable declarations in project $p$ \item $name(s)$ is the default value expression of slot $s$ \item $default(s)$ is the default value expression of slot $s$ \item $elements(c)$ is the set of all element values in a collection \item $isNested(c)$ whether a collection is a nested collection - \item $refines(c)$ is the set of all compounds refining $c$ (excluding $c$), $refines^+(c)=refines(c) \cup \{c\}$ i; both empty if not compound - \item $dfltSlots(v) = \{s|s\in slots(v) \wedge default(s) \neq \perp\}$, empty for all non-compound types - \item assignment states - \item $cup$ is the set union, $\addSeq$ is adding elements to a sequence + \item $isDerived(t)$ whether $t$ is a derived type. In this case, $basis(t)$ is the basis type $t$ is derived from, else $basis(t) =\undef$ + \item $refines(t)$ is the set of compounds directly refining compound $t$, if there are none or $t$ is not a compound $refines(t)=\emptySet$ + \item $constraints(t)$ is the set of constraints defined for type $t$, similarly for a declaration $d$. Let $s$ be a set of types or declarations, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. + \item $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 + \item $alBase(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}$ + \item $allRefines(t) = \begin{cases}\emptySet, & \text{if } refines(t) = \emptySet \\ allRefines(t) \cup \bigcup_{u\in refines(t)} allRefines(u), & \text{else}\\ \end{cases}$ + \item $allRefines^+(t) = \begin{cases}allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ \emptySet, & \text{else} \\ \end{cases}$ \end{itemize} +\TBD{Algorithms + implementation name} + \section{Reasoning algorithm} @@ -39,5 +69,5 @@ 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}. -Relevant IVML projects are identified throgh the (potentially cyclic) import structure performing a depth-first search starting with the top-level project of a configuration. $discoverProjects(cfg)$ returns a sequence of IVML projects for $cfg$ listing the projects with less import dependencies first. Following this sequence, Algorithm \ref{algMainLoop} first identifies the constraints determining default values, then the remaining constraints and registers the constraints with the respective variables. The constraints are added to the constraint $base$ in this sequence to ensure that variables are properly initialized before other constraints are considered. We will discuss the relevant expressions, constraints and their transformations in detail in Section \ref{sectConstraintTranslation}. +Relevant IVML projects are identified throgh the (potentially cyclic) import structure performing a depth-first search starting with the top-level project of a configuration. $discoverProjects(cfg)$ returns a sequence of IVML projects for $cfg$ listing the projects with less import dependencies first. Following this sequence, Algorithm \ref{algMainLoop} first identifies the constraints determining default values, then the remaining constraints and registers the constraints with the respective variables. The constraints are appended to the constraint $base$ in this sequence to ensure that variables are properly initialized before other constraints are considered. We will discuss the relevant expressions, constraints and their transformations in detail in Section \ref{sectConstraintTranslation}. Following this sequence, the $evaluateConstraints$ function (cf. Algorithm \ref{algEvalLoop}) evaluates each constraint in $base$ in sequence until no more (failing) constraints are available. If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation by Algorithm \ref{algVarChange}. Finally, the main reasoning algorithm composes a structured reasoning result based on persisting recorded evaluation problems. @@ -48,17 +78,18 @@ \KwData{problem records $m$, relevant constraints $t$} \KwResult{Reasoning result $r$} - $projects \leftarrow$ discoverImports(cfg)\; - \For{$p \leftarrow projects$}{ + + $projects \assng discoverImports(cfg)$\; + \ForAll{$p \iterAssng projects$}{ %evaluator.init()\; %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\; %evaluator.setScopeAssignments(sAssng)\; - $base \leftarrow collectDefaults(p, t)$\; - $base \leftarrow base \addSeq collectConstraints(p, t)$\; + $base \assng translateDefaults(p, t)$\; + $base \assng base \addSeq translateConstraints(p, t)$\; $evaluateConstraints(p, base)$\; $freeze(p)$\; %evaluator.clear()\; } - $r \leftarrow createReasoningResult(m)$ - \caption{Main reasoning loop.}\label{algMainLoop} + $r \assng createReasoningResult(m)$ + \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop} \end{algorithm} @@ -79,16 +110,17 @@ \KwIn{project $p$, constraint $base$} \KwData{scope assignments $a$, problem records $m$, used variables $u$, constraint evaluator $e$} + $clearScopeAssignments(a)$\; $setDispatchScope(e, p)$\; %evaluator.setDispatchScope \While {$|base| > 0$} { - $c \leftarrow pop(base)$\; + $c \assng pop(base)$\; $clear(u)$\; $setAssignmentState(e, isDefault(c))$\; - $m \leftarrow m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\; - } - \caption{Constraint evaluation loop.}\label{algEvalLoop} -\end{algorithm} - -\TBD{Variable change} + $m \assng m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\; + } + \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop} +\end{algorithm} + +When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a collection operation nor a local variable defined in a let-expression, the change is registered within the actual scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value changes}) for both, parent and client variables of $v$ are identified. Both, parents and children must be considered, as value in compounds may have impact on both kinds of siblings. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint base. \begin{algorithm}[H] @@ -96,23 +128,60 @@ \KwIn{decision variable $v$} \KwData{scope assignments $a$, relevant constraints $t$} + \If{$\neg isLocal(v)$}{ $registerScopeAssignment(a, v)$\; - $base \leftarrow base \cup constraintsForParent(v)$\; - $base \leftarrow base \cup constraintsForChilds(v)$\; - } - \caption{Modification of constraint base upon variable change.}\label{algVarChange} -\end{algorithm} - -\section{Constraint translation}\label{sectConstraintTranslation} + \MISSING{change constraints if dynamic value type changes}\; + $base \assng base \addSeqNoDupl constraintsForParent(v)$\; + $base \assng base \addSeqNoDupl constraintsForChilds(v)$\; + } + \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange} +\end{algorithm} + + + +\section{Default value translation}\label{sectDefltTranslation} + +IVML allows defining default value expressions for all variables including top-level project variables as well as compound slots. From the perspective of IVML and its object model, a default value is part of a variable declaration, i.e., per se not a constraint, i.e., the syntax + +\texttt{Type variable = expression;} + +must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. + +The top-level transformation is defined by Algorithm \ref{algTranslateDefaults}. It considers all variable declarations in the given project and +\begin{itemize} + \item translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of internal constraints $c_i$ + \item \TBD{fill} +\end{itemize} + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{project $p$} + \KwData{constraint $base$, variable mapping $m$, internal constraints $c_i$} + + \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDefaultForDeclaration + $c_i \assng c_i \cup translateDerivedDatatypeConstraints(d)$\; + \TBD{fill}\; + } + \caption{Translating default value expressions to constraints (\IVML{translateDefaults, translateDefaultForDeclaration}).}\label{algTranslateDefaults} +\end{algorithm} + +\subsection{Derived types}\label{sectDerivedTypes} + +In IVML, a derived datatype $d$ is defined based on a known base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ using a local variable $decl(d)$ to express the constraints. \TBD{decl(d) is not introduced above. Needed?}. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. If a variable $v$ is declared of type $d$, all constraints defined for $d$ over $b$ and, transitively over the base types of $b$ apply. Whether these constraints are fullfilled depends on the actual value of $v$. Therefore, we translate all constraints defined on type $d$ (of $v$) to constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for basis types substituting in each constraint the respective local variable by the actual variable $d$. The resulting constraints + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$} + \KwOut{instantiated constraints for derived type $d$} + + $\setWith{c|_{decl(s)=d}}{c\in constraints(s) \wedge s\in allBase(type(d))}$\; + \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} +\end{algorithm} \subsection{Default constraints} -IVML allows defining default value expressions for all variables including top-level project variables as well as compound slots. From the perspective of IVML and its object model, a default value is part of a variable declaration, i.e., per se not a constraint, i.e., the syntax - -\texttt{Type variable = expression;} - -must be translated into a constraint $variable = expression$. Expressions may be simple variables, calculations or operation calls, in compounds also using the predefined variable \texttt{self} indicating the actual instance of the respective compound. These constraints must be evaluated upon each variable instantiation, i.e., for top-level basic variables, top-level compound variables, compound values within compounds as well as compound values within container initialiers, each potentially with a different access expression to make the variable unique. - \subsubsection{Compound default constraints} + +%Expressions may be simple variables, calculations or operation calls, in compounds also using the predefined variable \texttt{self} indicating the actual instance of the respective compound. These constraints must be evaluated upon each variable instance, i.e., for top-level basic variables, top-level compound variables, compound values within compounds as well as compound values within container initialiers, each potentially with a different access expression to make the variable unique. \subsubsection{Collection default constraints}\label{deflt_collections} @@ -125,5 +194,5 @@ \item \textbf{Parameter:} collection $c$ -\item \textbf{Elements:} $elts = \bigcup_{v\in\{refines^+(c)|c \in elements(c) \}} : dfltSlots(v)$ +\item \textbf{Elements:} $elts = \bigcup_{v\in\setWith{allRefines^+(c)}{c \in elements(c)}} : dfltSlots(v)$ \item \textbf{Transformation ($s\in elts$):} $\langle flatten(c)\rightarrow forAll(i|assng(i.\bf{name(s)}, \bf{default(s)}|_{self=i}\rangle$ @@ -132,9 +201,11 @@ \end{itemize} -\subsection{Other constraints} +\section{Constraint translation}\label{sectConstraintTranslation} + + \section{Completeness} -\begin{table*}[t] +\begin{table*}[h] \centering \begin{tabular}{|l|c||l|c|} @@ -157,4 +228,6 @@ Compound constraint & & & \\ \hline +Eval & & & \\ +\hline \end{tabular} \caption{IVML concepts vs. reasoning constraint transformations.} @@ -163,3 +236,9 @@ + +\section{Conclusion} + +\TBD{End here if we do not turn this into a TR or more. Else, evaluate, e.g., along the different test versions of EASy, the synthetic cases of Roman, etc.} + + \end{document}