Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 99) +++ /reasoner/reasoner.tex (revision 100) @@ -104,5 +104,5 @@ As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \setEmpty as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter). -For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need \emph{sequences}, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates. +For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need \emph{sequences}, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty{} as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. Accessing the $i$-th element in sequence $q$ is expressed by $q[i]$. We denote adding an element to an existing sequence / the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates. We also want to express that a \emph{mapping} from a certain key to a value is recorded, retrieved and used in some algorithms. We simply denote such a map as a set of entries $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. As key-value pairs are unique within a mapping, in particular there is only one mapping for a certain key, using a set of such entries is reasonable. We denote adding an entry to a map by $m \assng m \addMap \mapEntry{k}{v}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ will return undefined denoted by $\undef$. Iterating over a map means iterating over the entries of a map. @@ -355,10 +355,12 @@ \subsection{Main Reasoning Loop}\label{sectTopLevelMainReasoningLoop} -The main reasoning loop implements the overall control for the IVML reasoning process. First, Algorithm \ref{algMainLoop} sets up\footnote{In the implementation, also the re-scheduling of changed variables (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) and recording assigned variables are registered with the expression evaluator, but this is not shown here.} the expression evaluator in line \ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. For IVML, the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. As shown in Algorithm \ref{algMainLoop}, first the relevant IVML projects and their sequence are identified. Therefore, $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. +The main reasoning loop implements the overall control for the IVML reasoning process. First, Algorithm \ref{algMainLoop} sets up\footnote{In the implementation, also the re-scheduling of changed variables (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) and recording assigned variables are registered with the expression evaluator, but this is not shown here.} the expression evaluator in line \ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. The remainder of the algorithm is separated into two parts, 1) the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and 2) the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part. + +For IVML, the full execution of the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. As shown in Algorithm \ref{algMainLoop}, first a structure is created to store constraints for reuse (if $reuse$ is enabled). Then, the relevant IVML projects and their sequence are identified. Therefore, $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. \begin{algorithm}[H] \SetAlgoLined \KwIn{configuration $cfg$} - \KwData{problem records $\problemRecords$, scope assignments $\scopeAssignments$, expression evaluator $e$, reasoning start time $startTime$, flags $hasTimeout$ and $stop$} + \KwData{problem records $\problemRecords$, scope assignments $\scopeAssignments$, expression evaluator $e$, reasoning start time $startTime$, flags $hasTimeout$ and $stop$, $resue$ instance flag, $projects$ sequence, constraint base copy $base_c$} \KwResult{Reasoning result $r$} @@ -367,11 +369,23 @@ %evaluator.setScopeAssignments(sAssng)\; $setup(e, cfg, \scopeAssignments)$\; \label{algMainLoopSetupEval} - $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} $startTime = now()$\;\label{algMainLoopStartTime} - \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart} + \uIf{$base_c = \undef$}{ \label{algMainLoopFullStart} + \If{$reuse$}{ + $base_c = \seqEmpty{}$\; %sequence? + } + $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} + \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart} $translateConstraints(p)$\; \label{algMainLoopTranslate} $evaluateConstraints(p)$\; \label{algMainLoopEvaluate} $freeze(cfg, p)$\; \label{algMainLoopFreeze} - } \label{algMainLoopEnd} + } \label{algMainLoopEnd}\label{algMainLoopFullEnd} + }\Else {\label{algMainLoopIncStart} + \ForAll{$i \in \set{0, \ldots, |base_c|} \wedge \neg hasTimeout \wedge \neg stop$}{ + $base \assng base_c[i]$\; + $p \assng projects[i]$\; + $evaluateConstraints(p)$\; + $freeze(cfg, p)$\; + } + }\label{algMainLoopIncEnd} $r \assng createReasoningResult(m, hasTimeout, stop)$\; \label{algMainLoopResult} \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop} @@ -381,4 +395,6 @@ For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ (and populates the constraint base as a side effect, line \ref{algMainLoopTranslate} discussed / Section \ref{sectTopLevelConstraintsTranslation}) and performs the forward-chaining evaluation of the constraint base, i.e., for $p$, in line \ref{algMainLoopEvaluate} / Section \ref{sectTopLevelConstraintsEvaluation}. If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation by Algorithm \ref{algVarChange}. As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the main reasoning algorithm composes\footnote{In the implementation, this step happens in the class \class{Engine.java}, the actual reasoner instance, which utilizes and calls instances of \class{Resolver.java}.} a detailed reasoning result based on persisting recorded evaluation problems in line \ref{algMainLoopResult}. This reasoning result also includes whether a timeout or a user-requested cancellation of the reasoning occurred. + +For incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to take the constraints for the respective project, and, as before, to evaluate the constraints and to freeze the variables. \subsection{Variable Mapping}\label{sectVarMapping} @@ -421,5 +437,4 @@ \KwData{constraint $base$, constraint base copy $base_c$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$, incremental mode flag $inc$, eval-blocks flag $inEval$} - \If{$base_c = \undef \vee |base_c| = 0$} { \tcp{start of model visitor}%>ConstraintTranslationVisitor \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart} @@ -428,4 +443,5 @@ $add(\topLevelConstraints, constraints(p), true)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints} \ForAll{$a \iterAssng assignments(p)$}{ + $add(\topLevelConstraints, constraints(a), true)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} $translateAnnotationAssignments(a, \undef, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments} } \label{algTranslateConstraintsTranslationEnd} @@ -440,8 +456,7 @@ $\otherConstraints \assng \setEmpty$\; \label{algTranslateConstraintsClearSetsEnd} \uIf{$base_c \neq \undef$}{ \label{algTranslateConstraintsBaseCopyStart} - $base_c \assng \setWith{c}{c \in base}$\tcp*[l]{copy contents} + $base_c \assng base_c \addSeq \seqWith{c}{c \in base}$\tcp*[l]{copy/add contents} }\label{algTranslateConstraintsBaseCopyEnd} $clear(\variableMapping)$\; \label{algTranslateConstraintsClearMapping} - } \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints} \end{algorithm} @@ -554,5 +569,5 @@ \lIf{$dflt \neq \undef$}{$t \assng type(d)$} \uIf{$isCompound(t)$}{ - $f \assng d$\; + $f \assng d$\; \label{algTranslateDeclarationTranslateSelf1} $translateCompoundDeclaration(d, v, ca, t)$\; \label{algTranslateDeclarationTranslateCompound} } \uElseIf{$ isContainer(type(d)) $}{ \label{algTranslateDeclarationHasDefault} @@ -568,7 +583,7 @@ $ac\assng \closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}$\;\label{algTranslateDeclarationTranslateAnnotationAccess} }\uElse{ - $ac \assng \closedCases{ca, & \text{if } f = ca \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess} + $ac \assng \closedCases{ca, & \text{if } f = ca \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess} \label{algTranslateDeclarationTranslateSelf2} } - \lIf{$\IVMLself{} \in dflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$}\lElse{$dfltS \assng \defaultConstraints$} + \lIf{$\IVMLself{} \in dflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$}\lElse{$dfltS \assng \defaultConstraints$} \label{algTranslateDeclarationTranslateSelf3} $add(dfltS, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, dflt)}{f}})$\; \label{algTranslateDeclarationTranslateDefault} } @@ -626,5 +641,5 @@ Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The compound type $t_c$ indicates the type to be processed, i.e., where to take slot and annotation definitions from. The access expressions $ca$ is optional as usual and, if given, utilized as prefix to create access expressions for slots and annotations. Finally, a target type $t_t$ is given if the access via $ca_s$ or $ca_t$ requires a type cast so that specific slots of $t_t$ can be accessed. Type casts are required if if the actual value is of a refined type of $t_c$, as otherwise slots defined on the more specific type are not accessible and access is rejected by static type checking of IVML expressions. -Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t_c$ and creates for each slot a respective accessor. If a preceding compound access expression for the slots $ca_s$ is not given, it creates a static accessor based on $v$. If an accessor is given, we create an accessor based on $ca_s$ and include a type cast to $t_t$\footnote{In fact, the type cast can be omitted if $t=type(value(v))$. This is done by the implementation, but not detailed here as a type cast to the actual type does not have an effect.}. The created accessor is then registered with $\variableMapping$. Similarly, we iterate over all annotations for the current slot, create an accessor expression based on $ca_a$ and register the result with $\variableMapping$. +Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t_c$ and creates for each slot a respective accessor. If a preceding compound access expression for the slots $ca_s$ is not given, it creates a static accessor based on $v$. If an accessor is given, we create an accessor based on $ca_s$ and include a type cast to $t_t$\footnote{The type cast can be omitted if $t=type(value(v))$. This is done by the implementation, but not detailed here as a type cast to the actual type does not have an effect.}. The created accessor is then registered with $\variableMapping$. Similarly, we iterate over all annotations for the current slot, create an accessor expression based on $ca_a$ and register the result with $\variableMapping$. \begin{algorithm}[H] @@ -718,7 +733,7 @@ Below we illustrate the translation schema: $d$ denotes the variable declaration containing the compound (may alternatively be a compound or container accessor). \IVML{flatten} provides access even to deeply nested container entries. \IVML{selectByKind} if we translate for slots of a specific given type $t$ with $\subTypeEqOf{t}{s}$. Finally, we apply an all quantor over the elements of the collection using the temporary iterator variable $l$ to the respective constraint $c$ after appropriate variable substitution, in particular replacing \IVMLself{} by $l$. % -$$ +\begin{displaymath} d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested(c)}}\IVML{forAll}(l|c) -$$ +\end{displaymath} % Thus, the core idea of this algorithm is to consider all elements over all used types. If no value is available, we resort to the static type of the declaration of the containser variable. We create all-quantized constraints for all used types and distinguish between constraint containers, where the values directly turn into constraints, compound containers, where slots, constraints and annotations lead to further constraints, and derived types. @@ -762,7 +777,7 @@ By storing constraint information on the stack of $\variableMapping$ and assembling the information in one place, we can even handle recursive compound containers, which leads to a recursive creation of constraints. The formula below indicates the constraint that we must create in case of a compound container nested into a compound container. % -$$ +\begin{displaymath} \underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}|\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}|c)) -$$ +\end{displaymath} % In the first iteration, we start with $ca$ (indicated by $1:ca$, may also be some $d$) and append flatten/typeSelect as needed to form $e$ (indicated by $1:e$, i.e., recursion level and parameter/variable name). In the first iteration, we also create a temporary variable $l$ as iterator variable. We store $l$ and $e$ on the stack of $\variableMapping$ and pass $l$ on as accessor to the translation of compound content in Algorithm \ref{algTranslateCompoundContent}. There, we create an accessor for a slot, let's say $s$, i.e. $l.s$, which is then passed on in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT}, respectively, to the translation of declarations in Algorithm \ref{algTranslateDeclaration}. As a further compound container is nested into the initial compound container, we end up again in Algorithm \ref{algTranslateCompoundContainer}. Now $l.s$ is considered as accessor (indicated by $2:ca$), flatten(typeSelect are added as needed to form $e$ (now $2:e$), which is stored along with the temporary iterator variable $l_2$ on the stack. In this context, we apply the constraint $c$ within an all-quantor (after appropriate variable substitution, in particular \IVMLself{} by $l_2$). The quantor expressions for completing the full constraint are created by the $add$ algorithm (details in Section \ref{algAddConstraints}). @@ -893,5 +908,5 @@ \begin{itemize} - \item It filters out irrelevant constraints, in particular simple (default value) assignment constraints during incremental reasoning, are assumed to be already processed during previous iterations. + \item It filters out irrelevant constraints, in particular simple (default value) assignment constraints during incremental reasoning, are assumed to be already processed during previous iterations. Also constraints with all variables frozen or local (used for iterator variables in quantors) are filtered out ($isFrozen(c)$) if enabled, e.g., to speed up runtime reasoning. \item It serves as the central place to finally compose constraints for nested compound containers using Algorithm \ref{algComposeExpression} and the variable mapping $\variableMapping$. \item It analyzes the given constraint $c$ for the use of compound or container initializers. As explained above, these structures only occur in value assignments and actually must be analyzed for constraint variables, which must be turned into individual constraints. We perform this through the two recursive helper operations $checkContainerInitializer$ and $checkCompoundInitializer$ shown below. @@ -903,5 +918,5 @@ \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$} \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$ , incremental flag $inc$, evals flag $inEvals$} - \If{$\neg inc \vee (inc \wedge \neg isAssignment(c))$} { + \If{$\neg inc \vee (inc \wedge \neg (isAssignment(c) \vee isFrozen(c)))$} { $c = composeExpression(\variableMapping, c)$\; \If{$check$}{ @@ -971,4 +986,5 @@ Assignment block & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelAnnotationAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnAI1 \\ +$\triangleright$ constraints & 2.2.2 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelAnnotationConstraints} & AI2 \\ Partial evaluation & 2.2.5.3 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelEvals} & Ev1\\ @@ -1006,4 +1022,6 @@ \pagebreak +\TBD{Check quantized instance constraints.} + \begin{table*}[h] %\begin{adjustbox}{angle=90} @@ -1039,7 +1057,10 @@ Constraints & & \tabAlgLines{algTranslateCompoundDeclaration}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd}& Cn1 \\ +\IVML{self} & 3.1.6 & \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf1}, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf2}, \tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateSelf3} & CnA3 \\ + Annotation & 2.2.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationTranslateSlotsStart}{algTranslateCompoundDeclarationTranslateSlotsEnd}\tabAlgFollow\tabAlg{algTranslateDeclaration} $\ldots$, cf. Table \ref{tab:completenessTopLevelTypes} & CnA3\\ Assignment blocks & 2.2.2 & \tabAlgLine{algTranslateCompoundContent}{algTranslateCompoundDeclarationCompoundAssignments}\tabAlgFollow\tabAlg{algTranslateAnnotationAssignments} & CnAI2, CnAI3 \\ +$\triangleright$ constraints & 2.2.2 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationAllStart}{algTranslateCompoundDeclarationAllEnd} & CnA4 \\ Partial evaluation & 2.2.5.3 & \tabAlgLines{algTranslateCompoundContent}{algTranslateCompoundDeclarationEvalStart}{algTranslateCompoundDeclarationEvalEnd} & CnEv1 \\ @@ -1263,4 +1284,5 @@ I2 & \class{integer/IntegerAssignTest.ivml}\\ AI1 & \class{integer/IntegerAnnotationTest.ivml}\\ +AI2 & \class{runtime/runtimeReasoning.ivml}\\ IT1 & \class{operations/typedef.ivml}\\ IT2 & \class{operations/typedefOfTypedefValid.ivml}\\ @@ -1339,4 +1361,5 @@ ACs1 & \class{attributes/ConstraintAnnotationTest.ivml}\\ CnA3 & \class{attributes/CompoundIndividualAssign.ivml}\\ +CnA4 & \class{attributes/BlockAssignNestedConstraintFail.ivml}\\ Cs1 & \class{constraintVariables/constraintAssigned.ivml}\\ Cs2 & \class{constraintVariables/constraintDefault.ivml}\\