Keywords

1 Introduction

Multilevel modeling (MLM) extends conventional techniques from the area of Model-Driven Engineering by providing model hierarchies with multiple levels of abstraction. The advantages of allowing multiple abstraction levels (e.g. reducing accidental complexity in software models and avoiding synthetic type-instance anti-patterns) and flexible typing (e.g. multiple typing, linguistic extension and deep instantiation), as well as the exact nature of the techniques used for MLM are well studied in the literature [1, 4,5,6, 8, 10, 17]. Our particular approach [19, 20] to MLM facilitates the separation of concerns by allowing integration of different multilevel modeling hierarchies as separate aspects of the system to be modelled. In addition, we enhance reusability of concepts and their behaviour by allowing the definition of flexible transformation rules which are applicable to different hierarchies with a variable number of levels. In this paper, we present a revised and extended formalisation of these rules using graph theory and category theory.

Fig. 1.
figure 1

MLM terminology

Full size image

As models are usually represented abstractly as graphs, we outline in this paper the graph theoretic foundations of our approach to MLM using multilevel typed graphs, prior to introducing our formalisation of multilevel typed rule definition and application. Multilevel models are organized in hierarchies, where any graph \(G_{}^{}\) is multilevel typed over a typing chain of graphs (see Fig. 1). The typing relations of elements within each graph are represented via graph morphisms. Since we allow for deep instantiation [4,5,6, 8], which refers to the ability to instantiate an element at any level below the level in which it is defined, these morphisms need to be partial graph homomorphisms. Moreover, more than one model can be typed by the same typing chain (or, conversely, models can be instantiated more than once), hence, all the paths that contain such typing relations constitute a full, tree-shaped multilevel modelling hierarchy (see Example 1). Finally, the topmost model \(G_{0}^{}\) in any hierarchy is fixed, and the typing relations of all models (and the elements inside them) must converge, directly or via a sequence of typing morphisms, into \(G_{0}^{}\). Therefore, the graph morphisms into \(G_{0}^{}\) are always total.

Multilevel typed graph transformation rules are cospans

figure c

of inclusion graph homomorphisms, with \(I=L\cup R\), where the three graphs are multilevel typed over a common typing chain \(\mathcal {MM}_{}\). A match of the left-hand side \(L_{}^{}\) of the rule in a graph \(S_{}^{}\), at the bottom of a certain hierarchy, multilevel typed over a typing chain \(\mathcal {TG}_{}\), is given by a graph homomorphism \(\mu :L_{}^{}\rightarrow S_{}^{}\) and a flexible typing chain morphism from \(\mathcal {MM}_{}\) into \(\mathcal {TG}_{}\). The typing chain \(\mathcal {MM}_{}\) is local for the rules and is usually different from \(\mathcal {TG}_{}\) which is determined by the path from \(S_{}^{}\) to the top of the hierarchy (see Fig. 1).

Fig. 2.
figure 2

Rule structure and basic constructions for rule application

Full size image

To apply these rules we rely on an adaptation of the Sesqui pushout (Sq-PO) approach [7] to cospans. We construct first the pushout and then the final pullback complement (FPBC) of the underlying graph homomorphisms in the category as shown in Fig. 2. Based on these traditional constructions we want to build, in a canonical way, type compatible multilevel typings of the result graphs \(D_{}^{}\) and \(T_{}^{}\) over the typing chain \(\mathcal {TG}_{}\). For this to work, we need quite reasonable type compatibility conditions for rules and relatively flexible conditions for matches, formulated as equations and inequations, resp., between composed partial typing morphisms.

We introduce typing chain morphisms, and the corresponding category of typing chains and typing chain morphisms, to formalize flexible matching and application of multilevel typed rules. The composition of partial graph homomorphisms is based on pullbacks in the category , thus type compatibility conditions can be equivalently expressed by commutativity and pullback conditions in . Therefore, we formalize and analyze multilevel typing as well as describe constructions and prove the intended results, in a systematic way, within the category . Especially, we show that the first step in a rule application can be described by a pushout in . Moreover, the second step is described as a canonical construction in , however, it is an open question whether this is a final pullback construction in or not.

A preliminary version of typing chains are an implicit constituent of the concept “deep metamodeling stack” introduced in [22] to formalize concepts like parallel linguistic and ontological typing, linguistic extensions, deep instantiation and potencies in deep metamodeling. We revised this earlier version and further developed it to a concept of its own which serves as a foundation of our approach to multilevel typed model transformations in [20, 26]. Compared to [20], we present in this paper a radically revised and extended theory of multilevel typed graph transformations. In particular, the theory is now more powerful, since we drop the condition that typing chain morphisms have to be closed (see Definition 5). Moreover, we detail the FPBC step which is missing in [20]. Due to space limitations, we will not present the background results concerning the equivalence between the practice of individual direct typing – which are used in applications and implementations – and our categorical reformulation of this practice by means of typing chains. These equivalence results as well as examples and proofs can be found in [26].

2 Typing Chains and Multilevel Typing of Graphs

  denotes the category of (directed multi-) graphs \(G_{}^{} = {(G_{}^{N}, G_{}^{A}, sc ^{G}, tg ^{G})}\) and graph homomorphisms \(\phi =(\phi ^N\!{,}\phi ^A):G_{}^{}\rightarrow H_{}^{}\) [12]. We will use the term element to refer to both nodes and arrows.

Multilevel typed graphs are graphs typed over a typing chain, i.e., a sequence \([G_{n}^{}, G_{n-1}^{}, \dots , G_{1}^{}, G_{0}^{}]\) of graphs where the elements in any of the graphs \(G_{i}^{}\), with \(n\ge i\ge 1\), are, on their part, multilevel typed over the sequence \([G_{i-1}^{}, \dots , G_{1}^{}, G_{0}^{}]\). Paths in our MLM hierarchies give rise to typing chains. The indexes \(i\) refer to the abstraction levels in a modeling hierarchy where \(0\) denotes the most abstract top level.

Following well-established approaches in the Graph Transformations field [12], we define typing by means of graph homomorphisms. This enables us to establish and develop our approach by reusing, variating, and extending the wide range of constructions and results achieved in that field. Moreover, this paves the way to generalize the present “paradigmatic” approach, where models are just graphs, to more sophisticated kinds of diagrammatic models, especially those that take advantage of diagrammatic constraints [22, 23].

We allow typing to jump over abstraction levels, i.e., an element in graph \(G_{i}^{}\) may have no type in \(G_{i-1}^{}\) but only in one (or more) of the graphs \(G_{i-2}^{}, \dots , G_{1}^{}, G_{0}^{}\). Two different elements in the same graph may have their types located in different graphs along the typing chain. To formalize this kind of flexible typing, we use partial graph homomorphisms that we introduced already in [22].

Definition 1

A partial graph homomorphism \(\varphi : G_{}^{} {\circ \longrightarrow }H_{}^{}\) is given by a subgraph \(D(\varphi ) \sqsubseteq G_{}^{}\), called the domain of definition of \(\varphi \), and a graph homomorphism \(\varphi : D(\varphi ) \xrightarrow {} H_{}^{} \).

Note that we use, in abuse of notation, the same name for both the partial and the corresponding total graph homomorphisms. To express transitivity of typing and later also compatibility of typing, we need as well the composition of partial graph homomorphisms as a partial order between partial graph homomorphisms.

Definition 2

The composition \(\varphi ;\psi :G_{}^{} {\circ \longrightarrow }K_{}^{}\) of two partial graph homomorphisms \(\varphi : G_{}^{} {\circ \longrightarrow }H_{}^{}\) and \(\psi :H_{}^{} {\circ \longrightarrow }K_{}^{}\) is defined as follows:

  • \(D(\varphi ;\psi ) := \varphi ^{-1} (D(\psi ))\),

  • \((\varphi ;\psi )^N(\texttt {e}):= \psi ^N(\varphi ^N(\texttt {e}))\) for all \(\texttt {e}\in D(\varphi ;\psi )^N\) and \((\varphi ;\psi )^A(\texttt {f}):= \psi ^A(\varphi ^A(\texttt {f}))\) for all \(\texttt {f}\in D(\varphi ;\psi )^A\).

More abstractly, the composition of two partial graph homomorphisms is defined by the following commutative diagram of total graph homomorphisms.

figure m

Note that \(D(\varphi ;\psi ) = D(\varphi )\) if \(\psi \) is total, i.e., \(H_{}^{} = D(\psi )\).

Definition 3

For any two partial graph homomorphisms \(\varphi ,\phi : G_{}^{} {\circ \longrightarrow }H_{}^{}\) we have and \(\varphi \), \(\phi \) coincide on \(D(\varphi )\).

Now, we can define typing chains as a foundation for our investigation of multilevel typed graph transformations in the rest of the paper.

Definition 4

A typing chain \(\mathcal {G}_{} = (\overline{G}_{},{n},\tau ^{\mathcal {G}}_{})\) is given by a natural number \(n\), a sequence \(\overline{G} = [G_{n}^{}, G_{n-1}^{}, \dots , G_{1}^{}, G_{0}^{}]\) of graphs of length \(n+1\) and a family of partial graph homomorphisms, called typing morphisms, satisfying the following properties:

  • Total: All the morphisms with are total.

  • Transitive: For all we have .

  • Connex: For all we have , moreover, and coincide on .

Due to Definitions  2 and 3, transitivity and connexity together mean that , i.e., we do have a (unique) total graph homomorphism and the following commutative diagram of total graph homomorphisms

figure aa

Remark 1

For any element e in any graph \(G_{i}^{}\) in a typing chain, with \(i>0\), there exists a unique index \(m_\texttt {e}\), with \(i>m_\texttt {e}\ge 0\), such that e is in the domain of the typing morphism but not in the domain of any typing morphism with . We call the direct type of e. For any other index \(k\), with \(m_\texttt {e}>k\ge 0\), we call , if it is defined, a transitive type of e.

Example 1

Figure 3 depicts the typing morphisms between the graphs in a simplified sample hierarchy. The direct types for nodes and arrows are indicated with blue and cursive labels, respectively. All typing morphisms in the simple typing chain \(\mathcal {TG}_{}\), determined by the sequence \([\texttt {hammer\_plant},\texttt {generic\_plant},\texttt {Ecore}] \) of graphs, are total except the one from hammer_plant to generic_plant, since the direct type of has is located in Ecore. We have chosen Ecore as the top-most graph since it provides implementation support through the Eclipse Modeling Framework [24]. This enables our approach to MLM to exploit the best from fixed-level and multi-level concepts [18].    \(\square \)

Fig. 3.
figure 3

Multilevel modeling hierarchy with typing morphisms

Full size image

To describe later the flexible matching of multilevel typed rules and the result of rule applications, we need a corresponding flexible notion of morphisms between typing chains.

Definition 5

A typing chain morphism \((\phi ,f) : \mathcal {G}_{} \rightarrow \mathcal {H}_{}\) between two typing chains \(\mathcal {G}_{} = (\overline{G}_{},{n},\tau ^{\mathcal {G}}_{})\) and \(\mathcal {H}_{} = (\overline{H}_{},{m},\tau ^{\mathcal {H}}_{})\) with \(n\le m\) is given by

  • a function \(f: [n] \rightarrow [m] \), where \([n] = \{0, 1, 2, \ldots , n\} \), such that (1) \(f(0) = 0\) and (2) \(j> i\) implies \(f(j) - f(i)\ge j- i\) for all \(i, j\in [n]\), and

  • a family of total graph homomorphisms \(\phi = (\phi _i: G_{i}^{} \rightarrow H_{f(i)}^{} \mid i\in [n] )\) such that

    (1)

    i.e., due to Definitions 2 and 3, we assume for any \(n\ge j> i\ge 0\) the existence of a total graph homomorphism \(\phi _{j\mid i}\) that makes the diagram of total graph homomorphisms displayed in Fig. 4 commutative.

A typing chain morphism \((\phi ,f) : \mathcal {G}_{} \rightarrow \mathcal {H}_{}\) is closed iff for all , i.e., the right lower square in Fig. 4 is a pullback.

Fig. 4.
figure 4

Establishing a morphism between two typing chains, level-wise

Full size image

Typing morphisms are composed by the composition of commutative squares.

Definition 6

The composition \((\phi ,f);(\psi ,g) : \mathcal {G}_{} \rightarrow \mathcal {K}_{}\) of two typing chain morphisms \((\phi ,f) : \mathcal {G}_{} \rightarrow \mathcal {H}_{}\), \((\psi ,g) : \mathcal {H}_{} \rightarrow \mathcal {K}_{}\) between typing chains \(\mathcal {G}_{} = (\overline{G}_{},{n},\tau ^{\mathcal {G}}_{})\), \(\mathcal {H}_{} = (\overline{H}_{},{m},\tau ^{\mathcal {H}}_{})\), \(\mathcal {K}_{} = (\overline{K}_{},{l},\tau ^{\mathcal {K}}_{})\) with \(n\le m\le l\) is defined by , where \(\psi _{\downarrow f} := (\psi _{f(i)} : H_{f(i)}^{} \rightarrow K_{g(f(i))}^{} \mid i\in [n])\), and thus \(\phi ;\psi _{\downarrow f} := (\phi _i;\psi _{f(i)} : G_{i}^{} \rightarrow K_{g(f(i))}^{} \mid i\in [n])\).

  denotes the category of typing chains and typing chain morphisms.

A natural way to define multilevel typing of a graph \(H_{}^{}\) over a typing chain \(\mathcal {G}_{}\) would be a family \(\sigma _{}^{\mathcal {}} = (\sigma _{i}^{\mathcal {}} : H_{}^{} {\circ \longrightarrow }G_{i}^{} \mid n\ge i\ge 0)\) of partial graph homomorphisms satisfying certain properties. However, as shown in [26], those families are not appropriate to state adequate type compatibility requirements for rules and matches and to construct the results of rule applications. Therefore, we employ the sequence of the domains of definition of the \(\sigma _{i}^{\mathcal {}}\)’s as a typing chain and describe multilevel typing by means of typing chain morphisms. The following Lemma describes how any sequence of subgraphs gives rise to a typing chain.

Lemma 1

Any sequence \(\overline{H} = [H_{n}^{}, H_{n-1}^{}, \dots , H_{1}^{}, H_{0}^{}]\) of subgraphs of a graph \(H_{}^{}\), with \(H_{0}^{} = H\), can be extended to a typing chain \(\mathcal {H}_{} = (\overline{H}_{},{n},\tau ^{\mathcal {H}}_{})\) where for all \(n\ge j>i\ge 0\) the corresponding typing morphism is given by and the span of total inclusion graph homomorphisms

figure am

We call the typing chain \(\mathcal {H}_{} = (\overline{H}_{},{n},\tau ^{\mathcal {H}}_{})\) an inclusion chain on \(H_{}^{}\).

A multilevel typing of a graph \(H_{}^{}\) over a typing chain \(\mathcal {G}_{} = (\overline{G}_{},{n},\tau ^{\mathcal {G}}_{})\) is given by an inclusion chain \(\mathcal {H}_{} = (\overline{H}_{},{n},\tau ^{\mathcal {H}}_{})\) on \(H_{}^{}\) (of the same length as \(\mathcal {G}_{}\)) and a typing chain morphism \((\sigma _{}^{\mathcal {H}},id_{[n]}) : \mathcal {H}_{} \rightarrow \mathcal {G}_{}\).

3 Multilevel Typed Graph Transformations

Underlying Graph Transformation. To meet the characteristics of our application areas [19,20,21] we work with cospans

figure an

of inclusion graph homomorphisms, where \(I=L\cup R\), as the underlying graph transformation rule of a multilevel typed rule. To apply such a rule [7, 12, 13], we have to find a match \(\mu :L_{}^{}\rightarrow S_{}^{}\) of \(L_{}^{}\) in a graph \(S_{}^{}\) at the bottom-most level of an MLM hierarchy. To describe the effect of a rule application, we adapt the Sq-PO approach [7] to our cospan-rules: First, we construct a pushout and, second, a final pullback complement (FPBC) to create the graphs \(D_{}^{}\) and \(T_{}^{}\), resp. (see Fig. 2). The details behind choosing cospan rules and Sq-PO, as opposed to span rules and double-pushout (DPO), are out of the scope of this paper. In short, however: (i) cospan rules are more suitable from an implementation point-of-view since they allow for first adding new elements then deleting (some of the) old elements [13], and (ii) having both old and new elements in I allows us to introduce constraints on new elements depending on old constraints involving elements to be deleted [23]. Moreover, we apply the rules using our variant of Sq-PO [7, 13] since (i) the pushout complement in DPO, even if it exists, may not be unique, in contrast the FPBC, if it exists, is always unique (up to isomorphism), (ii) FPBC allows faithful deletion in unknown context, i.e., dangling edges may be deleted by applying the rules, however, the co-match \(\nu \) is always total, i.e., if the match \(\mu \) identifies elements to be removed with elements to be preserved, the FPBC will not exist and the application will not be allowed.

Multilevel Typed Rule. We augment the cospan rule to a multilevel typed rule by chosing a typing chain , the typing chain of the rule, together with coherent multilevel typings over \(\mathcal {MM}_{}\) of \(L\) and \(R\), respectively. That is, we choose an inclusion chain \(\mathcal {L}_{} = (\overline{L}_{},{n},\tau ^{\mathcal {L}}_{})\) on \(L\), an inclusion chain \(\mathcal {R}_{} = (\overline{R}_{},{n},\tau ^{\mathcal {R}}_{})\) on \(R\) and typing chain morphisms \((\sigma _{}^{\mathcal {L}},id_{[n]}) : \mathcal {L}_{} \rightarrow \mathcal {MM}_{}\) with \(\sigma _{}^{\mathcal {L}} =(\sigma _{i}^{\mathcal {L}} :L_{i}^{} \rightarrow MM_{i}^{} \mid i\in [n])\), \((\sigma _{}^{\mathcal {R}},id_{[n]}) : \mathcal {R}_{} \rightarrow \mathcal {MM}_{}\) with \(\sigma _{}^{\mathcal {R}} =(\sigma _{i}^{\mathcal {R}} : R_{i}^{} \rightarrow MM_{i}^{} \mid i\in [n])\) (see Fig. 5), such that \(L_{i}^{}\cap R_{}^{} =L_{}^{}\cap R_{i}^{} =L_{i}^{}\cap R_{i}^{}\) and, moreover, \(\sigma _{i}^{\mathcal {L}}\) and \(\sigma _{i}^{\mathcal {R}}\) coincide on the intersection \(L_{i}^{}\cap R_{i}^{}\) for all \(i\in [n]\).

Fig. 5.
figure 5

Rule morphisms and their type compatibility

Full size image

The inclusion chain \(\mathcal {I}_{} = (\overline{I}_{},{n},\tau ^{\mathcal {I}}_{})\) on the union (pushout) \(I=L\cup R\) is simply constructed by level-wise unions (pushouts): \(I_{i}^{} := L_{i}^{}\cup R_{i}^{}\) for all \(i\in [n]\); thus, we have \(I_{0}^{}=I_{}^{}\). Since is an adhesive category [12], the construction of \(\mathcal {I}_{}\) by pushouts and the coherence condition ensure that we get for any \(i\in [n]\) two pullbacks as shown in Fig. 6. The existence of these pullbacks implies, according to the following Lemma, that we can reconstruct the inclusion chains \(\mathcal {L}_{}\) and \(\mathcal {R}_{}\), respectively, as reducts of the inclusion chain \(\mathcal {I}_{}\).

Lemma 2

Let be given two inclusion chains \(\mathcal {G}_{} = (\overline{G}_{},{n},\tau ^{\mathcal {G}}_{})\) and \(\mathcal {H}_{} = (\overline{H}_{},{m},\tau ^{\mathcal {H}}_{})\) with \(n\le m\) and a function \(f: [n] \rightarrow [m]\) such that \(f(0) = 0\) and \(j> i\) implies \(f(j) - f(i)\ge j- i\) for all \(i, j\in [n]\). For any family \(\phi = (\phi _i: G_{i}^{} \rightarrow H_{f(i)}^{} \mid i\in [n])\) of graph homomorphisms the following two requirements are equivalent:

  1. 1.

    For all \(n\ge j> 0\) the left-hand square in Fig. 7 is a pullback.

  2. 2.

    The pair \((\phi ,f)\) constitutes a closed typing chain morphism \((\phi ,f) : \mathcal {G}_{} \rightarrow \mathcal {H}_{}\) where for all \(n\ge j>i\ge 0\) the right-hand diagram in Fig. 7 consists of two pullbacks.

Given a closed typing chain morphism \((\phi ,f) : \mathcal {G}_{} \rightarrow \mathcal {H}_{}\) between inclusion chains, as described in Lemma 2, we call \(\mathcal {G}_{}\) the reduct of \(\mathcal {H}_{}\) along \(\phi _0 : G_{0}^{} \rightarrow H_{0}^{}\) and \(f: [n] \rightarrow [m]\) while \((\phi ,f) : \mathcal {G}_{} \rightarrow \mathcal {H}_{}\) is called a reduct morphism. Note that the composition of two reduct morphisms is a reduct morphism as well.

Fig. 6.
figure 6

Type compatibility of rule morphisms level-wise

Full size image
Fig. 7.
figure 7

Reduct of inclusion chains

Full size image

Lemma 2 ensures that the families \((\lambda _{i}:L_{i}^{} \rightarrow I_{i}^{} \mid i\in [n])\) and \((\rho _{i}:R_{i}^{} \rightarrow I_{i}^{} \mid i\in [n])\) of inclusion graph homomorphisms establish reduct morphisms \((\lambda ,id_{[n]}): \mathcal {L}_{}\rightarrow \mathcal {I}_{}\) and \((\rho ,id_{[n]}): \mathcal {R}_{}\rightarrow \mathcal {I}_{}\), resp., as shown in Fig. 5.

Finally, we have to construct a typing chain morphism \((\sigma _{}^{\mathcal {I}},id_{[n]}) : \mathcal {I}_{} \rightarrow \mathcal {MM}_{}\) making the diagram in Fig. 5 commute: For all \(i\in [n]\), we constructed the union (pushout) \(I_{i}^{} := L_{i}^{}\cup R_{i}^{}\). Moreover, \(\sigma _{i}^{\mathcal {L}}\) and \(\sigma _{i}^{\mathcal {R}}\) coincide on \(L_{i}^{}\cap R_{i}^{}\), by coherence assumption, thus we get a unique \(\sigma _{i}^{\mathcal {I}} :I_{i}^{} \rightarrow MM_{i}^{}\) such that (see Fig. 6)

$$\begin{aligned} \sigma _{i}^{\mathcal {L}} = \lambda _{i};\sigma _{i}^{\mathcal {I}} \quad \text{ and }\quad \sigma _{i}^{\mathcal {R}} = \rho _{i};\sigma _{i}^{\mathcal {I}} \end{aligned}$$
(2)

Since is adhesive, Lemma 2 ensures that the family \(\sigma _{}^{\mathcal {I}} =(\sigma _{i}^{\mathcal {I}} : I_{i}^{} \rightarrow MM_{i}^{} \mid i\in [n])\) of graph homomorphisms establishes indeed a typing chain morphism \((\sigma _{}^{\mathcal {I}},id_{[n]}) : \mathcal {I}_{} \rightarrow \mathcal {MM}_{}\) while the Eq. 2 ensure that the diagram in Fig. 5 commutes indeed.

Example 2

Figure 8 shows a multilevel typed rule CreatePart from a case study [20]. This rule can be used to specify the behaviour of machines that create parts, by matching an existing type of machine that generates a certain type of parts, and in the instance at the bottom, generating such a part. META defines a typing chain \(\mathcal {MM}_{}\) of depth \(3\). It declares the graph (

figure ar

) that becomes \(MM_{2}^{}\). The declaration of the direct types Machine, creates, Part for the elements in \(MM_{2}^{}\) declares, implicitly, a graph \(MM_{1}^{}:=\) (

figure as

) that is in turn, implicitly, typed over \(MM_{0}^{}:=\texttt {ECore}\). All the morphisms in are total and uniquely determined thus we have, especially, .

FROM and TO declare as well the left-hand side \(L:=(\,\texttt {m1}\,)\) and the right-hand-side \(R:=\) (

figure av

), resp., of the rule and the direct types of the elements in \(L\) and \(R\). These direct types are all located in \(MM_{2}^{}\) thus \(L_{2}^{}=L_{}^{}\) and \(R_{2}^{}=R_{}^{}\) where the direct types define nothing but the typing morphisms \(\sigma _{2}^{\mathcal {L}}:L_{2}^{}\rightarrow MM_{2}^{}\) and \(\sigma _{2}^{\mathcal {R}}:R_{2}^{}\rightarrow MM_{2}^{}\), resp. The other typing morphisms are obtained by “transitive closure”, i.e., , and , , thus we have \(L_{}^{}=L_{0}^{}=L_{1}^{}=L_{2}^{}\) and \(R_{}^{}=R_{0}^{}=R_{1}^{}=R_{2}^{}\).

For the “plain variant” of the rule CreatePart (in Fig. 15), \(\mathcal {MM}_{}\) consists only of the graphs \(MM_{1}^{}\) = (

figure ba

), \(MM_{0}^{}=\texttt {ECore}\) and the trivial .

Multilevel Typed Match. In the multilevel typed setting all the graphs \(S_{}^{}\), \(D_{}^{}\), \(T_{}^{}\) are multilevel typed over a common typing chain , with \(n\le m\), that is determined by the path from \(S_{}^{}\) to the top of the current MLM hierarchy (see Fig. 1).

Fig. 8.
figure 8

CreatePart: a sample rule

Full size image

A match of the multilevel typed rule into a graph \(S\) with a given multilevel typing over \(\mathcal {TG}_{}\), i.e., an inclusion chain \(\mathcal {S}_{} = (\overline{S}_{},{m},\tau ^{\mathcal {S}}_{})\) with \(S_{0}^{}=S_{}^{}\) and a typing chain morphism \((\sigma _{}^{\mathcal {S}},id_{[m]}) : \mathcal {S}_{} \rightarrow \mathcal {TG}_{}\), is given by a graph homomorphism \(\mu :L\rightarrow S\) and a typing chain morphism \((\beta ,f) : \mathcal {MM}_{} \rightarrow \mathcal {TG}_{}\) such that the following two conditions are satisfied:

  • Reduct: \(\mathcal {L}_{}\) is the reduct of \(\mathcal {S}_{}\) along \(\mu :L\rightarrow S\) and \(f:[n]\rightarrow [m]\), i.e., \(\mu _{0} := \mu : L_{0}^{} = L_{}^{} \longrightarrow S_{0}^{} = S_{}^{}\) extends uniquely (by pullbacks) to a reduction morphism \((\mu ,f): \mathcal {L}_{}\rightarrow \mathcal {S}_{}\) with \(\mu = (\mu _{i}:L_{i}^{} \rightarrow S_{f(i)}^{} \mid i\in [n])\) (see Fig. 9).

  • Type compatibility: \((\sigma _{}^{\mathcal {L}},id_{[n]});(\beta ,f) = (\mu ,f);(\sigma _{}^{\mathcal {S}},id_{[m]})\), i.e., we require

    $$\begin{aligned} \sigma _{i}^{\mathcal {L}};\beta _{i} = \mu _{i};\sigma _{f(i)}^{\mathcal {S}} \text{ for } \text{ all } n\ge i> 0. \end{aligned}$$
    (3)
Fig. 9.
figure 9

Conditions for multilevel typEd Match

Full size image

Application of a Multilevel Typed Rule – Objectives. The basic idea is to construct for a given application of a graph transformation rule, as shown in Fig. 2, a unique type compatible multilevel typing of the result graphs \(D\) and \(T\). The parameters of this construction are typing chains \(\mathcal {MM}_{}\), \(\mathcal {TG}_{}\); a coherent multilevel typing of the graph transformation rule over \(\mathcal {MM}_{}\); a multilevel typing of the graph \(S\) over \(\mathcal {TG}_{}\) and a typing chain morphism \((\beta ,f) : \mathcal {MM}_{} \rightarrow \mathcal {TG}_{}\) extending the given match \(\mu :L\rightarrow S\) of graphs to a multilevel typed match satisfying the two respective conditions for multilevel typed matches.

Example 3 (Multilevel Typed Match)

To achieve precision in rule application the elements Machine, creates, Part in the original rule CreatePart are constants required to match syntactically with elements in the hierarchy. In such a way, \(MM_{1}^{}\) = (

figure bd

)has to match with generic_plant while \(MM_{2}^{}\) = (

figure be

) could match with hammer_plant or stool_plant. We will observe later that for the plain version of the rule CreatePart in Fig. 15 we could match \(MM_{1}^{}\) = (

figure bf

either with \(TG_{2}^{}\) = hammer_plant or \(TG_{1}^{}\) = generic_plant in the hierarchy in Fig. 3, where the second match would lead to undesired results (see Example 4).

Pushout step. As shown later, the pushout of the span

figure bg

in extends, in a canonical way, to a pushout of the span

figure bi

of reduct morphisms in such that the result typing chain \(\mathcal {D}_{} = (\overline{D}_{},{m},\tau ^{\mathcal {D}}_{})\) is an inclusion chain and the typing chain morphisms \((\varsigma , id_{[m]}) : \mathcal {S}_{} \hookrightarrow \mathcal {D}_{}\) and \((\delta ,f):\mathcal {I}_{}\rightarrow \mathcal {D}_{}\) become reduct morphisms (see the bottom in Fig. 10).

Fig. 10.
figure 10

Pushout step

Full size image

We get also a type compatible typing chain morphism from \(\mathcal {D}_{}\) into \(\mathcal {TG}_{}\): The back triangle in Fig. 10 commutes due to the type compatibility of the rule (see Fig. 5). The roof square commutes since the match is type compatible (see Fig. 9). This gives us \((\mu , f) ; (\sigma _{}^{\mathcal {S}},id_{[m]}) = (\lambda , id_{[n]});(\sigma _{}^{\mathcal {I}} , id_{[n]}) ; (\beta , f)\), thus the universal property of the pushout bottom square provides a unique chain morphism \((\sigma _{}^{\mathcal {D}} , id_{[m]}) : \mathcal {D}_{} \rightarrow \mathcal {TG}_{}\) such that both type compatibility conditions \((\varsigma , id_{[m]}) ; (\sigma _{}^{\mathcal {D}} , id_{[m]}) = (\sigma _{}^{\mathcal {S}} , id_{[m]})\) and \((\delta , f);(\sigma _{}^{\mathcal {D}} , id_{[m]}) = (\sigma _{}^{\mathcal {I}} , id_{[n]}) ; (\beta , f)\) are satisfied.

Pullback Complement Step. As shown later, the final pullback complement

figure bk

in extends, in a canonical way, to a sequence of reduct morphisms

figure bm

in such that the bottom square in Fig. 11 commutes.

Fig. 11.
figure 11

Pullback complement step

Full size image

Pushout of Reduct Morphisms – Two Steps. We discuss the intended pushout of the span

figure bo

of reduct morphisms in . The reduct morphism \((\lambda ,id_{[n]})\) is surjective w.r.t. levels, thus the pushout inclusion chain \(\mathcal {D}_{}\) should have the same length as \(\mathcal {S}_{}\). The rule provides, however, only information how to extend the subgraphs of \(S_{0}^{} = S_{}^{}\) at the levels \(f([n]) \subseteq [m]\). For the subgraphs in \(\mathcal {S}_{}\) at levels in \([m] \setminus f([n])\) the rule does not impose anything thus we let the subgraphs at those levels untouched. In terms of typing chain morphisms, this means that we factorize the reduct morphism \((\mu ,f)\) into two reduct morphisms and that we will construct the resulting inclusion chain \(\mathcal {D}_{}\) in two pushout steps (see Fig. 12) where \(\mathcal {S}_{\downarrow f} := (\overline{S}_{\downarrow f},{n},\tau ^{\mathcal {S}}_{\downarrow f})\) with \(\overline{S}_{\downarrow f} := [S_{f(n)}^{}, S_{f(n-1)}^{}, \ldots , S_{f(1)}^{}, S_{f(0)=0}^{}]\) and Note, that \(\overline{S}_{\downarrow f}:=[S_{f(n)}^{}, \ldots , S_{f(0)}^{}]\) is just a shorthand for the defining statement: \((\overline{S}_{\downarrow f})_i:= S_{f(i)}^{}\) for all \(n\ge i\ge 0\).

Fig. 12.
figure 12

Two pushout steps to construct the inclusion chain \(\mathcal {D}_{}\)

Full size image

The reduct morphism \((\overline{id}^{\mathcal {S}_{}}_{\downarrow f},f): \mathcal {S}_{\downarrow f} \rightarrow \mathcal {S}_{}\) is a level-wise identity and just embeds an inclusion chain of length \(n+1\) into an inclusion chain of length \(m+1\), i.e., \( \overline{id}^{\mathcal {S}_{}}_{\downarrow f} = (id_{f(i)}: S_{f(i)}^{} \rightarrow S_{f(i)}^{} \mid i\in [n] ). \) In the pushout step (1) we will construct a pushout of inclusion chains of equal length and obtain a chain \(\mathcal {D}_{\downarrow f} := (\overline{D}_{\downarrow f},{n},\tau ^{\mathcal {D}}_{\downarrow f})\) with \(\overline{D}_{\downarrow f} = [D_{f(n)}^{}, D_{f(n-1)}^{},\ldots ,D_{f(1)}^{},D_{f(0)=0}^{}]\) and .

In the pushout step (2) we will fill the gaps in \(\mathcal {D}_{\downarrow f}\) with the corresponding untouched graphs from the original inclusion chain \(\mathcal {S}_{}\).

Pushouts of Graphs for Inclusion Graph Homomorphisms. Our constructions and proofs rely on the standard construction of pushouts in for a span of an inclusion graph homomorphism \(\phi : G_{}^{} \hookrightarrow H_{}^{}\) and an arbitrary graph homomorphism \(\psi : G_{}^{} \rightarrow K_{}^{}\) where we assume that \(H_{}^{}\) and \(K_{}^{}\) are disjoint. The pushout \(P_{}^{}\) is given by \(P_{}^{N} := K_{}^{N} \cup H_{}^{N} \setminus G_{}^{N}\), \(P_{}^{A} := K_{}^{A} \cup H_{}^{A} \setminus G_{}^{A}\) and \( sc ^{P}(e) := sc ^{K}(e)\), if \(e \in K_{}^{A}\), and \( sc ^{P}(e) :=\psi ^A( sc ^{H}(e))\), if \(e \in H_{}^{A} \setminus G_{}^{A}\). \( tg ^{P}\) is defined analogously. \(\phi ^*: K_{}^{} \hookrightarrow P_{}^{}\) is an inclusion graph homomorphism by construction and \(\psi ^*: H_{}^{} \rightarrow P_{}^{}\) is defined for \(X\in \{A,N\}\) by \(\psi ^{*X}(v) := \psi ^X(v)\), if \(v \in G_{}^{X}\) and \(\psi ^{*X}(v) := v\) , if \(v \in H_{}^{X} \setminus G_{}^{X}\).

The pair \(G_{}^{} \setminus H_{}^{} := (H_{}^{N} \setminus G_{}^{N}, H_{}^{A} \setminus G_{}^{A})\) of subsets of nodes and arrows of \(H_{}^{}\) is, in general, not establishing a subgraph of \(H_{}^{}\). We will nevertheless use the notation \(P_{}^{} = K_{}^{} + H_{}^{} \setminus G_{}^{}\) to indicate that \(P_{}^{}\) is constructed as described above. \(\psi ^*\) can be described then as a sum of two parallel pairs of mappings

$$\begin{aligned} \psi ^*= \psi + id_{H_{}^{}\setminus G_{}^{}} := (\psi ^N+ id_{H_{}^{N}\setminus G_{}^{N}}, \psi ^A+ id_{H_{}^{A}\setminus G_{}^{A}}) \end{aligned}$$
(4)

Pushout for Inclusion Chains with Equal Depth. We consider now the span

figure bt

of reduct morphisms in (see Fig. 12). For each level \(i\in [n]\) we construct the corresponding pushout of graph homomorphisms. This ensures, especially,

$$\begin{aligned} \lambda _{i};\delta _i= \mu _{i};\varsigma _{f(i)} \quad \text{ for } \text{ all }\quad i\in [n]. \end{aligned}$$
(5)
Fig. 13.
figure 13

Level-wise pushout construction

Full size image

We look at an arbitrary level \(n\ge i\ge 1\) together with the base level \(0\) (see Fig. 13). We get a cube where the top and bottom square are pushouts by construction. In addition, the left and back square are pullbacks since \((\mu ,id_{[n]})\) and \((\lambda ,id_{[n]})\), respectively, are reduct morphisms. We get a unique graph homomorphism that makes the cube commute. By the uniqueness of mediating morphisms and the fact that the top pushout square has the Van Kampen property (see [12, 25]), we can conclude that the front and the right square are pullbacks as well. That the back square is a pullback means nothing but \(L_{i}^{} = L_{}^{}\cap I_{i}^{}\). This entails \(I_{i}^{}\setminus L_{i}^{} \subseteq I_{}^{}\setminus L_{}^{}\) thus turns out to be the sum of the two inclusions and and is therefore an inclusion itself.

The sequence \([D_{f(n)}^{}, D_{f(n-1)}^{}, \dots , D_{f(1)}^{}, D_{0}^{}]\) of subgraphs of \(D_{}^{}=D_{0}^{}\) defines the intended inclusion chain \(\mathcal {D}_{\downarrow f}\). Since the front and right squares in Fig. 13 are pullbacks, Lemma 2 ensures that the family \(\varsigma _{\downarrow f}=(\varsigma _{f(i)}: S_{f(i)}^{} \hookrightarrow D_{f(i)}^{} \mid i\in [n])\) of inclusion graph homomorphisms constitutes a reduct morphism \((\varsigma _{\downarrow f},id_{[n]}): \mathcal {S}_{\downarrow f} \rightarrow \mathcal {D}_{\downarrow f}\) while the family \(\delta =(\delta _{i}: I_{i}^{} \rightarrow D_{f(i)}^{} \mid i\in [n])\) of graph homomorphisms constitutes a reduct morphism \((\delta ,id_{[n]}): \mathcal {I}_{} \rightarrow \mathcal {D}_{\downarrow f}\). Finally, Eq. 5 ensures that the resulting square (1) of reduct morphisms in Fig. 12 commutes. The proof that we have constructed a pushout in is given in [26].

Remark 2 (Only one pushout)

\(\varsigma _{f(i)}\) and \(\delta _{i}\) are jointly surjective for all \(n\ge i\ge 1\) thus we can describe \(D_{f(i)}^{}\) as the union \(D_{f(i)}^{}= \varsigma (S_{f(i)}^{}) \cup \delta (I_{i}^{})\). Hence in practice, there is no need for an explicit construction of pushouts at all the levels \(n\ge i\ge 1\); these are all constructed implicitly by the pushout construction at level 0.

Pushout by Chain Extension. To obtain an inclusion chain \(\mathcal {D}_{}\) of length \(m+1\), we fill the gaps in \(\mathcal {D}_{\downarrow f}\) by corresponding subgraphs of \(S\): \(D_{a}^{} :=D_{a}^{}\) if \(a\in f([n])\) and \(D_{a}^{} := S_{a}^{}\) if \(a\in [m] \setminus f([n])\) and obtain the intended inclusion chain \(\mathcal {D}_{} = (\overline{D}_{},{m},\tau ^{\mathcal {D}}_{})\). The family \(\overline{id}^{\mathcal {D}_{}}_{\downarrow f} = (id_{D_{f(i)}^{}}: D_{f(i)}^{} \rightarrow D_{f(i)}^{} \mid i\in [n])\) of identities defines trivially a reduct morphism \((\overline{Id}^{\mathcal {D}_{}}_{\downarrow f},f) : \mathcal {D}_{\downarrow f} \rightarrow \mathcal {D}_{}\). One can show that the family \(\varsigma = (\varsigma _{a}: S_{a}^{} \rightarrow D_{a}^{} \mid a \in [m])\) of graph homomorphisms defined by

$$\begin{aligned} \varsigma _{a} := {\left\{ \begin{array}{ll} \varsigma _{a} : S_{a}^{} \hookrightarrow D_{a}^{} &{}\text{ if } a \in f([n])\\ id_{S_{a}^{}} : S_{a}^{} \rightarrow D_{a}^{} = S_{a}^{} &{}\text{ if } a \in [m] \setminus f([n]) \end{array}\right. } \end{aligned}$$

establishes a reduct morphism \((\varsigma , id_{[m]}) : \mathcal {S}_{} \rightarrow \mathcal {D}_{}\). The two reduct morphisms \((\overline{id}^{\mathcal {D}_{}}_{\downarrow f},f) : \mathcal {D}_{\downarrow f} \rightarrow \mathcal {D}_{}\) and \((\varsigma , id_{[m]}) : \mathcal {S}_{} \rightarrow \mathcal {D}_{}\) establish square (2) in Fig. 12 that commutes trivially. In [26] it is shown that square (2) is also a pushout in .

Pullback Complement. We construct the reduct of \(\mathcal {D}_{} = (\overline{D}_{},{m},\tau ^{\mathcal {D}}_{})\) along \(\theta :T_{}^{}\hookrightarrow D_{}^{}\) and \(id_{[m]}\) by level-wise intersection (pullback) for all \(n\ge i\ge 1\) (see the pullback square below). Due to Lemma 2, we obtain, in such a way, an inclusion chain \(\mathcal {T}_{} = (\overline{T}_{},{m},\tau ^{\mathcal {T}}_{})\) together with a reduct morphism \((\theta ,id_{[m]}):\mathcal {T}_{}\rightarrow \mathcal {D}_{}\). The multilevel typing of \(\mathcal {T}_{}{}\) is simply borrowed from \(\mathcal {D}_{}\), that is, we define (see Fig. 11)

$$\begin{aligned} (\sigma _{}^{\mathcal {T}},id_{[m]}) := (\theta ,id_{[m]}); (\sigma _{}^{\mathcal {D}},id_{[m]}) \end{aligned}$$
(6)

and this gives us trivially the intended type compatibility of \((\theta ,id_{[m]})\). The typing chain morphism \((\nu ,f) : \mathcal {R}_{} \rightarrow \mathcal {T}_{}\) with \(\nu = (\nu _i: R_{i}^{} \rightarrow T_{f(i)}^{} \mid i\in [n])\) such that

$$\begin{aligned} (\rho ,id_{[n]});(\delta ,f) = (\nu ,f);(\theta ,id_{[m]}) \end{aligned}$$
(7)

is simply given by pullback composition and decomposition in : For each \(n\ge i\ge 1\) we consider the following incomplete cube on the right-hand side:

figure cc

The back square, the left square as well as the front square are pullbacks since \((\rho ,id_{[n]})\), \((\delta ,f)\) and \((\theta ,id_{[m]})\), respectively, are reduct morphisms. The top square is constructed as a pullback complement. The diagonal square from to is a pullback due to the composition of the back pullback and the left pullback. The decomposition of this diagonal pullback w.r.t. the front pullback gives us \(\nu _i: R_{i}^{} \rightarrow T_{i}^{}\) making the cube, and especially the bottom square, commute and making the right square to a pullback as well.

According to Lemma 2 the family \(\nu = (\nu _i: R_{i}^{} \rightarrow T_{f(i)}^{} \mid i\in [n])\) of graph homomorphisms defines a reduct morphism \((\nu ,f) : \mathcal {R}_{} \rightarrow \mathcal {T}_{}\) where condition 7 is simply satisfied by construction. Finally, \((\nu ,f)\) is also type compatible since conditions 6 and 7 ensure that the roof square in Fig. 11 commutes.

Example 4

To present a non-trivial rule application for our example, we discuss the undesired application of the plain version of rule CreatePart (see Fig. 14), mentioned in Example 3, for a state of the hammer configuration with only one node ghead, as shown in hammer_config_0 in Fig. 15. So, we have \(f:[1]\rightarrow [2]\), with \(f(0)=0, f(1)=1\), and the “undesired match” of \(MM_{1}^{}\) = (

figure cf

) with \(TG_{1}^{}\) = generic_plant = (

figure cg

) together with the trivial match of the left-hand side \(L=(\,\texttt {m1}\,)\) of the rule with \(\texttt {hammer\_config\_0} = (\,\texttt {ghead}\,)\). The resulting inclusion chains \(\mathcal {S}_{}\), \(\mathcal {L}_{}\), \(\mathcal {R}_{}\) and two reduct morphisms between them are depicted in Fig. 14. Note, that the ellipse and cursive labels indicate here the corresponding typing chain morphisms \((\sigma _{}^{\mathcal {S}},id_{[2]})\), \((\sigma _{}^{\mathcal {L}},id_{[1]})\) and \((\sigma _{}^{\mathcal {R}},id_{[1]})\), respectively.

Fig. 14.
figure 14

Inclusion chains for the plain version of CreatePart

Full size image
Fig. 15.
figure 15

Plain version of CreatePart and its application

Full size image

For the two levels in \(f([1])=\{0,1\}\subset [2]\) we construct the pushouts \(D_{0}^{}\) and \(D_{1}^{}\) while \(D_{2}^{}\) is just taken as \(S_{2}^{}\). The lowest level in \(\mathcal {D}_{}\), where the new elements p1 and c appear, is level \(1\) thus the constructed direct types of p1 and c are Part and creates, resp., as shown in hammer_config_1 in Fig. 15.

4 Conclusions, Related and Future Work

Conclusion. Multilevel modeling offers more flexibility on top of traditional modeling techniques by supporting an unlimited number of abstraction levels. Our approach to multilevel modeling enhances reusability of concepts and their behaviour by allowing the definition of flexible transformation rules which are applicable to different hierarchies with a variable number of levels. In this paper, we have presented a formalization of these flexible and reusable transformation rules based on graph transformations. We represent multilevel models by multilevel typed graphs whose manipulation and transformation are carried out by multilevel typed graph transformation rules. These rules are cospans of three graphs and two inclusion graph homomorphisms where the three graphs are multilevel typed over a common typing chain. As these rules are represented as cospans, their application is carried out by a pushout and a final pullback complement construction for the underlying graphs in the category . We have identified type compatibility conditions, for rules and their matches, which are crucial for rule applications. Moreover, we have shown that typed graph transformations can be generalized to multilevel typed graph transformations improving preciseness, flexibility and reusability of transformation rules.

Related work. The theory and practise of graph transformations are well-studied, and the concept of model transformations applied to MLM is not novel. Earlier works in the area have worked in the extension of pre-existing model transformation languages to be able to manipulate multilevel models and model hierarchies. In [3], the authors adapt ATL [15] to manipulate multilevel models built with the Melanee tool [2]. In a similar manner, [11] proposes the adaptation of ETL [16] and other languages from the Epsilon family [14] for the application of model transformation rules into multilevel hierarchies created with MetaDepth [8]. These works, however, tackle the problem from the practical point of view. That is, how to reuse mature off-the-shelf tools for model transformation in the context of MLM, via the manipulation of a “flattened” representation of the hierarchy to emulate multilevel transformations. Our approach, on the contrary, has been developed from scratch with a multilevel setting in mind, and we believe it can be further extended to tackle all scenarios considered by other approaches. Therefore, to the best of our knowledge, there are no formal treatments of multilevel typed graph transformations in the literature except for our previous works [19, 20, 26] (see Sect. 4 in [26]). Hence, we consider our approach the first approximation to formally address the challenges which come with multilevel modeling and multilevel model transformations.

Common for our work and [9] is that the concepts of typing chains, multilevel typed graphs and multilevel models originate in [22]. However, [9] presents partial morphisms as spans of total morphisms and does not use the composition of those spans explicitly. Wrt. typing chains, a multilevel model in [9] is a sequence of graphs \([G_{n}^{}, G_{n-1}^{}, \dots , G_{1}^{}, G_{0}^{}]\) together with the subfamily of typing morphisms.

Future work. Although it is trivial to see that the bottom square in the cube for the pullback complement step becomes a pullback for all \(n\ge i\ge 1\), we leave it for future work to prove that we indeed have constructed a final pullback complement in . A utilization of our theory to deal with coupled transformations [21] in the setting of multilevel typed modelling is also desirable. Furthermore, it would be interesting to investigate the category for its own; e.g., study its monomorphisms and epimorphisms, possible factorization systems, and the conditions for existence of general pushouts and pullbacks.