Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 30) +++ /reasoner/reasoner.tex (revision 31) @@ -88,16 +88,9 @@ \newcommand\defaultConstraints[0]{c_d} \newcommand\deferredDefaultConstraints[0]{c_{dd}} -\newcommand\derivedTypeConstraints[0]{c_r} -\newcommand\constraintVariablesConstraints[0]{c_v} -\newcommand\defaultAnnotationConstraints[0]{c_{ad}} -\newcommand\compoundConstraints[0]{c_{c}} -\newcommand\collectionCompoundConstraints[0]{c_{ccc}} -\newcommand\collectionConstraints[0]{c_{cc}} -\newcommand\compoundEvalConstraints[0]{c_{ce}} -\newcommand\assignmentConstraints[0]{c_{ac}} -\newcommand\assignedAttributeConstraints[0]{c_{aa}} -\newcommand\unresolvedConstraints[0]{c_{u}} -\newcommand\topLevelConstraints[0]{c_{t}} +\newcommand\usualConstraintsStageThree[0]{c_{u3}} +\newcommand\usualConstraintsStageTwo[0]{c_{u2}} +\newcommand\usualConstraintsStageOne[0]{c_{u1}} \newcommand\variableMapping[0]{vm} +\newcommand\relevantConstraints[0]{r_t} The reasoner performs forward reasoning, i.e., it identifies all constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. @@ -109,12 +102,8 @@ \begin{itemize} \item Default constraints $\defaultConstraints$ containing constraints setting the default values. - \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$ \TBD{also $\defaultAnnotationConstraints$?}. - \item Default annotation constraints $\defaultAnnotationConstraints$ relating to default values of annotations. - \item Constraints $\derivedTypeConstraints$ representing instantiated restricting constraints from derived types. - \item Constraints representing constraint variables $\constraintVariablesConstraints$. - \item Constraints related to compound types and their slots $\compoundConstraints$. - \item Constraints related to compound types used in collections $\collectionCompoundConstraints$. - \item Top-level constraints $\topLevelConstraints$ - \item TBD{check: $\assignedAttributeConstraints$} + \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$ \TBD{also $\usualConstraintsStageThree$?}. + \item Default annotation constraints and assigned annotation constraints $\usualConstraintsStageThree$. + \item Usual constraints such as compound types used in collections, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints $\usualConstraintsStageTwo$. + \item Usual constraints such as top-level project, derived type constraints$\usualConstraintsStageOne$ \end{itemize} Further, the algorithm maintains a global variable mapping $\variableMapping$, a map of already processed variables to accessors so that later processed complex expressions can be substituted with the correct accessors. @@ -127,5 +116,5 @@ \SetAlgoLined \KwIn{configuration $cfg$, incremental $inc$, \TBD{consider frozen}} - \KwData{problem records $m$, relevant constraints $t$ \TBD{$t$??}} + \KwData{problem records $m$, relevant constraints $\relevantConstraints$ \TBD{$t$??}} \KwResult{Reasoning result $r$} @@ -140,5 +129,5 @@ $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\; } - $addConstraints(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\; + $add(\usualConstraintsStageOne,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\; \ForAll{a \iterAssng assignments(p)}{ $translateAnnotationAssignments(a, \undef, \undef)$\; @@ -186,5 +175,5 @@ \SetAlgoLined \KwIn{decision variable $v$} - \KwData{scope assignments $a$, relevant constraints $t$} + \KwData{scope assignments $a$, relevant constraints $\relevantConstraints$} \If{$\neg isLocal(v)$}{ @@ -210,18 +199,18 @@ Algorithm \ref{algTranslateDeclarationDefaults} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm \begin{itemize} - \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\derivedTypeConstraints$. - \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\defaultAnnotationConstraints$ + \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\usualConstraintsStageOne$. + \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\usualConstraintsStageThree$ \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 Collects all transformed collection compounds based on the actual used types if $d$ is a collection. If $d$ is a collection over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_collections}). \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. - \item Translates usual collection compound constraints independent of any default value expression and stores them into $\collectionCompoundConstraints$. \TBD{check} - \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\compoundConstraints$. \TBD{check, also section ref} + \item Translates usual collection compound constraints independent of any default value expression and stores them into $\usualConstraintsStageTwo$. \TBD{check} + \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\usualConstraintsStageTwo$. \TBD{check, also section ref} \end{itemize} -Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $\constraintVariablesConstraints$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $\defaultConstraints$ or $\deferredDefaultConstraints$ as determined before. +Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $\usualConstraintsStageTwo$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $\defaultConstraints$ or $\deferredDefaultConstraints$ as determined before. \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$, variable $v$, access $ca$, incremental $inc$} - \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\constraintVariablesConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$} + \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\usualConstraintsStageTwo$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$} $translateDerivedDatatypeConstraints(d)$\; @@ -245,5 +234,5 @@ } } \uElse{$ dflt \assng \undef $\;} - $\collectionCompoundConstraints \assng \collectionCompoundConstraints \cup translateCollectionCompoundConstraints(d, v, \undef)$\; + $add(\usualConstraintsStageTwo, translateCollectionCompoundConstraints(d, v, \undef), true)$\; \If{$isContainer(t) \wedge isDerived(contained(t))$}{ $translateCollectionDerivedDatatypeConstraints(d, \undef)$\; @@ -251,7 +240,9 @@ \If{$ deflt \neq \undef $}{ \uIf{$isConstraint(t)$}{ - \lIf{$ ca == \undef $}{$\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup (\createConstraint{dflt}, v)$} + \lIf{$ ca == \undef $}{ + $add(\usualConstraintsStageTwo, \createConstraint{dflt}, true)$\; + $\relevantConstraints \assng \relevantConstraints \cup (\createConstraint{dflt}, v)$} }\Else{ - $addConstraint(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)})$\; + $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)})$\; } } @@ -262,13 +253,13 @@ \subsection{Derived types}\label{sectDerivedTypes} -In IVML, a derived datatype $d$ is defined based on a known base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ using a local variable $decl(d)$ to express the constraints. \TBD{decl(d) is not introduced above. Needed?}. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. If a variable $v$ is declared of type $d$, all constraints defined for $d$ over $b$ and, transitively over the base types of $b$ apply. Whether these constraints are fullfilled depends on the actual value of $v$. Therefore, we translate all constraints defined on type $d$ (of $v$) to constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for basis types substituting in each constraint the respective local variable by the actual variable $d$. The resulting constraints are stored in the gobal set of derived type constraints $\derivedTypeConstraints$. +In IVML, a derived datatype $d$ is defined based on a known base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ using a local variable $decl(d)$ to express the constraints. \TBD{decl(d) is not introduced above. Needed?}. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. If a variable $v$ is declared of type $d$, all constraints defined for $d$ over $b$ and, transitively over the base types of $b$ apply. Whether these constraints are fullfilled depends on the actual value of $v$. Therefore, we translate all constraints defined on type $d$ (of $v$) to constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for basis types substituting in each constraint the respective local variable by the actual variable $d$. The resulting constraints are stored in $\usualConstraintsStageOne$. \begin{algorithm}[H] \SetAlgoLined \KwIn{declaration $d$} - \KwData{derived type constraints $\derivedTypeConstraints$} + \KwData{derived type constraints $\usualConstraintsStageOne$} $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\; - $addConstraints(\derivedTypeConstraints, \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\; + $add(\usualConstraintsStageOne, \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\; \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} \end{algorithm} @@ -279,8 +270,8 @@ \SetAlgoLined \KwIn{derived type $t$, declaration $d$, compound access $ca$} - \KwData{derived type constraints $\derivedTypeConstraints$} + \KwData{derived type constraints $\usualConstraintsStageOne$} $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\; - $addConstraints(\derivedTypeConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\; + $add(\usualConstraintsStageOne, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\; \caption{Translating constraints for derived collection types (\IVML{translateCollectionDerivedDatatypeConstraints}).}\label{algTranslateCollectionDerivedDatatypeConstraints} \end{algorithm} @@ -294,8 +285,8 @@ \SetAlgoLined \KwIn{configuration $cfg$, declaration $d$, compound access $ca$} - \KwData{attribute constraints $\defaultAnnotationConstraints$} + \KwData{constraints $\usualConstraintsStageThree$} $a \assng annotations(decision(cfg, d))$\; - $addConstraints(\defaultAnnotationConstraints, \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}, false)$\; + $add(\usualConstraintsStageThree, \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}, false)$\; \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults} \end{algorithm} @@ -342,5 +333,5 @@ First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclarationDefaults}. -Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\constraintVariablesConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound collection, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateCollectionCompoundConstraints}. +Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\usualConstraintsStageTwo$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound collection, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateCollectionCompoundConstraints}. Finally, the algorithm translates all attribute assignments using Algorithm \ref{algTranslateAnnotationAssignments}, all direct compound constraints (substituting \IVMLself{} and registered variables), and translates and collects all eval constraints (\TBD{no self??}). @@ -349,5 +340,5 @@ \SetAlgoLined \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$} - \KwData{compound (eval) constraints $\compoundConstraints$ and $\compoundEvalConstraints$, variable mapping $\variableMapping$} + \KwData{constraints $\usualConstraintsStageTwo$, variable mapping $\variableMapping$} \ForAll{s \iterAssng slots(v)} { %actual slots @@ -360,10 +351,10 @@ \ForAll{s \iterAssng slots(v)} { %actual slots \If{$isConstraintContainer(type(s))$} { - $addConstraints(\constraintVariablesConstraints, \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}, true)$\; + $add(\usualConstraintsStageTwo, \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}, true)$\; } \If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{ - $addConstraints(\constraintVariablesConstraints, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\; - } - $addConstraints(\compoundConstraints, translateCollectionCompoundConstraints(s, v, \variableMapping[s]), true)$\; + $add(\usualConstraintsStageTwo, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\; + } + $add(\usualConstraintsStageTwo, translateCollectionCompoundConstraints(s, v, \variableMapping[s]), true)$\; } \If{$\neg inc$} { @@ -372,6 +363,6 @@ } } - $addConstraints(\compoundConstraints, \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}, true)$\; - $addConstraints(\compoundEvalConstraints, \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; + $add(\usualConstraintsStageTwo, \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}, true)$\; + $add(\usualConstraintsStageTwo, \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; \caption{Translating annotation defaults (\IVML{translateCompoundDefaults}).}\label{algTranslateCompoundDefaults} @@ -388,15 +379,15 @@ If a compound accessor $ca$ is given, it takes precedence and the annotation is accessed through $ca$ and the respective annotation defined for the given variable declaration $d$ through ($annotation(d, name(a))$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$ (\TBD{are variables or declarations mapped}), $d$ is taken as accessor, else the actual accessor in $\variableMapping$. The accessor is used as the left side of an IVML assignment, the right side (value) is made up of the default value expression given by the assignment data $a$. -Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it creates the variable mapping. When the mapping is complete, it performs the transformation defined above and collects the created constraints in the set of assignment constraints $\assignmentConstraints$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). +Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it creates the variable mapping. When the mapping is complete, it performs the transformation defined above and collects the created constraints in $\usualConstraintsStageThree$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). \begin{algorithm}[H] \SetAlgoLined \KwIn{assignment block $a$, effective assignment data $ea$, compound access $ca$} - \KwData{assignment constraints $\assignmentConstraints$} + \KwData{constraints $\usualConstraintsStageThree$} $ea \assng ea \cup assignmentData(a)$\; \ForAll{$e \iterAssng ea$}{ \ForAll{$d \iterAssng slots(a)$} { - $addConstraints(\assignmentConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false)$\; + $add(\usualConstraintsStageThree, \set{translateAnnotationAssignment(e, d, ca)}, false)$\; \If{$isCompound(type(d))$} { \ForAll{$s \iterAssng slots(d)$} { @@ -406,5 +397,5 @@ \ForAll{$s \iterAssng slots(d)$} { $b \assng translateAnnotationAssignment(e, s, c)$\; - $addConstraint(\assignmentConstraints, \set{b})$\; + $add(\usualConstraintsStageThree, \set{b})$\; } } @@ -432,5 +423,5 @@ \KwData{deferred default constraints $\deferredDefaultConstraints$} \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{ - $addConstraint(\deferredDefaultConstraints, \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i, \variableMapping})})$\; + $add(\deferredDefaultConstraints, \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i, \variableMapping})})$\; } @@ -487,14 +478,17 @@ \begin{algorithm}[H] \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$} - \KwData{variable mapping $\variableMapping$} + \KwData{variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$ } \If{$check$}{ \If{$isContainerInitializer(c)$} { - $\collectionConstraints \assng \collectionConstraints \addSeq checkCompoundInitializer(c, m)$\; + $\usualConstraintsStageTwo \assng \usualConstraintsStageTwo \addSeq checkCompoundInitializer(c, m)$\; }\ElseIf{$isCompoundInitializer(c)$}{ - $\collectionConstraints \assng \collectionConstraints \addSeq checkCompoundInitializer(c, m)$\; + $\usualConstraintsStageTwo \assng \usualConstraintsStageTwo \addSeq checkCompoundInitializer(c, m)$\; } } $s \assng s \addSeq c$\; - \caption{Records and analyzes a constraint (\IVML{addConstraint}).}\label{algAddConstraint} + \If{$\neg isSimpleConstraint(c)$}{ + $\relevantConstraints \assng \relevantConstraints \cup \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; % assignConstraintsToVariables + } + \caption{Records and analyzes a constraint (add, \IVML{addConstraint}).}\label{algAddConstraint} \end{algorithm} @@ -515,6 +509,6 @@ \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$} \KwData{variable mapping $\variableMapping$} - \ForAll{d \iterAssng c} { - addConstraint(s, d, c); + \ForAll{$d \iterAssng c$} { + $add(s, d, c)$\; } \caption{Records and analyzes a constraint sequence.}\label{algAddConstraints} @@ -524,22 +518,15 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{project $p$, relevant constraints $t$ \TBD{??}, incremental $inc$, \TBD{consider frozen}} - \KwData{constraint $base$ , variable mapping $\variableMapping$ \TBD{join, reorder, beautify, leave out non-incremental on-the-fly}} - - $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \derivedTypeConstraints \addSeq\topLevelConstraints \addSeq \compoundEvalConstraints \addSeq \compoundConstraints \addSeq \constraintVariablesConstraints \addSeq \collectionCompoundConstraints \addSeq \collectionConstraints$\; - $t \assng t \cup \setWith{\mapEntry{v}{c}}{v\in variables(c) \wedge c\in c_s}$\; % assignConstraintsToVariables - $c_s \assng \setWith{c}{c\in c_s \wedge (\neg inc \vee (inc \wedge \neg isAssignmentConstraint(c)))}$\; - $base \assng c_s \addSeq \defaultAnnotationConstraints \addSeq \assignedAttributeConstraints$\; + \KwIn{project $p$, relevant constraints $\relevantConstraints$ \TBD{??}, incremental $inc$, \TBD{consider frozen}} + \KwData{constraint $base$ , variable mapping $\variableMapping$} + + $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \usualConstraintsStageOne \addSeq \usualConstraintsStageTwo$ \TBD{add with flag}\; + % $c_s \assng \setWith{c}{c\in c_s \wedge (\neg inc \vee (inc \wedge \neg isAssignmentConstraint(c)))}$\; + $base \assng c_s \addSeq \usualConstraintsStageThree$\; $\defaultConstraints \assng \set{}$\; $\deferredDefaultConstraints \assng \set{}$\; - $\topLevelConstraints \assng \set{}$\; - $\derivedTypeConstraints \assng \set{}$\; - $\compoundConstraints \assng \set{}$\; - $\compoundEvalConstraints \assng \set{}$\; - $\constraintVariablesConstraints \assng \set{}$\; - $\collectionCompoundConstraints \assng \set{}$\; - $\collectionConstraints \assng \set{}$\; - $\defaultAnnotationConstraints \assng \set{}$\; - $\assignedAttributeConstraints \assng \set{}$\; + $\usualConstraintsStageOne \assng \set{}$\; + $\usualConstraintsStageTwo \assng \set{}$\; + $\usualConstraintsStageThree \assng \set{}$\; \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}