Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 107) +++ /reasoner/reasoner.tex (revision 108) @@ -38,6 +38,8 @@ \newcommand\subTypeEqOf[2]{t \succeq s} \newcommand\createConstraint[1]{\langle #1 \rangle} -\newcommand\createDefaultConstraint[1]{\langle_d\text{ } #1 \rangle} -%\newcommand\createInternalConstraint[1]{\langle_i\text{ } #1 \rangle} +\newcommand\createDefaultConstraint[1]{\langle #1 \rangle_d} +\newcommand\isDefaultConstraint[1]{isDefault(#1)} +\newcommand\createConstraintConstraint[1]{\langle #1 \rangle_c} +\newcommand\isConstraintConstraint[1]{isVariableConstraint(#1)} \newcommand\createExpression[1]{\langle\langle #1 \rangle\rangle} \newcommand\closedCases[1]{\left.\begin{cases}#1\end{cases}\right\}} @@ -208,5 +210,5 @@ As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a $\variableMapping=\set{\mapEntry{e_s, e_t}}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. As we use the '$|$' symbol for variable substitutions, using the same symbol in some transformations in IVML quantor expressions would be confusing. Thus, we use in this document the respective syntax parts ':' as introduced for sets in Section \ref{sectGeneralNotation} instead of the syntactically correct '$|$', e.g., \IVML{forall(x:c(x))} instead of the correct IVML notation \IVML{forall(x|c(x))}. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i:i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i:i>20)}}$. -For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, i.e., for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$. +For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, e.g., for creating a default constraint, we denote $b \assng \createDefaultConstraint{\IVML{assign}(x, 25)}$ for which $\isDefaultConstraint{b} = true$ holds. Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds. In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. When creating expressions, sometimes a temporary (local) variable is needed, e.g., for an IVML let-expression or a container iterator. We state this by $\IVMLMeta{var}(t)$, i.e., create the temporary variable of type $t$ (we don't care for the name of the variable here). For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. @@ -506,5 +508,5 @@ $c \assng pop(base)$\; \label{algEvalLoopPop} $\usedVariables \assng \setEmpty$\; \label{algEvalLoopClear} - $setAssignmentState(e, isDefault(c))$\; \label{algEvalLoopAssngState} + $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} $\problemRecords \assng \problemRecords \addSeq analyzeEvaluationResult(evaluate(e, c), \usedVariables)$\; \label{algEvalLoopAssngEval} $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} @@ -572,4 +574,5 @@ %\lIf{$value(v) \neq \undef$}{$t \assng type(value(v))$} \lIf{$dflt \neq \undef$}{$t \assng type(d)$} + \lIf{$v \neq \undef \wedge value(v) \neq \undef$}{$t \assng type(value(v))$} \uIf{$isCompound(t)$}{ $f \assng d$\; \label{algTranslateDeclarationTranslateSelf1} @@ -959,5 +962,5 @@ \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$} \If {$c \neq \undef$} { - $c \assng \createConstraint{\varSubstitutionSelfVarMapping{c}{f}}$\; + $c \assng \createConstraintConstraint{\varSubstitutionSelfVarMapping{c}{f}}$\; $add(\otherConstraints, \set{c}, true)$\; $registerConstraint(v, c)$\; @@ -1008,5 +1011,5 @@ %\end{align*} \begin{align*} -check&ContainerInitializer(c, \variableMapping) =\\ &\seqWith{\closedCases{checkContainerInitializer(e), & \text{if } isContainerInitializer(e) \\ \createConstraint{\varSubstitutionVarMapping{e}}, &\text{else}}}{e\in expr(c)} +check&ContainerInitializer(c, \variableMapping) =\\ &\seqWith{\closedCases{checkContainerInitializer(e), & \text{if } isContainerInitializer(e) \\ \createConstraintConstraint{\varSubstitutionVarMapping{e}}, &\text{else}}}{e\in expr(c)} \end{align*} \begin{align*} @@ -1155,5 +1158,5 @@ Constraint type & 3.10.1 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd}, change \tabAlg{algVarChange}\TBD{addLine} & CsCn1, CsCn2, CsCtCn1 \\ -Constraints & & \tabAlgLines{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd}& Cn1 \\ +Constraints & & \tabAlgLines{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd}& Cn1, CnCs1 \\ \IVML{self} & 3.1.6 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf1}, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf2}, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf3} & CnA3 \\ @@ -1298,7 +1301,7 @@ \begin{itemize} - \item For lists of unknown size and for the expected capacity of IVML models, use \textbf{linked lists} instead of array lists. Main operations are adding, iterating over all, and removing elements to clean up memory incrementally, i.e., linked lists can avoid performance-impacting resizing effects. Index-based access is not needed, constraints are just added and one iteration is needed to build up the constraint base or to perform reasoning. Pre-calculation of the expected size of the data structures per model seems to be unfeasible as this requires a second run over all model elements. + \item For lists of unknown size and for the expected capacity of IVML models, use \textbf{linked lists} instead of array lists. Main operations are adding, iterating over all, lookup of and removing elements to clean up memory incrementally, i.e., linked lists can avoid performance-impacting resizing effects. To speed up removal and lookup, we combined a linked list and a hashtable in a special constraint base class. Index-based access is not needed, constraints are just added and one iteration is needed to build up the constraint base or to perform reasoning. Pre-calculation of the expected size of the data structures per model seems to be unfeasible as this requires a second run over all model elements. \item Process the \textbf{constraint base} iteratively and remove processed constraints directly after processing. This again requires a linked list as otherwise incremental resizing effects can affect the performance. In summary, building the constraint base and reasoning causes peak memory effects that are better from a performance point of view than (re-)allocating big array memory blocks. - \item Avoid having too many unneeded \textbf{partitions of the constraint base} being stored during the translation in different lists, that are finally added to the constraint base. Try to directly add constraints where possible to the constraint base, e.g., for default constraints to avoid iterating over the complete constraint base before reasoning. However, due to the prioritization of the constraint types and their required sequence, this is not always possible. One alternative, a numeric prioritization of the individual constraints would require sorting the constraint base, at the new parts not the left-over constraints to be re-evaluated from a previous reasoning steps. However, implicit sorting on insertion according to priorities could help here. + \item Avoid having too many unneeded \textbf{partitions of the constraint base} being stored during the translation in different lists, that are finally added to the constraint base. Try to directly add constraints where possible to the constraint base, e.g., for default constraints to avoid iterating over the complete constraint base before reasoning. However, due to the prioritization of the constraint types and their required sequence, this is not always possible. One alternative, a numeric prioritization of the individual constraints would require sorting the constraint base, at the new parts not the left-over constraints to be re-evaluated from a previous reasoning steps. However, implicit sorting on insertion according to priorities could help here. To speed up operations for such constraint lists, we use a specific linked constraint list, which transfers the nodes the linked nodes upon adding the constraints to the constraint base (based on this specific linked list). \item Create/translate a \textbf{constraint in one step}, if required in compounds split into filling the variability mapping and then creating the constraints based on the actual mapping. \item Try to figure out whether a certain \textbf{constraint (type) is actually needed} for reasoning and avoid its translation/creation wherever feasible. \TBD{Can we move the decision about keeping a constraint from adding it to the constraint base before constraint creation. However, this requires changes/additional alternatives for different code parts.}. Thus, don't re-process or filter certain constraint types at the end (done in the initial version for default and derived type constraints), as this implies iterating multiple times over the (partial) constraint base and re-creating/throwing away constraint instances in memory. @@ -1435,13 +1438,14 @@ CnCt3 & \class{compounds/CompoundContainerTest1.ivml}\\ CnCt4 & \class{compounds/CompoundContainerTest2.ivml}\protect\footnotemark\\ +CnCs1 & \class{compounds/changingValues/changingValues.ivml}\\ ACt1 & \class{collectionConstraints/ContainerAnnotationTest.ivml}\\ ACn1 & \class{compounds/CompoundAnnotationTest.ivml}\\ AFCn1 & \class{compounds/ReferenceCompoundAnnotationTest.ivml}\\ ATCn1 & \class{compounds/DerivedCompoundAnnotationTest.ivml}\\ -CsCtCn1 & \class{compounds/CompoundConstraintTest.ivml}\\ +CsCtCn1 & \class{constraintsVariables/changingConstraints/changingConstraints.ivml}\\ CnTCt1 & \class{collectionConstraints/constraintSetDerivedCompound.ivml}\\ CnTCt2 & \class{collectionConstraints/constraintSetSetDerivedCompound.ivml}\\ CtTCt1 & \class{collectionConstraints/setDerivedSet.ivml}\\ -CtTF1 & \class{collectionConstraints/RefernceDerivedCollectionTest.ivml}\\ +CtTF1 & \class{collectionConstraints/ReferenceDerivedCollectionTest.ivml}\\ TFCnCtCsA1 & \class{collectionConstraints/QM.ivml}\\ ITCn1 & \class{operations/typedefNestedInCompoundValid.ivml}\\