Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 26) +++ /reasoner/reasoner.tex (revision 27) @@ -12,4 +12,5 @@ \newcommand\addSet[0]{\cup} \newcommand\addSeq[0]{\oplus} +\newcommand\addMap[0]{\otimes} \newcommand\addSeqNoDupl[0]{\uplus} \newcommand\assng[0]{\leftarrow} @@ -85,10 +86,4 @@ \section{Reasoning algorithm} -The reasoner performs forward reasoning, i.e., it identifies all constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. - -For IVML, the reasoner must take the structure of IVML models into account, i.e., in particular IVML projects. An IVML projects constitutes a reasoning scopes, i.e., no duplicated variable assignment must occur within a project. Moreover, a project acts as search space for dynamic dispatch of user-defined operations. The main reasoning loop over the involved IVML projects for a given configuration $cfg$ is shown in Algorithm \ref{algMainLoop}. - -Relevant IVML projects are identified throgh the (potentially cyclic) import structure performing a depth-first search starting with the top-level project of a configuration. $discoverProjects(cfg)$ returns a sequence of IVML projects for $cfg$ listing the projects with less import dependencies first. Following this sequence, Algorithm \ref{algMainLoop} first identifies the constraints determining default values, then the remaining constraints and registers the constraints with the respective variables. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of - \newcommand\defaultConstraints[0]{c_d} \newcommand\deferredDefaultConstraints[0]{c_{dd}} @@ -104,4 +99,10 @@ \newcommand\unresolvedConstraints[0]{c_{u}} \newcommand\variableMapping[0]{vm} + +The reasoner performs forward reasoning, i.e., it identifies all constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. + +For IVML, the reasoner must take the structure of IVML models into account, i.e., in particular IVML projects. An IVML projects constitutes a reasoning scopes, i.e., no duplicated variable assignment must occur within a project. Moreover, a project acts as search space for dynamic dispatch of user-defined operations. The main reasoning loop over the involved IVML projects for a given configuration $cfg$ is shown in Algorithm \ref{algMainLoop}. + +Relevant IVML projects are identified throgh the (potentially cyclic) import structure performing a depth-first search starting with the top-level project of a configuration. $discoverProjects(cfg)$ returns a sequence of IVML projects for $cfg$ listing the projects with less import dependencies first. Following this sequence, Algorithm \ref{algMainLoop} first clears the actual variable mapping $\variableMapping$ as its scope is for a single project. Then, it identifies the constraints determining default values, then the remaining constraints and registers the constraints with the respective variables. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of \begin{itemize} @@ -240,5 +241,5 @@ }\ElseIf{$ca \neq \undef$}{ \lIf{$\IVMLself{} \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} - $dflt \assng dflt|_{\IVMLself =ca}$\; + $dflt \assng dflt|_{\IVMLself =ca, \variableMapping}$\; } } @@ -338,5 +339,5 @@ Algorithm \ref{algTranslateCompoundDefaults} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. -First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors to the slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclarationDefaults}. +First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclarationDefaults}. Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\constraintVariablesConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound collection, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateCollectionCompoundConstraints}. @@ -350,6 +351,8 @@ \ForAll{s \iterAssng slots(v)} { %actual slots - $c \assng \mapEntry{s}{\createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}}}$\; - $\variableMapping \assng \variableMapping \cup \set{c}$\; + $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}}$\; + $\variableMapping \assng \variableMapping \addMap \set{\mapEntry{s}{x}}$\; + } + \ForAll{s \iterAssng slots(v)} { %actual slots $translateDeclarationDefaults(s, decision(v, s), c)$\; } @@ -382,5 +385,5 @@ If a compound accessor $ca$ is given, it takes precedence and the annotation is accessed through $ca$ and the respective annotation defined for the given variable declaration $d$ through ($annotation(d, name(a))$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$ (\TBD{are variables or declarations mapped}), $d$ is taken as accessor, else the actual accessor in $\variableMapping$. The accessor is used as the left side of an IVML assignment, the right side (value) is made up of the default value expression given by the assignment data $a$. -Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it performs the transformation defined above and collects the created constraints in the set of assignment constraints $\assignmentConstraints$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). +Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it creates the variable mapping. When the mapping is complete, it performs the transformation defined above and collects the created constraints in the set of assignment constraints $\assignmentConstraints$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given). \begin{algorithm}[H] @@ -395,5 +398,9 @@ \If{$isCompound(type(d))$} { \ForAll{$s \iterAssng slots(d)$} { - $b \assng translateAnnotationAssignment(e, s, \IVMLMeta{acc}(\closedCases{d, & \text{if } ca = \undef\\ ca, &\text{else}}, s))$\; + $c \assng \IVMLMeta{acc}(\closedCases{d, & \text{if } ca = \undef\\ ca, &\text{else}}, s)$\; + $\variableMapping \assng \variableMapping \addMap \mapEntry{s}{c}$\; + } + \ForAll{$s \iterAssng slots(d)$} { + $b \assng translateAnnotationAssignment(e, s, c)$\; $\assignmentConstraints \assng \assignmentConstraints \cup \set{b}$\; } @@ -422,5 +429,5 @@ \KwData{deferred default constraints $\deferredDefaultConstraints$} \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{ - $\deferredDefaultConstraints \assng \deferredDefaultConstraints \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i})}$\; + $\deferredDefaultConstraints \assng \deferredDefaultConstraints \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i, \variableMapping})}$\; } @@ -457,5 +464,5 @@ $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$ \ForAll{s \iterAssng slots(t)} { - $\variableMapping \assng \variableMapping \cup \mapEntry{s}{\createExpression{\IVMLMeta{acc}(v,s)}}$\; + $\variableMapping \assng \variableMapping \addMap \mapEntry{s}{\createExpression{\IVMLMeta{acc}(v,s)}}$\; } \ForAll{$e \iterAssng allCompoundConstraints(t)$} { @@ -492,10 +499,9 @@ \KwData{constraint $base$ , variable mapping $\variableMapping$ \TBD{join, reorder, beautify, leave out non-incremental on-the-fly}} - \MISSING{Late substitution is wrong as only the lastest mapping is available.}\; $c_s \assng \set{}$\; \If{$\neg inc$} { - $c_s \assng c_s \addSeq \seqWith{\createDefaultConstraint{c|_{\variableMapping}}}{c\in \defaultConstraints \addSeq \deferredDefaultConstraints}$\; - } - $c_s \assng c_s \addSeq \seqWith{\createConstraint{c|_{\variableMapping}}}{c \in \derivedTypeConstraints}$\; + $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints$\; + } + $c_s \assng c_s \addSeq \derivedTypeConstraints$\; $c_s \assng c_s \addSeq \seqWith{constraints(e)}{e\in evals(p)}$\; $c_s \assng c_s \addSeq \compoundEvalConstraints$\; @@ -529,5 +535,5 @@ $\unresolvedConstraints \assng \set{}$\; - \caption{Translating constraints(\IVML{translateConstraints}).}\label{algTranslateConstraints} + \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints} \end{algorithm}