Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 115) +++ /reasoner/reasoner.tex (revision 116) @@ -379,10 +379,11 @@ \newcommand\otherConstraints[0]{c_{o}} \newcommand\topLevelConstraints[0]{c_{t}} -\newcommand\relevantConstraints[0]{r_t} +\newcommand\relevantConstraintsPerType[0]{r_t} +\newcommand\relevantConstraintVariables[0]{r_c} \newcommand\scopeAssignments[0]{a} \newcommand\usedVariables[0]{u} \newcommand\problemRecords[0]{m} -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. +The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), stores constraint relations (the relevant constraints per type $\relevantConstraintsPerType$ and the relevant constraint variables per decision variable ($\relevantConstraintVariables$), 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 reasoner data structures in Section \ref{sectDataStructures}, 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}. @@ -402,5 +403,5 @@ \SetAlgoLined \KwIn{configuration $cfg$} - \KwData{problem records $\problemRecords$, scope assignments $\scopeAssignments$, expression evaluator $e$, reasoning start time $startTime$, flags $hasTimeout$ and $stop$, $resue$ instance flag, $projects$ sequence, relevant constraints $\relevantConstraints$}, constraint base copy $base_c$ and $base_{\relevantConstraints}$ + \KwData{problem records $\problemRecords$, scope assignments $\scopeAssignments$, expression evaluator $e$, reasoning start time $startTime$, flags $hasTimeout$ and $stop$, $resue$ instance flag, $projects$ sequence, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerType}, base_{\relevantConstraintVariables}$} \KwResult{Reasoning result $r$} @@ -413,5 +414,6 @@ \If{$reuse$}{ $base_c = \seqEmpty{}$\; %sequence? - $base_{\relevantConstraints} = \setEmpty{}$\; %map? + $base_{\relevantConstraintsPerType} = \setEmpty{}$\; %map? + $base_{\relevantConstraintVariables} = \setEmpty{}$\; %map? } $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} @@ -422,5 +424,6 @@ } \label{algMainLoopEnd}\label{algMainLoopFullEnd} }\Else {\label{algMainLoopIncStart} - $\relevantConstraints \assng base_{\relevantConstraints}$\; + $\relevantConstraintsPerType \assng base_{\relevantConstraintsPerType}$\; + $\relevantConstraintVariables \assng base_{\relevantConstraintVariables}$\; \ForAll{$i \in \set{0, \ldots, |base_c|} \wedge \neg hasTimeout \wedge \neg stop$}{ $base \assng base_c[i]$\; @@ -434,5 +437,5 @@ \end{algorithm} -For IVML, the full execution of the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. As shown in Algorithm \ref{algMainLoop}, first a structure is created to store constraints for reuse (if $reuse$ is enabled). Then, the relevant IVML projects and their sequence are identified. Therefore, $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 a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. +For IVML, the full execution of the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. 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 type ($base_{\relevantConstraintsPerType}$) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$). Then, the relevant IVML projects and their sequence are identified. Therefore, $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 a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. Following this sequence, the main reasoning loop considers all IVML projects for a given configuration $cfg$, as long as no timeout occurred (global flag $hasTimeout$) or the user requested a stop of the reasoning operations (global flag $stop$). Further, the algorithm records the start time in line \ref{algMainLoopStartTime} in order to be able to detect timeouts. @@ -498,5 +501,5 @@ \SetAlgoLined \KwIn{project $p$} - \KwData{constraint $base$, constraint base copy $base_c$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$, incremental mode flag $inc$, eval-blocks flag $inEval$} + \KwData{constraint $base$, constraint base copy $base_c$, variable mapping $\variableMapping$, incremental mode flag $inc$, eval-blocks flag $inEval$} \tcp{start of model visitor}%>ConstraintTranslationVisitor @@ -551,5 +554,5 @@ \SetAlgoLined \KwIn{project $p$} - \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, used variables $\usedVariables$, relevant constraints $\relevantConstraints$, expression evaluator $e$, flags $hasTimeout$ and $stop$} + \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, used variables $\usedVariables$, relevant constraints $\relevantConstraintsPerType$, expression evaluator $e$, flags $hasTimeout$ and $stop$} $clearAssignments(\scopeAssignments)$\; \label{algEvalLoopClearScope}%clearScopeAssignment @@ -562,5 +565,5 @@ $\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)}$\; + $\relevantConstraintsPerType \assng \relevantConstraintsPerType \cap \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; }\label{algEvalLoopClearEnd} $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} @@ -581,5 +584,5 @@ \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}. +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 $\relevantConstraintsPerType$ 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}. @@ -620,5 +623,5 @@ \SetAlgoLined \KwIn{declaration $d$, variable $v$, access $ca$} - \KwData{variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental $inc$} + \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} @@ -822,5 +825,5 @@ \SetAlgoLined \KwIn{declaration $d$, variable $v$, access $ca$, type $t$} - \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$} + \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, incremental flag $inc$} $pushContext(\variableMapping, false)$\; @@ -1049,5 +1052,5 @@ \SetAlgoLined \KwIn{constraint expression $c$, actual value for \IVMLself{} $f$, variable $v$} - \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$} + \KwData{other constraints $\otherConstraints$} \If {$c \neq \undef$} { $c \assng \createConstraintConstraint{\varSubstitutionSelfVarMapping{c}{f}}$\; @@ -1076,5 +1079,5 @@ \begin{algorithm}[H] \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$} - \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$ , incremental flag $inc$, evals flag $inEvals$} + \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerType$ , incremental flag $inc$, evals flag $inEvals$} \If{$\neg inc \vee (inc \wedge \neg (isAssignment(c) \vee isFrozen(c)))$} { $c = composeExpression(\variableMapping, c)$\; @@ -1092,5 +1095,5 @@ } \If{$\neg isSimpleConstraint(c)$}{ - $\relevantConstraints \assng \relevantConstraints \cup \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; % assignConstraintsToVariables + $\relevantConstraintsPerType \assng \relevantConstraintsPerType \cup \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; % assignConstraintsToVariables } } @@ -1124,12 +1127,12 @@ \SetAlgoLined \KwIn{variable $v$, constraint expression $c$} - \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$}, relevant constraints copy $base_{\relevantConstraints}$ + \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraintVariables$}, relevant constraints copy $base_{\relevantConstraintVariables}$ \If{$v \neq \undef$}{ - $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{c}{v}$\; - $\relevantConstraints[v] \assng \relevantConstraints[v] \cup \set{c}$\; - \If{$base_{\relevantConstraints} \neq \undef$} { - $base_{\relevantConstraints} \assng base_{\relevantConstraints} \addMap \mapEntry{c}{v}$\; - $base_{\relevantConstraints}[v] \assng base_{\relevantConstraints}[v] \cup \set{c}$\; + $\relevantConstraintVariables \assng \relevantConstraintVariables \addMap \mapEntry{c}{v}$\; + $\relevantConstraintVariables[v] \assng \relevantConstraintVariables[v] \cup \set{c}$\; + \If{$base_{\relevantConstraintVariables} \neq \undef$} { + $base_{\relevantConstraintVariables} \assng base_{\relevantConstraintVariables} \addMap \mapEntry{c}{v}$\; + $base_{\relevantConstraintVariables}[v] \assng base_{\relevantConstraintVariables}[v] \cup \set{c}$\; } } @@ -1138,5 +1141,5 @@ \end{algorithm} % -Recording happens only if $v$ is defined, which may not be the case if this algorithm is called while processing container values. +Recording happens only if $v$ is defined, which may not be the case if this algorithm is called while processing container values. Then, we recorder the relation of the variable $v$ to its \section{Constraint Re-scheduling}\label{sectTopLevelConstraintsRescheduling} @@ -1147,11 +1150,11 @@ \SetAlgoLined \KwIn{decision variable $v$, old value $val$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraints$} + \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$} \If{$\neg isLocal(v)$}{ $addAssignment(\scopeAssignments, 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 - $base \assng base \addSeqNoDupl \seqWith{\relevantConstraints[n]}{n\in allNested(v)}$\; \label{algVarChangeRescheduleNested}%constraintsForParent + $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerType[p]}{p\in allParents(v)}$\; \label{algVarChangeRescheduleParents}%constraintsForParent + $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerType[n]}{n\in allNested(v)}$\; \label{algVarChangeRescheduleNested}%constraintsForParent % $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}\relevantConstraints[c]$\; \label{algVarChangeRescheduleNested}%constraintsForChilds, nested geht für alle variablen }