Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 19) +++ /reasoner/reasoner.tex (revision 20) @@ -23,4 +23,5 @@ \title{The SSE IVML reasoner} +\author{Holger Eichelberger} \date{} \maketitle @@ -59,5 +60,5 @@ \item $isNested(c)$ whether a collection is a nested collection \item $isCompound(d)$, $isContainer(d)$, $isConstraint(d)$ - \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 $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$. $decl(d)$ is the specific variable of a derived type used to define restricting constraints. \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 $base(t)$ the type $t$ is derived from if $isDerived(t)$, $contained(t)$ the type contained in $t$ if $isCollection(t)$ or $t$ @@ -81,5 +82,21 @@ 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 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}. +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. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of + +\newcommand\defaultConstraints[0]{c_d} +\newcommand\deferredDefaultConstraints[0]{c_{dd}} +\newcommand\derivedTypeConstraints[0]{c_r} +\newcommand\constraintVariablesConstraints[0]{c_v} +\newcommand\defaultAnnotationConstraints[0]{c_{ad}} + +\begin{itemize} + \item Default constraints $\defaultConstraints$ containing constraints setting the default values. + \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$ \TBD{also $\defaultAnnotationConstraints$?}. + \item Default annotation constraints $\defaultAnnotationConstraints$ relating to default values of annotations. + \item Constraints $\derivedTypeConstraints$ representing instantiated restricting constraints from derived types. + \item Constraints representing constraint variables $\constraintVariablesConstraints$. +\end{itemize} + +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. @@ -151,5 +168,4 @@ - \section{Default value translation}\label{sectDefltTranslation} @@ -165,5 +181,5 @@ \SetAlgoLined \KwIn{project $p$, configuration $cfg$} - \KwData{constraint $base$, variable mapping $m$, internal constraints $c_i$, attribute constraints $c_a$} + \KwData{constraint $base$, variable mapping $m$, derived type constraints $\derivedTypeConstraints$, attribute constraints $\defaultAnnotationConstraints$} \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults @@ -175,20 +191,22 @@ Algorithm \ref{translateDeclarationDefaults} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm \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 Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $c_i$ + \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\derivedTypeConstraints$. + \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\defaultAnnotationConstraints$ \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm substitutes all occurrences of \IVML{self} by the actual declaration as well as all mapped variables from $m$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified. \item Collects all transformed collection compounds based on the actual used types if $d$ is a collection. If $d$ is a collection over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_collections}). - \item Translates remaining (slot) default value expression by replacing potential self usages with the compound access. In case that self is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($c_{dd}$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. + \item Translates remaining (slot) default value expression by replacing potential self usages with the compound access. In case that self is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($\deferredDefaultConstraints$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. + \item Translates usual collection compound constraints independent of any default value expression. \TBD{check} + \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression. \TBD{check, also section ref} \end{itemize} -\TBD{Check - why here: Then, usual collection compound constraints as well as internal collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) are collected}. Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $c_v$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $c_d$ or $c_{dd}$ as determined before. +Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $\constraintVariablesConstraints$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $\defaultConstraints$ or $\deferredDefaultConstraints$ as determined before. \begin{algorithm}[H] \SetAlgoLined \KwIn{configuration $cfg$, declaration $d$, variable $v$, access $ca$} - \KwData{constraint $base$, variable mapping $m$, internal constraints $c_i$, attribute constraints $c_a$, constraint variables $c_v$, default (deferred) constraints $c_d$ and $c_{dd}$} - - $c_i \assng c_i \cup translateDerivedDatatypeConstraints(d)$\; - $c_a \assng c_a \cup translateAnnotationDefaults(cfg, d, \undef)$\; - $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng c_d$\; + \KwData{constraint $base$, variable mapping $m$, constraint variables $\constraintVariablesConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$} + + $translateDerivedDatatypeConstraints(d)$\; + $translateAnnotationDefaults(cfg, d, \undef)$\; + $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$\; \uIf{$isCompound(t)$}{ \lIf{$ dflt \neq \undef $}{$t = type(dflt)$} @@ -198,18 +216,21 @@ \uIf{$ isContainer(type(d)) $}{ \ForAll{$u \iterAssng usedTypes(dflt)$}{ - $collectDefaultsCompoundsCollection(d, u)$\; + \MISSING{derived types: coCompoundConstraints, translateCollIntConstraints here?} + $translateDefaultsCompoundsCollection(d, u)$\; } }\ElseIf{$ca \neq \undef$}{ - \lIf{$self \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng c_{dd}$} + \lIf{$self \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} $dflt \assng dflt|_{self=ca}$\; } - } - $c_c \assng c_c \cup \TBD{collectionCompoundConstraints(d, v, \undef)}$\; - \lIf{$isContainer(t)$}{$\TBD{collectionInternalConstraints(d, \undef)}$} + } + $c_c \assng c_c \cup \TBD{collectionCompoundConstraints(d, v, \undef)}$\; + \If{$isContainer(t) \wedge isDerived(contained(t))$}{ + $translateCollectionDerivedDatatypeConstraints(d, \undef)$ + } \If{$ deflt \neq \undef $}{ \uIf{$isConstraint(t)$}{ - \lIf{$ ca == \undef $}{$c_v \assng c_v \cup (\createConstraint{dflt}, v)$} + \lIf{$ ca == \undef $}{$\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup (\createConstraint{dflt}, v)$} }\Else{ - $dfltS \assng dfltS \cup \createDefaultConstraint{\IVML{assign}(\left.\begin{cases}ca, & \text{if } dfltS == c_d \\ d, &\text{else}\end{cases}\right\}, deflt)}$\; + $dfltS \assng dfltS \cup \createDefaultConstraint{\IVML{assign}(\left.\begin{cases}ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}\end{cases}\right\}, deflt)}$\; } } @@ -220,14 +241,28 @@ \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 +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 are stored in the gobal set of derived type constraints $\derivedTypeConstraints$. \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$} - \KwOut{instantiated constraints for derived type $d$} - - $\setWith{\createInternalConstraint{c|_{decl(s)=d}}}{c\in constraints(s) \wedge s\in allBase(type(d))}$\; - \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints, createInternalConstraints}).}\label{algTranslateDerivedDatatypeConstraints} -\end{algorithm} + \KwData{derived type constraints $\derivedTypeConstraints$} + + $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\; + $\derivedTypeConstraints \assng \derivedTypeConstraints \cup \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}$\; + \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} +\end{algorithm} + +The translation of derived datatypes for collections can be done similarly, but must consider the nested values/variables of a collection. As accessor to the collection, Algorithm \ref{algTranslateCollectionDerivedDatatypeConstraints} uses either the declaration $d$ or, if given, the accesor $ca$. In contrast to Algorithm \ref{algTranslateDerivedDatatypeConstraints}, Algorithm \ref{algTranslateCollectionDerivedDatatypeConstraints} introduces an all-quantor and substitutes the specific variable of a derived datatype definition by the actual declaration $d$ to be processed. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{derived type $t$, declaration $d$, compound access $ca$} + \KwData{derived type constraints $\derivedTypeConstraints$} + + $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\; + $\derivedTypeConstraints \assng \derivedTypeConstraints \cup \setWith{\createConstraint{\left.\begin{cases}d, & \text{if } ca = \undef \\ ca, &\text{else}\end{cases}\right\}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}$\; + \caption{Translating constraints for derived collection types (\IVML{translateCollectionDerivedDatatypeConstraints}).}\label{algTranslateCollectionDerivedDatatypeConstraints} +\end{algorithm} + \subsection{Annotation default expressions}\label{sectAnnotationDefaults} @@ -238,13 +273,11 @@ \SetAlgoLined \KwIn{configuration $cfg$, declaration $d$, compound access $ca$} - \KwOut{instantiated constraints for annotations of $v$} + \KwData{attribute constraints $\defaultAnnotationConstraints$} $a \assng annotations(decision(cfg, d))$\; - $\setWith{\createDefaultConstraint{\IVML{assign}(\left.\begin{cases}d.r, & \text{if } ca = \undef \\ ca.r, &\text{else}\end{cases}\right\}, default(r))}}{r\in a}$\; + $\defaultAnnotationConstraints \assng \defaultAnnotationConstraints \cup \setWith{\createDefaultConstraint{\IVML{assign}(\left.\begin{cases}d.r, & \text{if } ca = \undef \\ ca.r, &\text{else}\end{cases}\right\}, default(r))}}{r\in a}$\; \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults} \end{algorithm} - - \subsection{Default expressions} @@ -255,17 +288,15 @@ \subsubsection{Collection default constraints}\label{deflt_collections} -Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algCollectDefaultsCompoundCollection} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested collection). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the collection using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVML{self} substituted by the iterator variable $i$. - -\TBD{What about typedefs/derived?} +Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundCollection} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested collection). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the collection using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVML{self} substituted by the iterator variable $i$. \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$, (specific) type $t$} - \KwData{deferred default constraints $c_{dd}$} + \KwData{deferred default constraints $\deferredDefaultConstraints$} \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{ - $c_{dd} \assng c_{dd} \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(i|\IVML{assign}(i.name(s), default(s)|_{self=i})}$\; + $\deferredDefaultConstraints \assng \deferredDefaultConstraints \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(i|\IVML{assign}(i.name(s), default(s)|_{self=i})}$\; } - \caption{Translates and collects defaults in compound collections (\IVML{collectDefaultsCompoundCollection}).}\label{algCollectDefaultsCompoundCollection} + \caption{Translates and collects defaults in compound collections (\IVML{translateDefaultsCompoundCollection}).}\label{algTranslateDefaultsCompoundCollection} \end{algorithm} @@ -312,4 +343,7 @@ \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.} +\section{Acknowledgements} + +We are grateful to Phani Saripalli for implementing the initial IVML reasoner based on the Jess rules engine. We are also grateful to Roman Sizonenko for implementing and experimenting with the Drools-based IVML reasoner and for realizing the initial SSE IVML reasoner used as basis for the actual version of the reasoner and this documentation. \end{document}