Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 55) +++ /reasoner/reasoner.tex (revision 56) @@ -95,5 +95,5 @@ For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need \emph{sequences}, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates. -We also want to express that a \emph{mapping} from a certain key to a value is recorded, retrieved and used in some algorithms. We simply denote such a map as a set of entries $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. As key-value pairs are unique within a mapping, in particular there is only one mapping for a certain key, using a set of such entries is reasonable. We denote adding an entry to a map by $m \assng m \addMap \set{\mapEntry{k}{v}}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ will return undefined denoted by $\undef$. Iterating over a map means iterating over the entries of a map. +We also want to express that a \emph{mapping} from a certain key to a value is recorded, retrieved and used in some algorithms. We simply denote such a map as a set of entries $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. As key-value pairs are unique within a mapping, in particular there is only one mapping for a certain key, using a set of such entries is reasonable. We denote adding an entry to a map by $m \assng m \addMap \mapEntry{k}{v}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ will return undefined denoted by $\undef$. Iterating over a map means iterating over the entries of a map. In general, we use $\undef$ to denote an \emph{undefined result/value}. If not indicated otherwise, all operations introduced below that are bound to a certain type, e.g., an IVML compound, return $\undef$ if the operation is used with another type, e.g., an IVML basic type. @@ -167,5 +167,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 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}$. +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}$. 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)}$ @@ -418,56 +418,62 @@ \subsection{Translate Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} -Algorithm \ref{algTranslateDeclaration} 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 derived type constraints $\topLevelConstraints$. - \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\otherConstraints$ - \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 \IVMLself{} by the actual declaration as well as all mapped variables from $\problemRecords$ 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 container compounds based on the actual used types if $d$ is a container. If $d$ is a container over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{sectContainerDefaults}). - \item Translates remaining (slot) default value expression by replacing potential \IVMLself{} usages with the compound access. In case that \IVMLself{} 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 container compound constraints independent of any default value expression and stores them into $\otherConstraints$. \TBD{check} - \item Translates container constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\otherConstraints$. \TBD{check, also section ref} -\end{itemize} -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 $\otherConstraints$. 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. +Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and respective variable $v$ through their actual type. Basically, the algorithm considers for the given variable, depending on the actual type, derived type constraints, annotation defaults, compound constraints, container constraints, and constraints of overridden slots leading to a deferred default initialization through the global constraints set $\deferredDefaultConstraints$. + +In more detail, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the actual type $t$ (to be overridden by the type of the default value expression if needed), the default value expression $dflt$, the actual set of default constraints ($\defaultConstraints$ or $\deferredDefaultConstraints$) to be utilized for adding the final constraint and the actual value of self $s$ (for compound types only). Then, if $t$ is a derived data type, constraints are translated and collected through Algorithm \ref{algTranslateDerivedDatatypeConstraints}. In non-incremental mode, i.e., we shall translate default value expressions to assignment constraints, the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDefaults}. Due to potential type interactions, we determine now the actual type through the type of the default value expression if defined. If $t$ is a compound type, we set the value of self $v$ to the actual variable declaration $d$ and execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. Otherwise, if there is a compound accessor, a default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, we determine the target constraint set (deferred or not deferred) and translate the constraint to replace self by the compound accessor. Remaining default constraints are not translated in incremental mode. + +If there is finally a default value expression to be translated, we distinguish whether the actual variable is a constraint variable or another variable. In the first case, we jan cust add the constraint and there is no compound accessor, then we can add default value expression, which is actually a constraint, to the set of other constraints $\otherConstraints$ and register the relevant variables for the new constraint and the causing variable $v$. For all remaining default constraints, we create a value assignment, either for the compound accessor if given or $d$ with a value determined by the default value expression (having self and $\variableMapping$ substituted). \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$, variable $v$, access $ca$} + \KwData{variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental $inc$} + + $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$; $s \assng \undef$\; \label{algTranslateDeclarationDecl} + \lIf{$isDerived(t)$} {$translateDerivedDatatypeConstraints(d, t)$} \label{algTranslateDeclarationDerivedDatatype} + \lIf{$\neg inc$} { + $translateAnnotationDefaults(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault} + } + \lIf{$dflt \neq \undef$}{$t \assng type(d)$} + \uIf{$isCompound(t)$}{ + $s \assng d$\; + $translateCompoundDeclaration(d, v, ca, t)$\; + } \uElseIf{$ isContainer(type(d)) $}{ \label{algTranslateDeclarationHasDefault} + $translateContainerDeclaration(d, v, t)$\; + } \uElseIf{$ca \neq \undef$}{ + \If{$dflt \neq \undef \wedge \neg inc$}{ + \lIf{$\IVMLself{} \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} + $dflt \assng \varSubstitutionSelfVarMapping{dflt}{ca}$ \TBD{double translation, s=ca}\; + } + }\lElseIf{$inc$}{$ dflt \assng \undef $} + \If{$ deflt \neq \undef $}{ + \uIf{$isConstraint(type(d))$}{ + \If{$ ca == \undef $}{ + $add(\otherConstraints, \createConstraint{dflt}, true)$\TBD{Substitution here?}\; + $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{\createConstraint{dflt}}{v}$ + } + }\Else{ + $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, \varSubstitutionSelfVarMapping{dflt}{s})})$\; \label{algTranslateDeclarationTranslateDefault} + } + } + \caption{Translating declaration constraints (\IVML{translateDeclaration}).}\label{algTranslateDeclaration} +\end{algorithm} + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, access $ca$, type $t$} \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$} - $translateDerivedDatatypeConstraints(d)$\; \label{algTranslateDeclarationDerivedDatatype} - \lIf{$\neg inc$} { - $translateAnnotationDefaults(cfg, d, \undef)$ \label{algTranslateDeclarationAnnotationDefault} - } -\MISSING{CHECKING: Here}\; - $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$; $s \assng \undef$\; - \uIf{$isCompound(t)$}{ - \lIf{$ dflt \neq \undef $}{$t = type(dflt)$; $s = \createExpression{v}$} - $translateCompoundDefaults(d, v, ca, t)$\; - %\lIf{$ dflt \neq \undef $}{$ dflt \assng \varSubstitutionSelfVarMapping{deflt}{d}$} - } \uElseIf{$ dflt \neq \undef \wedge \neg inc$}{ \label{algTranslateDeclarationHasDefault} - \uIf{$ isContainer(type(d)) $}{ - $translateDefaultsCompoundsContainer(d);$\; - }\ElseIf{$ca \neq \undef$}{ - \lIf{$\IVMLself{} \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} - $dflt \assng \varSubstitutionSelfVarMapping{dflt}{ca}$\; + \uIf{$ dflt \neq \undef \wedge \neg inc $}{ + \ForAll{$u \iterAssng usedTypes(default(d))$}{ + \MISSING{derived types?} + $translateDefaultsCompoundsContainer(d, u)$\; + } } - } \uElse{$ dflt \assng \undef $\;} $add(\otherConstraints, translateContainerCompoundConstraints(d, v, \undef), true)$\; \If{$isContainer(t) \wedge isDerived(contained(t))$}{ - $translateContainerDerivedDatatypeConstraints(d, \undef)$\; + $translateContainerDerivedDatatypeConstraints(contained(t), d, \undef)$\; } - \If{$ deflt \neq \undef $}{ - \uIf{$isConstraint(t)$}{ - \lIf{$ ca == \undef $}{ - \MISSING{substitution here?}\; - $add(\otherConstraints, \createConstraint{dflt}, true)$\; - $\relevantConstraints \assng \relevantConstraints \cup (\createConstraint{dflt}, v)$} - }\Else{ - $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, \varSubstitutionSelfVarMapping{deflt}{s})})$\; \label{algTranslateDeclarationTranslateDefault} - } - } - \caption{Translating default value expressions to constraints (\IVML{translateDeclaration}).}\label{algTranslateDeclaration} -\end{algorithm} - + \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration} +\end{algorithm} \subsection{Derived types}\label{sectDerivedTypes} @@ -477,8 +483,8 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{declaration $d$} + \KwIn{declaration $d$, type $t$} \KwData{derived type constraints $\topLevelConstraints$} - - $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\; + \TBD{check isDerived(t)}\; + $cs \assng \bigcup_{t \in allBase(t)} constraints(t)$\; $add(\topLevelConstraints, \setWith{\createConstraint{\varSubstitution{c}{decl(c)=d}}}{c\in cs}, true)$\; \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} @@ -504,8 +510,8 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{configuration $cfg$, declaration $d$, compound access $ca$} - \KwData{constraints $\otherConstraints$} - - $a \assng annotations(decision(cfg, d))$\; + \KwIn{declaration $d$, variable $v$, compound access $ca$} + \KwData{configuration $cfg$, constraints $\otherConstraints$} + + $a \assng annotations(v)$\; $add(\otherConstraints, \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}, false)$\; \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults} @@ -549,9 +555,9 @@ \end{align*} % -Algorithm \ref{algTranslateCompoundDefaults} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. - -First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration}. - -Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular 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 constraint variables ($\otherConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound container, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateContainerCompoundConstraints}. +Algorithm \ref{algTranslateCompoundDeclaration} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. + +First, Algorithm \ref{algTranslateCompoundDeclaration} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration}. + +Second, Algorithm \ref{algTranslateCompoundDeclaration} considers all slots, in particular 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 constraint variables ($\otherConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound container, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateContainerCompoundConstraints}. Finally, the algorithm translates all attribute assignments using Algorithm \ref{algTranslateAnnotationAssignments}, all direct compound constraints (substituting \IVMLself{} and registered variables), and translates and collects all eval constraints (\TBD{no self??}). @@ -576,5 +582,7 @@ $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\; } + \If{$isContainer(type(s))$} { $add(\otherConstraints, translateContainerCompoundConstraints(s, v, \variableMapping[s]), true)$\; + } } \If{$\neg inc$} { @@ -586,5 +594,5 @@ $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionVarMapping{c}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; - \caption{Translating annotation defaults (\IVML{translateCompoundDefaults}).}\label{algTranslateCompoundDefaults} + \caption{Translating annotation defaults (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} \end{algorithm} @@ -636,17 +644,6 @@ \subsection{Container default constraints}\label{sectContainerDefaults} -Constraints defined on types that are implicitly instantiated within a container 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{algTranslateDefaultsCompoundContainer} performs this transformation by identifying the actual types used in a container and by deriving all constraints for this container. In turn, it calls Algorithm \ref{algTranslateDefaultsCompoundContainer2}. - -Algorithm \ref{algTranslateDefaultsCompoundContainer2} 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 container). 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 container 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 \IVMLself{} substituted by the iterator variable $i$. - -\begin{algorithm}[H] - \SetAlgoLined - - \ForAll{$u \iterAssng usedTypes(default(d))$}{ - \MISSING{derived types?} - $translateDefaultsCompoundsContainer(d, u)$\; - } - \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer} -\end{algorithm} +Constraints defined on types that are implicitly instantiated within a container 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{algTranslateDefaultsCompoundContainer} 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 container). 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 container 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 \IVMLself{} substituted by the iterator variable $i$. + \begin{algorithm}[H] @@ -658,5 +655,5 @@ } - \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer2} + \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer} \end{algorithm} @@ -669,5 +666,4 @@ \KwOut{resulting constraints $c$} - \If{$isContainer(type(d)$ \TBD{check: move up}} { $c \assng \set$\; $tc \assng contained(type(d))$\; @@ -676,5 +672,4 @@ $c \assng c \cup translateContainerCompoundConstraints(t, tc, d, ca)$\; } - } } \caption{Translating compound constraints from a container (\IVML{translateContainerCompoundConstraints}).}\label{algTranslateContainerCompoundConstraints}