Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 48) +++ /reasoner/reasoner.tex (revision 49) @@ -259,4 +259,6 @@ \newcommand\relevantConstraints[0]{r_t} \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. This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}. @@ -264,21 +266,22 @@ \subsection{Main Reasoning Loop}\label{sectTopLevelMainReasoningLoop} -The main reasoning loop implements the overall control for the IVML reasoning process. For IVML, 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 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. +The main reasoning loop implements the overall control for the IVML reasoning process. First, Algorithm \ref{algMainLoop} sets up\footnote{In the implementation, also the re-scheduling of changed variables (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) and recording assigned variables are registered with the expression evaluator, but this is not shown here.} the expression evaluator in line \ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. For IVML, 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 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. \begin{algorithm}[H] \SetAlgoLined \KwIn{configuration $cfg$} - \KwData{problem records $m$, reasoning start time $startTime$, global flags $hasTimeout$ and $stop$} + \KwData{problem records $\problemRecords$, scope assignments $\scopeAssignments$, expression evaluator $e$, reasoning start time $startTime$, flags $hasTimeout$ and $stop$} \KwResult{Reasoning result $r$} + %evaluator.init()\; + %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\; + %evaluator.setScopeAssignments(sAssng)\; + $setup(e, cfg, \scopeAssignments)$\; \label{algMainLoopSetupEval} $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} $startTime = now()$\;\label{algMainLoopStartTime} \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart} - %evaluator.init()\; - %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\; - %evaluator.setScopeAssignments(sAssng)\; $translateConstraints(p)$\; \label{algMainLoopTranslate} $evaluateConstraints(p)$\; \label{algMainLoopEvaluate} - $freeze(p)$\; \label{algMainLoopFreeze} + $freeze(cfg, p)$\; \label{algMainLoopFreeze} } \label{algMainLoopEnd} $r \assng createReasoningResult(m, hasTimeout, stop)$\; \label{algMainLoopResult} @@ -292,5 +295,5 @@ \subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation} -Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. The variable mapping is a core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed. +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. The variable mapping is a core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed. From a technical point of view, the variability mapping consists of mapping entries relating a variable declaration with an access expression if needed. For directly accessible variables such as top-level variables directly defined within a project, no such mapping is needed ($\undef$). For variables used in constraints within compounds or containers, an appropriate accessor is needed, created and registered when starting to translate the respective type. The respective constraints for that type are then enumerated, copied and while copying the variables registered in the variable mapping are replaced by the accessor expressions in the mapping. It is important to ensure that the mapping for the respective type is complete before constraint translation, so that all variables including cross references within the same type can be replaced properly. References to other variables are already given as accessor expressions and do not need to be considered here. @@ -299,22 +302,27 @@ \SetAlgoLined \KwIn{project $p$} - \KwData{constraint $base$ , variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$, incremental mode flag $inc$} - - $\variableMapping \assng \setEmpty$\; \label{algTranslateConstraintsClearMapping} - %>ConstraintTranslationVisitor - \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart} %translateDeclarationDefaults - $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\; - } - $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\; \label{algTranslateConstraintsAdd} - \ForAll{a \iterAssng assignments(p)}{ - $translateAnnotationAssignments(a, \undef, \undef)$\; - } \label{algTranslateConstraintsTranslationEnd} - %ConstraintTranslationVisitor + \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart} %translateDeclarationDefaults + $translateDeclarationDefaults(d, decision(cfg, d), \undef)$\; + } + $add(\topLevelConstraints, constraints(p), true)$\; \label{algTranslateConstraintsAdd} + \ForAll{a \iterAssng assignments(p)}{ + $translateAnnotationAssignments(a, \undef, \undef)$\; + } \label{algTranslateConstraintsTranslationEnd} + $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}$\; + \tcp{end of model visitor}% 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart} $c \assng pop(base)$\; \label{algEvalLoopPop} - $clear(u)$\; \label{algEvalLoopClear} + $\usedVariables \assng \setEmpty$\; \label{algEvalLoopClear} $setAssignmentState(e, isDefault(c))$\; \label{algEvalLoopAssngState} - $m \assng m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\; \label{algEvalLoopAssngEval} + $\problemRecords \assng \problemRecords \addSeq analyzeEvaluationResult(evaluate(e, c), \usedVariables)$\; \label{algEvalLoopAssngEval} $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} } \label{algEvalLoopLoopEnd} @@ -358,9 +366,9 @@ 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}). -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 $u$ (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. +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 $m$. + \item Constraint $c$ is evaluated successfully so that existing problem records for $c$ can be removed from $\problemRecords$. \item Constraint $c$ is evaluated as undefined. As specified by IVML \ref{IVML-LS}, a constraint for which at least one variables or expressions is evaluated to undefined, is also considered undefined. This situation 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 is created including the used variables $u$ for detailed error reporting or further (external) analysis. + \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} @@ -410,5 +418,5 @@ \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\topLevelConstraints$. \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\otherConstraints$ - \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm substitutes all occurrences of \IVMLself{} by the actual declaration as well as all mapped variables from $m$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified. + \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm substitutes all occurrences of \IVMLself{} by the actual declaration as well as all mapped variables from $\problemRecords$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified. \item Collects all transformed container compounds based on the actual used types if $d$ is a container. If $d$ is a container over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_containers}). \item Translates remaining (slot) default value expression by replacing potential \IVMLself{} usages with the compound access. In case that \IVMLself{} is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($\deferredDefaultConstraints$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. @@ -420,6 +428,6 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{declaration $d$, variable $v$, access $ca$, incremental $inc$} - \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$} + \KwIn{declaration $d$, variable $v$, access $ca$} + \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$} $translateDerivedDatatypeConstraints(d)$\;