Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 98) +++ /reasoner/reasoner.tex (revision 99) @@ -307,5 +307,5 @@ In IVML, a \emph{configuration reference} points to a variable defined in the same or another project (if made available through imports). A reference is a type $t$ defined for a base type $base(t)$ the reference points to. If $t$ is a reference, $isReference(t)$ returns true. In some cases, we must dereference a set $s$ of reference types through % -$$deref(t)=\begin{cases} base(t), & \text{if } isDerived(t) \wedge \neg isDerived(base(t))\\ dereference(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ t, & \text{else}\\\end{cases}$$ +$$deref(t)=\begin{cases} deref(base(t)), & \text{if } isDerived(t) \wedge \neg isDerived(base(base(t)))\\ deref(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ t, & \text{else}\\\end{cases}$$ % and @@ -583,5 +583,5 @@ If a variable $v$ is declared as of a derived type $t$, all constraints defined for $t$ over $base(t)$ and, transitively all constraints over all base types $allBase(t)$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. The constraint translation follows this nested type structure and instantiates all constraints defined along the nesting. -For a given variable $v$ (in terms of declaration $d$ and specific type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraint.} all constraints defined for $dref(allBase(t))$, i.e., for all base types also through references types, as constraints of $d$. Thereby, we must consider whether we perform this instantiation for a container variable. If it is a container variable, we create an all-quantifying constraint over all container values, whereby the iterator variable substitutes $decl(t)$. If it is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$. % shall not make a difference for nested variables as they are already initialized +For a given variable $v$ (in terms of declaration $d$ and specific type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraint.} all constraints defined for $dref(allBase(t))$, i.e., for all base types also through references types, as constraints of $d$. Thereby, we must consider whether we perform this instantiation for a container variable. If it is a container variable, we create an all-quantifying constraint over all container values, whereby the iterator variable substitutes $decl(t)$. If it is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. Moreover, if the type $t$ consists of reference types, we need to de-reference $i$ by the number of reference types (through the internal IVML \IVML{refBy} operation). The respective composite expression for $i$ is created through the function $deref(t, ex)$ shown below. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$. % shall not make a difference for nested variables as they are already initialized \begin{algorithm}[H] @@ -592,12 +592,12 @@ $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\; $add(\topLevelConstraints, \setWith{\createConstraint{ - \closedCases{d\rightarrow\IVML{forAll(i}|\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{i}}\IVML{)}, & \text{if } isC \\ + \closedCases{d\rightarrow\IVML{forAll(i}|\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{deref(t, i)}}\IVML{)}, & \text{if } isC \\ \varSubstitutionOtherVarMapping{c}{decl(t)=d}, &\text{else}} }}{c\in cs}, true)$\; \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} \end{algorithm} - - - +% +$$deref(t, ex)=\begin{cases} deref(base(t), ex), & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ \IVML{refBy}(deref(base(base(t)), ex)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ ex, & \text{else}\\\end{cases}$$ +% \subsection{Compound types}\label{sectCompoundDefaults} @@ -1027,11 +1027,11 @@ Enum type & 2.1.3.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & ECo1, ECo2\\ -Derived type & 2.1.3.4 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CnTCt1, CnTCt2 \\ +Derived type & 2.1.3.4 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationDerivedDatatype}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CnTCt1, CnTCt2, CnTF1 \\ + +Reference type & 2.2.3.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & FCn1, FCn2, FCn3, CnTF1 \\ Compound type & 2.1.3.5 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateCompound}\tabAlgFollow\tabAlg{algTranslateCompoundDeclaration} $\ldots$ & Cn2, Cn3 \\ Container type & 2.1.3.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateContainer}\tabAlgFollow Table \ref{tab:completenessContainers} & CnCt3, CnCt4 \\ - -Reference type & 2.2.3.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & FCn1, FCn2, FCn3 \\ Constraint type & 3.10.1 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} & CsCn1, CsCn2 \\ @@ -1083,9 +1083,9 @@ Derived compound type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes} \tabAlgFollow \tabAlg{algTranslateDerivedDatatypeConstraints} & ITCnCt1, ITCnCt2 \\ -Container type & 2.1.3.3 & \tabAlgLines{algTranslateContainerDeclaration}{algTranslateContainerDeclarationCompoundContainerStart}{algTranslateContainerDeclarationCompoundContainerEnd}\tabAlgFollow\tabAlgLines{algTranslateCompoundContainer}{algTranslateDefaultsCompoundContainerMapping}{algTranslateDefaultsCompoundContainerContent}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & CnCt2, CnTCt2 \\ - -Derived container type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CtTCt1 \\ - -Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & CnFCt1 \\ +Container type & 2.1.3.3 & \tabAlgLines{algTranslateContainerDeclaration}{algTranslateContainerDeclarationCompoundContainerStart}{algTranslateContainerDeclarationCompoundContainerEnd}\tabAlgFollow\tabAlgLines{algTranslateCompoundContainer}{algTranslateDefaultsCompoundContainerMapping}{algTranslateDefaultsCompoundContainerContent}\tabAlgFollow\tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$ & CnCt2, CtTF1 \\ + +Derived container type & 2.1.3.3 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationDerivedTypes}\tabAlgFollow\tabAlg{algTranslateDerivedDatatypeConstraints} & CtTCt1, CtTF1 \\ + +Reference type & 2.2.3.2 & no specific constraints, cf. Section \ref{sectNotationOthers} & CnFCt1, CnTFCt1 \\ Constraint type & 3.1.10 & \tabAlgLine{algTranslateContainerDeclaration}{algTranslateContainerDeclarationConstraintContainer}\TBD{change} & CnCt1, CnCt2 \\ @@ -1209,5 +1209,5 @@ \section{Reasoner test cases}\label{appendixTestCases} -In this section, we list a representative subset of the implemented reasoner test cases, which aim at validating translation and reasoning for specific IVML concepts and combinations. Please note that reasoner test cases defined as part of the test suite for the \class{ReasonerCore} bundle of EASy-Producer contains more than 280 test cases are applied to the reasoner, many constructed in a similar way for different types, i.e., exhaustively listing all of them is neither possible her nor intended. Among them, there are also more complex test cases taken from real scenarios, evaluation models as well as challenge test cases. +In this section, we list a representative subset of the implemented reasoner test cases, which aim at validating translation and reasoning for specific IVML concepts and combinations. Please note that reasoner test cases defined as part of the test suite for the \class{ReasonerCore} bundle of EASy-Producer contains more than 310 test cases are applied to the reasoner, many constructed in a similar way for different types, i.e., exhaustively listing all of them is neither possible her nor intended. Among them, there are also more complex test cases taken from real scenarios, evaluation models as well as challenge test cases. For referencing the test cases, we use identifiers composed for the main concepts to be validated. We use the abbreviations shown in Table \ref{tab:testCaseIdSchema} to compose identifiers. For example, test case nuber one on Integer (I) variables used as compound (Co) slots is identified by 'ICo1'. Table \ref{tab:reasonerTestCasesBasics} and Table \ref{tab:reasonerTestCasesAdvanced} list the test cases referenced in this document. Test case names ending with 'Valid' indicate that there is an associate test case testing also the failing of the constraint under test. @@ -1317,4 +1317,5 @@ CnTCt2 & \class{collectionConstraints/constraintSetSetDerivedCompound.ivml}\\ CtTCt1 & \class{collectionConstraints/setDerivedSet.ivml}\\ +CtTF1 & \class{collectionConstraints/RefernceDerivedCollectionTest.ivml}\\ TFCnCtCsA1 & \class{collectionConstraints/QM.ivml}\\ ITCn1 & \class{operations/typedefNestedInCompoundValid.ivml}\\ @@ -1332,4 +1333,5 @@ Cn2 & \class{compounds/CompoundCompoundTest1.ivml}\\ Cn3 & \class{compounds/CompoundCompoundTest2.ivml}\protect\footnotemark\\ +CnTF1 & \class{collectionConstraints/RefernceDerivedCompoundTest.ivml}\\ A1 & \class{attributes/DefaultAssign.ivml}\\ A2 & \class{attributes/IndividualAssign.ivml}\\