Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 111) +++ /reasoner/reasoner.tex (revision 112) @@ -135,7 +135,15 @@ \subsubsection{Variable Declarations} -An IVML \emph{variable declaration} $d$ specifies a variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. $isDeclaration(d)$ is true for a variable declaration $d$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$ and $isAnnotation(d)$ returns whether a variable declaration is an annotation. Let $annotation(d, n) = a$ if $a\in annotations(d) \wedge name(a)=m$, else $annotation(d, n) = \undef$. -% -For an arbitrary model element $e$ (including type definitions, projects and variable declarations), $parent(e)$ returns the parent model element and $isAssngBlock(e)$ returns whether $e$ is an assignment block. +An IVML \emph{variable declaration} $d$ specifies a variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. $isDeclaration(d)$ is true for a variable declaration $d$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$ and $isAnnotation(d)$ returns whether a variable declaration is an annotation. Let $annotation(d, n) = a$ if $a\in annotations(d) \wedge name(a)=m$, else $annotation(d, n) = \undef$. +% +For an arbitrary model element $e$ (including type definitions, projects and variable declarations), $parent(e)$ returns the parent model element and $isAssngBlock(e)$ returns whether $e$ is an assignment block. Moreover, +% +$$ + annotations^+(e) = \begin{cases} + annotations(e), &\text{if } parent(e) = \undef \\ + annotations(e) \cup annotations(parent(e)), &\text{else} +\end{cases} +$$ +returns all declared annotations for an arbutrary model element $e$, in particular a variable declaration or a slot, assuming that $annotations(e)=\emptySet$ for model elements that do not declare annotations. \subsubsection{Configuration Variables}\label{sectNotationConfigVars} @@ -378,5 +386,5 @@ The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. Some algorithms call others recursively due to the potentially recursive structure of some IVML types, in particular compounds and containers. Algorithm \ref{algAddConstraint} and \ref{algComposeExpression} appear disconnected, but are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nesting of containers and compounds. -This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the global variable mapping structure used during the translation in Section \ref{sectVarMapping}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, 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 forrRe-scheduling of constraints during evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. +This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the global variable mapping structure used during the translation in Section \ref{sectVarMapping}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, 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 of constraints during evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. \begin{figure}[ht] @@ -525,5 +533,5 @@ \SetAlgoLined \KwIn{project $p$} - \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, used variables $\usedVariables$, expression evaluator $e$, flags $hasTimeout$ and $stop$} + \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, used variables $\usedVariables$, relevant constraints $\relevantConstraints$, expression evaluator $e$, flags $hasTimeout$ and $stop$} $\scopeAssignments \assng \setEmpty{}$\; \label{algEvalLoopClearScope}%clearScopeAssignment @@ -534,4 +542,7 @@ $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} $\problemRecords \assng \problemRecords \addSeq analyzeEvaluationResult(evaluate(e, c), \usedVariables)$\; \label{algEvalLoopAssngEval} + \If{$constraintFulfilled(e) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} + $\relevantConstraints \assng \relevantConstraints \cap \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; + }\label{algEvalLoopClearEnd} $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} } \label{algEvalLoopLoopEnd} @@ -544,4 +555,5 @@ In order 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, this causes that the subsequent value assignments during the evaluation of $c$ are done with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) through the constraint evaluator. If configuration variables are changed as part of the constraint evaluation, the variables are recorded in $\usedVariables$ (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, e.g., due to duplicate variable assignments in the same project scope etc. Here, we distinguish three cases. + \begin{enumerate} \item Constraint $c$ is evaluated successfully so that existing problem records for $c$ can be removed from $\problemRecords$. @@ -549,4 +561,6 @@ \item The constraint evaluation fails and a problem record is created including the used variables $\usedVariables$ for detailed error reporting or further (external) analysis. \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 the set of relevant constraints $\relevantConstraints$ in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This information is particularly relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}. @@ -601,10 +615,7 @@ \uIf{$isCompound(t)$}{ $f \assng d$\; \label{algTranslateDeclarationTranslateSelf1} - $dflt = translateCompoundDeclaration(d, v, ca, t, dflt)$\; \label{algTranslateDeclarationTranslateCompound} - } \uElseIf{$ isContainer(type(d)) $}{ \label{algTranslateDeclarationHasDefault} - $translateContainerDeclaration(d, v, ca, t)$\; \label{algTranslateDeclarationTranslateContainer} } \uElseIf{$dflt \neq \undef \wedge \neg inc$}{ \lIf{$ca \neq \undef$}{$s \assng ca$} \label{algTranslateDeclarationTranslateInCompound} - }\lElseIf{$inc$}{$ dflt \assng \undef $} + }\lElseIf{$inc \wedge \neg isContainer(t)$}{$ dflt \assng \undef $} \If{$ deflt \neq \undef \wedge \neg(isAttribute(d) \wedge isAssngBlock(parent(d)))$}{ \uIf{$isConstraint(type(d))$}{ \label{algTranslateDeclarationTranslateConstraintDefaultStart} @@ -619,10 +630,17 @@ $add(dfltS, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, dflt)}{f}})$\; \label{algTranslateDeclarationTranslateDefault} } + \uIf{$isCompound(t)$}{ + $translateCompoundDeclaration(d, v, ca, t, dflt)$\; \label{algTranslateDeclarationTranslateCompound} + } \uElseIf{$ isContainer(t) $}{ \label{algTranslateDeclarationHasDefault} + $translateContainerDeclaration(d, v, ca, t)$\; \label{algTranslateDeclarationTranslateContainer} + } \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$ 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 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$. +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. \subsection{Derived types}\label{sectDerivedTypes} @@ -649,6 +667,6 @@ $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\; $add(\topLevelConstraints, \setWith{\createConstraint{ - \closedCases{d\rightarrow\IVML{forAll(i}:\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{deref(t, i)}}\IVML{)}, & \text{if } isC \\ - \varSubstitutionOtherVarMapping{c}{decl(t)=d}, &\text{else}} + \varSubstitutionOtherVarMapping{\closedCases{\IVML{forAll(i:}c\IVML{)}, & \text{if } isC \\ + c, &\text{else}}}{decl(t)=deref(t, i)} }}{c\in cs}, true)$\; \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} @@ -686,5 +704,5 @@ $transferTypeExcludes(\variableMapping, t)$\; $e \assng \createExpression{d}$\; - $registerCompoundMapping(t, ca, e, type(value(v)))$\; + $registerCompoundMapping(t, ca, v, e, type(value(v)))$\; $translateCompoundContent(d, v, t, ca)$\; \If{$dflt \neq \undef$} { \label{algTranslateCompoundSubstStart} @@ -707,15 +725,18 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{compound type $t_c$, acccess $ca$, variable $v$, target type $t_t$} + \KwIn{compound type $t_c$, acccess $ca$, variable $v$, declaration expression $e_d$ target type $t_t$} \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t_c)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} $registerMapping(\variableMapping, s, x)$\; \ForAll{$a \iterAssng annotations(s)$}{ - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping} - $registerMapping(\variableMapping, a, x)$\; + $registerMapping(\variableMapping, a, \createExpression{\IVMLMeta{acc}(ca,a)})$\; \label{algRegisterCompoundMappingAnnotationMapping} } }\label{algRegisterCompoundMappingVarMappingEnd} + \ForAll{$a \iterAssng annotations^+(decl(e_d))$}{ + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping} + $registerMapping(\variableMapping, a, x)$\; % left out origins + } \caption{Registering the compound mapping (\IVML{registerCompoundMapping}).}\label{algRegisterCompoundMapping} @@ -742,5 +763,5 @@ \If{$\neg inc$} { \ForAll{$a \iterAssng assignments(t)$}{ - $translateAnnotationAssignments(a, \undef, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments} + $translateAnnotationAssignments(a, v, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments} } } @@ -754,4 +775,6 @@ \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent} \end{algorithm} + +As stated above, we defer all constraint translation work to a recursive execution of Algorithm \ref{algTranslateDeclaration}. However, correctly initializing compounds can be tricky, as both, default slot values and compound initializer expressions, i.e., complex value assignments to compounds must be considered while reasoning. We solve this as follows: Algorithm \ref{algTranslateDeclaration} is triggered by a compound variable declaration. If a default value for the compound variable is defined, Algorithm \ref{algTranslateDeclaration} creates a respective constraint and then continues with the creation of the slot defaults and the compound constraints in Algorithm \ref{algTranslateCompoundContent}. Mixing both happens behind the scenes through the constraint evaluator: Assigning a value to a compound variable (or a slot) causes the creation of a compound instance with the desired values for the specified slots. The following assignment constraints for the default values are executed if no other value has been assigned (otherwise they are ignored) and finally removed by the main constraint evaluation loop in Algorithm \ref{algEvalLoop}. Dependent default values are evaluated as soon as the required variables have values assigned. \subsection{Container types}\label{sectContainerDefaults} @@ -841,5 +864,5 @@ $pushContext(\variableMapping, \undef, e, l, true)$\; - $registerCompoundMapping(t, l, d, t)$\; \label{algTranslateDefaultsCompoundContainerMapping} + $registerCompoundMapping(t, l, \undef, d, t)$\; \label{algTranslateDefaultsCompoundContainerMapping} $translateCompoundContent(l, \undef, t, \closedCases{\undef, & \text{if } ca = \undef\\l & \text{else}})$\; \label{algTranslateDefaultsCompoundContainerContent} $popContext()$\; @@ -879,5 +902,4 @@ Utilizing quantor constraints here implies that default initializations, which remain undefined if some dependent variables have not been determined so far, cause a re-evaluation for all elements of the container. Here, unfolding the implicit loop of such a quantor may be a solution, as then only individual constraints are triggered. However, this only works for sequences, as sets do not provide element-wise/index-based access and unfolding the constraint for a large container also may create a huge number of constraints. Currently, we stay with the compromise of creating a single quantized constraint for all slots with default values. - \subsection{Annotations}\label{sectAnnotationDefaults} @@ -934,5 +956,5 @@ 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). +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. @@ -942,10 +964,15 @@ \KwData{constraints $\otherConstraints$} - $ea \assng ea \cup assignmentData(a)$\; - \ForAll{$e \iterAssng ea$}{ + $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)$\; $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))$\; @@ -956,5 +983,5 @@ \If{$isCompound(t)$} { \ForAll{$s \iterAssng slots(t)$} { - $add(\otherConstraints, translateAnnotationAssignment(e, s, v, \variableMapping[s]))$\; + $add(\otherConstraints, translateAnnotationAssignment(e, s, v, \createExpression{\IVMLMeta{acc}(a, s)}))$\; } } @@ -974,6 +1001,6 @@ \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}}, \\ - &findAnnotation(d, name(a))), \varSubstitutionSelfVarMapping{default(a)}{ca})} + \createConstraint{\varSubstitutionSelfVarMapping{\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}}, \\ + &findAnnotation(d, name(a))), default(a))}{ca}} \end{align*} @@ -1005,4 +1032,8 @@ \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint} \end{algorithm} + +It is important to note that the constraint translation for collection leads to quantor expressions for initializing constraint variables. This is per se dangerous, as due to the variable substitutions, a constraint acting as a value may then relate to the quantor iterator variable(s). Evaluating such a constraint leads to undefined expressions, as the iterator variables are unbound and shall be substituted by appropriate variables (in most cases \IVMLself{}). When utilizing quantor expressions, defining individual substitutions based on the involved instances does not work (as this is the purpose of the quantor). So one solution is to unfold the implicit loop as discussed in Section \ref{sectContainerDefaults}. However, as quantor expressions over variable assignments are valid IVML and may be utilized in a model, the reasoner and the constraint evaluation must be able to work with them anyway. + +As solution, we perform the variable replacement when changing the constraint value, i.e., during constraint re-scheduling (Section \ref{sectTopLevelConstraintsRescheduling}). For short, we utilize the quantor expressions as discussed in this section, during quantor evaluation we register also the temporary iterator variables in the actual context, let the quantor evaluation assign the constraints to the variables, and consider this dynamically modified context during constraint re-scheduling. Constraint re-scheduling is anyway notified about the variable change and utilized to replace the old constraint by the new one in the constraint base. Thereby, we perform a variable substitution to bind the constraint to the actual variable taking into account the actual context including the iterator variables, i.e., we accept a temporary inconsistent constraint with unbound variables for the short time between assigning the constraint variable value and the directly subsequent constraint re-scheduling for this value change. However, this finally corrected constraint must be stored in the configuration so that saving the configuration can happen with the actual (consistent) constraint. \subsection{Constraint base operations}\label{sectContainerBase} @@ -1083,5 +1114,5 @@ \section{Constraint Re-scheduling}\label{sectTopLevelConstraintsRescheduling} -When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the variable is relevant for re-scheduling. First, Algorithm \ref{algVarChange} registers in lines \ref{algVarChangeScopeStart}-\ref{algVarChangeScopeEnd} the change of $v$ within the actual project scope (\TBD{correct? also \IVML{DEFAULT}? Test case needed!}) if the value of $v$ actually has been affected by reasoning. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value type changes}) for a variable are identified and become subject to re-scheduling. The identification includes both, parent (line \ref{algVarChangeRescheduleParents}) and nested (line \ref{algVarChangeRescheduleNested}) variables, which is in particular relevant to capture all relevant constraints for variables in compound and container values. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint $base$. +When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the variable is relevant for re-scheduling. First, Algorithm \ref{algVarChange} registers in line \ref{algVarChangeScope} the change of $v$ within the actual project scope if the value of $v$ actually has been affected by reasoning. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value type changes}) for a variable are identified and become subject to re-scheduling. The identification includes both, parent (line \ref{algVarChangeRescheduleParents}) and nested (line \ref{algVarChangeRescheduleNested}) variables, which is in particular relevant to capture all relevant constraints for variables in compound and container values. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint $base$. \begin{algorithm}[H] @@ -1091,7 +1122,5 @@ \If{$\neg isLocal(v)$}{ - \If{$state(v) == \IVML{DERIVED}$}{\label{algVarChangeScopeStart} %addScopeAssignment - $\scopeAssignments \assng \scopeAssignments \cup \set{v}$\; - }\label{algVarChangeScopeEnd} + $\scopeAssignments \assng \scopeAssignments \cup \set{v}$\; \label{algVarChangeScope} %addScopeAssignment \MISSING{change constraints if dynamic value type changes}\; $base \assng base \addSeqNoDupl \seqWith{\relevantConstraints[p]}{p\in allParents(v)}$\; \label{algVarChangeRescheduleParents}%constraintsForParent