Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 84) +++ /reasoner/reasoner.tex (revision 85) @@ -587,5 +587,5 @@ -\subsection{Compound constraints}\label{sectCompoundDefaults} +\subsection{Compound types}\label{sectCompoundDefaults} A compound can define constraints in several places, namely through types and defaults of its slots and annotations (including constraint variables as well as refined slots and annotations), as constraints listed directly within a compound, within assignment-blocks or within eval-blocks. For slots and annotations we can resort to Algorithm \ref{algTranslateDeclaration}, i.e., compound types, derived types, constraint variables and collections, while for the remaining constraints, we must visit these structures, instantiate and collect the respective constraints. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. In particular, if the IVML keyword \IVMLself{} is used within a constraint, it must be substituted by the actual variable of the respective compound type. Moreover, it is important to recall that a variable $v$ of type $type(v)$ can contain instances of any refined type $allRefines^+(t)$, and in this case the translation must consider the default values of the potentially larger slot, additional constraints and nested structures. @@ -617,8 +617,8 @@ \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t_c)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping} $registerMapping(\variableMapping, s, x)$\; \ForAll{$a \iterAssng annotations(s)$}{ - $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t, a), &\text{else}}}$\; + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t, a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping} $registerMapping(\variableMapping, a, x)$\; } @@ -660,5 +660,5 @@ \end{algorithm} -\subsection{Container constraints}\label{sectContainerDefaults} +\subsection{Container types}\label{sectContainerDefaults} Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing (the contents of) a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. @@ -912,5 +912,5 @@ %\begin{adjustbox}{angle=90} \centering -\begin{tabular}{|p{4cm}|r||p{6cm}|p{3cm}|} +\begin{tabular}{|p{3.5cm}|c||p{6cm}|p{3.5cm}|} \hline \textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation Trace} & \textbf{Test}\\ @@ -923,26 +923,33 @@ Partial evaluation & 2.2.5.3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelEvals} & Ev1, Ev2 \MISSING{prio?}\\ \hline - \multicolumn{4}{|c|}{Types (typed decision variable, starting in \tabAlg{algTranslateDeclaration}}\\ -\hline -Integer type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & \\ -Double type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & \\ + \multicolumn{4}{|c|}{Types (typed decision variable, starting in \tabAlg{algTranslateDeclaration})}\\ +\hline +Integer type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & I1, I2\\ +Real type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & R1, R2\\ Boolean type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & B1, B2, B3 \\ -String type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & \\ -Enum type & 2.1.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectotationOthers} & \\ +String type & 2.1.3.1 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & S1, S2\\ +Enum type & 2.1.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & E1, E2\\ Reference type & 2.2.3.2 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault}, cf. Sect. \ref{sectNotationOthers} & \\ \TBD{} Derived type & 2.1.3.4 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints}, type specific translation, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationConstraintVariableConstraint} or \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \\ Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers}, constraint value in \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationConstraintVariableConstraint} & \\ -Compound type & 2.1.3.5 & complex value: Alg. \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateCompound} $\rightarrow$ Alg.\ref{algTranslateCompoundDeclaration} & \\ -+ Integer type & 2.1.3.1 & no specific constraints, cf. Section \ref{sectNotationOthers} & \\ -+ Double type & 2.1.3.1 & no specific constraints, cf. Section \ref{sectNotationOthers} & \\ -+ Boolean type & 2.1.3.1 & no specific constraints, cf. Section \ref{sectNotationOthers} & BCo1, BCo2, BCo3 \\ -+ String type & 2.1.3.1 & no specific constraints, cf. Section \ref{sectNotationOthers} & \\ -+ Enum type & 2.1.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & \\ -+ Derived type & 2.1.3.4 & Alg. \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationDerivedDatatype} $\rightarrow$ Alg.\ref{algTranslateDerivedDatatypeConstraints} & \\ -+ Compound type & 2.1.3.5 & Alg. \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateCompound} $\rightarrow$ Alg.\ref{algTranslateCompoundDeclaration} & \\ -+ Container type & 2.1.3.3 & & \\ -+ Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & \\ -+ Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers}, constraint value in \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationConstraintVariableConstraint} via compound access line \ref{algTranslateDeclarationTranslateInCompound} & \\ +\hline + \multicolumn{4}{|c|}{Compound types (typed decision variable, starting with \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateCompound}\tabAlgFollow\tabAlg{algTranslateCompoundDeclaration})}\\ +\hline +Integer type & 2.1.3.1 & \tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingVarMapping}, \tabAlgLine{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationTranslateSlotsV}\tabAlgFollow +\tabAlg{algTranslateDeclaration} & ICo1, ICo2\\ +Real type & 2.1.3.1 & \tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingVarMapping}, \tabAlgLine{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationTranslateSlotsV}\tabAlgFollow +\tabAlg{algTranslateDeclaration} & RCo1, RCo2\\ +Boolean type & 2.1.3.1 & \tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingVarMapping}, \tabAlgLine{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationTranslateSlotsV}\tabAlgFollow +\tabAlg{algTranslateDeclaration} & BCo1, BCo2, BCo3 \\ +String type & 2.1.3.1 & \tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingVarMapping}, \tabAlgLine{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationTranslateSlotsV}\tabAlgFollow +\tabAlg{algTranslateDeclaration} & SCo1, SCo2\\ +Enum type & 2.1.3.2 & \tabAlgLine{algRegisterCompoundMapping}{algRegisterCompoundMappingVarMapping}, \tabAlgLine{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationTranslateSlotsV}\tabAlgFollow +\tabAlg{algTranslateDeclaration} & ECo1, ECo2\\ +Derived type & 2.1.3.4 & Alg. \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationDerivedDatatype} $\rightarrow$ Alg.\ref{algTranslateDerivedDatatypeConstraints} & \\ +Compound type & 2.1.3.5 & Alg. \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateCompound} $\rightarrow$ Alg.\ref{algTranslateCompoundDeclaration} & \\ +Container type & 2.1.3.3 & & \\ +Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & \\ +Constraint type & 3.10.1 & no specific constraints, cf. Section \ref{sectNotationOthers}, constraint value in \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationConstraintVariableConstraint} via compound access line \ref{algTranslateDeclarationTranslateInCompound} & \\ \hline \end{tabular} @@ -995,4 +1002,8 @@ %A=Annotation, AssignmentBlock %Ev=Eval +%I=Integer +%R=Real +%S=String +%E=Enum \begin{table*}[h] @@ -1009,4 +1020,20 @@ BCo3 & \class{booleanProblem/BooleanCompoundDefaultsTest.ivml}\\ BCo3 & \class{booleanProblem/BooleanCompoundImpliesTest.ivml}\\ +I1 & \class{integer/IntegerDefaultsTest.ivml}\\ +I2 & \class{integer/IntegerAssignTest.ivml}\\ +ICo1 & \class{integer/IntegerInCompoundDefaultsTest.ivml}\\ +ICo2 & \class{integer/IntegerInCompoundAssignTest.ivml}\\ +R1 & \class{real/RealDefaultsTest.ivml}\\ +R2 & \class{real/RealAssignTest.ivml}\\ +RCo1 & \class{real/RealInCompoundDefaultsTest.ivml}\\ +RCo2 & \class{real/RealInCompoundAssignTest.ivml}\\ +S1 & \class{string/StringDefaultsTest.ivml}\\ +S2 & \class{string/StringAssignTest.ivml}\\ +SCo1 & \class{string/StringInCompoundDefaultsTest.ivml}\\ +SCo2 & \class{string/StringInCompoundAssignTest.ivml}\\ +E1 & \class{enums/EnumDefaultsTest.ivml}\footnote{similar tests for ordered enums are in place}\\ +E2 & \class{enums/EnumAssignTest.ivml}\\ +ECo1 & \class{enums/EnumCompoundDefaultsTest.ivml}\\ +ECo2 & \class{enums/enumCompoundAssignTest.ivml}\\ CnCt1 & \class{collectionConstraints/constraintSetDefault.ivml}\\ CnCt2 & \class{collectionConstraints/constraintSetSetDefault.ivml}\\