modelverse/techreport/general/conformance.tex

\chapter{Conformance}
Model management operations (\textit{e.g.}, conformance checking, or versioning) frequently act upon both the model and the metamodel, or should be applicable on all models, independently of their metamodel.
As such, they are often in conflict with the principle of strict metamodelling.
We try to find a balance between strict metamodelling (\axiomHumanInteraction), and the principle of modelling everything explicitly (\axiomModelEverything).

By introducing multiple definitions of conformance, we can keep strict metamodelling while still implementing such model management functions.
The basic idea is to allow a single model to conform to multiple metamodels.
The conceptual graph, representing the model, is interpreted depending on the metamodel being used.
Examples of metamodels might be a domain-specific metamodel (\textit{e.g.}, a Petri Net metamodel), or a more physically-oriented metamodel (\textit{e.g.}, a Graph metamodel).
Depending on the interpretation given to the levels, different level hierarchies are constructed.
It is these level hierarchies that impose the restrictions on strict metamodelling.

\begin{figure}
    \center
    \includegraphics[width=0.4\columnwidth]{images/RelationLingPhys.pdf}
    \caption{Different conformance relations}
    \label{fig:conformance}
\end{figure}

Fig.~\ref{fig:conformance} presents some different notions of conformance that can be devised on the Modelverse.
While the amount of conformance relations can vary, each model will have a mapping to the PTM, which is required to physically represent the model.
And it will have a mapping to the Linguistic Type Model (LTM), using conformance$_\perp$.
This relates to \axiomMultiView, as a single model can be seen from different views, and relates to \axiomInteroperability, as it allows for the uniform representation of all data.

\section{Graph conformance}
As all our data is (conceptually) represented using a graph, the graph instance can also be interpreted as a linguistic instance of a graph metamodel.
Because all defined CRUD operations constrain the result to a well-formed graph, all models in the Modelverse conform to this metamodel by construction.
Every model represented in the Modelverse is conceptually representable as a graph.
Knowing this, the complete Modelverse can be flattened to a single level, which conforms to the graph formalism.
Within this single level, all operations and links between elements are non-level crossing, and are therefore correctly typed (by the graph metamodel).
Note however, that these methods are unable to guarantee conformance to any linguistic metamodel, apart from the graph metamodel.
As such, all multi-formalism models can also be represented using this single metamodel, thus partially addressing \axiomMultiFormalism and \axiomMultiAbstraction.
Multiple users (\axiomMultiUser) can also use this view to collaborate on a single model, while having different interpretations of it.

\section{Linguistic conformance}
Finally there is the linguistic conformance between the model and the metamodel, which is necessary to complete the support for our axioms (\axiomHumanInteraction).
It is the highest level, and offers the most features to the user, but is also the most fragile.
Linguistic conformance cannot be guaranteed at all, and requires continuous checking to make sure it is enforced for the desired model and metamodel.
In contrast, conformance$_\perp$ was guaranteed by design.

Because a conformance$_L$ view is only a specific view on a model, a single model can conform to multiple metamodels.
The function $conforms : \mathcal{G} \times \mathcal{G} \times 2^{IDS \rightarrow IDS} \rightarrow \mathbb{B}$ is defined to determine linguistic conformance, and can be implemented by the user.
It takes three parameters: two graphs --- a model and a metamodel, both subgraphs of the MvS graph --- and a mapping between them.
This mapping encapsulates all typing information, thus typing is completely separated from the model and metamodels.
Since multiple mappings can be stored, multiple typing relations are supported.
During syntax-directed editing, a mapping will be constructed (and used) with the information provided by the user.
Retyping can be done by modifying the mapping, and checking conformance afterwards.

We define a possible conformance$_L$ relation, to be seen as an example of our approach.
This relation bases itself on the top level model: the Model at the MetaCircular Level (MMCL).
In this model, we have three basic elements: a \textit{Class} (mapped to nodes), an \textit{Association} (connecting classes; mapped to edges), and \textit{Inheritance} between classes (mapping to the union type).
Using \textit{Inheritance}, the \textit{Association} becomes a special kind of \textit{Class} in our MMCL.
We call our example conformance relation \textit{conformance$_\alpha$} to indicate that it is one of many possible implementations.

First, we define a subfunction which defines transitive closure of inheritance links, where $A \leq B$ means that $A$ is a (possibly indirect) subclass of $B$.
$A \xrightarrow{{} \inheritancearrow {}} B$ means that there is an association, typed by the \textit{Inheritance} link, from $A$ to $B$.

\begin{align*}
A \xrightarrow{{} \inheritancearrow {}} B      &\Rightarrow A \leq B \\
A \leq C \land C \leq B &\Rightarrow A \leq B \\
A == B                  &\Rightarrow A \leq B \\
\end{align*}

A conformance relation for the primitive elements is defined, constraining the provided map.

\begin{gather*}
conforms: (N \cup E) \times (N \cup E) \times 2^{IDS \times IDS} \rightarrow \mathbb{B} \\
conforms(x, y, m) =
\left\{ \begin{array}{lr}
N_T(N_V(x)) == N_V(y) & if~x, y \in dom(N_V) \land (x,y) \in m \\         % Primitives
True & if~x, y \in N \land x, y \not\in dom(N_V) \land (x,y) \in m \\     % Nodes
conforms(x_s, y_s, m) \land conforms(x_t, y_t, m)   & if~(x, y), (x_s, y_s), (x_t, y_t) \in m \land (x_s, x, x_t), (y_s, y, y_t) \in E \\ % Edges
False & else \\                                                           % Else
\end{array}
\right.
\end{gather*}

The first line is for nodes with a primitive value: a node $x$ conforms to a node $y$ if both nodes have a value, with the type of the value of node $x$ being the value of node $y$.
The second line is for nodes without a primitive value: a node $x$ conforms to a node $y$ if such a mapping exists in the provided mapping.
Neither node is allowed to have a primitive value.
The third line is for edges: an edge $x$ conforms to an edge $y$ if their sources and targets conform to each other.
It is thus basically a recursive call.
However, there is no possibility for an infinite loop, because of our restriction on the IDs of edges: the source and target ID are always smaller than the ID of the edge.
The final line is for all other cases (\textit{e.g.}, comparing nodes to edges, or primitives to non-primitives), in which case there is no conformance possible.

Finally, $conforms_{\alpha,G}: \mathcal{G} \times \mathcal{G} \times 2^{IDS \rightarrow IDS} \rightarrow \mathbb{B}$ is the actual conformance function being called.
It tries to find a mapping between the specified model and metamodel, for which the conforms function holds.

\begin{gather*}
conforms_{\alpha,G}(M, MM, map) = True \\
\Leftrightarrow \\
map' = \lbrace (a, b) \; \vert \; a \in IDS_M, b \in IDS_{MM} \rbrace \\
\forall n \in N_M : \exists n' \in N_{MM} . conforms(n, n', map') \\
\forall e \in IDS_{E, M} : \exists e' \in IDS_{E, MM} . conforms(e, e', map') \\
\forall (a_i, b_i), (a_i, b_j) \in map' : (b_i \leq b_j) \\
\forall (a_i, b_i) \in map' : (a_i \rightarrow b_k) \in map \land b_k \leq b_i \\
\forall a, b \in IDS : a \leq b \land b \leq a \Rightarrow a == b
\end{gather*}

A map is generated which contains all possible mappings between the model and metamodel.
This map is then constrained by enforcing a mapping for the nodes and edges.
Source and target of the edges are recursively checked for conformance using the mapping.
We finally prune the set of possible mappings by only keeping a single type mapping for every node, with the exception being subclasses.
Finally, this mapping is pruned to a function by keeping the most specific (or a more specific) subclass of all present mappings.

Just like a model can conform to multiple metamodels, a model can also conform to the same metamodel multiple times, with different mappings.

Using this function, we can now check whether a model conforms to a specified metamodel, using a specified mapping.
It is also possible to generate a set of all possible mappings between a model and a metamodel.

\begin{gather*}
MAP = 2^{IDS \rightarrow IDS} \\
mappings_{\alpha,G} : \mathcal{G} \times \mathcal{G} \rightarrow 2^{MAP} \\
mappings_{\alpha,G}(M, MM) = s \\
s = \lbrace map \in MAP \; \vert \; conforms_{\alpha,G}(M, MM, map) \rbrace\\
\end{gather*}

\section{MMCL}
\begin{lstlisting}[caption=HUTN$_\perp$ construction of the MMCL,float,label=listing:mmcl0]
Node Class()
Value Type(Type)
Value String(String)
Edge Attribute_ (Class, Type)
Edge AttributeAttrs (Attribute_, Type)
Edge Attribute (Class, Type)
Edge Name (Attribute, String)
Edge Association (Class, Class)
Edge Inheritance (Class, Class)
Edge inherit_association (Association, Class)
Edge inherit_attribute (Attribute_, Class)
\end{lstlisting}

\begin{lstlisting}[caption=HUTN$_L$ construction of the MMCL,float,label=listing:mmcl1]
Class Class()
Type Type(Type)
Type String(String)
Attribute_ Attribute_ (Class, Type)
Attribute_ AttributeAttrs (Attribute_, Type)
Attribute_ Attribute (Class, Type)
AttributeAttrs Name (Attribute, String)
Association Association (Class, Class)
Association Inheritance (Class, Class)
Inheritance (Association, Class)
Inheritance (Attribute_, Class)
\end{lstlisting}

We present an encoding of our MMCL, in Listing~\ref{listing:mmcl0}, using the HUTN language respecting conformance$_\perp$.
The action code in this language is translated to an abstract syntax graph in the Modelverse, by a HUTN compiler.
The HUTN compiler lives in a Modelverse Interface (MvI).

Using this MMCL, we can now re-encode it, as in Listing~\ref{listing:mmcl1}, now using the HUTN language with conformance$_L$.
Alternatively, it is possible to directly use the definition in Listing~\ref{listing:mmcl1}, as elements can directly be typed by themselves in the Modelverse.

Finally, we encode our conformance checking algorithm, in Listing~\ref{listing:conforms}, using the HUTN action language.
With this example we show
(1) an example of modelling, as the action code is a model, and thus an element of the Modelverse;
(2) an example of our action code;
(3) the possibility for reflection and introspection, as the conformance check can also run on itself, to check whether or not it conforms to some kind of metamodel; and
(4) the possibility for metamodelling, as type hierarchies can be built using the provided conformance function.

\begin{lstlisting}[caption=HUTN conformance check algorithm,label=listing:conforms]
include "primitives.al"

Element function set_copy(elem : Element):
    Element result
    Integer counter
    Integer max

    result = create_node()

    // Expand the provided list by including all elements that need to be checked
    counter = 0
    max = read_nr_out(elem)
    while (integer_lt(counter, max)):
        set_add(result, read_edge_dst(read_out(elem, counter)))
        counter = integer_addition(counter, 1)

    return result

Boolean function is_subclass_of(superclass : Element, subclass : Element, types : Element, inheritance_link : Element):
    Integer counter_iso
    Integer i
    Element edge
    Element destination

    if (element_eq(superclass, subclass)):
        return True

    counter_iso = read_nr_out(subclass)
    i = 0
    while (integer_lt(i, counter_iso)):
        edge = read_out(subclass, i)
        if (dict_in_node(types, edge)):
            if (element_eq(dict_read_node(types, edge), inheritance_link)):
                // It is an inheritance edge, so follow it to its destination
                destination = read_edge_dst(edge)
                if (is_subclass_of(superclass, destination, types, inheritance_link)):
                    return True
        i = integer_addition(i, 1)

    // No link seems to have been found, so it is False
    return False

String function conformance_scd(model : Element, extra : Element):
    // Initialization
    Element work_conf
    Element model_src
    Element metamodel_src
    Element model_dst
    Element metamodel_dst
    Element models
    Element metamodels
    models = set_copy(model)

    Element typing
    typing = dict_read(extra, "typing")
    metamodels = set_copy(dict_read_node(typing, model))
    Element inheritance
    inheritance = dict_read(extra, "inheritance")

    // Iterate over all model elements and check if they are typed (in "typing") and their type is in the metamodel
    while (integer_gt(dict_len(models), 0)):
        work_conf = set_pop(models)
        // Basic check: does the element have a type
        if (bool_not(dict_in_node(typing, work_conf))):
            return string_join("Model has no type specified: ", cast_e2s(work_conf))

        // Basic check: is the type of the element part of the metamodel
        if (bool_not(set_in(metamodels, dict_read_node(typing, work_conf)))):
            return string_join("Type of element not in specified metamodel: ", cast_e2s(work_conf))

        // Basic check: type of the value agrees with the actual type
        // this is always checked, as it falls back to a sane default for non-values
        if (bool_not(type_eq(dict_read_node(typing, work_conf), typeof(work_conf)))):
            output(dict_read_node(typing, work_conf))
            output(typeof(work_conf))
            return string_join("Primitive type does not agree with actual type: ", cast_e2s(work_conf))

        // For edges only: check whether the source is typed according to the metamodel
        if (is_edge(work_conf)):
            model_src = read_edge_src(work_conf)
            metamodel_src = read_edge_src(dict_read_node(typing, work_conf))
            if (bool_not(is_subclass_of(metamodel_src, dict_read_node(typing, model_src), typing, inheritance))):
                return string_join("Source of model edge not typed by source of type: ", cast_e2s(work_conf))

        // For edges only: check whether the destination is typed according to the metamodel
        if (is_edge(work_conf)):
            model_dst = read_edge_dst(work_conf)
            metamodel_dst = read_edge_dst(dict_read_node(typing, work_conf))
            if (bool_not(is_subclass_of(metamodel_dst, dict_read_node(typing, model_dst), typing, inheritance))):
                return string_join("Destination of model edge not typed by destination of type: ", cast_e2s(work_conf))

    return "OK"
\end{lstlisting}

\begin{figure}
    \center
    \includegraphics[width=0.8\textwidth]{images/conformance_petrinet.pdf}
    \label{fig:conformance_petrinet}
    \caption{Conformance example for a petri net.}
\end{figure}