Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 53) +++ /reasoner/reasoner.tex (revision 54) @@ -244,5 +244,5 @@ \subsection{Other IVML Elements}\label{sectNotationOthers} -No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real String) as well as for enums as IVML does not support attaching constraints directly to these types. Constraints can be attached indirectly through variable declarations / compound slots or derived types. The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning. +No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real String), the constraint type as well as for enums as IVML does not support modifying these types or does not allow attaching constraints directly to these types. Constraints can be attached indirectly through variable declarations / compound slots or derived types. The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning. In IVML, a \emph{configuration reference} points to a variable defined in the same or another project (if made available through imports). As the actual IVML specification \cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are translated for / evaluated on the referenced variable. @@ -431,6 +431,7 @@ $translateDerivedDatatypeConstraints(d)$\; \label{algTranslateDeclarationDerivedDatatype} \If{$\neg inc$} { - $translateAnnotationDefaults(cfg, d, \undef)$\; - } + $translateAnnotationDefaults(cfg, d, \undef)$\; \label{algTranslateDeclarationAnnotationDefault} + } +\MISSING{Here}\; $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$\; \uIf{$isCompound(t)$}{ @@ -438,5 +439,5 @@ $translateCompoundDefaults(d, v, ca, t)$\; \lIf{$ dflt \neq \undef $}{$ dflt \assng deflt|_{\IVMLself{}=d, \variableMapping}$} - } \uElseIf{$ dflt \neq \undef \wedge \neg inc$}{ + } \uElseIf{$ dflt \neq \undef \wedge \neg inc$}{ \label{algTranslateDeclarationHasDefault} \uIf{$ isContainer(type(d)) $}{ \ForAll{$u \iterAssng usedTypes(dflt)$}{ @@ -453,11 +454,11 @@ $translateContainerDerivedDatatypeConstraints(d, \undef)$\; } - \If{$ deflt \neq \undef $}{ + \If{$ deflt \neq \undef $}{ \uIf{$isConstraint(t)$}{ \lIf{$ ca == \undef $}{ $add(\otherConstraints, \createConstraint{dflt}, true)$\; $\relevantConstraints \assng \relevantConstraints \cup (\createConstraint{dflt}, v)$} - }\Else{ - $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)})$\; + }\Else{ + $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)})$\; \label{algTranslateDeclarationTranslateDefault} } } @@ -734,5 +735,5 @@ \textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} \\ \hline -Decision variable & 2.1.4 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTranslationDeclaration} $\rightarrow$ Alg. \ref{algTranslateDeclaration} \TBD{check} \\ +Decision variable & 2.1.4 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTranslationDeclaration} $\rightarrow$ Alg. \ref{algTranslateDeclaration} for default values, basic/enum values in lines \ref {algTranslateDeclarationHasDefault}, \ref{algTranslateDeclarationTranslateDefault}; annotation defaults in line \ref {algTranslateDeclarationAnnotationDefault} $\rightarrow$ Alg. \ref{algTranslateAnnotationDefaults}\\ Constraint & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelConstraints} \\ Annotation assignment & 2.2.2 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments} $\rightarrow$ Alg. \ref{algTranslateAnnotationAssignments} \\ @@ -741,37 +742,37 @@ \multicolumn{3}{|c|}{Types}\\ \hline -Basic types & 2.1.3.1 & No translation, cf. Section \ref{sectNotationOthers} \\ -Enum types & 2.1.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -Derived types & 2.1.3.4 & Alg. \ref{algTranslateDeclaration}, line \ref{algTranslateDeclarationDerivedDatatype} $\rightarrow$ Alg. \ref{algTranslateDerivedDatatypeConstraints} \\ -Compound types & 2.1.3.5 & \\ -+ Basic types & 2.1.3.1 & No translation, cf. Section \ref{sectNotationOthers} \\ -+ Enum variable & 2.1.3.2 & \\ -+ Derived variable & 2.1.3.4 & \\ -+ Compound variable & 2.1.3.5 & \\ -+ Container variable & 2.1.3.3 & \\ -+ Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -+ Constraint variable & 3.10.1 & \\ +Basic 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} \\ +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} \\ +Compound type & 2.1.3.5 & \\ ++ Basic 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 & \\ ++ Compound type & 2.1.3.5 & \\ ++ 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 & 2.1.3.5 & \\ + Refined compounds & 2.2.3.1 & \\ + Partial evaluation & 2.2.5.3 & \\ -Container variable & 2.1.3.3 & \\ -+ Basic variable & 2.1.3.1 & \\ -+ Enum variable & 2.1.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -+ Derived type variable & 2.1.3.4 & \\ -+ Compound variable & 2.1.3.5 & \\ -+ Container variable & 2.1.3.3 & \\ -+ Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -+ Constraint variable & 3.10.1 & \\ -+ Assignment Block & 2.2.2 & \\ -Annotation & 2.2.2 & \\ -+ Basic variable & 2.1.3.1 & \\ -+ Enum variable & 2.1.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -+ Derived type variable & 2.1.3.4 & \\ -+ Compound variable & 2.1.3.5& \\ -+ Container variable & 2.1.3.3 & \\ -+ Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -+ Constraint variable & 3.10.1 & \\ -Reference variable & 2.2.3.2 & No translation, cf. Section \ref{sectNotationOthers} \\ -Constraint variable & 3.10.1 & \\ ++ Assignment block & 2.2.2 & \\ +Container type & 2.1.3.3 & \\ ++ Basic 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 & \\ ++ Compound type & 2.1.3.5 & \\ ++ 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} \\ +Annotation of & 2.2.2 & \\ ++ Basic 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 & \\ ++ Compound type & 2.1.3.5& \\ ++ 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}\\ \hline \end{tabular}