Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 140) +++ /reasoner/reasoner.tex (revision 141) @@ -165,5 +165,5 @@ While variable declarations as introduced in Section \ref{sectNotationVarDecls} as well as types as introduced below allow defining (a meta-model of) configuration options, \emph{configuration variables} are part of the configuration of a specific product and hold the actual configured value for a variable declaration. A configuration variable $v$ (representing a decision, inspired by decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}) is defined through a variable declaration $d$, but for a single variable declaration $d$ in a model, multiple configuration variables can exist in different configurations. -Let $v$ be a (top-level) configuration variable of variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$ and $parent(v)=cfg$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, for any other IVML element/type $false$. +Let $v$ be a configuration variable with declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$ and $parent(v)=cfg$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, for any other IVML element/type $false$. $value(v)$ denotes the actual value of $v$ and $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$, in particular if $type(v)$ is a refined type through inheritance (cf.~\cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy). We will detail some relevant properties of values below in Section \ref{sectNotationValues}. @@ -213,5 +213,5 @@ In IVML, an \emph{annotation assignment} is a kind of block, which allows assigning annotation values to the variables defined within the block, i.e., the specified annotation values shall be applied to all contained variable declarations. The declared variables shall behave as if they are defined in the innermost containing element that is not an annotation assignment. For convenience, also constraints relating to the contained variable declarations can be stated within an annotation assignment. To indicate orthogonal combinations of annotation assignments in IVML models, annotation assignments can be nested referring to different annotations. For convenience, only the innermost annotation value assignment shall be applied in nested assignment blocks in order to avoid accidental multiple assignments to the same annotation within the same project scope. -$assignments(p)$ is the set of (potentially nested) annotation assignments of project $p$. If $a\in assignments(p)$ then $decls(a)$ returns the variables declared in $a$ and $constraints(a)$ the constraints declared within $a$. Further, $assignments(a)$ returns the annotation assignments nested within $a$. All three results may be empty. Further, $assignmentData(a)$ provides access to the affected annotations and the intended values values, i.e., if $f \in assignmentData(a)$ then $name(f)$ is the name of the affected attribute and $default(f)$ the intended default value expression that shall be assigned to all attributes with name $name(f)$ for all declarations within the containing assignment-block. $isAnnotationAssignment(a)=true$ and for an arbitrary model element $e$, $isAnnotationAssignment(e)$ returns whether $e$ is an assignment block. +$assignments(p)$ is the set of (potentially nested) annotation assignments of project $p$. If $a\in assignments(p)$ then $decls(a)$ returns the variables declared in $a$ and $constraints(a)$ the constraints declared within $a$. Further, $assignments(a)$ returns the annotation assignments nested within $a$. All three results may be empty. Further, $assignmentData(a)$ provides access to the affected annotations and the intended values values, i.e., if $f \in assignmentData(a)$ then $name(f)$ is the name of the affected attribute and $default(f)$ the intended default value expression that shall be assigned to all attributes with name $name(f)$ for all declarations within the containing assignment-block. $isAnnotationAssng(a)=true$ and for an arbitrary model element $e$, $isAnnotationAssng(e)$ returns whether $e$ is an assignment block. Using these functions, $allAssignmentConstraints(a)$ determines all assignment constraints within an assignment $a$ considering potentially further nested annotation assignments: @@ -239,5 +239,5 @@ 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 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. +Technically, a constraint is an expression, which may consist of several (sub-)expressions, such as constants, variable uses, or function calls. An expression $e$ evaluates to a value of some IVML type, i.e., $type(e)$ returns the static value type of an expression. In particular, let $c$ be a constraint then $type(c) = \IVML{Boolean}$. Expressions are used to determine the default value of variables. Let $v$ be a variable then we denote by $e(v)$ that expression $e$ is using variable $v$ and by $var(e)$ the set of variables used in $e$. Moreover, if $c$ is an assignment constraint representing $x = y$, the $rightSide(c) = y$ returns the right side expression $y$, else $\undef$. If $e$ represents a constant, $const(e)$ returns the constant value, else $\undef$. 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. @@ -334,5 +334,5 @@ \end{equation*} % -\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})}$. +\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})}$. Let $ce$ be an accessor expression, then $compound(e)$ returns the part referring to the compound if $e$ is a compound accessor, $\undef$ else. 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. @@ -411,4 +411,13 @@ %----------------------------------------------------------------------------------------------------------------- + +% trim={ } +\begin{figure}[h] +\center +%\frame{...} +\includegraphics[scale=0.48,trim={5.1cm 6.2cm 26.5cm 0.3cm},clip]{figures/structure.pdf} +\caption{Structuring blocks, algorithms and sections.} +\label{figStructure} +\end{figure} \section{Reasoning algorithm}\label{sectReasoning} @@ -428,16 +437,11 @@ This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the reasoner data structures in Section \ref{sectDataStructures}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, and the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation}. The algorithms for constraint translation will be discussed in detailed in Section \ref{sectTranslation} and the algorithms for re-scheduling constraints in Section \ref{sectTopLevelConstraintsRescheduling}. -% trim={ } -\begin{figure}[ht] -\center -%\frame{...} -\includegraphics[scale=0.48,trim={5.1cm 6.2cm 26.5cm 0.3cm},clip]{figures/structure.pdf} -\caption{Structuring blocks, algorithms and sections.} -\label{figStructure} -\end{figure} - \subsection{Main Reasoning Loop}\label{sectTopLevelMainReasoningLoop} The main reasoning loop implements the overall control for the IVML reasoning process. The reasoning loop receives a configuration $cfg$ as input and utilizes various global data structures. + +First, Algorithm \ref{algMainLoop} sets up the global configuration variable $cfg$ and the expression evaluator\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These details are omitted here.} in lines \ref{algMainLoopSetupVar}-\ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. In line \ref{algMainLoopStartTime} it stores the start time to terminate potentially endless loops induced by ping-pong assignments among constraints within a given maximum time. The remainder of the algorithm is separated into two parts, the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part. + +As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per declaration ($base_{\relevantConstraintsPerDeclaration}$, a mapping of declarations to using constraints) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$, bidirectional mapping between constraint values assigned to configured decision variables). Then, the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, which is determined by the top-level IVML project making up $cfg$ and a cycle-free traversal of the imports of the top-level project. $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns the processing sequence of all projects involved in $cfg$, i.e., the imported projects sorted in ascending manner according to their number of import dependencies. The loop processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user requests a stop of the reasoning (global flag $stop$). \begin{algorithm}[H] @@ -478,7 +482,4 @@ \end{algorithm} -First, Algorithm \ref{algMainLoop} sets up the global configuration variable $cfg$ and the expression evaluator\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These details are omitted here.} in lines \ref{algMainLoopSetupVar}-\ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. In line \ref{algMainLoopStartTime} it stores the start time to terminate potentially endless loops induced by ping-pong assignments among constraints within a given maximum time. The remainder of the algorithm is separated into two parts, the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part. - -As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per declaration ($base_{\relevantConstraintsPerDeclaration}$, a mapping of declarations to using constraints) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$, bidirectional mapping between constraint values assigned to configured decision variables). Then, the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, which is determined by the top-level IVML project making up $cfg$ and a cycle-free traversal of the imports of the top-level project. $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns the processing sequence of all projects involved in $cfg$, i.e., the imported projects sorted in ascending manner according to their number of import dependencies. The loop processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user requests a stop of the reasoning (global flag $stop$). For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ and populates the constraint base as a side effect of the constraint translation called in line \ref{algMainLoopTranslate} (detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled through $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerDeclaration}$ and $base_{\relevantConstraintVariables}$. Then the algorithm performs a forward-chaining evaluation of the constraint base in line \ref{algMainLoopEvaluate} (explained in Section \ref{sectTopLevelConstraintsEvaluation}). If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. @@ -605,7 +606,7 @@ %$\usedVariables \assng \emptySet$\; \label{algEvalLoopClear} $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} - $\problemRecords analyzeEvaluationResult(\problemRecords, evaluate(e, c))$\; \label{algEvalLoopAssngEval} + $analyzeEvaluationResult(\problemRecords, evaluate(e, c))$\; \label{algEvalLoopAssngEval} \If{$constraintFulfilled(e) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} - $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cap \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; \MISSING{mapping to set!} + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cap \setWith{\mapEntry{v}{c}}{v\in var(c)}$\; }\label{algEvalLoopClearEnd} $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} @@ -654,59 +655,69 @@ } -Let $v$ be a given variable with default value expression $deflt$, then the first transformation pattern above turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression is required. In the transformation pattern, we indicate this by a generic access expression ($ca.$) on the right side, which is empty for top-level variables. The second pattern refers to annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables allowing an an orthogonal configuration dimension for 'ordinary' variables. Thus, an annotation is translated similarly to an ordinary variable, but requires in addition a qualification through the respective ordinary variable. - -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$. - - -For a $v$ of compound or container type, Algorithm \ref{algTranslateDeclaration} dispatches to the other algorithms constituting the reasoner as we will discus in the following sections. Then the patterns can also be applied for initializing compound slots. As a consequence, Algorithm \ref{algTranslateDeclaration} may be called recursively with an incrementally constructed access expression $ca$ that is prefixed before the right side, e.g., let $c$ be the top-level variable of compound type, then $ca=c$ and the pattern $\patternDerivation{v}{ca.v = deflt}$ becomes $c.v=deflt$. In particular in such recursive calls, occurrences of other variables in $deflt$ recorded in $\variableMapping$, e.g., other slots as well as \IVML{self} denoting the actual compound must be substituted properly, i.e., the result is at least $c.v=\varSubstitution{deflt}{\IVML{self}, \variableMapping}$. - -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 incremental mode, we can skip all default value expressions as they are already assigned except for constraint variables that must be taken over into the constraint base (line \ref{algTranslateDeclarationDefltUndef}). In non-incremental mode, we translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDeclarations} (line \ref{algTranslateDeclarationAnnotationDefault}). Due to potential type interferences with derived types, we determine then the actual type through the type of the default value expression if defined. %parasplit +Let $v$ be a variable with default value expression $deflt$. The first transformation pattern above turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression is required in the resulting constraint. In the transformation pattern, we indicate this by a generic access expression ($ca.$) on the right side, which is empty for top-level variables. The second pattern refers to annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables represent an an orthogonal configuration dimension on top of 'ordinary' variables. Thus, an annotation $a$ is translated similarly to an ordinary variable, but requires in addition a qualification through the respective ordinary variable $v$. + +Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable $v$ (and its declaration $d$) based on the actual type of $v$. As complex types such as compounds may occur, Algorithm \ref{algTranslateDeclaration} delegates such types to more specialized algorithms, which then use Algorithm \ref{algTranslateDeclaration} recursively for nested variable declarations (with a respective access expression $ca$ and an adequately prepared variable mapping $\variableMapping$). These specialized algorithms will be discussed in the following sections. Assignment constraints created in Algorithm \ref{algTranslateDeclaration} are stored either in the global set for default constraints $\defaultConstraints$ or the set for deferred default constraints $\deferredDefaultConstraints$. \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$, variable $v$, access $ca$} - \KwData{variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, incremental $inc$} - - $t \assng type(d)$; $dflt \assng default(d)$; $f \assng \undef$; $c_m\assng NONE$\; \label{algTranslateDeclarationDecl} - $translateDerivedDatatypeConstraints(d, t)$\; \label{algTranslateDeclarationDerivedDatatype} - \uIf{$inc$} { - \lIf{$\neg isConstraint(type(d))$}{$dflt \assng \undef$} \label{algTranslateDeclarationDefltUndef} - }\uElse{ - $translateAnnotationDeclarations(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault} - } - %\lIf{$value(v) \neq \undef$}{$t \assng type(value(v))$} - \lIf{$dflt \neq \undef$}{$t \assng type(d)$} - \lIf{$v \neq \undef \wedge value(v) \neq \undef$}{$t \assng type(value(v))$} + \KwData{variable mapping $\variableMapping$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, incremental flag $inc$} + + $e_d \assng \closedCases{\undef & \text{if } inc \\ default(d) & \text{else}}$; $f \assng \undef$; $c_m\assng NONE$\; \label{algTranslateDeclarationDecl}\label{algTranslateDeclarationInitStart} + $t \assng \closedCases{type(value(v)) & \text{if } v \neq \undef \wedge\text{ } value(v) \neq \undef \\ type(e_d) & \text{if } e_d \neq \undef \\ type(d) & \text{else}}$\; \label{algTranslateDeclarationRefinedType} \uIf{$isCompound(t)$}{ $f \assng d$\; \label{algTranslateDeclarationTranslateSelf1} $c_m \assng translateCompoundDeclaration(d, v, ca, t, REGISTER)$\; \label{algTranslateDeclarationRegisterCompound} - } \uElseIf{$dflt \neq \undef \wedge \neg inc$}{ - \lIf{$ca \neq \undef$}{$s \assng ca$} \label{algTranslateDeclarationTranslateInCompound} - }\lElseIf{$inc \wedge \neg isContainer(t)$}{$ dflt \assng \undef $} - \If{$ deflt \neq \undef \wedge \neg(isAttribute(d) \wedge isAnnotationAssignment(parent(d)))$}{ + }\label{algTranslateDeclarationInitEnd} + + \If{$e_d \neq \undef \wedge \neg(isAttribute(d) \wedge isAnnotationAssng(parent(d)))$}{ \label{algTranslateDeclarationDefaultStart} + $e_f \assng compound(ca)$\; \label{algTranslateDeclarationTranslateInCompound} \uIf{$isConstraint(type(d))$}{ \label{algTranslateDeclarationTranslateConstraintDefaultStart} - $createConstraintVariableConstraint(dflt, s, v)$\; \label{algTranslateDeclarationConstraintVariableConstraint} + $createConstraintVariableConstraint(e_d, e_f, v)$\; \label{algTranslateDeclarationConstraintVariableConstraint} }\label{algTranslateDeclarationTranslateConstraintDefaultEnd} - \uIf{$isAnnotation(v)$}{ + \uIf{$isAnnotation(v)$}{\label{algTranslateDeclarationCreateACStart} $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 } f = ca \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess} \label{algTranslateDeclarationTranslateSelf2} - } - \lIf{$\IVMLself{} \in dflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$}\lElse{$dfltS \assng \defaultConstraints$} \label{algTranslateDeclarationTranslateSelf3} - $add(dfltS, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, dflt)}{f}}, true, v)$\; \label{algTranslateDeclarationTranslateDefault} - } + $ac \assng \closedCases{ca, & \text{if } e_f \neq \undef \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess} \label{algTranslateDeclarationTranslateSelf2} + }\label{algTranslateDeclarationCreateACEnd} + \leIf{$\IVMLself{} \in var(e_d) \vee isOverridenSlot(d)$}{$c_{e_d} \assng \deferredDefaultConstraints$}{$c_{e_d} \assng \defaultConstraints$} \label{algTranslateDeclarationTranslateSelf3} + $add(c_{e_d}, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, e_d)}{f}}, true, v)$\; \label{algTranslateDeclarationTranslateDefault} + }\label{algTranslateDeclarationDefaultEnd} + + \lIf{$\neg inc$} {$translateAnnotationDeclarations(d, v, \undef)$}\label{algTranslateDeclarationAnnotationDefault}\label{algTranslateDeclarationComplexStart} + $translateDerivedDatatypeConstraints(d, type(d))$\; \label{algTranslateDeclarationDerivedDatatype} \uIf{$isCompound(t)$}{ $translateCompoundDeclaration(d, v, ca, t, c_m)$\; \label{algTranslateDeclarationTranslateCompound} } \uElseIf{$ isContainer(t) $}{ \label{algTranslateDeclarationHasDefault} $translateContainerDeclaration(d, v, ca, t)$\; \label{algTranslateDeclarationTranslateContainer} - } + }\label{algTranslateDeclarationComplexEnd} \caption{Translating declarations (\IVML{translateDeclaration}).}\label{algTranslateDeclaration} \end{algorithm} -If $t$ is a compound type, we set the value of self $v$ to the actual variable declaration $d$. 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 (non-container) 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. - -Then we process the default value for the actual declaration. In particular for a correct compound initialization, which may mix default and provided values, it is important that the potentially overriding value expression of the variable is scheduled to the constraint base before the default values of the compounds slots. If there is a default value and $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block), we have to check whether the actual variable is a constraint variable or an usual variable. If the variable is a constraint variable, we apply Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}) to create an evaluatable constraint from $dflt$. In any 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$. - -Finally, if $t$ is a compound type, we execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. +Algorithm \ref{algTranslateDeclaration} consists of three parts: identifying the actual type and preparing the variable mapping (lines \ref{algTranslateDeclarationInitStart}-\ref{algTranslateDeclarationInitEnd}), translating the default value expression (lines \ref{algTranslateDeclarationDefaultStart}-\ref{algTranslateDeclarationDefaultEnd}) and translating complex types (lines \ref{algTranslateDeclarationComplexStart}-\ref{algTranslateDeclarationComplexEnd}). + +In the first part, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the default value expression $e_d$ (ignored in incremental mode), the actual value of self $f$ (for compound types only, overridden in line \ref{algTranslateDeclarationTranslateSelf1}) and the compound translation mode ($c_m$, overridden in line \ref{algTranslateDeclarationRegisterCompound} for use in line \ref{algTranslateDeclarationTranslateCompound}). In line \ref{algTranslateDeclarationRefinedType}, the actual type of the variable is determined, either based on the declaration, the default value expression or the actual value if defined. If $t$ is a compound type, we set in line \ref{algTranslateDeclarationTranslateSelf1} the value of self $v$ to the actual variable declaration $d$ and create the variable mapping for all slots in line \ref{algTranslateDeclarationRegisterCompound} by calling Algorithm \ref{algTranslateCompoundDeclaration}. Typically, this creates a new context frame in the variable mapping $\variableMapping$, which must be correctly cleaned up at the end of Algorithm \ref{algTranslateDeclaration}. We indicate this by the compound mode $c_m$, which is adjusted here and considered in the translation call in line \ref{algTranslateDeclarationTranslateCompound}. + +A remaining default value expression $e_d$ is turned into an assignment constraint if $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block). If the $v$ variable is a constraint variable, we also have to add $e_d$ to the constraint base. This is done by calling Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). Then, we turn the default value expression into an assignment expression. However, the creation of the sub-expression $ac$ representing the variable $v$ technically depends on whether $d$ is a (nested) annotation or 'ordinary' variable (lines \ref{algTranslateDeclarationCreateACStart}-\ref{algTranslateDeclarationCreateACEnd}). Further, we must determine the constraint set for adding the assignment constraint (line \ref{algTranslateDeclarationTranslateSelf3}): We add the constraint to $\deferredDefaultConstraints$ if the assignment may override a previous value assignment through a complex value. This is (potentially) the case if \IVML{self} is used in $e_d$ or if $d$ is an overridden slot that may be overriden accidentally by a complex compound value. Else, we add the constraint to the set of default constraints $\defaultConstraints$. Ultimately, we create an expression assigning $e_d$ to $ac$, substitute \IVML{self} and the actual variable mapping in this assignment expression, turn the result into a default constraint and add it to the respective constraint set in line \ref{algTranslateDeclarationTranslateDefault}. + +Akin to default value expressions, orthogonal annotation declarations are only translated in full (non-incremental) reasoning mode in line \ref{algTranslateDeclarationAnnotationDefault} using Algorithm \ref{algTranslateAnnotationDeclarations}. +Finally, we translate constraints induced by the actual type of $v$. This can happen through derived, compound or container types. If $t$ is a derived data type, type-defined constraints are translated by Algorithm \ref{algTranslateDerivedDatatypeConstraints} in line \ref{algTranslateDeclarationDerivedDatatype}. If $t$ is a compound type, we call Algorithm \ref{algTranslateCompoundDeclaration} with the actual compound mode $c_m$ in line \ref{algTranslateDeclarationTranslateCompound}. If $t$ is a container type, we call Algorithm \ref{algTranslateContainerDeclaration} in line \ref{algTranslateDeclarationTranslateContainer}. + + +%set in line \ref{algTranslateDeclarationTranslateSelf1} the value of self $v$ to the actual variable declaration $d$ and create the variable mapping for all slots in line \ref{algTranslateDeclarationRegisterCompound}. As for container types, the actual translation happens at the end of Algorithm \ref{algTranslateDeclaration} as expressions for slots or elements may refer to each other. + + +%the reasoner is not operating incremental mode as there no default value assignments are needed. Then we process the default value for the actual declaration. In particular for a correct compound initialization, which may mix default and provided values, it is important that the potentially overriding value expression of the variable is scheduled to the constraint base before the default values of the compounds slots. If there is a default value and $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block), we have to check whether the actual variable is a constraint variable or an usual variable. + +. + + + + + +%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. + + +%Finally, if $t$ is a compound type, we execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. \subsection{Derived types}\label{sectDerivedTypes}