Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 22) +++ /reasoner/reasoner.tex (revision 23) @@ -8,4 +8,5 @@ \newcommand\MISSING[1]{{\color{red}MISSING: #1}} \newcommand\IVML[1]{\texttt{#1}} +\newcommand\IVMLself[0]{\texttt{self}} \newcommand\IVMLMeta[1]{\texttt{\underline{#1}}} \newcommand\addSeq[0]{\oplus} @@ -34,6 +35,4 @@ \TBD{structure} - - \section{Notation/Terminology} @@ -52,17 +51,18 @@ \item usually, if not used otherwise, $v$ is variable, $d$ is declaration, $t$ is type, $val$ is value \item $\undef$ is the undefined value, e.g., an undfined constraint, type or declaration. \TBD{what is a constraint, how to denote a constraint creation in contrast to mathematical/algorithmic notation} - \item $decision(cfg, d)$ the variable from the configuration $cfg$. In contrast to a declaration, a (decision) variable is linked to a respective configuration, has an assignment state and holds the actually configured value. + \item $decision(cfg, d)$ the variable from the configuration $cfg$. In contrast to a declaration, a (decision) variable is linked to a respective configuration, has an assignment state and holds the actually configured value. $decision(v, s)$ returns the decision variable related to the nested slot $s$ of a compound variable $v$. \item $declaration(v)$ the declaration of variable $v$ \item $parent(d)$ the model element the declaration $d$ is nested within \item $type(d)$ the type of the declaration $d$, similarly $type(v) = type(declaration(v))$ and $type(val)$ the (potentially sub-)type of the value $val$ - \item $annotations(d)$ returns the set of orthogonal IVML annotations declarations for declaration $d$. Similarly, $annotations(v)$ returns the set of actual annotations for the variable $v$. There is a significant difference between $annotations(d)$ and $annotations(decision(cfg,d))$, as a declaration can only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations applied to the containing project or variables (in case of compounds or collections). + \item $annotations(d)$ returns the set of orthogonal IVML annotations declarations for declaration $d$. Similarly, $annotations(v)$ returns the set of actual annotations for the variable $v$. There is a significant difference between $annotations(d)$ and $annotations(decision(cfg,d))$, as a declaration can only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations applied to the containing project or variables (in case of compounds or collections). \item $varDeclarations(p)$ the set of all variable declarations in project $p$ \item $name(s)$ is the default value expression of slot $s$ \item $default(s)$ is the default value expression of slot $s$ \item $elements(c)$ is the set of all element values in a collection - \item $isNested(c)$ whether a collection is a nested collection - \item $isCompound(d)$, $isContainer(d)$, $isConstraint(d)$ + \item $isNested(c)$ whether a collection is a nested collection and $nestedType(c)$ is the (innermost) nested type + \item $isCompound(d)$, $isContainer(d)$, $isConstraint(d)$, $isConstraintContainer(d) = isNested(c) \wedge isConstraint(nestedType(c))$ \item $isDerived(t)$ whether $t$ is a derived type. In this case, $basis(t)$ is the basis type $t$ is derived from, else $basis(t) =\undef$. $decl(d)$ is the specific variable of a derived type used to define restricting constraints. - \item $refines(t)$ is the set of compounds directly refining compound $t$, if there are none or $t$ is not a compound $refines(t)=\emptySet$, $slots(t)$ the set of slots of a compound (nested variable declarations),$assignments(t)$ the potentially nested set of annotation assignments, i.e., if $a\in assignments(t)$ then $constraints(a)$ is defined, but may be empty, similarly for $assignments(a)$. $inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$. + \item $evals(p)$ the potentially nested set of annotation assignments of project $p$, i.e., if $e\in assignments(p)$ then $constraints(e)$ is defined, but may be empty, similarly for $assignments(e)$. $d \in assignmentData(a)$ for an assignment $a$ provides access to the name of the attribute $name(d)$ and the default value expression $default(a)$ specifying the value to be assigned to the attribute with $name(a)$. + \item $refines(t)$ is the set of compounds directly refining compound $t$, if there are none or $t$ is not a compound $refines(t)=\emptySet$, $slots(t)$ the set of slots of a compound (nested variable declarations),$assignments(t)$ the potentially nested set of annotation assignments, i.e., if $a\in assignments(t)$ then $constraints(a)$ is defined, but may be empty, similarly for $assignments(a)$. Analogously, $evals(t)$ is defined. $inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$. \item $base(t)$ the type $t$ is derived from if $isDerived(t)$, $contained(t)$ the type contained in $t$ if $isCollection(t)$ or $t$ \item $constraints(t)$ is the set of constraints defined for type $t$, similarly for a declaration $d$. Let $s$ be a set of types or declarations, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. @@ -76,5 +76,5 @@ \item $isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$ \end{itemize} -\TBD{Algorithms + implementation name} +\TBD{Algorithms + implementation name, for simplicity we ignore here that variable values can be \IVML{null}, would lead to $\undef$ on some operations and shall be filtered out/considered properly by an implementation.} @@ -92,4 +92,9 @@ \newcommand\constraintVariablesConstraints[0]{c_v} \newcommand\defaultAnnotationConstraints[0]{c_{ad}} +\newcommand\compoundConstraints[0]{c_{c}} +\newcommand\collectionCompoundConstraints[0]{c_{cc}} +\newcommand\compoundEvalConstraints[0]{c_{ce}} +\newcommand\assignmentConstraints[0]{c_{ac}} +\newcommand\variableMapping[0]{vm} \begin{itemize} @@ -99,5 +104,8 @@ \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$. \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. The constraints are appended to the constraint $base$ in this sequence to ensure that variables are properly initialized before other constraints are considered. We will discuss the relevant expressions, constraints and their transformations in detail in Section \ref{sectConstraintTranslation}. @@ -179,10 +187,10 @@ must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. -The top-level transformation is defined by Algorithm \ref{algTranslateDefaults}. It considers all variable declarations in the given project and runs Algorithm \ref{translateDeclarationDefaults} on them. +The top-level transformation is defined by Algorithm \ref{algTranslateDefaults}. It considers all variable declarations in the given project and runs Algorithm \ref{algTranslateDeclarationDefaults} on them. \begin{algorithm}[H] \SetAlgoLined \KwIn{project $p$, configuration $cfg$} - \KwData{constraint $base$, variable mapping $m$, derived type constraints $\derivedTypeConstraints$, attribute constraints $\defaultAnnotationConstraints$} + \KwData{constraint $base$, derived type constraints $\derivedTypeConstraints$, attribute constraints $\defaultAnnotationConstraints$} \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults @@ -192,13 +200,13 @@ \end{algorithm} -Algorithm \ref{translateDeclarationDefaults} 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 +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 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 \IVML{self} 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 $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 self usages with the compound access. In case that self 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. \TBD{check} - \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression. \TBD{check, also section ref} + \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} \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. @@ -206,6 +214,6 @@ \begin{algorithm}[H] \SetAlgoLined - \KwIn{configuration $cfg$, declaration $d$, variable $v$, access $ca$} - \KwData{constraint $base$, variable mapping $m$, constraint variables $\constraintVariablesConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$} + \KwIn{declaration $d$, variable $v$, access $ca$} + \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\constraintVariablesConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$} $translateDerivedDatatypeConstraints(d)$\; @@ -214,6 +222,6 @@ \uIf{$isCompound(t)$}{ \lIf{$ dflt \neq \undef $}{$t = type(dflt)$} - \TBD{$resolveCompoundDefaultValueForDeclaration(d, v, ca, t)$}\; - \lIf{$ dflt \neq \undef $}{$ dflt \assng deflt|_{self=d, m}$} + $translateCompoundDefaults(d, v, ca, t)$\; + \lIf{$ dflt \neq \undef $}{$ dflt \assng deflt|_{\IVMLself{}=d, \variableMapping}$} } \ElseIf{$ dflt \neq \undef $}{ \uIf{$ isContainer(type(d)) $}{ @@ -223,9 +231,9 @@ } }\ElseIf{$ca \neq \undef$}{ - \lIf{$self \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} - $dflt \assng dflt|_{self=ca}$\; + \lIf{$\IVMLself{} \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} + $dflt \assng dflt|_{\IVMLself =ca}$\; } } - $c_c \assng c_c \cup translateCollectionCompoundConstraints(d, v, \undef)$\; + $\collectionCompoundConstraints \assng \collectionCompoundConstraints \cup translateCollectionCompoundConstraints(d, v, \undef)$\; \If{$isContainer(t) \wedge isDerived(contained(t))$}{ $translateCollectionDerivedDatatypeConstraints(d, \undef)$\; @@ -238,5 +246,5 @@ } } - \caption{Translating default value expressions to constraints (\IVML{translateDeclarationDefaults}).}\label{translateDeclarationDefaults} + \caption{Translating default value expressions to constraints (\IVML{translateDeclarationDefaults}).}\label{algTranslateDeclarationDefaults} \end{algorithm} @@ -283,11 +291,121 @@ \end{algorithm} + + \subsection{Compound default constraints} +Translating a compound into all its constraints requires considering all slots, all constraints defined within a compound, as well as all supported nested structures, such as eval blocks or attribute value assignment blocks. In particular, if the IVML keyword \IVMLself{} is used, it must be replaced by the actual variable of the respective compound type. First, we define some helper functions, then the translation algorithms. + %Expressions may be simple variables, calculations or operation calls, in compounds also using the predefined variable \texttt{self} indicating the actual instance of the respective compound. These constraints must be evaluated upon each variable instance, i.e., for top-level basic variables, top-level compound variables, compound values within compounds as well as compound values within container initialiers, each potentially with a different access expression to make the variable unique. +The function $allAssignmentConstraints(a)$ collects all the assignment constraints within an assignment $a$ considering potentially further nested assignment structures: +% +\begin{align*} +all&AssignmentConstraints(a) = \\ + &constraints(a) \cup \setWith{allAssignmentConstraints(b)}{b \in assignments(a)} +\end{align*} +% +Similarly, the function $allEvalConstraints(e)$ collects all constraints stated in \IVML{eval} blocks nested in the \IVML{eval} block $e$. +% +\begin{align*} +all&EvalConstraints(e) = \\ + &constraints(e) \cup \setWith{allEvalConstraints(f)}{f \in evals(e)} +\end{align*} +% +If $isCompound(t)$, all nested eval constraints within a compound $t$ can be enumerated using +% +\begin{equation*} + allEvalConstraints(t) = \bigcup_{e\in evals(t)}{allEvalConstraints(e)} +\end{equation*} +% +Moreover, he function $allCompoundConstraints(t, b)$ collect all constraints defined a compound type $t$. This includes the directly defined constraints, the constraints stemming from inherited constraint variables, the refined compound constraints and all constraints in (nested) assignment environments. Parameter $b$ is just used to indicate whether the function is called recursively, i.e., to collect constraint variables only directly for $t$. \TBD{Why not constraint variables via refines?} +% +\begin{align*} +all&CompoundConstraints(t, b) = constraints(t)\text{ }\cup \\ + &\closedCases{\setWith{\createConstraint{s}}{s\in inheritedSlots(t) \wedge isConstraint(type(s))}, & \text{if } b \\ \set{}, &\text{else}} \cup \\ + &\setWith{getAllCompoundContraints(r, false)}{r \in refines(t)} \cup \\ + &{allAssignmentConstraints(assignments t)} +\end{align*} +% +Algorithm \ref{algTranslateCompoundDefaults} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. + +First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors to the 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}. + +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??}). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$} + \KwData{compound (eval) constraints $\compoundConstraints$ and $\compoundEvalConstraints$, variable mapping $\variableMapping$} + + \ForAll{s \iterAssng slots(v)} { %actual slots + $c \assng (s, \createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}})$\; + $\variableMapping \assng \variableMapping \cup \set{c}$\; + $translateDeclarationDefaults(s, decision(v, s), c)$\; + } + \ForAll{s \iterAssng slots(v)} { %actual slots + \If{$isConstraintContainer(type(s))$} { + $\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}$\; + } + \If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{ + $\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}$\; + } + $\compoundConstraints \assng \compoundConstraints \cup translateCollectionCompoundConstraints(s, v, \variableMapping[s])$\; + } + \ForAll{$a \iterAssng assignments(t)$}{ + $translateAnnotationAssignments(a, \undef, ca)$\; + } + $\compoundConstraints \assng \compoundConstraints \cup \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}$\; + $\compoundEvalConstraints \assng \compoundEvalConstraints \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}$\; + + \caption{Translating annotation defaults (\IVML{translateCompoundDefaults}).}\label{algTranslateCompoundDefaults} +\end{algorithm} + +We translate annotation assignments in two steps, the translation of an individual assignment as well as the translation of an assignment block (in Algorithm \ref{algTranslateAnnotationAssignments}). The translation of a single assignment from an assignment data $a$ leads to the creation of an assignment constraint as shown below: + +\begin{align*} + translate&AnnotationAssignment(a, d, ca) = \createConstraint{\IVML{assign}(\\ + &\IVMLMeta{ann}(\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}, annotation(d, name(a))), \\ + & default(a))} +\end{align*} + +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 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). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{assignment block $a$, effective assignment data $ea$, compound access $ca$} + \KwData{assignment constraints $\assignmentConstraints$} + + $ea \assng ea \cup assignmentData(a)$\; + \ForAll{$e \iterAssng ea$}{ + \ForAll{$d \iterAssng slots(a)$} { + $\assignmentConstraints \assng \assignmentConstraints \cup \set{translateAnnotationAssignment(e, d, ca)}$\; + \If{$isCompound(type(d))$} { + \ForAll{$s \iterAssng slots(d)$} { + $b \assng translateAnnotationAssignment(e, s, \IVMLMeta{acc}(\closedCases{d, & \text{if } ca = \undef\\ ca, &\text{else}}, s))$\; + $\assignmentConstraints \assng \assignmentConstraints \cup \set{b}$\; + } + } + } + } + + \ForAll{$b \iterAssng assignments(a)$} { + $translateAnnotationAssignments(b, ea, ca)$\; + } + + \caption{Translating attribute assignments(\IVML{translateAnnotationAssignments}).}\label{algTranslateAnnotationAssignments} +\end{algorithm} + +\TBD{check whether $c_c$ sets are filled incrementally or only at one position (add vs. assign); use $d_?$ as notation for default constraint sets?; are only default constraints translated above or also other constraints (mixed) - can we then join the translations? Can we change the translation sequence in a way that the constraint basis is sufficient (avoiding the different constraint sets)?} + + + \subsection{Collection default constraints}\label{deflt_collections} -Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundCollection} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested collection). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the collection using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVML{self} substituted by the iterator variable $i$. +Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundCollection} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested collection). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the collection using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$. \begin{algorithm}[H] @@ -296,5 +414,5 @@ \KwData{deferred default constraints $\deferredDefaultConstraints$} \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{ - $\deferredDefaultConstraints \assng \deferredDefaultConstraints \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{self=i})}$\; + $\deferredDefaultConstraints \assng \deferredDefaultConstraints \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i})}$\; } @@ -322,24 +440,8 @@ \end{algorithm} -We introduce two helper functions: $allAssignmentConstraints(a)$ is collecting all the assignment constraints within an assignment $a$ considering potentially further nested assignment structures: - -\begin{align*} -all&AssignmentConstraints(a) = \\ - &constraints(a) \cup \setWith{allAssignmentConstraints(b)}{b \in assignments(a)} -\end{align*} - -The second function $allCompoundConstraints(t, b)$ collect all constraints defined a compound type $t$. This includes the directly defined constraints, the constraints stemming from inherited constraint variables, the refined compound constraints and all constraints in (nested) assignment environments. Parameter $b$ is just used to indicate whether the function is called recursively, i.e., to collect constraint variables only directly for $t$. \TBD{Why not constraint variables via refines?} - -\begin{align*} -all&CompoundConstraints(t, b) = constraints(t)\text{ }\cup \\ - &\closedCases{\setWith{\createConstraint{s}}{s\in inheritedSlots(t) \wedge isConstraint(type(s))}, & \text{if } b \\ \set{}, &\text{else}} \cup \\ - &\setWith{getAllCompoundContraints(r, false)}{r \in refines(t)} \cup \\ - &{allAssignmentConstraints(assignments t)} -\end{align*} - \begin{algorithm}[H] \SetAlgoLined \KwIn{compound type $t$, declared compound type $dt$, declaration $d$, compound access $ca$} - \KwData{variable mapping $m$} + \KwData{variable mapping $\variableMapping$} \KwOut{resulting constraints $c$} @@ -347,10 +449,10 @@ $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$ \ForAll{s \iterAssng slots(t)} { - $m \assng m \cup (s, \createExpression{\IVMLMeta{acc}(v,s)})$\; + $\variableMapping \assng \variableMapping \cup (s, \createExpression{\IVMLMeta{acc}(v,s)})$\; } \ForAll{$e \iterAssng getAllCompoundConstraints(t)$} { $coll \assng\createExpression{\closedCases{ca, & \text{if } ca = \undef \\ d, &\text{else}}}$\; $coll \assng\createExpression{coll.\closedCases{\IVML{selectByKind}(a, t), & \text{if } t \neq dt \\ &\text{else}}}$\; - $c\assng c \cup \createConstraint{coll\rightarrow\IVML{forAll}(i|\text{ }e|_{m})}$\; + $c\assng c \cup \createConstraint{coll\rightarrow\IVML{forAll}(i|\text{ }e|_{\variableMapping})}$\; }