Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 155) +++ /reasoner/consTranslation.tex (revision 156) @@ -22,5 +22,5 @@ } -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 $access(e)$ on the right side, which returns the given expression $e$ if $e$ is an access to a top-level variable and prefixes $e$ appropriately if $e$ expresses an access to a nested variable. 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$. +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 $access(e)$ on the right side, which returns the given expression $e$ if $e$ is an access to a top-level variable and prefixes $e$ appropriately if $e$ expresses an access to a nested variable. 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$. We will defer annotations to Section \ref{sectAnnotationDefaults} and develop here generic functionality for the instantiation of default values, which can then be used by the translation of annotations. 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$. @@ -332,5 +332,4 @@ $registerCompoundMapping(t, l, d)$\; \label{algTranslateCompoundContainerMapping} -% $translateCompoundContent(l, \undef, t, \closedCases{\undef, & \text{if } ca = \undef\\l & \text{else}})$\; \label{algTranslateCompoundContainerContent} $translateCompoundContent(l, \undef, t, l)$\; \label{algTranslateCompoundContainerContent} $popContext()$\; \label{algTranslateCompoundContainerPopContext} @@ -378,30 +377,30 @@ \subsection{Annotations}\label{sectAnnotationDefaults} -In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those orthogonal variables, the reasoner must create constraints to perform the evaluation and assignment of the default values before all other constraints are considered for reasoning. It is important to recall that IVML annotations are not recursive~\cite{IVML-LS}, although the reasoner algorithms could support this. 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. - -The first transformation pattern for the direct translation of annotations is the second pattern from Section \ref{sectTranslationDeclarationTypesDefaults}. More specifically, Algorithm \ref{algTranslateDeclaration} from \ref{sectTranslationDeclarationTypesDefaults} calls the algorithms in this section, which in turn call Algorithm \ref{algTranslateDeclaration}, i.e., the algorithms here prepare the application of Algorithm \ref{algTranslateDeclaration} by composing specific accessor expressions. The second pattern relates to annotation blocks, i.e., specific assignment constraints (accessor expression $ca$ is determined by the top-level or compound context of the annotation block) is created for the variables declared in the assignment block for values mentioned in the assignment data (clause). It is important to note that annotation blocks may be nested in order to indicate orthogonal annotations, i.e., the constraint translation must take this nesting and the respective precedence of the assignment data due to their nesting into account. +IVML annotations are orthogonal typed variables that can be attached to a variable. However, annotations cannot be further annotated~\cite{IVML-LS}. Reasoning must consider two cases, namely the creation of assignment constraints for annotation default values (not directly handled by Algorithm \ref{algTranslateDeclaration}) and the translation of annotation assignments (except for nested constraints handled for top-level by Algorithms \ref{algTranslateConstraints} line \ref{algTranslateConstraintsTopLevelAnnotationConstraints} and for compounds by Algorithm \ref{algTranslateCompoundContent}, line \ref{algTranslateCompoundDeclarationAll}). The related transformation patterns are: \grayPara{ \begin{gather*} - \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{ca.v.a = deflt}\\ - \patternDerivation{\IVML{assign (} a = deflt \IVML{) to \{} T v \IVML{ assign} \ldots \IVML{\}}}{ca.v.a = deflt \ldots} + \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{access(v.a) = deflt}\\ + \patternDerivation{\IVML{assign (} a = deflt \IVML{) to \{} T~v\IVML{;} \IVML{ assign} \ldots \IVML{\}}}{access(v.a) = deflt \ldots}\\ \end{gather*} } +The first transformation pattern for annotation default value expressions was already introduced in Section \ref{sectTranslationDeclarationTypesDefaults}, but deferred to this section. There, Algorithm \ref{algTranslateDeclaration} implements the generic instantiation of default value expressions and calls for the currently processed variable $v$ the algorithms in this section, which in turn call Algorithm \ref{algTranslateDeclaration} for the annotations of $v$ with annotation-specific accessor expressions. The second pattern targets annotation assignments. An annotation assignment is syntactic sugar for assigning the same annotation value (usually differs from the default value of the annotation declaration) at once to a set of decision variables. Annotation assignments can be nested to indicate orthogonal sets of variables that are annotated with the same (combination of multiple annotations and their) values. To avoid accidental re-assignments, only the innermost value(s) shall ultimatly be assigned to the listed variables and annotations~\cite{IVML-LS}. + \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$, variable $v$, compound access $ca$} - \KwData{constraints $\otherConstraints$} - - $ca\assng \closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}$\;\label{algTranslateAnnotationDeclarationsCa} + \KwData{variable mapping $\variableMapping$} + + $ca\assng \closedCases{\createExpression{d}, & \text{if } ca = \undef \\ ca, &\text{else}}$\;\label{algTranslateAnnotationDeclarationsCa} \uIf{$v \neq \undef$}{\label{algTranslateAnnotationDeclarationsTranslateVStart} \ForEach{$a\in annotations(v)$}{ - $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } qualifyAnnotation(v, a, ca)\\ ca, &\text{else}}$\; - $translateDeclaration(decl(a), a, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclV} +% $ac\assng \closedCases{\createExpression{\IVMLMeta{acc}(ca,a)}, & \text{if } ca \neq \undef \wedge~qualifyAnnotation(v, a)\\ ca, &\text{else}}$\; + $translateDeclaration(decl(a), a, annAc(a, v, ca, \variableMapping))$\;\label{algTranslateAnnotationDeclarationsTranslateDeclV} } }\Else{\label{algTranslateAnnotationDeclarationsTranslateVEnd}\label{algTranslateAnnotationDeclarationsTranslateDStart} \ForEach{$a\in annotations(d)$}{ - $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } qualifyAnnotation(v, a, ca)\\ ca, &\text{else}}$\; - $translateDeclaration(a, \undef, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD} +% $ac\assng \closedCases{\createExpression{\IVMLMeta{acc}(ca,a)}, & \text{if } \neq \undef \wedge~qualifyAnnotation(v, a)\\ ca, &\text{else}}$\; + $translateDeclaration(a, \undef, annAc(a, v, ca, \variableMapping))$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD} } }\label{algTranslateAnnotationDeclarationsTranslateDEnd} @@ -412,41 +411,28 @@ \end{algorithm} -with +Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration $d$ of the variable $v$ that shall be processed as well as an optional access expression $ca$ in case that $d$ is a compound slot. The idea for Algorithm \ref{algTranslateAnnotationDeclarations} is to iterate over all annotations, either in terms of decision variables or declarations\footref{fnVariableNull}, and to process each annotation as if it was an ordinary variable, i.e., by calling Algorithm \ref{algTranslateDeclaration} with a respective access expression. + +First, Algorithm \ref{algTranslateAnnotationDeclarations} determines in line \ref{algTranslateAnnotationDeclarationsCa} the actual base access expression as either $ca$ (e.g., as $d$ is a compound slot) if given or $d$. Annotations are translated based on nested variables of $v$ and their actual values, if $v$ is given (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}). Alternatively, e.g., for configuration initialization, the translation of annotations is done based on nested declarations of $d$ (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). In both cases, Algorithm \ref{algTranslateDeclaration} is called on the respective declaration, variable (if available) and accessor expression. The accessor expression is created by: % \begin{align*} -qualifyAnnotation(v, a, & ca) = ca \neq \undef \wedge \neg isContextRegistering(\variableMapping) \wedge \\ &(size(\variableMapping) > 1 \vee isCompound(base^*(type(v)))) +ann&Acc(a, v, ca, \variableMapping) =\\ &\closedCases{\createExpression{\IVMLMeta{acc}(ca,a)}, & \text{if } ca \neq \undef \wedge \\ &(size(\variableMapping) > 1 \vee isCompound(base^*(type(v))))\\ ca, &\text{else}} \end{align*} % -which requests creating an extended accessor expression if we are translating a nested annotation block (implying context registering) or if we are translating an annotation of a compound type. - -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. The actual access expression is either $ca$ if given or $d$ if $ca$ is not given (line \ref{algTranslateAnnotationDeclarationsCa}). Annotations are translated based on $v$ if given (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}), for configuration initialization also based on $d$ if $v$ is not given (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). - -For all annotations of $v$ -%(as for $v$ here all inherited annotations are available) -, the algorithm creates the respective constraints by creating a specific access expression according to $qualifyAnnotation(v, a, ca)$ through calling Algorithm \ref{algTranslateDeclaration}. For top-level annotation assignments , no specific access expressions except for the one created in line \ref{algTranslateAnnotationDeclarationsCa} are needed, as they are created in Algorithm \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateAnnotationAccess}. - -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 declared 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 is caused by Algorithm \ref{algTranslateCompoundDeclaration} in line \ref{algTranslateCompoundDeclarationCompoundAssignments} (variable mapping in Algorithm \ref{algRegisterCompoundMapping} line \ref{algRegisterCompoundMappingVarMapping} and slot translation in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT} in Algorithm \ref{algTranslateCompoundDeclaration} along with the decision variables of the compound value). 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). However, only the innermost assignment is relevant in case of nested assignment blocks~\cite{IVML-LS}, so that we build a mapping based on the annotation names overriding assignments inherited from the containing assignment blocks. -For a given assignment-block $a$, the algorithm performs then the transformation of each individual assignment and collects the created constraints in $\otherConstraints$. If the type of the slot (if available the dynamic type of the value) is a compound, the algorithm performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). It is important to note that we temporarily activate a context frame of $\variableMapping$ for each declaration $d$ if a context has been created/registered before during compound translation. This is required as the constraints are actually created after the translation of the types and otherwise we would still use the original variables specified in the model rather than the instantiated ones needed for reasoning. Finally, the algorithm recursively processes contained assignment-blocks. - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{assignment-block $a$, variable $v$ effective assignment data $ea$, compound access $ca$} - \KwData{constraints $\otherConstraints$} +The function $annAcc$ creates an specific annotation accessor in case that we are translating a nested annotation assignment (the content stack contains here more than one frame) or the underlying variable holding the annotation is of a compound type and must be qualified explicitly. + +We turn now to the second pattern, the translation of annotation assignments. The idea of Algorithm \ref{algTranslateAnnotationAssignments} is to incrementally create the set of effective assignments for the actual annotation assignment in order to ensure that only the innermost assignment data is applied. More technically, we build a mapping based on the names of the annotations and override inherited assignments with by those specified by the annotation assignment to be processed. + +Algorithm \ref{algTranslateAnnotationAssignments} receives the annotation assignment $a$ to process, the optional parent variable $v$ containing $a$, the mapping of effective assignment data objects $ea$ and an optional access expression $ca$ to $v$. Initially, Algorithm \ref{algTranslateAnnotationAssignments} is called with an empty mapping $ea=\emptyMap$. In line \ref{algTranslateAnnotationAssignmentsUpdateEA}, Algorithm \ref{algTranslateAnnotationAssignments} updates $ea$ by adding all assignment data objects defined by the actual annotation assignment $a$. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{annotation assignment $a$, variable $v$, effective assignment data $ea$, compound access $ca$} + \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} - $ea \assng ea \addMap \setWith{\mapEntry{name(a)}{a}}{a \in assignmentData(a)}$\; - \ForAll{$\mapEntry{n}{e} \iterAssng ea$}{ - \ForAll{$d \iterAssng slots(a)$} { - $activate(\variableMapping, d)$\; - $add(\otherConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false, \undef)$\; + $ea \assng ea \addMap \setWith{\mapEntry{name(a)}{a}}{a \in assignmentData(a)}$\;\label{algTranslateAnnotationAssignmentsUpdateEA} + \ForAll{$d \iterAssng decls(a)$} {\label{algTranslateAnnotationAssignmentsLoopStart} + $a_d\assng ea[name(d)]$\; \label{algTranslateAnnotationAssignmentsObtainEA} + $add(\otherConstraints, \set{translateAnnotationAssignment(a_d, d, ca)}, false, \undef)$\; \label{algTranslateAnnotationAssignmentsTranslateBasic} $t \assng type(d)$\; - $ac \assng \closedCases{ - \createExpression{\IVMLMeta{acc}(ca, d)}, & \text{if } ca \neq \undef \\ - \createExpression{\IVMLMeta{acc}(\IVMLMeta{var}(decl(v)), d)}, & \text{if } var \neq \undef \\ - \createExpression{\IVMLMeta{var}(s)}, & \text{else} - }$\; \If{$v \neq \undef$}{ $w \assng nested^*(v, name(d))$\; @@ -456,10 +442,15 @@ } \If{$isCompound(t)$} { + $ac \assng \closedCases{ + \createExpression{\IVMLMeta{acc}(ca, d)}, & \text{if } ca \neq \undef \\ + \createExpression{\IVMLMeta{acc}(\IVMLMeta{var}(decl(v)), d)}, & \text{if } var \neq \undef \\ + \createExpression{\IVMLMeta{var}(s)}, & \text{else} + }$\; \ForAll{$s \iterAssng slots(t)$} { - $add(\otherConstraints, translateAnnotationAssignment(e, s, v, \createExpression{\IVMLMeta{acc}(a, s)}), false, \undef)$\; + $x \assng \createExpression{\IVMLMeta{acc}(ac, s)}$\; + $x \assng translateAnnotationAssignment(a_d, s, v, x)$\; + $add(\otherConstraints, x, false, \undef)$\; } - } - $deactivate(\variableMapping, d)$\; - } + }\label{algTranslateAnnotationAssignmentsLoopEnd} } @@ -470,4 +461,9 @@ \caption{Translating annotation assignments (\IVML{translateAnnotationAssignments}).}\label{algTranslateAnnotationAssignments} \end{algorithm} + +For a given annotation assignment $a$, the algorithm processes all declared variables (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates then default value assignment constraint and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsTranslateBasic}. + + + If the type of the slot (if available the dynamic type of the value) is a compound, the algorithm performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). Finally, the algorithm recursively processes contained assignment-blocks. Algorithm \ref{algTranslateAnnotationAssignments} relies on the translation of an individual assignment data object. 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$. Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 155) +++ /reasoner/notation.tex (revision 156) @@ -174,5 +174,5 @@ % \begin{align*} -all&CmpConstraints(t) = +all&CmpConstraints(t) = \\ &\setWith{constraints(s) \cup allAssignmentConstraints(s)}{s \in allRefines^+(t)} \end{align*} Index: /reasoner/reasoningAlg.tex =================================================================== --- /reasoner/reasoningAlg.tex (revision 155) +++ /reasoner/reasoningAlg.tex (revision 156) @@ -84,11 +84,12 @@ During the constraint translation, top-level constraints can directly be evaluated over involved top-level variables. As already mentioned in Section \ref{sectNotationConstraints}, constraints defined on compound slots or indirectly through use of compound instances in containers must be translated before evaluation. The particular issue here is that these constraints can be defined in an IVML model over types (for which no values can be assigned in a configuration) rather than over top-level variables. A solution is to rewrite these constraints by substituting type-local variables by appropriate accessors starting at top-level variables. To manage the various lots and access expressions, the translation utilizes a stack-based data structure, onto which we push/pop a context frame for each IVML project and each contained compound type, container type or combinations of both used in variables of a project. A context frame links all currently relevant variables to the correct accessor expressions, which are created before the respective variable substitutions are applied. -However, a simple stack is not sufficient for two reasons, namely nested complex types, excluded types and assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames can store the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. The constraint rescheduling re-uses the constraint transformation. However, performing a complete transformation of all types related to certain value change is typically not needed, so that excluding types from the translation speeds up the re-scheduling operations. Moreover, IVML projects and compounds can contain nested assignment blocks. An assignment block implicitly defines assignment constraints for its contained variable declarations including containers or compounds. If we translate first variable declarations and then the related constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, i.e., wrong constraints would be added to the constraint bae. Intermingling compund/container translation with annotation-block translation would be a potential solution, which increases the algorithm / code complexity. Thus, we opted to register a declaration with its context frame (which is then implicitly registered with its parent frame for proper cleanup) and to activate/deactivate such a frame, although it is not on top of the stack, when translating the implicit assignment constraints in an assignment block. Such stack frames are also removed from the stack when popping the respective parent context frame. +However, a simple stack is not sufficient for two reasons, namely nested complex types, excluded types and assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames can store the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. The constraint rescheduling re-uses the constraint transformation. However, performing a complete transformation of all types related to certain value change is typically not needed, so that excluding types from the translation speeds up the re-scheduling operations. +%Moreover, IVML projects and compounds can contain nested assignment blocks. An assignment block implicitly defines assignment constraints for its contained variable declarations including containers or compounds. If we translate first variable declarations and then the related constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, i.e., wrong constraints would be added to the constraint bae. Intermingling compund/container translation with annotation-block translation would be a potential solution, which increases the algorithm / code complexity. Thus, we opted to register a declaration with its context frame (which is then implicitly registered with its parent frame for proper cleanup) and to activate/deactivate such a frame, although it is not on top of the stack, when translating the implicit assignment constraints in an assignment block. Such stack frames are also removed from the stack when popping the respective parent context frame. In summary, the variable mapping stack structure $\variableMapping$ of the IVML reasoner provides the following operations: \begin{itemize} - \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. - \item $isContextsRegistering(\variableMapping)$ returns whether context registering is currently active. +% \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. +% \item $isContextsRegistering(\variableMapping)$ returns whether new context frames are automatically registered with the parent frame. \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, $r$ indicates whether the new frame shall be registered with the parent frame and whether already processed types (for handling nested complex types) shall be recorded by this context. \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating an all-quantified constraint prefix for all constraints added to the constraint base as long this frame is on the stack. The information includes the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}. @@ -98,6 +99,6 @@ \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If \linebreak[4] $isCompound(t)$, this function registers $allRefined^+(t)$. \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the enclosing context frames. - \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ taken from the current context frame. As long as the current context frame exists, this operation can be called again and again. If no context frame is registered for $d$, the stack is not modified. - \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists on the stack. +% \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ taken from the current context frame. As long as the current context frame exists, this operation can be called again and again. If no context frame is registered for $d$, the stack is not modified. +% \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists on the stack. \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}. \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type and avoids applying them some nested type. @@ -159,5 +160,5 @@ $add(\topLevelConstraints, constraints(p), true, \undef)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints} \ForAll{$a \iterAssng assignments(p)$}{ - $add(\topLevelConstraints, constraints(a), true, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} + $add(\topLevelConstraints, allAssignmentConstraints(a), true, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} $translateAnnotationAssignments(a, \undef, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments} } \label{algTranslateConstraintsTranslationEnd} @@ -192,4 +193,14 @@ The main loop (lines \ref{algEvalLoopLoopStart}-\ref{algEvalLoopLoopEnd}) runs as long as there are constraints for evaluation in the constraint $base$, no timeout and no user cancellation request occurred. The (size of the) constraint base changes dynamically during reasoning as Algorithm \ref{algEvalLoop} removes processed constraints and value (type) changes may add constraints, e.g., those involving the changed variable (see Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling} for details). If no value assignment cycles occur, which ultimately lead to a timeout, the evaluation loop either terminates when all constraints are successfully evaluated or failing constraints do not induce the evaluation of further constraints. + +In each iteration of the main loop, the algorithm pops a constraint for evaluation from $base$ (line \ref{algEvalLoopPop}). % and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}). +To assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} registers the actual assignment state for the current constraint $c$ (line \ref{algEvalLoopAssngState}). If $c$ is a default constraint, all subsequent value assignments during the evaluation of $c$ happen with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) by passing it to the constraint evaluator. %If configuration variables are changed as part of the constraint evaluation, the variables are recorded (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). +Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created. We distinguish three cases: + +\begin{enumerate} + \item Constraint $c$ is evaluated successfully so that either no problem record is created or potentially existing problem records for $c$ from previously failed evaluations can be removed from $\problemRecords$. + \item Constraint $c$ is evaluated as undefined. As specified by IVML~\cite{IVML-LS}, a constraint is also considered undefined, if at least one involved variable or expression is evaluated as undefined. This does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. + \item The constraint evaluation fails and a problem record for detailed error reporting or further (external) analysis is created. +\end{enumerate} \begin{algorithm}[H] @@ -214,14 +225,4 @@ \end{algorithm} -In each iteration of the main loop, the algorithm pops a constraint for evaluation from $base$ (line \ref{algEvalLoopPop}). % and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}). -To assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} registers the actual assignment state for the current constraint $c$ (line \ref{algEvalLoopAssngState}). If $c$ is a default constraint, all subsequent value assignments during the evaluation of $c$ happen with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) by passing it to the constraint evaluator. %If configuration variables are changed as part of the constraint evaluation, the variables are recorded (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). -Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created. We distinguish three cases: - -\begin{enumerate} - \item Constraint $c$ is evaluated successfully so that either no problem record is created or potentially existing problem records for $c$ from previously failed evaluations can be removed from $\problemRecords$. - \item Constraint $c$ is evaluated as undefined. As specified by IVML~\cite{IVML-LS}, a constraint is also considered undefined, if at least one involved variable or expression is evaluated as undefined. This does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. - \item The constraint evaluation fails and a problem record for detailed error reporting or further (external) analysis is created. -\end{enumerate} - Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. Please note that no modification of $\relevantConstraintVariables$, the mapping between decision variables and constraints, is needed, as no change of constraint variables or their values occurred here.