Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 221) +++ /reasoner/consTranslation.tex (revision 222) @@ -188,4 +188,8 @@ \end{itemize} +Algorithm \ref{algRegisterCompoundMapping} iterates over all slots of $t$ and its refined compounds using $slots^+(t)$, which contains all potentially visible slots for $t$ along the refinement hierarchy starting with the slots of $t$. Due to this processing sequence, the decision whether we must create a new accessor for slot $s$ just depends on if there is already an access expression defined for $name(s)$ in the actual (local) context frame (line \ref{algRegisterCompoundMappingExMapping}). Lines \ref{algRegisterCompoundMappingAccStart}-\ref{algRegisterCompoundMappingAccEnd} create such an accessor expression if none was found in the actual context frame. The accessor is either based on $ca$ (if given) or on $e_d$. The created accessor $x$ is then registered in the actual context frame of $\variableMapping$. Similarly, we create accessors for all declared annotations of $s$ based on the accessor $x$ for $s$. + +Finally, in lines \ref{algRegisterCompoundMappingEdStart}-\ref{algRegisterCompoundMappingEdEnd}, the algorithm creates accessors for all annotations directly declared for the underlying compound variable (through $e_d$). + \begin{algorithm}[H] \SetAlgoLined @@ -209,8 +213,4 @@ \caption{Registering the compound mapping (\IVML{registerCompoundMapping}).}\label{algRegisterCompoundMapping} \end{algorithm} - -Algorithm \ref{algRegisterCompoundMapping} iterates over all slots of $t$ and its refined compounds using $slots^+(t)$, which contains all potentially visible slots for $t$ along the refinement hierarchy starting with the slots of $t$. Due to this processing sequence, the decision whether we must create a new accessor for slot $s$ just depends on if there is already an access expression defined for $name(s)$ in the actual (local) context frame (line \ref{algRegisterCompoundMappingExMapping}). Lines \ref{algRegisterCompoundMappingAccStart}-\ref{algRegisterCompoundMappingAccEnd} create such an accessor expression if none was found in the actual context frame. The accessor is either based on $ca$ (if given) or on $e_d$. The created accessor $x$ is then registered in the actual context frame of $\variableMapping$. Similarly, we create accessors for all declared annotations of $s$ based on the accessor $x$ for $s$. - -Finally, in lines \ref{algRegisterCompoundMappingEdStart}-\ref{algRegisterCompoundMappingEdEnd}, the algorithm creates accessors for all annotations directly declared for the underlying compound variable (through $e_d$). \subsubsection{Translating Compound Constraints}\label{sectionTransComp} @@ -504,4 +504,6 @@ Algorithm \ref{algTranslateAnnotationAssignments} receives the annotation assignment block $a$ to process, the optional parent variable $v$ containing $a$, the effective assignment data objects $ea$ and an optional access expression $ca$ to $v$. As introduced in Section \ref{sectNotationProject}, an assignment data object consists of the name of an assignment variable and an associated default value expression. Initially, Algorithm \ref{algTranslateAnnotationAssignments} is called with an empty mapping $ea=\emptyMap$. + +In line \ref{algTranslateAnnotationAssignmentsUpdateEA}, Algorithm \ref{algTranslateAnnotationAssignments} updates the effective assignments $ea$ by adding mappings for all assignments, i.e., annotation name to data object, defined by the actual annotation assignment $a$. Then, the algorithm processes all variables declared declared in $a$ (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates the default value assignment constraint in line \ref{algTranslateAnnotationAssignmentsTranslateBasic} and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsAdd}. \begin{algorithm}[H] @@ -543,8 +545,8 @@ \end{algorithm} -In line \ref{algTranslateAnnotationAssignmentsUpdateEA}, Algorithm \ref{algTranslateAnnotationAssignments} updates the effective assignments $ea$ by adding mappings for all assignments, i.e., annotation name to data object, defined by the actual annotation assignment $a$. Then, the algorithm processes all variables declared declared in $a$ (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates the default value assignment constraint in line \ref{algTranslateAnnotationAssignmentsTranslateBasic} and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsAdd}. If the declared variable is of compound type (lines \ref{algTranslateAnnotationAssignmentsIsCompoundStart}-\ref{algTranslateAnnotationAssignmentsIsCompoundEnd}), we must also translate the annotations of the compound slots. Direct recursion is not needed, as this will happen through Algorithm \ref{algTranslateDeclaration}. Therefore, the algorithm determines in lines \ref{algTranslateAnnotationAssignmentsActTypeStart}-\ref{algTranslateAnnotationAssignmentsActTypeEnd} the actual type of $d$, which may differ from the declared type for annotations of compound type due to compound refinement. In line \ref{algTranslateAnnotationAssignmentsAccess}, the algorithm determines the access expression $ac$ for $d$, which may either be based on the nesting path of the accessor $ca.d$ if $ca$ is given, $v.d$ if $v$ is available or, in type-based translations, just $d$. Now, the algorithm can iterate over all slots of the compound annotation (lines \ref{algTranslateAnnotationAssignmentsSlotsStart}-\ref{algTranslateAnnotationAssignmentsSlotsEnd}), create the respective access expression $ac.s$ in line \ref{algTranslateAnnotationAssignmentsSlotAccess}, create the assignment constraint in line \ref{algTranslateAnnotationAssignmentsSlotConstraint} and add the resulting constraint to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsSlotConstraintAdd}. Finally, the algorithm processes the nested annotation assignments in lines \ref{algTranslateAnnotationAssignmentsNestedStart}-\ref{algTranslateAnnotationAssignmentsNestedEnd} by calling Algorithm \ref{algTranslateAnnotationAssignments} recursively. +If the declared variable is of compound type (lines \ref{algTranslateAnnotationAssignmentsIsCompoundStart}-\ref{algTranslateAnnotationAssignmentsIsCompoundEnd}), we must also translate the annotations of the compound slots. Direct recursion is not needed, as this will happen through Algorithm \ref{algTranslateDeclaration}. Therefore, the algorithm determines in lines \ref{algTranslateAnnotationAssignmentsActTypeStart}-\ref{algTranslateAnnotationAssignmentsActTypeEnd} the actual type of $d$, which may differ from the declared type for annotations of compound type due to compound refinement. In line \ref{algTranslateAnnotationAssignmentsAccess}, the algorithm determines the access expression $ac$ for $d$, which may either be based on the nesting path of the accessor $ca.d$ if $ca$ is given, $v.d$ if $v$ is available or, in type-based translations, just $d$. Now, the algorithm can iterate over all slots of the compound annotation (lines \ref{algTranslateAnnotationAssignmentsSlotsStart}-\ref{algTranslateAnnotationAssignmentsSlotsEnd}), create the respective access expression $ac.s$ in line \ref{algTranslateAnnotationAssignmentsSlotAccess}, create the assignment constraint in line \ref{algTranslateAnnotationAssignmentsSlotConstraint} and add the resulting constraint to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsSlotConstraintAdd}. Finally, the algorithm processes the nested annotation assignments in lines \ref{algTranslateAnnotationAssignmentsNestedStart}-\ref{algTranslateAnnotationAssignmentsNestedEnd} by calling Algorithm \ref{algTranslateAnnotationAssignments} recursively. In lines \ref{algTranslateAnnotationAssignmentsTranslateBasic} and \ref{algTranslateAnnotationAssignmentsSlotConstraint}, Algorithm \ref{algTranslateAnnotationAssignments} relies on the translation of an individual assignment data object. The translation of an assignment data object $a_d$ (in the context of declaration $d$, its accessor expression $ca$ and variable mapping $\variableMapping$) leads to the creation of an assignment constraint as shown below: - +% \begin{align*} translate&AnnotationAssignment(a_d, d, ca, \variableMapping) = \\ Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 221) +++ /reasoner/mainAlgorithms.tex (revision 222) @@ -3,5 +3,5 @@ \center %\frame{ -\includegraphics[scale=0.52,trim={5.9cm 7.0cm 27.5cm 0.4cm},clip]{figures/structure.pdf} +\includegraphics[scale=0.52,trim={5.9cm 6.5cm 27.5cm 0.4cm},clip]{figures/structure.pdf} %} \caption{Overview of reasoning algorithms and sections.} @@ -22,5 +22,5 @@ \newcommand\evaluator[0]{eval} -The reasoner performs forward reasoning, i.e., it identifies relevant constraints according to the reasoning mode, translates the constraints, maintains relations among constraints and model elements, evaluates the translated constraints in a loop until all constraints are processed and adjusts 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 may be involved in a recursion due to the potentially recursive structure of complex IVML types, in particular nested compounds or containers. Algorithms \ref{algComposeExpression} and \ref{algAddConstraint} shown in the lower part of Figure \ref{figStructure} may appear disconnected, but they are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nesting of complex IVML types. +The reasoner performs forward reasoning, i.e., it identifies relevant constraints according to the reasoning mode, translates the constraints, maintains relations among constraints and model elements, evaluates the translated constraints in a loop until all constraints are processed and adjusts 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 may be involved in a recursion due to the potentially recursive structure of complex IVML types, in particular nested compounds or containers. The algorithms in the lower part of Figure \ref{figStructure} may appear disconnected, but they are called by several translation algorithms to populate the constraint base and to compose quantified constraints for nested complex IVML types. This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the reasoner data structures in Section \ref{sectDataStructures}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, and the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation}. The algorithms for constraint translation will be discussed in detailed in Section \ref{sectTranslation} and the algorithms for re-scheduling constraints in Section \ref{sectTopLevelConstraintsRescheduling}.