Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 20) +++ /reasoner/reasoner.tex (revision 21) @@ -8,4 +8,5 @@ \newcommand\MISSING[1]{{\color{red}MISSING: #1}} \newcommand\IVML[1]{\texttt{#1}} +\newcommand\IVMLMeta[1]{\texttt{\underline{#1}}} \newcommand\addSeq[0]{\oplus} \newcommand\addSeqNoDupl[0]{\uplus} @@ -19,4 +20,6 @@ \newcommand\createDefaultConstraint[1]{\langle_d\text{ } #1 \rangle} \newcommand\createInternalConstraint[1]{\langle_i\text{ } #1 \rangle} +\newcommand\createExpression[1]{\langle\langle #1 \rangle\rangle} +\newcommand\closedCases[1]{\left.\begin{cases}#1\end{cases}\right\}} \begin{document} @@ -61,5 +64,5 @@ \item $isCompound(d)$, $isContainer(d)$, $isConstraint(d)$ \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$ + \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 $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}$. @@ -68,5 +71,5 @@ \item $allRefines(t) = \begin{cases}\emptySet, & \text{if } refines(t) = \emptySet \\ allRefines(t) \cup \bigcup_{u\in refines(t)} allRefines(u), & \text{else}\\ \end{cases}$ \item $allRefines^+(t) = \begin{cases}allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ \emptySet, & \text{else} \\ \end{cases}$ - \item Creating a constraint through OCL function call notation in angle brackets, e.g., $\createConstraint{\IVML{assign}(x, 25)}$ represents the IVML constraint \IVML{x = 25;}. If the constraint is marked as a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$, if it is an internal \TBD{clarify semantics }constraint for reasoning we use $\createInternalConstraint{\IVML{assign}(x, 25)}$. We indicate IVML operations in teletype font. + \item A constraint is a boolean expression that requires to be evaluated to \IVML{true}. Creating a constraint through OCL function call notation in angle brackets, e.g., $\createConstraint{\IVML{assign}(x, 25)}$ represents the IVML constraint \IVML{x = 25;} (knowing that the assignment IVML assignment operation returns a boolean value indicating its success). If the constraint is marked as a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$, if it is an internal \TBD{clarify semantics }constraint for reasoning we use $\createInternalConstraint{\IVML{assign}(x, 25)}$. We indicate IVML operations in teletype font. We denote a partial expression for incrementally building a constraint by $createExpression{expr}$ and indicate IVML meta operations for creating expression parts as follows: $\createExpression{\IVMLMeta{var}(i, t)}$ creates a temporary variable $i$ of type $t$. $\createExpression{\IVMLMeta{acc}(c, s)}$ creates an accessor $c.s$, e.g., to access slot $s$ on compound $c$ (implicitly requiring $isCompound(c) \wedge s\in slots(c)$). \item $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$ the set of (contained) types used in collection $c$ \item $parentCompound(d) = \begin{cases} parent(d), & \text{if } parent(d) \neq \undef \wedge{} isCompound(parent(d)) \\ parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ \undef, & \text{else}\end{cases}$ @@ -224,5 +227,5 @@ } } - $c_c \assng c_c \cup \TBD{collectionCompoundConstraints(d, v, \undef)}$\; + $c_c \assng c_c \cup collectionCompoundConstraints(d, v, \undef)$\; \If{$isContainer(t) \wedge isDerived(contained(t))$}{ $translateCollectionDerivedDatatypeConstraints(d, \undef)$ @@ -232,5 +235,5 @@ \lIf{$ ca == \undef $}{$\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup (\createConstraint{dflt}, v)$} }\Else{ - $dfltS \assng dfltS \cup \createDefaultConstraint{\IVML{assign}(\left.\begin{cases}ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}\end{cases}\right\}, deflt)}$\; + $dfltS \assng dfltS \cup \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)}$\; } } @@ -261,5 +264,5 @@ $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\; - $\derivedTypeConstraints \assng \derivedTypeConstraints \cup \setWith{\createConstraint{\left.\begin{cases}d, & \text{if } ca = \undef \\ ca, &\text{else}\end{cases}\right\}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}$\; + $\derivedTypeConstraints \assng \derivedTypeConstraints \cup \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}$\; \caption{Translating constraints for derived collection types (\IVML{translateCollectionDerivedDatatypeConstraints}).}\label{algTranslateCollectionDerivedDatatypeConstraints} \end{algorithm} @@ -276,15 +279,13 @@ $a \assng annotations(decision(cfg, d))$\; - $\defaultAnnotationConstraints \assng \defaultAnnotationConstraints \cup \setWith{\createDefaultConstraint{\IVML{assign}(\left.\begin{cases}d.r, & \text{if } ca = \undef \\ ca.r, &\text{else}\end{cases}\right\}, default(r))}}{r\in a}$\; + $\defaultAnnotationConstraints \assng \defaultAnnotationConstraints \cup \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}$\; \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults} \end{algorithm} -\subsection{Default expressions} - -\subsubsection{Compound default constraints} +\subsection{Compound default constraints} %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. -\subsubsection{Collection default constraints}\label{deflt_collections} +\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$. @@ -295,10 +296,67 @@ \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}(i|\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)|_{self=i})}$\; } - \caption{Translates and collects defaults in compound collections (\IVML{translateDefaultsCompoundCollection}).}\label{algTranslateDefaultsCompoundCollection} -\end{algorithm} - + \caption{Translating defaults in compound collections (\IVML{translateDefaultsCompoundCollection}).}\label{algTranslateDefaultsCompoundCollection} +\end{algorithm} + +C + + + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, compound access $ca$} + \KwOut{resulting constraints $c$} + + $c \assng \set$\; + \If{$isContainer(type(d))$}{ + $tc \assng contained(type(d))$\; + \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in elements(v)} \backslash\set{\undef}$}{ + \If{$isCompound(t)$}{ + \TBD{$c \assng c \cup translateCollectionCompoundConstraints(t, tc, d, ca)$} + } + } + } + + \caption{Translating compound constraints from a collection (\IVML{translateCollectionCompoundConstraints}).}\label{algTranslateCollectionCompoundConstraints} +\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$. + +\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$} + \KwOut{resulting constraints $c$} + + $c \assng \set$\; + $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$ + \ForAll{s \iterAssng slots(t)} { + $m \assng m \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})}$\; + } + + \caption{Translating compound constraints from a collection (\IVML{translateCollectionCompoundConstraints}).}\label{algTranslateCollectionCompoundConstraints} +\end{algorithm}