Index: /reasoner/appendixTests.tex =================================================================== --- /reasoner/appendixTests.tex (revision 225) +++ /reasoner/appendixTests.tex (revision 226) @@ -1,38 +1,8 @@ + \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 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. +In this section, we list a representative subset of the implemented reasoner test cases used in the argumentation in Section \ref{sectCompleteness}. Many test cases are defined as part of the test suite for the \class{ReasonerCore} bundle of EASy-Producer and contains more than 310 test cases. 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. - -\begin{table*}[ht] -%\begin{adjustbox}{angle=90} -\centering -\begin{tabular}{|l|l|} -\hline -\textbf{Id part / abbreviation} & \textbf{IVML concept}\\ -\hline - -B & Boolean \\ -Cn & Compound \\ -Ct & Container\\ -Cs & Constraint\\ -A & Annotation, AssignmentBlock\\ -Ev & Eval\\ -I & Integer\\ -R & Real\\ -S & String\\ -E & Enum\protect\footnotemark\\ -T & Typedef\\ -F & Reference\\ -If & Interface\\ -Sc & Scope, re-assignment\\ -\hline -\end{tabular} -\caption{Test case naming schema.} -\label{tab:testCaseIdSchema} -%\end{adjustbox} -\end{table*} -\footnotetext{Similarly, test cases for ordered enums are in place, but not referenced explicitly in this document.} - +The schema for composing test case identifiers was described in Section \ref{sectCompleteness}, in particular Table \ref{tab:testCaseIdSchema}. Tables \ref{tab:reasonerTestCasesBasics}, \ref{tab:reasonerTestCasesAdvanced} and \ref{tab:reasonerTestCasesAdvanced2} 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. Index: /reasoner/ivmlCompleteness.tex =================================================================== --- /reasoner/ivmlCompleteness.tex (revision 225) +++ /reasoner/ivmlCompleteness.tex (revision 226) @@ -3,16 +3,43 @@ In this section, we discuss the completeness of the reasoner with respect to IVML concepts. Although the algorithms are designed along the IVML specification~\cite{IVML-LS}, it is important to explicitly assess and validate the coverage of the design and the realization, in particular as a basis for future work. However, as explicitly stated in Section \ref{sectIntro}, reasoning completeness, e.g., involving advanced reasoning capabilities such as narrowing down value instances by limiting constraints or instance creation, is currently out of scope and may be subject of future work. -To assess the IVML completeness, we enumerate all IVML concepts relevant to reasoning, their defining section in the IVML specification~\cite{IVML-LS}, the transformation path along the algorithms presented in this report and the test cases validating the transformation and the reasoning results. The referenced test cases are detailed in Appendix \ref{appendixTestCases}. A '*' in a test id indicates a wildcard, e.g., A*1 means all annotation-related tests. Test cases are referenced by ids in order to indicate that all relevant combinations are subject to regression testing in the continuous build process of EASy-Producer. An entry 'no specific constraints' in the transformation path indicates that for the respective concept no constraints can be defined / translated as explained in Section \ref{sectNotationOthers}. - -We present the argumentation in four parts grouped according to IVML concepts, namely 1) top-level concepts / basic types (Table \ref{tab:completenessTopLevelTypes}), compound types (Table \ref{tab:completenessCompounds}), container types (Table \ref{tab:completenessContainers}) and annotations (Table \ref{tab:completenessAnnotations}). - -Table \ref{tab:completenessTopLevelTypes} summarizes the translations for top-level concepts, changes of variables and basic types. Some variable change properties are common such as validating variable re-assignments or handling variable change by forward reasoning are listed here and apply to all further concepts. Handing constraint variable changes depends on the context of the variable - here top-level variables only. - -Table \ref{tab:completenessCompounds} provides an overview on the possible combinations and transformations for compound types, here in particular including nested constraints, nested annotation assignments, eval blocks, but also changes of constraint slots and changing the actual type of a compound variable. - -Table \ref{tab:completenessContainers} summarizes the transformations and tests for containers, in particular also regarding the specific handling of containers consisting of compounds as well as containers consisting of constraints. - -Finally, Table \ref{tab:completenessAnnotations} indicates the transformation paths for annotations. Here, the possible combinations are limited as annotations cannot be recursive, cannot have nested annotation assignments or eval-blocks. - +To assess the IVML completeness, we enumerate in this section all IVML concepts relevant to reasoning, their defining section in the IVML specification~\cite{IVML-LS}, the transformation path along the algorithms presented in this report and the test cases validating the implementation of the transformation/reasoning. However, we do not aim at covering all IVML/reasoner test cases that are implemented in EASy-Producer, rather than the most relevant ones supporting the claimed coverage between language concept and reasoning algorithms. + +For referencing these test cases, we use identifiers composed from a classification of the main IVML concepts given in Table \ref{tab:testCaseIdSchema} and a number. For example, the first test case for Integer (I) variables used in a compound (Co), i.e., as slots, is identified by 'ICo1'. In Appendix \ref{appendixTestCases}, the identifiers are related to realized test cases in EASy-Producer. + +\begin{table*}[ht] +%\begin{adjustbox}{angle=90} +\centering +\begin{tabular}{|l|l|} +\hline +\textbf{Id part / abbreviation} & \textbf{IVML concept}\\ +\hline + +B & Boolean \\ +Cn & Compound \\ +Ct & Container\\ +Cs & Constraint\\ +A & Annotation, AssignmentBlock\\ +Ev & Eval\\ +I & Integer\\ +R & Real\\ +S & String\\ +E & Enum\protect\footnotemark\\ +T & Typedef\\ +F & Reference\\ +If & Interface\\ +Sc & Scope, re-assignment\\ +\hline +\end{tabular} +\caption{Test case naming schema.} +\label{tab:testCaseIdSchema} +%\end{adjustbox} +\end{table*} +\footnotetext{Similarly, test cases for ordered enums are in place, but not referenced explicitly in this document.} + +In some cases, we want to indicate that all test cases belonging to a certain IVML conccept/identifier cover a translation. We indicate this using the wildcard '*', e.g., * means just all test cases and A*1 means all (first) annotation-related tests. + +We present the argumentation in terms of four tables covering a certain set of IVML concepts, namely 1) top-level concepts and basic types in Table \ref{tab:completenessTopLevelTypes}, compound types in Table \ref{tab:completenessCompounds}, container types in Table \ref{tab:completenessContainers}, and annotations in Table \ref{tab:completenessAnnotations}. Entries marked with '-' indicate that a part does not exist, either because it is not mentioned in the IVML specification or it shall not exist at all, e.g., annotations of annotations. An IVML concept marked by $\triangleright$ indicates that it belongs to the preceding concept, e.g., constraints in an assignment block. An entry 'no specific constraints' in the transformation path indicates that for the respective concept no constraints can be defined at all as explained in Section \ref{sectNotationOthers}. + +Table \ref{tab:completenessTopLevelTypes} summarizes the translations for top-level concepts, changes of variables and basic types. Some variable change properties are common and occur in many test cases, such as variable re-assignments or handling variable changes by forward reasoning. Their validation is summarized here and applies similarly to all further concepts. Handing constraint variable changes depends on the context of the variable. In Table \ref{tab:completenessTopLevelTypes} we focus on top-level variables only. \begin{table*}[!h] @@ -79,4 +106,6 @@ \pagebreak +Table \ref{tab:completenessCompounds} provides an overview on the possible combinations and transformations for compound types, here in particular including nested constraints, nested annotation assignments, eval blocks, but also changes of constraint slots and changing the actual type of a compound variable. + \begin{table*}[!h] %\begin{adjustbox}{angle=90} @@ -136,4 +165,6 @@ \pagebreak +Table \ref{tab:completenessContainers} summarizes the transformations and tests for containers, in particular also regarding the specific handling of containers consisting of compounds as well as containers consisting of constraints. + \begin{table*}[!h] %\begin{adjustbox}{angle=90} @@ -190,4 +221,6 @@ \pagebreak +Finally, Table \ref{tab:completenessAnnotations} indicates the transformation paths for annotations. Here, the possible combinations are limited as annotations cannot be recursive, cannot have nested annotation assignments or eval-blocks. + \begin{table*}[!h] %\begin{adjustbox}{angle=90} @@ -233,3 +266,5 @@ \end{table*} +As all relevant IVML concepts and combinations are listed in the tables above and they either have a transformation path and test case assigned or shall not be realized at all, we conclude that the reasoning and translation algorithms presented in this report are IVML (not necessarily reasoning) complete. + \clearpage Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 225) +++ /reasoner/reasoner.tex (revision 226) @@ -103,4 +103,5 @@ \begin{appendices} +\pagebreak \input{appendixTests} \end{appendices}