Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 66) +++ /reasoner/reasoner.tex (revision 67) @@ -177,5 +177,5 @@ \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, then $decision(v, s)$ returns the variable related to slot $s$ in the configuration $v$ is a member of. For convenience, we introduce +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 @@ -215,5 +215,5 @@ $$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. Similar functions apply to access the constraints, the variable declarations and the assignment data. +Akin to projects, $assignments(t)$ is defined for a compound type $t$ and returns the annotation assignment blocks. Similar functions apply to access the constraints, the variable declarations and the assignment data. \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})}$. @@ -429,5 +429,5 @@ 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 translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDefaults}. Due to potential type interferences with derived types, we determine then 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 default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. Remaining default constraints are taken over as defined as long as the reasoner is not operating incremental mode as there no default value assignments are needed. +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 translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDeclarations}. Due to potential type interferences with derived types, we determine then 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 default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. Remaining default constraints are taken over as defined as long as the reasoner is not operating incremental mode as there no default value assignments are needed. 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$. @@ -443,5 +443,5 @@ \lIf{$isDerived(t)$} {$translateDerivedDatatypeConstraints(d, t)$} \label{algTranslateDeclarationDerivedDatatype} \lIf{$\neg inc$} { - $translateAnnotationDefaults(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault} + $translateAnnotationDeclarations(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault} } \lIf{$dflt \neq \undef$}{$t \assng type(d)$} @@ -459,7 +459,7 @@ }\Else{ \uIf{$isAnnotation(v)$}{ - $ac\assng \closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}$\; + $ac\assng \closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}$\;\label{algTranslateDeclarationTranslateAnnotationAccess} }\uElse{ - $ac \assng \closedCases{ca, & \text{if } s = ca \\ d, &\text{else}}$\; + $ac \assng \closedCases{ca, & \text{if } s = ca \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess} } \lIf{$\IVMLself{} \in dflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$}\lElse{$dfltS \assng \defaultConstraints$} @@ -490,28 +490,4 @@ \end{algorithm} - -\subsection{Annotation default expressions}\label{sectAnnotationDefaults} - -In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those ortogonal variables, the reasoner must create constraints to perform the evaluation and assignment of the default values before all other constraints are considered for reasoning. - -Algorithm \ref{algTranslateAnnotationDefaults} receives the declaration of the actual variable and a potential compound access expression $ca$ to $d$ if the algorithm is called for slots of a compound value. For all annotations of $v$ (as for $v$ here all inherited annotations are available), the algorithm creates the respective constraints through calling Algorithm \ref{algTranslateDeclaration}. - -%constraints that assign the annotation $a$ (accessed either directly through $d$ or, if given, through $ca$) the value of the default value expression of $a$ and substitutes variables in $\variableMapping$. The created constraints are either added to the set of default constraints $\defaultConstraints$. - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$} - \KwData{constraints $\otherConstraints$} - - %$s\assng \undef$\; - %\uIf{$isCompound(t)$}{$s \assng d$\;} \uElseIf{$ca \neq \undef$}{$s \assng ca$} - \ForEach{$a\in annotations(v)$}{ - $translateDeclaration(decl(a), a, ca)$\; - %$c\assng \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}, default(a))}{s}}$\; - %\uIf{$\IVMLself{} \in dflt$}{$dfltS \assng \deferredDefaultConstraints$}\uElse{$dfltS \assng \defaultConstraints$} - %$add(dfltS, c, false)$\; - } - \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults} -\end{algorithm} @@ -570,6 +546,6 @@ $\variableMapping \assng \variableMapping \addMap \set{\mapEntry{s}{x}}$\; } - \ForAll{s \iterAssng slots(v)} { %actual slots - $translateDeclaration(s, decision(v, s), c)$\; + \ForAll{s \iterAssng slots(v) \TBD{hint: contains vars from assignment block defs!}} { %actual slots + $translateDeclaration(s, decision(v, s), c)$\; \label{algTranslateCompoundDeclarationTranslateSlots} } \ForAll{s \iterAssng slots(v)} { %actual slots @@ -583,5 +559,5 @@ \If{$\neg inc$} { \ForAll{$a \iterAssng assignments(t)$}{ - $translateAnnotationAssignments(a, \undef, ca)$\; + $translateAnnotationAssignments(a, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments} } } @@ -589,51 +565,6 @@ $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionVarMapping{c}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; - \caption{Translating annotation defaults (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} -\end{algorithm} - -We translate annotation assignments in two steps, the translation of an individual assignment as well as the translation of an assignment block (in Algorithm \ref{algTranslateAnnotationAssignments}). The translation of a single assignment from an assignment data $a$ leads to the creation of an assignment constraint as shown below: - -\begin{align*} - translate&AnnotationAssignment(a, d, ca) = \createConstraint{\IVML{assign}(\\ - &\IVMLMeta{ann}(\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}, annotation(d, name(a))), \\ - & default(a))} -\end{align*} - -If a compound accessor $ca$ is given, it takes precedence and the annotation is accessed through $ca$ and the respective annotation defined for the given variable declaration $d$ through ($annotation(d, name(a))$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$ (\TBD{are variables or declarations mapped}), $d$ is taken as accessor, else the actual accessor in $\variableMapping$. The accessor is used as the left side of an IVML assignment, the right side (value) is made up of the default value expression given by the assignment data $a$. - -Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it creates the variable mapping. When the mapping is complete, it performs the transformation defined above and collects the created constraints in $\otherConstraints$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{assignment block $a$, effective assignment data $ea$, compound access $ca$} - \KwData{constraints $\otherConstraints$} - - $ea \assng ea \cup assignmentData(a)$\; - \ForAll{$e \iterAssng ea$}{ - \ForAll{$d \iterAssng slots(a)$} { - $add(\otherConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false)$\; - \If{$isCompound(type(d))$} { - \ForAll{$s \iterAssng slots(d)$} { - $c \assng \IVMLMeta{acc}(\closedCases{d, & \text{if } ca = \undef\\ ca, &\text{else}}, s)$\; - $\variableMapping \assng \variableMapping \addMap \mapEntry{s}{c}$\; - } - \ForAll{$s \iterAssng slots(d)$} { - $b \assng translateAnnotationAssignment(e, s, c)$\; - $add(\otherConstraints, \set{b})$\; - } - } - } - } - - \ForAll{$b \iterAssng assignments(a)$} { - $translateAnnotationAssignments(b, ea, ca)$\; - } - - \caption{Translating attribute assignments(\IVML{translateAnnotationAssignments}).}\label{algTranslateAnnotationAssignments} -\end{algorithm} - -\TBD{check whether $c_c$ sets are filled incrementally or only at one position (add vs. assign); use $d_?$ as notation for default constraint sets?; are only default constraints translated above or also other constraints (mixed) - can we then join the translations? Can we change the translation sequence in a way that the constraint basis is sufficient (avoiding the different constraint sets)?} - - + \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} +\end{algorithm} \subsection{Container default constraints}\label{sectContainerDefaults} @@ -710,4 +641,61 @@ \end{algorithm} + +\subsection{Annotations}\label{sectAnnotationDefaults} + +In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those ortogonal variables, the reasoner must create constraints to perform the evaluation and assignment of the default values before all other constraints are considered for reasoning. Moreover, we must translate assignment blocks, i.e., blocks assigning specific values to all variables declared within that block. In this section, we discuss first the translation of annotations, then the translation of annotation blocks. + +Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration of the actual variable and a potential compound access expression $ca$ to $d$ if the algorithm is called for slots of a compound value. For all annotations of $v$ (as for $v$ here all inherited annotations are available), the algorithm creates the respective constraints through calling Algorithm \ref{algTranslateDeclaration}. Plase note that no specific variable accessors are handled for such top-level annotation assignments through a specific constraint syntax tree node, which is created through \IVMLMeta{acc()} in Algorithm \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateAnnotationAccess}. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, compound access $ca$} + \KwData{constraints $\otherConstraints$} + + \ForEach{$a\in annotations(v)$}{ + $translateDeclaration(decl(a), a, ca)$\; + } + \caption{Translating annotation defaults (\IVML{translateAnnotationDeclarations}).}\label{algTranslateAnnotationDeclarations} +\end{algorithm} + +We turn now to the translation of annotation assignment blocks. In IVML, an assignment block is used on top-level or within compounds to declare compound slots with an implicit assignment of a value to each delcared annotation. Further, assignment blocks can be nested and the assignments defined for the outer blocks must be applied also to the inner blocks. + +The translation of assignment blocks on top-level is triggered by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. the translation of assignment blocks within compounds by Algorithm \ref{algTranslateCompoundDeclaration} in line \ref{algTranslateCompoundDeclarationCompoundAssignments} (there mapping all variable declarations in assignment blocks to $\variableMapping$ in line \ref{algTranslateCompoundDeclarationTranslateSlots}). In both cases, Algorithm \ref{algTranslateAnnotationAssignments} is called. Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the set of effective assignments data $ea$ that is relevant for the actual assignment block $a$ (initially $ea=\emptySet$ for a top-level assignment block). Then, for all assignment data and all declared slots, the algorithm creates the variable mapping entries for all assignments, in particular considering whether we are in a compound $ca \neq \undef$ or on top-level. When the mapping is created, the algorithm performs the transformation of each individual assignment and collects the created constraints in $\otherConstraints$. If the type \TBD{this is the static type} of the slot is a compound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{assignment block $a$, effective assignment data $ea$, compound access $ca$} + \KwData{constraints $\otherConstraints$} + + $ea \assng ea \cup assignmentData(a)$\; + \ForAll{$e \iterAssng ea$}{ + \ForAll{$d \iterAssng slots(a)$} { + $add(\otherConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false)$\; + \If{$isCompound(type(d))$} { + \ForAll{$s \iterAssng slots(d)$} { + $c \assng \IVMLMeta{acc}(\closedCases{d, & \text{if } ca = \undef\\ ca, &\text{else}}, s)$\; + $\variableMapping \assng \variableMapping \addMap \mapEntry{s}{c}$\; + } + \ForAll{$s \iterAssng slots(d)$} { + $add(\otherConstraints, translateAnnotationAssignment(e, s, \variableMapping[s]))$\; + } + } + } + } + + \ForAll{$b \iterAssng assignments(a)$} { + $translateAnnotationAssignments(b, ea, ca)$\; + } + + \caption{Translating attribute assignments (\IVML{translateAnnotationAssignments}).}\label{algTranslateAnnotationAssignments} +\end{algorithm} + +Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data. The translation of a single assignment from an assignment data $a$ leads to the creation of an assignment constraint as shown below. If a compound accessor $ca$ is given, the annotation is accessed through $ca$ and the respective annotation defined for the given variable declaration $d$ through ($annotation(d, name(a))$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$, $d$ is taken as accessor, else the actual accessor in $\variableMapping$. The accessor is used as the left side of an IVML assignment, the right side (value) is made up of the default value expression given by the assignment data $a$. + +\begin{align*} + translate&AnnotationAssignment(a, d, ca) = \\ + \createConstraint{\IVML{assign}&(\IVMLMeta{ann}(\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}, \\ + &annotation(d, name(a))), \varSubstitutionSelfVarMapping{default(a)}{ca})} +\end{align*} \subsection{Constraint variables}\label{sectConstraintVariables}