Agnès Arnould

Hakim Belhaouari

Thomas Bellet

Pascale Le Gall

Romain Pascual
email: romain.pascual@centralesupelec.fr

Preserving consistency in geometric modeling with graph transformations

Keywords: DPO graph transformation, topology-based geometric modeling, graph transformation with variables, generalized maps, consistency preservation, static analysis

Labeled graphs are particularly well adapted to represent objects in the context of topology-based geometric modeling. Thus, graph transformation theory is used to implement modeling operations and check their consistency. This article defines a class of graph transformation rules dedicated to embedding computations. Objects are here defined as a particular subclass of labeled graphs in which arc labels encode their topological structure (i.e." cell subdivision: vertex, edge, face, etc.) and node labels encode their embedding (i.e." relevant data: vertex positions, face colors, volume density, etc.). Object consistency is defined by labeling constraints which must be preserved by modeling operations that modify topology and/or embedding. Dedicated graph transformation variables allow us to access the existing embedding from the underlying topological structure (e.g., collecting all the points of a face) in order to compute the new embedding using user-provided functions (e.g., compute the barycenter of several points). To ensure the safety of the defined operations, we provide syntactic conditions on rules that preserve the object consistency constraints.

Introduction

Graphs can be used to represent geometric objects in 2D, 3D, or nD. For instance, a polygon soup is typically used in lighting simulation software for animated movies or Preprint submitted to Mathematical Structures in Computer Science 4 July 2022 video games. In topology-based geometric modeling, semantic information is added to the polygons to describe the topological relations between the object's elements. For instance, the tabletop and the legs of a table are linked together. More precisely, topologybased geometric modeling deals with the representation and manipulation of objects according to their topological structure (cell subdivision in vertices, edges, faces, etc.) and their embedding (geometry and other types of information attached to their topological cells). Using the topological model of generalized maps [START_REF] Lienhardt | N-dimensional generalized combinatorial maps and cellular quasimanifolds[END_REF][START_REF] Damiand | Combinatorial Maps: Efficient Data Structures for Computer Graphics and Image Processing[END_REF], objects are defined as a particular subclass of labeled graphs. In generalized maps, arc labels encode the topological structure of the object while node labels store the embedding values. Defining embeddings on topological cells implies two facts. First, each node in the graph may have several embedding values. Secondly, all nodes that belong to the same cell must have the same embedding value. To satisfy these two properties, the model can store the embedding value either once per cell or once per node. In the first case, the object's modifications rely on the possibility of efficiently retrieving these embedding values. In the second case, the application of a transformation operation can only be valid if it guarantees that all elements are adequately labeled, i.e., every node has a value for each embedding, and all nodes of a topological cell have the same value. For instance, Figure 1(a) depicts the triangulation of a face and Figure 1(b) the removal of an edge, both in a colored 2D object. In either figure, the topological structure of the object contains four faces (two triangles, a square, and a pentagon) glued together, and the embedding associates a color to each face. Note that both operations simultaneously transform the topological structure and the embedding. The face triangulation topologically subdivides the face into triangles. From the embedding point of view, the new faces' colors are computed as the mix of the subdivided face color and the neighboring face color. Topologically, the edge removal merges two neighboring faces by removing the shared edge, while the embedding modification mixes the two original face colors. Note that, in the case of the edge deletion, if we simply modify the graph nodes that describe this edge, we would create a unique face with two colors. Thus, we need to propagate the local modification to the whole face. However, when we delete an edge, we cannot assume the topology of the adjacent faces. These faces could have 3, 4, or arbitrary many edges and vertices. Therefore, we need a framework that ensures the preservation of consistency on a global scale. Topology-based geometric modeling exploits mathematically well-defined structures to specify algorithms expressing modeling operations. Proofs of correctness for these algorithms have to be done manually [START_REF] Damiand | Combinatorial Maps: Efficient Data Structures for Computer Graphics and Image Processing[END_REF] or with the help of a prover like Coq [START_REF] Puitg | Formal specification and theorem proving breakthroughs in geometric modeling[END_REF]. Each new operation must be proven to preserve model consistency for such solutions. On the other hand, procedural modeling relies on a small set of elementary rules that are shown to be coherent. Any other transformation is decomposed in a sequence of elementary rules and therefore preserves the model's consistency. In this case, the rules are tailored to the applicative domain and are not necessarily transposable to other domains. Capitalizing on both approaches, we propose a framework in which transformations can be expressed as rules that preserve the model consistency. Static analysis of the rules guarantees consistency preservation. Therefore, we only need to prove that the rule conditions do ensure the preservation of the model consistency.

As topological structures can be represented as a particular class of graphs, the use of graph transformations to define modeling operations has already been studied [START_REF] Smith | Local Specification of Surface Subdivision Algorithms[END_REF][START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF][START_REF] Spicher | Declarative Mesh Subdivision Using Topological Rewriting in MGS[END_REF][START_REF] Pascual | Topological consistency preservation with graph transformation schemes[END_REF]. Derived from string and tree rewriting techniques, this rule-based approach offers a natural way to describe complex transformations intuitively. Graph transformations have applications in many areas such as software engineering [START_REF] Baresi | Tutorial Introduction to Graph Transformation: A Software Engineering Perspective[END_REF][START_REF] Heckel | Graph Transformation for Software Engineers: With Applications to Model-Based Development and Domain-Specific Language Engineering[END_REF], concurrent and distributed systems [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation: Concurrency, Parallelism, and Distribution[END_REF], database design [START_REF] Gyssens | A graph-oriented object database model[END_REF], IT landscape modeling [START_REF] Haeusler | ChronoSphere: a graph-based EMF model repository for IT landscape models[END_REF], and in our case geometric modeling. Graph transformations mainly offer a sound framework to express the preservation of domain-specific properties. For our concerns, they provide a tool for constraint-preserving modeling operations. In [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF], we introduced dedicated rule variables to handle the topological genericity of modeling operations generically. These variables abstract topological cells and their transformations. To extend their usability, we showed that they offer a safer design of topological operations to produce a topological-based geometric modeler [START_REF] Bellet | Designing a topological modeler kernel: a rule-based approach[END_REF], which was more accessible than traditional ad hoc implementations that are fastidious to code and vulnerable to consistency bugs. In [START_REF] Bellet | Rule-based transformations for geometric modeling[END_REF], we defined a new graph category that allows nodes to have multiple labels in order to represent the multiple embedding types simultaneously (e.g., a face being labeled by both its color and its porosity). We proved the existence of graph transformations in this category and introduced a new type of dedicated variables and operators to express embedding transformations in rules.

In this article, we propose a generic graph transformation approach that allows the implementation of any application domain's modeling operations. More precisely, this paper addresses the embedding aspect of modeling operations considering a representation of embedded generalized maps as labeled graphs introduced in [START_REF] Bellet | Rule-based transformations for geometric modeling[END_REF] and in which node labels and associated labeling constraints encode the object embedding. Our first contribution is to give conditions on the relabeling graph transformations of [START_REF] Habel | Relabelling in Graph Transformation[END_REF] to guarantee the preservation of the embedding consistency. For example, in the case of the edge removal of Figure 1(b), we will ensure that by construction, after the application of the corresponding rules, all nodes of the resulting face end up labeled with the same color. Our second contribution is the generic computation of the new embedding values created by a transformation. This generic computation is achieved with a rule-based language-based on [START_REF] Hoffmann | Graph Transformation with Variables[END_REF]. For instance, the mix of face colors for any colored object will be computable.

The resulting rule schemes exploit dedicated graph transformation variables and terms to access the existing embedding through the topological structure and apply functions provided by the user with embedding data types. For example, the triangulation of Figure 1(a) will be defined by a rule scheme in which the colors of the created faces are computed by applying the user function " mix of two colors" to the subdivided face color and the respective adjacent face colors. The safety of this user-oriented language is as essential as its expressiveness. Therefore, our last contribution is providing syntactic conditions to guide rule scheme design and ensure the preservation of object consistency.

As a disclaimer, we wish to point out that we will refer to standard graph rewriting techniques, more precisely about versions of double-pushout rewriting. However, based on the specific needs of geometric modeling (e.g., orbit variables, computation of embedding values), the presented constructions will be a hand-curated version of DPO-rewriting exploiting element-based definitions to identify the various elements throughout the derivations. Essentially, we use inclusions instead of standard monomorphisms.

The remainder of this paper is structured as follows. First, Section 2 presents related works about L-system approaches of geometric modeling (usually referred to as procedural modeling) and some successful graph transformation applications. Sections 3 and 4 then present the theoretical foundations supporting our work. In Section 3, we describe relabeling in labeled graph transformations as introduced by [START_REF] Habel | Relabelling in Graph Transformation[END_REF] that will allow us to modify objects. We also present the use of variables in graph transformations as introduced by [START_REF] Hoffmann | Graph Transformation with Variables[END_REF]. The context of topological-based geometric modeling is then presented in Section 4. We focus on the topological model of generalized maps [START_REF] Lienhardt | N-dimensional generalized combinatorial maps and cellular quasimanifolds[END_REF] and give conditions from [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF][START_REF] Pascual | Topological consistency preservation with graph transformation schemes[END_REF] to preserve the model consistency. Section 5 then similarly presents our embedded version of generalized maps and conditions under which graph transformations preserve the embedding consistency. The subsequent three sections focus on the rule-based language dedicated to embedding modifications. Section 6 introduces the rule scheme syntax, in particular terms that allow generic computation of new embedding values from existing ones in the object (e.g., to mix two unspecified face colors). Section 7 presents the rule scheme application, especially how schemes are instantiated to propagate minimally defined modifications (e.g., automatically change the color of all nodes of one face). Section 8 provides syntactic conditions on rule schemes to ensure embedding consistency preservation. This article presents the final version of the variables as they are implemented in the toolset Jerboa [START_REF] Belhaouari | Jerboa: A Graph Transformation Library for Topology-Based Geometric Modeling[END_REF] that allows the generation of a geometric modeler kernel from a set of rules. Some applications done with Jerboa are shown in Section 9, while concluding remarks are given in Section 10.

Related Work

They are particularly useful for modeling objects that are too cumbersome to be modeled by hand and for coping with the increasing level of details and size used to build complex and realistic objects.

Intuitively, a transformation rule looks like A → B and stands for the modification of object A into object B. This description of modifications within the object is highly visual and eases the design of geometric objects drastically. Indeed, this approach has been successfully applied to generate objects such as plants [START_REF] Prusinkiewicz | Development models of herbaceous plants for computer imagery purposes[END_REF], terrains (see the survey done in [START_REF] Smelik | A survey of procedural methods for terrain modelling[END_REF]), buildings [START_REF] Müller | Procedural modeling of buildings[END_REF] or cities [START_REF] Parish | Procedural modeling of cities[END_REF].

In all these applications, object modifications are defined by a limited set of high-level operations such as creating a new branch, inserting a floor or subdividing a district with a road. Such operations do not contain all the low-level transformations on the actual object representation. Therefore, each high-level operation has its dedicated implementation and consistency preservation mechanism. This lack of adaptability entails that any change requires additional implementation and debugging efforts, which we avoid using graph transformations.

Graph transformations commonly refer to rule-based languages designed to manipulate graphs. The chosen framework for graph transformations is based on the definition of graphs and graph morphisms described using category theory. In that sense, graphs are defined by a set of objects, called nodes, and a set of links between these objects, called arcs. Among all graph transformation approaches, we choose the so-called double-pushout approach (or DPO) [START_REF] Corradini | Algebraic Approaches to Graph Transformation, Part I: Basic Concepts and Double Pushout Approach[END_REF][START_REF] Ehrig | Fundamentals of Algebraic Graph Transformation[END_REF]. We preferred double-pushout over single-pushout (or SPO) because in the SPO approach dangling edges after the deletion of the left-hand pattern are also deleted, which is less conservative. In other words, DPO eases the construction of conditions on rules to preserve constraints. The main drawback is having to check the dangling condition, which turns out to be doable in a static manner for our specific class of graphs, as shown in [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF]. Besides, we want to take advantage of the well-founded DPO framework given in [START_REF] Habel | Relabelling in Graph Transformation[END_REF], which allows the relabeling of nodes and arcs in graph transformations. [START_REF] Habel | Computational Completeness of Programming Languages Based on Graph Transformation[END_REF] showed that any computable function on graphs could be defined with a set of graph transformation rules supporting a non-deterministic application of rules, their composition, and their iteration. However, in practical applications, operations are simpler to express and verify when defined as a single rule. Graph transformations have been enriched with variables to make them more generic while customizable to meet the various application needs. Intuitively, a rule with variables is a meta-level rule that yields a concrete rule for each possible instantiation of the variables with concrete elements. Different variable types have been introduced to enrich graph transformations depending on the genericity purposes : node replacement graph grammars [START_REF] Engelfriet | Node replacement graph grammars[END_REF] and hyperedge graph grammars [START_REF] Habel | Hyperedge Replacement: Grammars and Languages[END_REF][START_REF] Drewes | Hyperedge replacement graph grammars[END_REF] somewhat generalized with cloning in adaptive star graph grammars [START_REF] Drewes | Adaptive star grammars and their languages[END_REF] or attribute graph grammars [START_REF] Plump | Towards Graph Programs for Graph Algorithms[END_REF] and used for the interpretation of schematic diagrams [START_REF] Bunke | Attributed Programmed Graph Grammars and Their Application to Schematic Diagram Interpretation[END_REF] or image parsing [START_REF] Han | Bottom-up/top-down image parsing by attribute graph grammar[END_REF].

Extensions made to graph transformations ease their integration in generic tools, such as GrGen.NET [START_REF] Geiß | GrGen: A Fast SPO-Based Graph Rewriting Tool[END_REF], Groove [START_REF] Rensink | The GROOVE Simulator: A Tool for State Space Generation[END_REF], AGG [START_REF] Taentzer | AGG: A Graph Transformation Environment for Modeling and Validation of Software[END_REF] or PROGRES [START_REF] Schürr | Graph grammar engineering with PRO-GRES[END_REF]. Besides, graph transformations operate at a low level on graph structures. Thus, rules are self-contained.

Therefore, a single rule application engine tailored to a given graph transformation class enables the application of all domain-related rules. These engines justifies the development of dedicated tools, such as Fujaba [START_REF] Nickel | The FUJABA environment[END_REF] for code refactoring, Gremlin [START_REF] Rodriguez | The Gremlin graph traversal machine and language (invited talk)[END_REF] for queries in graph databases, DiaGen [START_REF] Minas | DiaGen: a generator for diagram editors providing direct manipulation and execution of diagrams[END_REF] for the manipulation of diagrams, or GReTL [START_REF] Ebert | GReTL: an extensible, operational, graph-based transformation language[END_REF] for the parallel construction of metamodels and conforming models. This point is crucial in designing a generic modeling tool as it minimizes the implementation and debugging efforts.

In computer graphics, graph transformations have already been used for several purposes. For instance, in [START_REF] You | A Syntactic Approach to Shape Recognition Using Attributed Grammars[END_REF][START_REF] Tsai | Attributed Grammar-A Tool for Combining Syntactic and Statistical Approaches to Pattern Recognition[END_REF], attributed grammars were defined to describe and classify the syntactic structures of two-dimensional shapes. More recently, indoor scenes have been represented as graphs in [START_REF] Ikehata | Structured Indoor Modeling[END_REF], where graph grammars allowed the reconstruction of scenes from images acquired by cameras. In [START_REF] Vilgertshofer | Using graph rewriting methods for the semiautomatic generation of parametric infrastructure models[END_REF], graphs describe the modeling process of tunnels, and graph transformations specify modifications to this process. The main idea is to handle consistency between different levels of detail in the infrastructure during transformations. In [START_REF] Ong | A graph model and grammar for multi-scale modelling using XL[END_REF], multiscale modeling of plants also takes advantage of a graph grammar with the Relational Growth Grammar.

Graph Transformations

This section recalls the Double-PushOut (DPO) approach to graph transformations [START_REF] Ehrig | Fundamentals of Algebraic Graph Transformation[END_REF], their specification in the category of partially labeled graphs [START_REF] Habel | Relabelling in Graph Transformation[END_REF] and their extension to rules with variables [START_REF] Hoffmann | Graph Transformation with Variables[END_REF]. In the DPO approach, a transformation is expressed using two gluing diagrams defined in terms of category theory. More precisely, these diagrams are pushouts in the category of graphs and graph morphisms. To make the presentation more intuitive, let us consider the simple example of a DPO graph transformation given in Figure 2. The rule is given at the top of Figure 2 by the three graphs L, K, and R and by the two graph inclusions1 L ← K → R where the symbol → (resp. ← ) denotes the inclusion when the source graph is given first (resp. secondly) and the target graph secondly (resp. first). In a rule, L is called the left-hand side, R the right-hand side, and K the interface of r. In this example, nodes are identified by letters (a, b or c) while arcs are anonymous. Nodes and arcs are labeled by numbers (1, 3, or 5 for the nodes and 2 or 4 for the arcs). Intuitively, the left-hand side of the rule L is the pattern to transform, the right-hand side R is the transformed pattern, and the interface K is the preserved part common to both L and R. The graph morphism L → G allows the matched pattern (graph L) to be identified inside the graph under modification (graph G). In Figure 2, the match morphism coincides with the inclusion.

Double-pushout graph transformations

a b (L) 1 3 a b (K) 1 a b (R) 1 3 2 3 a b (G) 1 3 c 5 a b (D) 1 3 c 5 a b (H) 1 3 c 5 (1) (2) 2 2 2 2 2 4 4 4
In the first pushout (1), all elements (nodes and arcs) in L that are not in K are deleted from G to obtain D. In Figure 2, the two loops on nodes a and b are removed from L and thus are also removed in D. In the second pushout (2), elements in K are preserved while elements of R that are not already in K are added to D, yielding H. In Figure 2, an arc is added in the graph H between the two preserved nodes a and b. When the match morphism m : L → G meets some conditions,2 the double-pushout construction is well-defined and creates a unique graph H (up to graph isomorphism), that is the result of the application of the graph transformation As already pointed out in [START_REF] Habel | Relabelling in Graph Transformation[END_REF], graph morphisms have to preserve arc and nodes labels, preventing relabeling in classical DPO transformation. Note that the relabeling of an arc can still be achieved by removing it while adding an arc with a new label between the same source and target nodes. However, this solution does not make the relabeling of a node possible. Consequently, we prefer the DPO approach of [START_REF] Habel | Relabelling in Graph Transformation[END_REF] that allows relabeling by considering partially labeled graphs. Let us take the example of the relabeling rule of Figure 3. Node b is labeled 7 in the left-hand side L and 3 in the right-hand side R, and therefore it is unlabeled in the interface K. Note that the two morphisms K → L and K → R on partially labeled graphs L, K, R do not have to preserve labeling. In particular, the undefined label of b in K is not preserved.

L ← K → R through the match morphism L → G. a 1 b (L) 7 a 1 (R) 3 2 a b (K) b 2 1
We now present the main definitions and results of [START_REF] Habel | Relabelling in Graph Transformation[END_REF] on partially labeled graph transformations.

Graph transformations on partially labeled graphs

A partially labeled graph G = (V G , E G , s G , t G , l G,V , l G,E
) consists of two finite sets V G and E G of nodes and arcs, two source and target functions s G , t G : E G → V G , and two partial labeling functions3 l G,V : V G → C V for the nodes and l G,E : E G → C E for the arcs, where C V and C E are fixed sets of node and arc labels. We say that G is totally labeled if l G,V and l G,E are total functions. A path in a graph G is a sequence e 1 ...e k of arcs from E G with 1 ≤ k, such that t G (e i ) = s G (e i+1 ) for each 1 ≤ i < k. s G (e 1 ) and t G (e k ) are respectively called the path source and the path target and the word l G,E (e 1 )...l G,E (e k ) is called the path label. Moreover, if s G (e 1 ) = t G (e k ), the path is called a cycle. Moving forward, we will amalgamate nodes and arcs in statements that hold for both sets by omitting the indices E and V for labeling functions l G,V and l G,E . In the sequel, partially labeled graphs will be simply called graphs.

A graph morphism g : G → H between two graphs G and H consists of g V : V G → V H and g E : E G → E H , two functions that preserve sources, targets and labels, i.e., s

H • g E = g V • s G , t H • g E = g V • t G , and l H (g(x)) = l G (x) for all x in Dom(l G ). A morphism g is injective if g V
and g E are injective and g is an inclusion if g(x) = x for all x in G. In the latter case, the notation g : G → H is preferred to g : G → H. Finally, morphism composition is defined componentwise as function compositions.

A diagram of graph morphisms, as Figure 4

(a), is a pushout if (i) K → R → H = K → D → H and (ii) for every pair of graph morphisms (R → H ′ , D → H ′ ) with K → R → H ′ = K → D → H ′ , there is a unique morphism H → H ′ such that R → H ′ = R → H → H ′ and D → H ′ = D → H → H ′ . The same diagram is a pullback if property (i) holds and (iii) if for every pair of graph morphisms (K ′ → R, K ′ → D) with K ′ → R → H = K ′ → D → H, there is a unique morphism K ′ → K such that K ′ → R = K ′ → K → R and K ′ → D = K ′ → K → D. A pushout is natural if it is also a pullback. Definition 1 (Rule). A rule r : L ← K → R consists of two inclusions K → L and K → R such that: (1) for all x ∈ L, l L (x) = ⊥ implies x ∈ K and l R (x) = ⊥, (2) for all x ∈ R, l R (x) = ⊥ implies x ∈ K and l L (x) = ⊥.
Conditions (1) and (2) prevent invalid modifications of labels when the rule is matched to build a direct derivation.

Definition 2 (Direct derivation). A direct derivation from a graph G to a graph H via a rule r : L ← K → R consists of two natural pushouts as Figure 4(b), where m : L → G, called the match morphism, is injective. We write G ⇒ r,m H if there exists such a direct derivation.

/ / R D / / H 0 (a) L o o ? _ m (1) K / / (2) R G o o ? _ D / / H 0 (b)
Figure 4: A diagram and a direct derivation.

In [START_REF] Habel | Relabelling in Graph Transformation[END_REF], the authors studied the category of partially labeled graphs as a way to express relabeling in totally labeled graphs. In particular, given a rule r : L ← K → R and a match morphism m : L → G, they showed that (a) there exists a direct derivation G ⇒ r,m H as in Figure 4(b) if and only if m satisfies the following dangling condition: no node in m(L)\m(K) is incident to an arc in G\m(L), (b) D and H are unique up to isomorphism, and (c) H is totally labeled if and only if G is totally labeled.

We consider rules with two inclusions for both sides (instead of only one for the left-hand side) as it yields a more conservative framework for us to express property preservation over direct derivations. Indeed, enforcing the morphism K → R to be an inclusion forbids that two nodes (resp. arcs) of L are transformed into a single node (resp. arc) in R.

We will use the following simplifications throughout the present article. First, spans of injective morphisms are considered spans of inclusions. Therefore, in a rule r : L ← K → R, if x is an element of K, we also write x ∈ L and x ∈ R. This simplification is extended through the diagram of a direct derivation. In other words, for a element x of D (in the diagram of Figure 4(b)), we also write x ∈ G and x ∈ H. Second, we do not extensively write morphisms but express them throughout node naming. For instance, a and b are node names in Figure 3. The morphism K → L maps the nodes a and b in the graph K to the nodes a and b in the graph L. Unless explicitly given, the depicted morphisms always map nodes with the same name. The arc part of the graph morphism is obtained by considering that the morphism is the maximal inclusion that respects node naming. When applying graph transformations on generalized maps, the adjacent arcs condition will ensure the uniqueness of arcs adjacent to node per dimension, unambiguously defining the arc part of the morphisms.

Graph transformations with variables

A framework for graph transformations with variables has been introduced in [START_REF] Hoffmann | Graph Transformation with Variables[END_REF] revolving around three guidelines: the rule scheme syntax, the instantiation of variables, and the rule application process. Rule scheme. The sets C V and C E of node and arc labels are extended by a set X of variable names. Graphs built over 4 X are called graph schemes. Then, a rule scheme is a rule r : L ← K → R where L, K, and R are graph schemes. The kernel G of G is the graph obtained by removing all labels that contain a variable occurrence. Instantiation. A substitution function σ specifies how variable names occurring in a rule scheme are substituted. From the instantiation of variables in the graphs L, K, and R, yielding respectively the graphs L σ , K σ , and R σ , the instantiation of a rule scheme r : L ← K → R according to σ defines a particular rule instance r σ :

L σ ← K σ → R σ .
Note that r σ is a rule without variables as defined in Definition 1. Rule application. Let G be a graph, and r : L ← K → R be a rule scheme.

(1) Identify a kernel match m : L → G of the kernel L of L in G (if it exists);

(2) If possible, find a substitution σ such that there exists a morphism m : L σ → G extending m;

(3) Construct the instance r σ : L σ ← K σ → R σ and apply the instance r σ to get the direct derivation G ⇒ rσ,m H.

The substitution and the instantiation may differ depending on the variable type, but the generic framework remains valid. In [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF][START_REF] Bellet | Designing a topological modeler kernel: a rule-based approach[END_REF], we introduced variables that allow generic transformations of topological structures using this framework. However, neither of the previously defined variables exactly fits our usage: we need to access the node labels through the node names to allow topological structure traversals (e.g., to access the adjacent face color in the case of the colored triangulation given in the introduction). In the sequel, we will introduce new dedicated variables alongside a specific instantiation mechanism and ad hoc primitives for topological structure traversals.

Data types

In our setting, objects will be modeled by graphs labeled on nodes with geometric or dedicated data that we will generically call embedding. For the theoretical part of this paper, two examples of embeddings are considered, namely face colors and 2D positions of points, but Section 9 will present additional embeddings. These data are typed and provided with functions to perform computations on them.

As the same embedding value can appear multiple times in an object (e.g., in the transformed object of Figure 1, two faces have the same color), we need to identify these multiple occurrences when collecting object embedding values. We therefore consider for each data type τ , the type τ • , which corresponds to the multiset of elements of type τ . A multiset may be viewed as a function that associates its multiplicity (a natural number) to each element. We use the following notation:

for the empty multiset (of any type τ • ), a 1 , . . . , a p for a multiset with p occurrences of elements of type τ . For example, the multiset that contains the element A with the multiplicity 1, the element B with the multiplicity 2, and where all other elements are of multiplicity 0, is A, B, B . Similarly, the multiset of face colors of the transformed object of Figure 1 is , , , where each colored tablet directly encodes a particular color.

We then present the main elements of term construction and evaluation.

Signature. A data type signature Ω = (S, F ) consists of a set S of type names and a family of function names provided with a profile on S with S defined as the set S ∪ {s • | s ∈ S}. A function name f provided with a profile s 1 . . . s m+1 with s i ∈ S for i ∈ 1..m + 1 is denoted by f :

s 1 × . . . × s m → s m+1 .
Terms. For X = s∈S X s an S-indexed family of sets of variables, the set T Ω (X) = s∈S T Ω (X) s of terms over Ω is the least set satisfying:

• for all variables x in X s , x ∈ T Ω (X) s ;

• for all function names f :

s 1 × . . . × s m → s m+1 in F , for all terms t 1 ∈ T Ω (X) s 1 , . . . , t m ∈ T Ω (X) sm , then f (t 1 , . . . , t m ) ∈ T Ω (X) s m+1 .
We note t : s a term t in T Ω (X) s .

Algebra. An Ω-algebra A consists of

• an S-indexed family of nonempty sets s∈S A s , canonically extended with the family of sets s∈S A s • such that

A s • = { a 1 , . . . , a p | 0 ≤ p, ∀k ∈ 0..p, a k ∈ A s }.
• and an F -indexed family of functions f ∈F f A such that for each function f :

s 1 × . . .×s m → s m+1 in F , the function f A has the profile f A : A s 1 ×. . .×A sm → A s m+1 .
Evaluation. For σ = s∈S σ s an S-indexed family of assignments σ s : X s → A s , the evaluation σ : T Ω (X) s → A s of a term t : s is defined as:

• for all variables x in X s , σ(x) = σ s (x);

• for all function names f : s 1 × . . . × s m → s m+1 in F and all terms t 1 : s 1 , . . . , t m : s m , σ(f (t 1 , . . . , t m )) = f A (σ(t 1 ), . . . , σ(t m )).

In order to design a modeler, the user is expected to provide both a data type signature Ω = (S, F ) and an Ω-algebra A, with all the data types and functions required by its application domain to define its modeling operations. In the sequel, the considered user types are point_2D, vector_2D and color, that respectively model 2D positions, 2D vectors and colors. They are provided with all classical functions such as • + : point_2D × vector_2D → point_2D that represents the translation of a point by a vector,

• midpoint : point_2D × point_2D → point_2D that computes middle point of a line segment defined by its two endpoints,

• center : point_2D • → point_2D that computes the barycenter of a multiset of points,

• or mix : color × color → color that defines the average color of two given colors.

From now on, the algebra A will be left implicit. When needed, the carrier set A τ of a data type τ will be simply written ⌊τ ⌋.

By offering a concise and straightforward notation for multisets, our presentation of data types minimally meets our needs. Multiset properties such as commutativity of the element insertion or specification of the element multiplicity are semantically imposed. Note that multisets could also have been introduced by considering a higherorder approach as a starting point. We could have defined type constructions such as lists, sets, or tuples of elements of the same type. However, the resulting data types would have been more expressive than necessary, creating types such as sets of sets when we only need a generic construction for denoting multisets of basic type elements.

In the rest of the article, signatures introduced by the user will be called user signatures. As stated above, for the particular case of the example running throughout the paper, the user signature will contain the user types point_2D, vector_2D, and color.

Topological Generalized Maps as Partially Labeled Graphs

In topology-based modeling, objects are defined according to:

• their topological structure -i.e., their cell subdivision (vertices, edges, faces, volumes) and the adjacency relations between these cells; for example, the three objects of Figure 5 have the same topological structure: a closed face F that has four edges and four vertices;

• their embedding, which includes all other types of information attached to their topological cells, including the geometric information required to capture their shape; for the objects of Figure 5, geometric points are attached to topological vertices, and colors are attached to faces. Many topological structures allow one to represent different classes of objects: tetrahedral [START_REF] Lang | Simplicial sets and triangular patches[END_REF] or polyhedral [START_REF] Mäntylä | Introduction to Solid Modeling[END_REF][START_REF] Weiler | The radial-edge structure: A topological representation for non-manifold geometric boundary representations[END_REF][START_REF] Damiand | Combinatorial Maps: Efficient Data Structures for Computer Graphics and Image Processing[END_REF], fixed dimension (2D [START_REF] Mäntylä | Introduction to Solid Modeling[END_REF] or 3D [START_REF] Weiler | The radial-edge structure: A topological representation for non-manifold geometric boundary representations[END_REF]) or dimensionindependent [START_REF] Lang | Simplicial sets and triangular patches[END_REF][START_REF] Damiand | Combinatorial Maps: Efficient Data Structures for Computer Graphics and Image Processing[END_REF], and most of them can be seen as a particular class of graphs. Among those, we choose the topological model of generalized maps (or G-maps) [START_REF] Lienhardt | N-dimensional generalized combinatorial maps and cellular quasimanifolds[END_REF][START_REF] Damiand | Combinatorial Maps: Efficient Data Structures for Computer Graphics and Image Processing[END_REF] because its mathematical definition can be rather easily encoded within a formal framework. In G-maps, the topological structure is handled by both the graph structure and the arc labels, while the node labels define the embedding. More precisely, the class of G-maps that represents valid objects is defined by labeling constraints. Hence, to define modeling operations with graph transformations, we investigate under which conditions G-map constraints and object consistency are preserved by transformations. Examples of inconsistencies are given in Figure 6. For instance, an edge with a single extremity instead of two or two faces glued along a vertex instead of an edge are topological inconsistencies (See Figure 6(a)). However, faces embedded with two colors instead of one or without any defined color are embedding inconsistencies (See Figure 6(b)). The representation of an object as a G-map intuitively comes from its decomposition into topological cells. For example, the 2D topological object of Figure 7(a) can be decomposed into a 2-dimensional G-map. First, the object is split into faces in Figure 7(b). These faces are linked along their common edge with a 2-relation: the index 2 means that faces (cells of dimension 2) share a common edge. Similarly, faces are separated into edges connected with the 1-relation in Figure 7(c). Finally, edges are divided into vertices by the 0-relation yielding the 2-G-map of Figure 7(d). Nodes obtained at the end of the process are the G-map ones, and the different i-relations become labeled arcs: for a 2-dimensional G-map, labels i belong to {0, 1, 2}. Let G topo be the 2-G-maps obtained from the decomposed of the topological object of Figure 7(a) and depicted in Figure 7(e).

u w v x A B C D A D C B v w x u A D C B v w x u F F F

Generalized maps

A B C D E F G u v w x y z (a) 2 2 2 2 2 2 (b) 1 1 1 1 1 1 1 (c)
Therefore, G-maps are graphs labeled on the arcs by integers. More precisely, for a given dimension n, n-G-maps are graph with arcs totally labeled in C E = 0..n, where 0..n is the interval of integers between 0 and n. Moreover, G-maps are symmetric graph: for each i-arc of source v and target v ′ , there is also a corresponding reversed i-arc of source v ′ and target v. Graphically, double reversed arcs are represented with lines (see Figure 7(e)). Besides, instead of writing arc labels on the figures, we use the graphical codes introduced in Figure 7: black line for 0-arcs, red dashed line for 1-arcs, and blue double line for 2-arcs. Topological cells are implicitly defined as subgraphs in G-maps. They are computed as all elements reachable from a source node using a given set of arc labels. For example, in Figure 8(a), the 0-cell (vertex) adjacent to e is the subgraph which contains e, the nodes that can be reached from node e using 1-arcs or 2-arcs, and the arcs themselves. Note that the grey parts of the graphs in Figure 8 (later on in Figures 9 and21) do not belong to the orbits and are only drawn to help with the visualization. In Figure 8(b), the 1-cell adjacent to e (edge w in Figure 7(a)) is the subgraph that contains the node e and nodes reachable through 0-arcs and 2-arcs (nodes e, f , g, and h), and the corresponding arcs. Finally, in Figure 8(c), the 2-cell adjacent to e (face F in Figure 7(a)) is the subgraph built from node e with 1-arcs and 2-arcs. The set of arc labels used to build the topological cell as subgraphs is called an orbit type.

Definition 3 (Orbit type).

Let n ∈ N be a dimension.

An orbit type of dimension n is a subset of 0..n, noted as a word o and placed in square brackets ⟨o⟩. An element i of 0..n belongs to ⟨o⟩ if i occurs in o.

For instance, the orbit type {1, 2} can be noted indifferently ⟨1 2⟩ or ⟨2 1⟩. In the sequel, the dimension of an orbit type is often left implicit.

Subgraphs built using graph traversals on an orbit type are called orbits. Formally, an orbit is an equivalence class for the equivalence relation defined by the corresponding orbit type. Based on this equivalence relation, we consider the notion of completion, which can be seen as the union of equivalence classes generated by a subgraph. The following definition formally introduces these notions together with topological graphs that include G-maps and their transformation patterns. Note that the arc labeling function of topological graphs is denoted by α according to the notation commonly used in geometric modeling.

Definition 4 (n-topological graph and orbit). Let n ∈ N be a dimension.

A partially labeled graph G = (V, E, s, t, l V , α) is an n-dimensional topological graph if the arc labeling function α is a total function with codomain C E = 0..n.

For an orbit type ⟨o⟩ of dimension n, let ≡ G⟨o⟩ be the equivalence orbit relation defined on V × V as the reflexive, symmetric and transitive closure built from arcs with labels in o, i.e., ensuring that for each arc e of G labeled by a letter in o, we have s(e) ≡ G⟨o⟩ t(e).

For any node v of G = (V, E, s, t, l V , α), the ⟨o⟩-orbit of G adjacent to v, denoted by G⟨o⟩(v), is defined as the smallest subgraph

(V ′ , E ′ , s ′ , t ′ , l ′ V , α ′ ) of G such that (1) the set V ′ of nodes includes {v} ∪ {v ′ | v ′ ∈ E, ∃w ∈ V ′ , v ′ ≡ G⟨o⟩ w}, (2) the set E ′ of arcs includes {e | s(e) ∈ V ′ , t(e) ∈ V ′ , α(e) ∈ o}, (3) and s
′ , t ′ , l ′ V and α ′ are restrictions of corresponding functions in G to the sets V ′ or E ′ . If the context is clear, G⟨o⟩(v) is simply denoted ⟨o⟩(v).
More generally, for any subgraph

G ′ → G, the ⟨o⟩-completion of G ′ in G, denoted by G⟨o⟩(G ′ ), is defined as the smallest subgraph (V ′′ , E ′′ , s ′′ , t ′′ , l ′′ V , α ′′ ) of G such that (1) the set V ′′ of nodes includes V G ′ ∪ {v ′′ | v ′′ ∈ E, ∃w ∈ V ′′ , v ′′ ≡ G⟨o⟩ w}, (2) the set E ′′ of arcs includes {e | s(e) ∈ V ′′ , t(e) ∈ V ′′ , α(e) ∈ o}, (3)
and s ′′ , t ′′ , l ′′ V and α ′′ are restrictions of corresponding functions in G to the sets

V ′′ or E ′′ .
The topological cells are particular instances of orbits. For instance, an orbit of type ⟨0 1⟩ is a face, an orbit of type ⟨0 2⟩ is an edge, and an orbit of type ⟨1 2⟩ is a vertex. Some other standard topological objects can be expressed as orbits. For example, the orbit ⟨0⟩(e) in Figure 8(d Formally, a G-map is a topological graph satisfying some constraints that transcribe the object consistency. The constraints are the following.

Definition 5 (Generalized map). An n-dimensional generalized map, or n-G-map, is a totally labeled n-topological graph G = (V, E, s, t, l V , α) that satisfies the following topological consistency constraints:

• Symmetry constraint: G is symmetric,

• Adjacent arc constraint: each node is the source node of exactly n+1 arcs respectively labeled from 0 to n,

• Cycle constraint: for every i and j in 0..n such that i + 2 ≤ j, there exists a cycle labeled by ijij starting from each node.

These constraints ensure that objects represented by embedded G-maps are consistent manifolds [START_REF] Lienhardt | N-dimensional generalized combinatorial maps and cellular quasimanifolds[END_REF]. In particular, the cycle constraint ensures that in G-maps, two i-cells can only be adjacent along (i -1)-cells. For instance, in the 2-G-map of Figure 7(e), the 0202-cycle constraint implies that faces are glued along topological edges. Let us notice that thanks to loops (see the 2-loops in Figure 7(d)), these three constraints also hold at the border of objects.

Basic topological transformations

Within a geometric modeler, operations defined on objects are called topological (resp. geometric) if their primary purpose is to change the topological structure (resp. the embedding). Operations may fall under both aspects, such as the rounding operation consisting of replacing a vertex or a sharp edge with a curved surface [START_REF] Ledoux | Geometric Modelling with CASL[END_REF].

Intuitively, topological operations are applications that allow building new generalized maps from generalized maps. The definition of topological operations by graph transformation rules advantageously facilitates the study of stating whether or not the resulting graphs are also generalized maps. To achieve this, rules on generalized maps need to preserve the topological constraints of Definition 5 by construction.

In previous work [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF], we elaborated the following syntactic conditions that precisely ensure the preservation of topological consistency:

Theorem 1 (Topological consistency preservation). Let r : L ← K → R a graph transformation rule, G an n-G-map and m : L → G a match morphism.
The result H of the direct transformation G ⇒ r,m H is an n-G-map H if the following conditions of topological consistency preservation are satisfied:

• Symmetry condition: the three graphs L, K, and R are symmetric n-topological graphs.

• Adjacent arcs condition:

preserved nodes of K are sources of arcs having the same labels in both the left-hand side L and the right-hand side R;

removed nodes of L\K and added nodes of R\K must be source of exactly n + 1 arcs respectively labeled from 0 to n.

• Cycle condition: for every i and j in 0..n such that i + 2 ≤ j,

any added node of R\K is the source of an ijij-cycle;

any preserved node of K which is the source of an ijij-cycle in L, is also the source of an ijij-cycle in R;

any preserved node of K which is not the source of an ijij-cycle in L is source of the same i-arcs and j-arcs in L and R.

The interested reader can find some discussion on the conditions presented in this theorem in [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF], with its proof. In particular, we demonstrated that the dangling condition (see Subsection 3.2) is always ensured when a rule that satisfies those conditions is applied to a G-map. Topological variables introduced in [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF][START_REF] Bellet | Designing a topological modeler kernel: a rule-based approach[END_REF] and the corresponding rule schemes allow the abstraction of all orbits of a given type. Some syntactic conditions on the rule schemes were also given to ensure that instantiated rules satisfy the conditions of Theorem 1. These variables have been revisited with a functorial approach exploiting a product-based construction in [START_REF] Pascual | Topological consistency preservation with graph transformation schemes[END_REF]. Here we aim to discuss geometric operations, meaning that the embedding consistency is the issue tackled. Thus the topological consistency will not be discussed more thoroughly, and we will use the more specific presentation of [START_REF] Poudret | Graph Transformation for Topology Modelling[END_REF]. Nonetheless, a watchful reader can notice that all the rules in this paper verify the constraints of Theorem 1, which guarantees that generalized maps remain generalized maps after transformations.

Embedded Generalized Maps and their Basic Transformations

Our approach is generic in the dimension of the objects and nature of the considered embedding. In the sequel, n-G-maps will be called G-maps, and orbit type will implicitly be of dimension n. Moreover, all illustrative examples will present 2D objects with one of the two embedding data types of Figure 5: either 2D positions on vertices (i.e., ⟨1 2⟩-orbits) or colors on faces (i.e., ⟨0 1⟩-orbits).

Embedding representation

The topological structure of G-maps has been defined as graphs with arc labels. We complete this definition here with node labels to represent the embedding. In Section 3.4, we already sketched that every dedicated embedding has a data type and is defined on a particular kind of topological cell. A node labeling function defining an embedding will be typed both by an orbit type and a data type. We characterize such a node labeling function as an embedding operation π : ⟨o⟩ → τ where π is the operation name, τ is a data type, and ⟨o⟩ is an orbit type. Thus, for a G-map embedded on π : ⟨o⟩ → τ , the node label set C V is the set of values ⌊τ ⌋ of type τ . When the profile of π is obvious, the node labeling function is noted π. Therefore, an embedded5 G-map is a particular case of partially labeled graphs, generically denoted as a tuple (V, E, s, t, π, α).

In this article, we consider the following embedding operations defined on the user signature introduced in Section 3.4 (i.e., including types point_2D and color):

• pos : ⟨1 2⟩ → point_2D is the embedding that associates a 2D position to each vertex. Figure 10(a) shows the embedded G-map G pos = (V, E, s, t, pos, α) built on G topo (see Figure 7(d)). The embedding operation pos maps the 2D positions A, B, C, D, and E to the nodes of V ;

• col : ⟨0 1⟩ → color is the embedding that associates a color (values of type color) to each face (⟨0 1⟩-orbits) of a 2-G-map. As mentioned in Section 3.4, data types used to specify embedding come with operations to perform computations on the data. In the following, when referring to the user signature attached to a given embedding π : ⟨o⟩ → τ , we will generically note it as Ω π = (S π , F π ). In particular, S π contains the type τ and F π contains functions defined on

S π = S π ∪ {s • π | s π ∈ S π }.
Moreover, as an embedding operation π : ⟨o⟩ → τ is characterized by its domain orbit, all nodes of a common ⟨o⟩-orbit share the same label by π, also called π-label. For G pos of Figure 10(a), as pos is defined on orbit type ⟨1 2⟩ characterizing vertices, all nodes of a same ⟨1 2⟩-orbit have the same value by pos. Thus, nodes c, e, g, and i that belong to the same vertex orbit ⟨1 2⟩ are labeled by the same value B. Similarly, in Figure 10(b),nodes a,b,c,d,e, and f that belong to the same face are labeled with the same yellow color. This property is captured by an embedding constraint [START_REF] Bellet | Rule-based transformations for geometric modeling[END_REF]: Definition 6 (Embedded graph and embedded generalized map). Let π : ⟨o⟩ → τ be an embedding operation with ⟨o⟩ an orbit type and τ a data type.

• Embedded graph: A graph embedded on π, or π-embedded graph, is an ntopological graph G = (V, E, s, t, π, α) where π labels nodes on C V = ⌊τ ⌋.

• Embedding consistency constraint: A π-embedded graph satisfies the embedding consistency constraint if for all nodes v and w such that v ≡ ⟨o⟩ w, π(v) ̸ = ⊥ and π(w) ̸ = ⊥, then π(v) = π(w).

• Embedded G-map: A π-embedded G-map is an n-G-map embedded on π satisfying the embedding consistency constraint and such that π is a total function (i.e., Dom(π) = V ).

Note that the embedding consistency constraint allows an ⟨o⟩-orbit to be partially π-labeled as long as the defined π-labels are equal. Because embedded G-maps are totally labeled, the constraint entails that all nodes of a ⟨o⟩-orbit share the same embedding value, i.e., for all nodes v and w such that v ≡ ⟨o⟩ w, π(v) = π(w) with π(v) ̸ = ⊥. Similar to the construction of the DPO approach to graph transformation in [START_REF] Habel | Relabelling in Graph Transformation[END_REF], we consider partially labeled objects in rules to ease the modification of totally labeled objects.

As we have already noticed with the embedded G-maps G pos and G col , the topological structure of a π-embedded graph G can then be found by forgetting its node labels. For G = (V, E, s, t, π, α), G α = (V, E, s, t, ⊥, α) denotes the underlying topological structure where the everywhere undefined function ⊥ replaces the node labeling function π.

Given an equivalence relation ≡ on a set X, [x] is the equivalence class of an element x of X, i.e., {y ∈ X | y ≡ x}, whereas X /≡ is the quotient set {[x] | x ∈ X}. In a π-embedded graph G, the relation ≡ ⟨o⟩ defines a partition of the nodes if it satisfies the embedding consistency constraint. Consequently, the quotient of G by ≡ ⟨o⟩ is well-defined and yields its ⟨o⟩-orbits. In a G, all nodes of a ⟨o⟩-orbit are unlabeled or share the same π-label. Therefore, if this π-label exists, it is directly inherited by the resulting quotient node. For the quotient set of arcs, we consider the set of arcs inherited from G, redefining the source and target nodes with their corresponding quotient nodes and preserving their labels.

For example, the quotient along ⟨1 2⟩-orbits of the embedded G-map G pos of Figure 10(a) is the graph of Figure 11(a). As nodes c, g, e, and i belong to the same vertex orbit, they share the same embedding B and give rise to the B-labeled quotient node v in Figure 11(a). The quotient graph contains 5 nodes, one per ⟨1 2⟩-orbit, with a well-defined π-label. Let us note that arcs in a ⟨1 2⟩-orbit become loops. For instance, all 1-arcs and 2-arcs adjacent to c, e, g, or i are transformed into loops on node v in the quotient graph.

Similarly, Figure 11 Definition 7 (Embedding quotient). Let π : ⟨o⟩ → τ be an embedding operation and let G = (V, E, s, t, π, α) be a graph embedded on π that satisfies the embedding consistency constraint.

The π-quotient graph of G is the graph

G /π = (V /π , E /π , s /π , t /π , π /π , α /π )
defined by:

• V /π = V /≡ ⟨o⟩ ;
• E /π = E such that for all e ∈ E /π , α /π (e) = α(e), s /π (e) = [s(e)] and t /π (e) = [t(e)];

• for [v] in V /≡ ⟨o⟩ , π /π ([v]) = π(w) if there exists w in G⟨o⟩(v) such that π(w) ̸ = ⊥, otherwise π /π ([v]) = ⊥.
The π-quotient morphism q : G → G /π is defined by: for all v in V , q V (v) = [v] and q E = id.

Note that as embedded G-maps satisfy the embedding consistency constraint and are totally labeled, their quotient graphs are also totally labeled.

Basic embedding transformations

The operations defined in this section introduce the notion of embedding transformation. They are not the rules used in practice, as it would be too cumbersome to define all rules for all possible cases. However, these transformations have the advantage of defining the format in which our rules will be instantiated. We now investigate how modeling operations on embedded G-maps that modify their geometry can be defined using graph transformation rules according to Definition 1. As an example, we consider the two operations given in Figure 12 that apply to objects with the position embedding pos. The vertex translation of Figure 12(a) is a purely geometric operation as it does not affect the topological structure. Position B is translated to F . Conversely, the vertex insertion of Figure 12(b) affects both the topological structure and the embedding. An edge of the square face is split into two edges by introducing a new vertex embedded by the point_2D value G.

The critical point in defining basic geometric modeling operations is to ensure that the consistency constraints of embedded G-maps are preserved by rules applications, provided that rules satisfy some syntactic conditions.

In the same way that we gave syntactic conditions for the preservation of topological consistency constraints in Theorem 1, we here investigate syntactic conditions to ensure that embedded G-maps are transformed into embedded G-maps. Let us take the example of the vertex translation of Figure 12(a). Intuitively, we could consider the rule of Figure 13(a). Unfortunately, such a rule is not appropriate for our needs. Indeed, by matching node e of the rule of Figure 13(a) with node e of the G-map of Figure 10(a), its application results in the graph given in Figure 13(b). This graph does not satisfy the embedding consistency constraint as node e does not have the same label as the other nodes of its vertex orbit (c, g, and i). All node labels of an embedding orbit should be modified simultaneously and in the same manner. For example, the rule of Figure 14(a) matches (respectively rewrites) a full vertex orbit in L (respectively in R): indeed, all nodes are connected with both 1-arcs and 2-arcs. In fact, both L and R are full ⟨1 2⟩-orbits. Thus, the application of this rule to the pos-embedded 2-G-map of Figure 10(a) along the identity match morphism gives the pos-embedded 2-G-map of Figure 14(b).

The following theorem introduces syntactic conditions on rules that ensure embedding consistency preservation.

Theorem 2 (Preservation of the embedding consistency). Let π : ⟨o⟩ → τ be an embedding operation on an orbit type ⟨o⟩, let r : L ← K → R be a π-embedded graph transformation rule that satisfies the conditions of topological consistency preservation (Theorem 1), let G be a π-embedded G-map and let m : L → G be a match morphism.

The result H of the direct transformation G ⇒ r,m H is a π-embedded G-map if the following conditions of embedding consistency preservation are satisfied: (B) Full match of transformed embeddings:

g h q r (R) g h (K) g h (L)
if v is a node of K such that π L (v) ̸ = π R (v),
then every node of R⟨o⟩(v) is labeled and is the source of exactly one i-arc for each i of ⟨o⟩.

(C) Labeling of extended embedding orbits: if v is a node of K and there exists a node w in R⟨o⟩(v) such that w is not in L⟨o⟩(v), then there exists

v ′ in K with v ′ ≡ L⟨o⟩ v and v ′ ≡ R⟨o⟩ v such that π L (v ′ ) ̸ = ⊥.
Before giving the proof, let us now comment on the constraints given in Theorem 2. The first of these conditions is straightforward: it requires that all parts of the rule satisfy the embedding consistency constraint. For example, the rule of Figure 15(a) breaks this condition as it adds a new vertex (nodes o, p, q and r) embedded with two different positions F and G.

The second condition forbids the partial redefinition of the embedding shared by an ⟨o⟩-orbit as it would break the embedding consistency. If a preserved node has a transformed embedding, then its ⟨o⟩-orbit in R is a totally labeled full orbit. The rule of Figure 13(a) falls in this case as node e has its label changed from B to F without fully matching the topological vertex (1-arc and 2-arc are missing). Hence, an embedding value can only be modified if it is modified for the whole support orbit.

The last condition forbids the extension of an ⟨o⟩-orbit (by adding new nodes or merging with another ⟨o⟩-orbit) without matching the existing embedding value of the orbit. For example, the rule of Figure 15(b) breaks this condition as a half-edge whose embedding is unmatched is added to another half-edge whose vertices are embedded by the two positions F and G. Therefore, applying this rule to the object of Figure 10(a) along the identity morphism would break the embedding consistency. Indeed, node b would be labeled A while its added 2-neighbor u would be labeled F . The third condition entails that nodes b and d are labeled in L (and thus in R), meaning the rule labeling should be completed. In R, nodes b and d should be labeled by F and G, respectively, due to the embedding consistency condition. In L, these nodes should also be labeled by F and G. Indeed, the condition of full match of transformed embeddings prevents changing their labels while the two vertex orbits are not fully matched by the rule (1-neighbors of b and d are not matched).

Let us now prove Theorem 2.

Proof. Consider π : ⟨o⟩ → τ an embedding operation on an orbit type ⟨o⟩, r : L ← K → R a π-embedded graph transformation rule that satisfies the conditions of topological consistency preservation and the conditions of embedding consistency preservation, G a π-embedded G-map and m : L → G a match morphism. Let H be the result of the direct transformation G ⇒ r,m H according to the following diagram:

L o o ? _ m (1)
K / / (2) R m ′ G o o ? _ D / / H
Note that m ′ is the morphism from R to H. Because the rule r satisfies the conditions of topological consistency preservation, the direct transformation G ⇒ r,m H is well-defined and H is a totally labeled [START_REF] Habel | Relabelling in Graph Transformation[END_REF]. In particular, π is defined on every node of H.

It remains to prove that H is a π-embedded G-map. Since H is totally labeled, the embedding constraint states that for every v, w in V H , v ≡ H⟨o⟩ w implies π H (v) = π H (w). Note that ≡ H⟨o⟩ is an equivalence relation; thus, it suffices to show that for any i-arc e in

H with i ∈ ⟨o⟩, π H (s H (e)) = π H (t H (e)).
Consider an i-arc e in H with i in ⟨o⟩, and let v be the source of e and w be the target of e. In the following proof, when e, v, or w has an antecedent by m ′ it will respectively be denoted by e ′ , v ′ , and w ′ .

(1) If v and w are in G.

• Assume the π-labels of v and w are not changed by the rule. Since G satisfies the embedding consistency constraint, π

H (v) = π G (v) = π G (w) = π H (w).
• Otherwise, assume the π-labels of v or w is changed by the rule. Without loss of generality, we can suppose that π

G (v) ̸ = π H (v). This means v ′ is in K and π L (v ′ ) ̸ = π R (v ′ ).
The subcondition (B) ensures v ′ is the source of an i-arc in R. The adjacent arcs condition from Theorem 1 guarantees that this arc is the antecedent of e in m ′ (R), that π R (v ′ ) ̸ = ⊥, and that π R (w ′ ) ̸ = ⊥.

Since R satisfies the embedding consistency constraint (subcondition

(A)), π H (v) = π R (v ′ ) = π R (w ′ ) = π H (w).
(2) If one of v and w is in G and the other is not. Without loss of generality, assume that v is in G and

w ′ in R \ K. Because w ′ is in R \ K, e ′ is in R \ K and v ′ is in K, and π R (w ′ ) ̸ = ⊥ (otherwise π H (w) = ⊥). • Assume π R (v ′ ) ̸ = ⊥. Since R satisfies the embedding consistency constraint (subcondition (A)), π H (v) = π R (v ′ ) = π R (w ′ ) = π H (w). • Otherwise, we have π R (v ′ ) = ⊥ and π H (v) = π G (v). Because w ′ is not in K, w ′ is not in L. Therefore, subcondition (C) ensures the existence of a node x in K such that x ≡ L⟨o⟩ v ′ , x ≡ R⟨o⟩ v ′ , and π L (x) ̸ = ⊥. Since x ≡ L⟨o⟩ v ′ , we can deduce that m(x) ≡ G⟨o⟩ v and π G (v) = π G (m(x)) = π L (x). Moreover, π R (v ′ ) = ⊥ and one node of R⟨o⟩(x) is unlabeled. The contraposition of subcondition (B) ensures that π L (x) = π R (x). Similarly to the other cases, subcondition (A) grants π H (v) = π R (x) = π R (w ′ ) = π H (w).
(3) If none of v and w is in G then e, v, w are in m ′ (R\K) and the embedding consistency constraint satisfied by R ensures that:

π H (v) = π R (v ′ ) = π R (w ′ ) = π H (w).
Thereafter H is a π-embedded G-map.

Let us illustrate some of the proof of Theorem 2. For example, Figure 16 details the application of the vertex insertion operation presented in Figure 12(b) on the embedded G-map of Figure 10(a). The 1-arc that links nodes a and b in H falls into the trivial case. The arc and the two nodes belong to the graph G and are not matched by the rule. As G satisfies the embedding consistency constraint of embedded G-maps, nodes a and b have the same pos-label in G and, therefore, in H. In the case of the 1-arc between nodes i and g in H, the rule does not match the arc and node g but matches node i. As the vertex orbit containing both nodes i and g in G is not fully matched, the condition of the full match of transformed embeddings prevents the rule from modifying the pos-labels of node i. Thus, nodes i and g have the same pos-label in H as they have the same pos-label in G. Finally, the 1-arc that links nodes u and v with defined labels in R is an added arc between added nodes. Thus, the embedding consistency condition ensures that their π-labels are equal in R.

Rule Schemes

The transformation rules in Section 5 modify an object according to its particular embedding values. The rule schemes introduced in this section create a level of abstraction and allow us to define modeling operations independently of the object's actual embedding values.

Node variables

Computing new embedding values requires accessing the existing ones throughout the topological structure. To access and store embedding values in the node labels, we introduce new variables called node variables together with dedicated operators that allow us to reach neighboring nodes. Instead of defining a new set of user variable names, our approach uses the identifiers of the left-hand side's nodes as default variable names. Figure 12 illustrates two operations on the position embedding: the translation of a vertex and the insertion of a vertex to fold an edge. Figure 14(a) gives the transformation rule corresponding to the translation of vertex B to vertex F . To generalize this transformation, the position of vertices B and F are abstracted and the operation is described as the translation by the vector -→ v = --→ BF . This generalization yields the rule scheme of Figure 17(a). Likewise, Figure 17(b) illustrates the folding of an edge by inserting a vertex. The added vertex is the translation of the edge midpoint by -→ w . By convention, rule schemes will be identified by double dotted lines (see Figure 17). Conversely, single dotted lines are used for instantiated rules (see Figure 14 embedding values and expressing the computation of the new one. In Figure 17(a), the term e.pos refers to the 2D position of the matched vertex, while the term e.pos + -→ v defines the new position of the translated vertex. 7 At the scheme application, the node variable e of L will be substituted by the node matched by e, and the operator .pos will grant access to its pos-label in the transformed object. Similarly, in Figure 17(b), i.pos and k.pos are the positions associated to the extremities of the matched edge and midpoint(i.pos, k.pos) defines the corresponding midpoint position. More generally, an operator .π is used to retrieve the π-label of a node. As described in Section 4, n-G-maps are highly regular graphs. Every node has n + 1 neighbors respectively connected by arc labeled 0, 1, . . . , n. Therefore, for all i in 0..n, we can define a .α i operator on node variables that gives access to their unique i-neighbor.

Let us consider the face triangulation of Figure 18 in the case of the color embedding col : ⟨0 1⟩ → color. Each created triangle is colored by the mix between the triangulated face's original color and the one of its adjacent face, smoothing face colors. This operation is defined by the rule scheme of Figure 19 At application on the object of Figure 19(a) along the identity morphism, this 2neighbor is g and the face color is defined as mix(e.col, g.col) = mix( , ) = . The Let us remark that in the rule scheme of Figure 19(b), the same terms occur several times, e.g., the term u occurs 6 times in R. The term u refers to a color embedding. The embedding col : ⟨0 1⟩ → color is carried out by a face orbit ⟨0 1⟩. Recall that the embedding consistency requires that labels are equal in an embedding orbit. In this case, the condition for the embedding consistency is trivially satisfied since all the terms of the orbit are syntactically identical. The evaluation mechanism will compute the embedding value associated with the term u and assign it to all the corresponding nodes. As a result, the evaluation of this rule scheme will always result in a rule that preserves the embedding consistency. By writing identical terms from an early stage, we avoid the question of deciding on the equality of evaluated terms. In the rest of the paper, embedding labels of rule schemes will be compared via the strict syntactic equality of terms, even if dedicated embedding operators (_.π, _.α i or π ⟨o⟩ ) and user-defined operations may induce other equalities when considering evaluation.

We restrict ourselves to the syntactic equality of terms for simplicity and because we have not yet studied the rewriting of terms modulo equivalence induced by dedicated embedding operators.

Collect operators

Consider the triangulation operation in the case of the position embedding pos : ⟨1 2⟩ → point_2D (Figure 19). The pre-existing vertices of the triangulated face have the same position after the operation. This explains that nodes a, b, c, d, e, and f are unlabeled on both left-hand side and right-hand side of the rule. However, we need to give a position to the newly created vertex, i.e., to the 6 nodes created on the right-hand side. Commonly, this created vertex is located at the barycenter of the triangulated face. For instance, the triangulation of the top triangle in Figure 20(a) should add a vertex positioned at the barycenter of A, B, and C. Thus, we need to fetch the positions of A, B, and C. In other words, we need to retrieve the positions of all vertices of the face we are trying to triangulate. To do so, we introduce operators that collect all the embedding values of a given orbit.

To collect the positions carried by the adjacent face, the rule scheme of Figure 20(b) uses the operator pos ⟨0 1⟩ . At scheme application, pos ⟨0 1⟩ (a) will collect the multiset of positions in the ⟨0 1⟩-orbit adjacent to the node matched by a. For instance, in the scheme application to the object of Figure 20(a) along the identity match morphism, a from L is matched to a in G. Therefore, pos ⟨0 1⟩ (a) collects the multiset A, B, C . Similarly, in the scheme application along the match morphism that sends respectively a, b, c, d, e, and f in L to g, h, i, j, k, and l in G (i.e., the application to the bottom triangle), pos ⟨0 1⟩ (g) collects the multiset B, C, D . Intuitively, these operators are based on the quotient representation introduced in Definition 7 that associates each embedding orbit to a single node and, therefore, to a single label. Consequently, the multiplicity in the multiset does not depend on the orbit sizes but depends on the number of embedding orbits sharing the same value. In the case of the position embedding, each position value appears only in a single ⟨0 1⟩-orbit because we do not want two vertices to coincide. Thus, any collection of position values would result in a multiset having each position at most once. For instance, in Figure 20(a), A appears 4 times and B appears 6 times but the evaluation of pos ⟨0 1⟩ (a) contains A and B only once.

However, for most applicative data such as colors, quantities, or densities, it is expected that one value appears multiple times in the modeled object. Let us consider the example of the operator col ⟨0 1 2⟩ that collects the face colors of the adjacent connected component. The evaluation of col ⟨0 1 2⟩ (a) on the colored object of Figure 19(a) results in the multiset , , , . In this multiset, has two occurrences as it labels two faces. More generally, for all embeddings π : ⟨o⟩ → τ and for all orbit types ⟨o ′ ⟩, we can define an operator π ⟨o ′ ⟩ on nodes. For a node v, π ⟨o ′ ⟩ (v) collects one embedding value for each ⟨o⟩-orbit in G⟨o ′ ⟩(v) (i.e., one value per ⟨o⟩-orbit in the ⟨o ′ ⟩-orbit adjacent to v) and stores the collected values in a multiset. Until now, the family of collect operators has been introduced only from an intuitive point of view. We will formally define it in the next sections, syntactically in Section 6.3 and semantically in Section 6.4.

Terms and schemes

To sum up, node variables are available as node identifiers on the left-hand side of the rule scheme L. At the rule scheme application, these variables are substituted by particular node identifiers of the G-map under transformation. New embedding values are defined by terms over these nodes thanks to the introduced G-map operators: the embedding access operators .π, the neighbor access operators .α i , and the collect operator π ⟨o⟩ . In addition to these operators, terms may include various operators and types provided by the user. For example, the translation scheme of Figure 17(a) uses the addition between a point and a vector, and the triangulation scheme of Figure 20(b) uses the operator center that defines the barycenter of a point multiset.

We define embedding terms on a user signature by considering node variables. A dedicated type (called N ode) provided with some predefined operations is introduced to manipulate these variables. Variables of type N ode coincide with node variables. Graph nodes of rule schemes will therefore be labeled with terms of a signature (see Section 3.4) built over a user signature extended by the type N ode and the operators .π, .α i , and π ⟨o ′ ⟩ . Definition 8 (Embedding terms signature, graph schemes, and rule schemes). Let π : ⟨o⟩ → τ be an embedding operation. Let Ω π = (S π , F π ) be a user signature such that S π is a set of type names including the π-type τ . Embedding terms signature. Ω Map = (S Map , F Map ) is the embedding term signature extended on G-maps defined as S Map = S π ∪ {Node} and F Map = F π ∪ F Node with F Node the set of function names that contains8 :

• _.π : Node → τ ; • _.α i : Node → Node for all i ∈ 0..n; • π ⟨o ′ ⟩ : Node → τ • for all orbit type ⟨o ′ ⟩. Graph schemes. Let X be a set of node variables. A graph scheme G = (V, E, s, t, π, α) on (Ω π , X) is a graph embedded on π : ⟨o⟩ → T Ω Map (X) τ . Rule schemes. A rule scheme r : L ← K → R on Ω π is a rule on graph schemes on (Ω π , V L ) with V L the node set of L.
When this eases reading, we will make the set of variables explicit in the notation of graph schemes or rule schemes, using G(X) instead of G or r(V L ) instead of r.

Figures 19(b) and 20(b) provide two versions of a face triangulation rule scheme on Ω col = (S col , F col ) and Ω pos = (S pos , F pos ), respectively, with: color in S col , point_2D in S pos , mix : color × color → color in F col , and center : point_2D • → point_2D in F pos .

Evaluation of embedding terms

At the rule scheme application, embedding terms are evaluated on the embedded G-map. For instance, when the triangulation scheme of Figure 20(b) is applied to the top triangle of Figure 20(a), the term pos ⟨0 1⟩ (a) has to be evaluated by the point multiset A, B, C in order to compute the barycenter. The evaluation of terms on G-maps operators is an extension of the user algebra on the signature Ω π . More precisely, given a π-embedded G-map and a Ω π -algebra, we define the extended Ω Map -algebra on embedding terms (see Section 3.4).

Definition 9 (Algebra extension by a G-map). Let G = (V, E, s, t, π, α) be an n-G-map embedded on π : ⟨o⟩ → τ , Ω π = (S π , F π ) be a user signature, and A be a Ω π -algebra.

The extended algebra A G from A by G is the Ω Map -algebra defined as:

• (A Map ) s = A s for s ∈ S π with S π = S π ∪ {s • π | s π ∈ S π }; • (A Map ) Node = V ; • for each f of F π , f A Map = f A ;
• .π A Map is the labeling function π;

• for all i ∈ 0..n, for each node v ∈ V , there exists a unique i-arc e ∈ E such that s(e) = v and the function .α i A Map associates v to t(e);

• for all orbit types ⟨o ′ ⟩, for each node v ∈ V , the function π ⟨o ′ ⟩ A Map associates v to the multiset of labels from the quotient of the ⟨o

′ ⟩-orbit of v 9 π ′ (v ′ ) | v ′ ∈ V ′ , where G⟨o ′ ⟩(v) /π = (V ′ , E ′ , s ′ , t ′ , π ′ , α ′ ).
Note that topological constraints of G-maps ensure that a node is the source of a unique i-arc. Therefore, α A G i is a well-defined function. Consequently, the collect operators are also well-defined functions, and the algebra extension by a G-map is a valid construction.

The evaluation of the collect operators is defined with the graph quotient introduced in Definition 7. For example, to evaluate the term pos ⟨0 1⟩ (a) for the object of Figure 21(a), we construct the quotient ⟨0 1⟩(a) /pos of the orbit ⟨0 1⟩(a) of Figure 21(b). The term evaluation is then defined as the multiset of node labels of that quotient, i.e., A, B, C .

9

We write π ′ (v ′ ) | v ′ ∈ V ′ the multiset of type τ • such that for all x : τ , the multiplicity of x is equal to the number of node of V ′ labeled by x. Here again, the graph's grey parts do not belong to the orbit or the quotient but are displayed for clarity. As described in Subsection 3.3, a scheme only requires a kernel match to be evaluated. We use a match morphism from the topological structure of the left-hand side m : L α → G. Recall that for a labeled graph L, L α denotes the graph L for which all node labels are undefined, and the arc labels are those of L. In other words, L α defines the topological structure underlying L. The match morphism m : L α → G removes variable occurrences but keeps the arc labels, allowing the match of the topological structure specified in the left-hand side of the rule scheme. Practically, pointing out that the set of variables X coincides with the set of node names of the left-hand side graph L of the rule, the node matching part m V : V L → V G of this morphism will be directly used for the substitution σ : X → V G . For example, an identity match morphism between the rule scheme and the object of Figure 19 assigns the variables a, b, and e to the nodes a, b, and e of the object, resulting in the rule of Figure 22(a). Similarly, the rule of Figure 22(b) results from a match morphism assigning the variables a, b, and e to the nodes i, g, and l of the object. Definition 10 (Rule scheme evaluation). Let G be a π-embedded G-map, Ω π a user signature, and A an Ω π -algebra. Graph scheme evaluation. Let S = (V, E, s, t, π, α) be a graph scheme on (Ω π , X) and σ : X → V G an assignment of X. The evaluated graph S σ of S along σ is the π-embedded graph (V, E, s, t, π σ , α) such that π σ (v) = σ(π(v)) for each node v ∈ V . Rule scheme evaluation. Let r : L ← K → R be a rule scheme on Ω π and m : L α → G a kernel match morphism. The evaluated rule of r along m is the π-embedded rule:

r m V : L m V ← K m V → R m V
The evaluated rules in Figure 22 match a face, which is precisely the orbit corresponding to the color embedding. However, a rule scheme is likely to match any piece of the Gmap. In particular, it might not match precisely an orbit. To circumvent such cases, Section 7 introduces completion mechanisms on rule schemes to automatically recover full embedding orbits.

Rule Scheme Instantiation

In this section, we define how rule schemes are instantiated without considering the consistency preservation, which is postponed to Section 8.

Need for simplicity

So far, every considered operation has been defined based on the transformed object's specific topological structure. For instance, the rule of Figure 14 explicitly defines the translation of a vertex adjacent to three edges. Operations based on such a specific structure are very restrictive and counter-intuitive from a user-end perspective. The vertex translation has a single meaning on a semantic level, independent of the number of adjacent edges. A user-friendly rule scheme should be as simple as in Figure 23 in which a single node relabeling encodes a single embedding transformation. The rule scheme matches a node, catches the value of its pos-embedding using the node variable a and replace it with a new position, namely a.pos + -→ v . Nonetheless, the discussion of Section 5.2 holds, and, similarly to the rule of Figure 13(a), the application of an evaluated rule based on this scheme can produce an inconsistent object.

Let us take a more significant case with the edge removal of Figure 24. This operation will be this section's guiding example and involves topological and embedding modifications. On the topological aspect, the edge is removed, and the two adjacent faces are merged. On the embedding aspect, the resulting face's color is obtained by mixing the colors of the two original faces. Figure 24: Edge removal on the color embedding.

Semantically, this operation does not depend on the configurations of the two faces. It corresponds to the simple rule scheme of Figure 25(a). But similarly to the translation, the application of the evaluated rule of Figure 25(b) to the object of Figure 19(a) results in the inconsistent object of Figure 25(c). This inconsistent application yields a face where some nodes are labeled with the color yellow, some with the color blue, and others with the color green. The expected behavior is that all nodes should have green as their col-label. The embedding modifications must be propagated to all nodes of the two faces to preserve the G-map consistency.

Therefore, the instantiation process must extend the evaluated rule to propagate embedding modifications. In our example, the evaluated rule of Figure 25(b) has to be extended into the correct rule of Figure 25(d). This extension is realized in two steps: the topological extension that matches all required nodes and the embedding propagation that ensures consistent relabeling.

The complete pipeline is presented in Figure 26, introducing the notion of topological extension, denoted by ⊕m, and the embedding propagation, denoted by ⊙π.

Step 1 corresponds to the evaluation process already defined in Section 6. At the end of step 1 (in the rule r m V ), all terms with variables are evaluated using the match morphism. Thus, terms with variables in the rule scheme are replaced by values in the evaluated rule.

Since the col-embedding is defined on faces (orbit ⟨0 1⟩), it is necessary to consider nodes reachable by arcs labeled in ⟨0 1⟩. The topological extension's role is, precisely, to retrieve the missing nodes for all ⟨0 1⟩-orbits. In step 2 , the topological extension matches the nodes corresponding to the yellow and blue faces in the original object. These gathered nodes are also added to the interface and the right-hand side of the rule (denoted (r m V ) ⊕m ). Note that these nodes are matched without their embedding value because otherwise, the topological extension would produce a rule that does not satisfy the embedding consistency of Theorem 2. All nodes added by the topological extension have undefined embedding values (depicted as white nodes). The embedding propagation depicted in step 3 relabels the nodes added by the topological extension using the embedding values computed on nodes matched from the evaluated rule. Notice that as the evaluated rule r m V satisfies the conditions of Definition 1, both the topological extension ((r m V ) ⊕m at step 2 ) and the embedding propagation (((r m V ) ⊕m ) ⊙π at step 3 ) produce well-defined rules.

d c j i g h e f d c j i (K) (L) d c j i (R) t = mix (e. col, g. col) t t t t u = e. col v = g. col u u u u v v v v (a) Rule scheme d c j i g h e f d c j i (K) (L) d c j i (R) (b) Evaluated rule l j k i a b d c (c) Inconsistent application (L) l j k i g h a b d e c f l j k i a b d c l j k i a b d c (K) (R) (d) Correct rule

Topological extension

Intuitively, the topological extension (step 2 in Figure 26) uses the match morphism to complete the partial embedding orbits defined by the evaluated rule with the actual full orbits of the transformed G-map. First, the extension L ⊕m of the left-hand side is computed in Figure 27(a) by pushout between the topological structure of the ⟨o⟩-orbit adjacent to the matched pattern G α ⟨o⟩(m(L α ) α ), and the left-hand side of the evaluated rule L. The pushout relies on the inclusion L α → L to transpose the embedding values and on the morphism m : L α → G and the orbit completion to extract the missing orbit nodes. The evaluated rule is then applied to the extension L ⊕m of the left-hand side. Here we are not only interested in the result graph L ⊕m ⇒ r,m ′ R ⊕m but in the three graphs L ⊕m , R ⊕m , and K as they define a new rule called the full extended rule r ⊕m . As shown in Figure 27(b), the full extended rule L ⊕m ← K ⊕m → R ⊕m is then computed using a DPO transformation : the nodes a, b, k, and l and their adjacent arcs from L ⊕m are in K ⊕m and R ⊕m .

(L ⊕m ) l j k i g h a b d e c f (L ) l j k i g h a b d e c f (G ⟨o⟩ (m(L ) )) α α (L) d c j i g h e f d c j i g h e f α α
m ⟨o⟩ (a) Extension of the left-hand side Definition 11 (Topological extension). Let π : ⟨o⟩ → τ be an embedding operation, let r : L ← K → R be a π-embedded graph transformation rule, and let m : L α → G be a kernel morphism on a π-embedded G-map G for the rule r.

(L ⊕m ) l j k i g h a b d e c f d c j i g h e f d c j i (K) (L) d c j i (R) l j k i a b d c l j k i a b d c (K ⊕m ) (R ⊕m ) (b) Application of the evaluated rule
Let L ⊕m be the result of the pushout between the inclusion L α → L and m ⟨o⟩ : L α → G α ⟨o⟩(m(L α ) α ), the restriction of m to the topological structure of the ⟨o⟩-orbit adjacent to the matched pattern:

L α / / m ⟨o⟩ L m ′ G α ⟨o⟩(m(L α ) α ) / / L ⊕m
The topological extension of r along the match morphism m is the rule r ⊕m : L ⊕m ← K ⊕m → R ⊕m defined by the following direct transformation:

L o o ? _ m ′ K / / m K R m R L ⊕m o o ? _ K ⊕m / / R ⊕m
The pushout construction of L ⊕m is well-founded since the morphisms L α → L and m : L α → G meet the conditions given in [START_REF] Habel | Relabelling in Graph Transformation[END_REF] ensuring the existence of natural pushouts. Also, note that the resulting rule of Figure 27 would still produce the inconsistent result of Figure 25(c) as extended parts' nodes are not relabeled.

By abusing the notation, the superscript ⊕m two distinct roles: affixed to L, it refers to a pushout construction, whereas affixed to K and R, it refers to a DPO construction with L ⊕m as the graph under transformation.

Embedding propagation

The final step of rule scheme instantiation consists in propagating node labels of the extended rule (step 3 in Figure 26). For example, in the extended rule of Figure 27(b), node labels have to be propagated in order to obtain the final of rule Figure 25(d). This step is a direct application of the quotient representation. For all graphs of the extended rule, each node is relabeled with its image label in the quotient graph. For example, in Figure 28 the three quotient graphs allow the embedding propagation of the extended rule of Figure 27(b) -e.g., node a unlabeled in L ⊕m can be labeled with the label of its image u in L ⊕m /π .

Definition 12 (Embedding propagation). Let π : ⟨o⟩ → τ be an embedding operation, G = (V, E, s, t, π, α) be a graph embedded on π : ⟨o⟩ → τ such that G satisfies the embedding consistency constraint, and q : G → G /π the quotient morphism with

G /π = (V /π , E /π , s /π , t /π , π /π , α /π ). The π-embedding propagation of G is the π-embedded graph G ⊙π = (V, E, s, t, π ′ , α) such for each node v in V , π ′ (v) = π /π (q V (v)).
Given an n-topological π-embedded rule r : L ← K → R, the π-embedding propagation of r is the rule Conversely to the construction of the topological extension, the embedding extension's construction is the same for L, K, and R. Besides, as the quotient existence depends on the satisfaction of the embedding consistency constraint, the embedding propagation only applies to rules for which all parts satisfy the constraint. The extended patterns must contain only one label value per embedding orbit for their quotient representation to preserve these unique labels. Let us consider the counterexample of Figure 29. The rule scheme defines the edge removal without consistently relabeling the face colors. Therefore, the face can be labeled with two distinct colors from the extended evaluated rule's righthand side. As this prevents the quotient's existence, the embedding propagation cannot be applied.

L ⊙π ← K ⊙π → R ⊙π , denoted r ⊙π . (L ) u v /π ⊕m (a) u (K ) /π ⊕m v (b) w (R ) /π ⊕m (c)
d c j i g h e f d c j i (K) (L) d c j i (R) u v v u u = e. col v = g. col u u u u v v v v u v u v (a) Rule scheme (L) l j k i g h a b d e c f l j k i a b d c l j k i a b d c (K) (R) (b) Extended rule

Rule scheme application

Regardless of consistency preservation, the instantiation of a rule scheme r(V L ) : L ← K → R to an object defined as an embedded G-map G along a kernel match morphism m : L → G consists in the three instantiation steps of Figure 26: (1) the evaluation r m V of the rule scheme r along m V to substitute node variables by nodes of G and evaluate the embedding expressions ;

(2) the topological extension (r m V ) ⊕m along m of the evaluated rule r m V ;

(3) the embedding propagation ((r m V ) ⊕m ) ⊙π ) along the extended rule (r m V ) ⊕m .

The final rule ((r m V ) ⊕m ) ⊙π is then applied on the targeted object G by DPO transformation, such as in Figure 30.

Note that the embedding propagation existence depends on the satisfaction of the embedding consistency constraint by all extended rule parts. This existence will be ensured by conditions on rule schemes provided in Section 8 to preserve G-map consistency. Therefore, rule schemes satisfying those conditions can always be instantiated for any kernel match morphism.

Definition 13 (Instantiation of rule scheme, application of rule scheme). Let r(V L ) : L ← K → R be a rule scheme on a user signature Ω π , and m : L α → G a kernel match morphism on a π-embedded G-map G.

Let

r m V = L m V ← K m V → R m V
be the evaluation of r along m (Definition 10). Let (r m V ) ⊕m be the topological extension of r m V along m (Definition 11). If all parts of (r m V ) ⊕m satisfy the embedding consistency constraint, let ((r m V ) ⊕m ) ⊙π be the π-embedding propagation of (r m V ) ⊕m (Definition 12).

The instantiation of r along m is ((

r m V ) ⊕m ) ⊙π denoted r m : L m ← K m → R m .
If there exists a morphism m * : L m → G extending m, the application of r to G along m denoted by G ⇒ r,m H is defined by the direct transformation G ⇒ r m , m * H.

(G) (H)

Figure 30: Rule scheme application.

Thanks to Definition 10 of graph scheme evaluations, the underlying topological structure of a rule scheme and any of its evaluations are equal. Thus, the rule can be directly extended along m. Finally, remark that similarly to the approach of [START_REF] Hoffmann | Graph Transformation with Variables[END_REF] recalled in Subsection 3.3, the substitution given by the kernel match morphism cannot always result in an extended full match of the instantiated rule. Let us take an example with the operation of edge removal of Figure 31. This time, rule scheme of Figure 31(a) removes an edge between two faces of the same color e.col. The rule scheme instantiation along the identity morphism on the object G of Figure 30 yields the rule of Figure 31(b) where the term e.col has been evaluated to yellow. As the extension process rests on the kernel match, the rule can always be extended regardless of the matched object's labels. However, the resulting rule cannot be applied to the object as an application match morphism cannot be induced because nodes g, h, i, j, k, and l of the object are blue.

Consistency Preservation

This section establishes and proves the conditions on rule schemes to preserve G-map constraints. Subsection 8.1 addresses the topological consistency while Subsections 8.2 and 8.3 focus on the embedding consistency. More precisely, we show that rule schemes that satisfy some given conditions can always be instantiated and that the instantiated rules satisfy the original conditions of embedding consistency preservation of Theorem 2.

Topological consistency preservation

The topological extension transforms the topological structure of the rule. It is the only part of the instantiation process that modifies the rule's topological structure. Thus, let us show that it preserves the conditions of topological consistency preservation of Theorem 1.

Lemma 1 (Topological consistency preservation of topological extension). Let r : L ← K → R be a rule embedded on π : ⟨o⟩ → τ and m : L α → G a kernel match morphism on a π-embedded G-map G.

If r satisfies the conditions of topological consistency preservation of Theorem 1, then the topological extended rule r ⊕m also satisfies these conditions.

Proof. Let π : ⟨o⟩ → τ be an embedding operation, let r : L ← K → R be a rule embedded on π, and let m : L α → G a kernel match morphism on a π-embedded G-map G.

The topological extension of r along the match morphism m suppose the computation of L ⊕m by ⟨o⟩-completion of m(L α ) α in G and the computation of K ⊕m and R ⊕m via the application of r on L ⊕m . Thus, elements in the graphs of r ⊕m either come from r and may be modified or come from the ⟨o⟩-completion and are preserved elements of K ⊕m . Therefore, properties from ⟨o⟩-orbits of a n-G-map and properties from L, K, and R are passed on to L ⊕m , K ⊕m , and R ⊕m .

Symmetry

For instance, ⟨o⟩-orbits are symmetric graphs and so are L, K, and R. Thus, L ⊕m , K ⊕m , and R ⊕m are symmetric graphs and r ⊕m satisfies the symmetry condition.

Adjacent arcs

When preserved nodes of K ⊕m are nodes coming from the ⟨o⟩-completion, then they and their corresponding nodes in L ⊕m and R ⊕m are sources of arcs having the same labels (those added with the ⟨o⟩-completion of m(L α ) α ). When preserved nodes of K ⊕m come from preserved nodes of K, they may have built from the ⟨o⟩-completion and may have arcs coming from r. If the arcs come from K or the ⟨o⟩-completion, they are preserved as in the previous case. Otherwise, the adjacent arcs condition verified by r guarantees that the preserved nodes are sources of arcs having the same labels in L and R. These arcs are kept in L ⊕m and R ⊕m .

In both cases, preserved nodes of K ⊕m are sources of arcs having the same labels in both L ⊕m and R ⊕m .

Nodes modified from L ⊕m to R ⊕m are issued from nodes modified from L to R (removed nodes of L \ K or added nodes of R \ K). By hypothesis on the rule r, they have exactly n + 1 arcs labeled from 0 to n, that remain present in the rule r ⊕m .

Therefore, r ⊕m satisfies the adjacent arc condition.

Cycle condition

Finally, the cycle condition holds likewise. Consider i and j in 0..n, such that i + 2 ≤ j.

• Added nodes of R ⊕m \K ⊕m come from R\K and the existence of an ijij-cycle is guaranteed by the cycle condition on r, i.e., added nodes of R \ K are sources of an iji-cycle.

• Preserved nodes of K ⊕m , sources of an ijij-cycle in L ⊕m that comes partly from the ⟨o⟩-completion, yield nodes in K that are not sources of an ijij-cycle in L.

Then, due to the cycle condition on r, the old arcs of L are preserved in R and are also in L ⊕m and R ⊕m . Together with the elements from the ⟨o⟩-completion, they build back the cycle in R ⊕m .

• Preserved nodes of K ⊕m , not sources of an ijij-cycle in L ⊕m , are sources of arcs coming either from the ⟨o⟩-completion or directly from r. The preservation of elements built from the orbit completion and the cycle condition hypothesis on r ensure the preservation of i-arcs and j-arcs necessary for the cycle condition for ijij-cycles.

Thus, r ⊕m satisfies the cycle condition. Consequently, r ⊕m satisfies the conditions of topological consistency preservation of Theorem 1.

As the embedding propagation only modifies the node labeling, it does not alter the topology, and thus, it preserves the topological consistency.

Lemma 2 (Topological consistency preservation of the embedding propagation). Let r : L ← K → R be a rule embedded on π : ⟨o⟩ → τ and m : L α → G a kernel match morphism on a π-embedded G-map G.

If r satisfies the conditions of topological consistency preservation of Theorem 1 then the embedding propagated rule r ⊙π satisfies the conditions of topological consistency preservation of Theorem 1.

Proof. As previously said, the embedding propagation step modifies node labeling. Thus, r : L ← K → R also satisfies the topological consistency conditions of Theorem 1.

From Lemmas 1 and 2, the preservation can be extended to the whole evaluation and instantiation process.

Theorem 3 (Topological consistency preservation of instantiation). Let r(V L ) : L ← K → R be a rule scheme on a user signature Ω π , and m : L α → G a kernel match morphism on a π-embedded G-map G.

If r(V L ) satisfies the conditions of topological consistency preservation of Theorem 1, then the instantiated rule r m = ((r m V ) ⊕m ) ⊙π , if it exists, also satisfies these conditions.

Proof. As r m V has the same topological structure as r(V L ), r m V satisfies the conditions of topological consistency preservation. Then, according to Lemma 1, (r m V ) ⊕m also does. Finally, according to Lemma 2, r m = ((r m V ) ⊕m ) ⊙π also satisfies these conditions.

Condition of non-overlap

Before we study the embedding consistency preservation, we mention a particularly undesirable situation likely to occur with the topological extension: the overlap of embedding orbits. By considering a minimal match of the transformed embeddings that relies on the automatic completion of transformed embedding orbits, we are exposed to unexpected merges of different embedding orbits. Let us consider the face stretching defined by the rule scheme of Figure 32.

The operation consists of matching two edges, defined by the orbits resp. ⟨0⟩(p) and ⟨0⟩(o), to translate vertices at their extremities, as defined by the pos embedding, in the two opposite directions, -→ v and --→ v . When the rule scheme is applied to the square face (BDCE), the extended rule of Figure 33 contains four vertices in R respectively embedded by as we wanted to match and translate four vertices but only match three. We call an overlap such a situation where different embedding orbits manipulated in the rule end up merged in the extended rule. We define a condition on the kernel morphism that prevents it. This condition can be seen as an extension of the injective condition on the match morphism to the embedding orbits.

B ′ = B -- → v , D ′ = D -- → v , C ′ = C + - → v and E ′ = E + - → v . (L) o q p r u (x) = x. pt + v s (x) = x. pt s (o) s (q) s (p) s (r) (K) o q p r (R) o q p r t (o) t (q) u (p) u (r) t (x) = x. pt -v
Lemma 3 (Non-overlap). Let r(V L ) : L ← K → R be a rule embedded on π : ⟨o⟩ → τ and m : L α → G a kernel match morphism on a π-embedded G-map G.

We say that the topological extension of r along m produces an overlap in L if for v and w two nodes of L such that v ̸ ≡ L⟨o⟩ w then m ′ (v) ≡ L ⊕m ⟨o⟩ m ′ (w), where the morphism m ′ : L → L ⊕m was defined in Definition 11. This definition is extended to K and R using the appropriate equivalence relations and morphisms. We say that the topological extension of r along m does not produce overlap if it produces no overlap in L, K, and R.

The topological extension of r along m does not produce overlap if m satisfies the following condition of non-overlap: for two nodes v and w of L, v ̸ ≡ L⟨o⟩ w implies that m(v) ̸ ≡ G⟨o⟩ m(w).

Proof. Let us show that L ⊕m does not contain overlap. Let us suppose that there exist v and w two nodes of L such that v ̸ ≡ L⟨o⟩ w and m ′ (v) ≡ L ⊕m ⟨o⟩ m ′ (w). Then, the overlap comes from the topological extension, i.e the node images m(v) and m(w) belong to the same orbit in G:

m(v) ≡ G⟨o⟩ m(w).
This contradicts the condition of non-overlap. The proof is similar for K ⊕m and R ⊕m .

The condition of non-overlap will be required to prevent such undesirable applications before considering embedding consistency preservation in Section 8.3.

Embedding consistency preservation

We now study how the non-overlap condition combined with the conditions of embedding consistency preservations on evaluated rule schemes ensure that the instantiated rules satisfy the 3 conditions (identified resp. by (A), (B), and (C) in Theorem 2) of embedding consistency preservation on rules given in Theorem 2. In particular, we will release the condition (B) of full match of transformed embeddings in a weak version, identified by (B'), as it was the goal of the automatic orbit completion of transformed embeddings (step 2 of the pipeline given in Figure 26).

We start with the topological extension step, i.e., step 2 . Note that as the topological extension nodes are not labeled, the extended rule is only expected to satisfy a weak version of the full match of transformed embeddings of Theorem 2 that does not require total labeling of the orbit.

Lemma 4 (Embedding consistency preservation of topological extension). Let r : L ← K → R be a rule embedded on π : ⟨o⟩ → τ and m : L α → G a kernel match morphism on a π-embedded G-map G. If:

(1) r satisfies the conditions of topological consistency preservation of Theorem 1, of transformation systems. The first solutions for correctness are the computation of a weakest precondition relative to a post-condition [START_REF] Dijkstra | A Discipline of Programming[END_REF]. The second one is the specification of a proof system sound with respect to the operational semantics of the language [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. Nested conditions support both solutions: see [START_REF] Habel | Correctness of high-level transformation systems relative to nested conditions[END_REF] for the computation of the weakest precondition and [START_REF] Poskitt | Hoare-Style Verification of Graph Programs[END_REF] for proof of partial correctness of the language GP [START_REF] Plump | The Graph Programming Language GP[END_REF].

One avenue of research could be to study the constraints of Definition 5 and Theorem 1 using nested conditions. However, the presented work studied the preservation of the embedding consistency. A generalized map G is correctly embedded on π : ⟨o⟩ → τ if all nodes share the same τ -value within each ⟨o⟩-orbit of G. Since an orbit corresponds to a subgraph induced by a set of arc labels, the embedding consistency constraint of Definition 6 is not expressible in first-order logic but requires monadic second-order logic. However, there is no extension of nested conditions encapsulating monadic second-order logic (at least to our knowledge).

As a final remark, let us point out that in general, G-maps are provided with several embeddings simultaneously, for instance, with col and pos embeddings for our running example of triangulation. Instead of a unique partial node labeling function π V , we have then to consider an I-indexed family (π V,i ) i∈I of partial labeling functions, where I is a given set of indexes [START_REF] Bellet | Rule-based transformations for geometric modeling[END_REF]. Rule application then requires superimposing several topological extensions, which is implemented in Jerboa (see Section 9.2), but which would make the explanations more intricate.

Applications

This section gives a presentation of applications done using the Jerboa framework, [1] that highlights the embeddings consistency preservation. As mentioned in the introduction, the primary motivation for our rule-based approach is developing the Jerboa platform to support the design of modelers dedicated to different application areas. Jerboa provides a rule editor where the modeler designer can define each specific operation. The operation is written as a rule statically analyzed to check the topological and geometric consistency preservation. The rule is then compiled to become a ready-to-use operation. Section 9.1 presents a new operation involving several embeddings. This operation computes exploded views of objects and allows better visualization of their structure. Section 9.2 illustrates exploded views of two 3D objects, a nightstand, and a hydraulic circulator pump, using the Jerboa platform. Section 9.3 gives some insights on other concrete applications implemented with Jerboa and exhibits some advantages of our rule-based approach for prototyping modelers.

Exploded view

The manipulation of objects often requires visualizing their topological structure. Thus, some software offers exploded views supporting the splitting of volumes, faces, etc. of the modeled object [START_REF] Mohammad | Automatic generation of exploded view by graph transformation[END_REF][START_REF] Li | Automated generation of interactive 3D exploded view diagrams[END_REF]. We introduce the notion of exploded view in a simplified way, in the context of 2D objects, to ease the reading of figures. A square face is often displayed as 4 edges connected to the 2D points associated with the face's vertices. An exploded view of the face slightly separates the edges, preserving as much as possible the appearance of the initial object in 2D. For an edge endpoint, its explosion is obtained by moving it slightly towards the second edge endpoint. Practically, each node is provided with two embeddings, pos : ⟨1 2⟩ → point_2D for the default display of objects and exp_pos : ⟨2⟩ → point_2D for the display in exploded views. For a node a, the computation of the 2D position in the exploded view relies on the position in the default display and looks like: barycenter(a.pos, coef 1 , center(pos ⟨0⟩ (a)), coef 2 ) with:

• barycenter : point_2D × f loat × point_2D × f loat → point_2D function, that
computes the weighted barycenter of two positions;

• center : point_2D • → point_2D function, that computes the geometric center of a multiset of positions;

• coef 1 and coef 2 two coefficients useful to modulate the display in exploded views.

Figure 35 presents a rule scheme to compute the exploded view of a vertex incident to two adjacent edges. In our structure, this explosion puts the α 1 -links forwards. The rule scheme is illustrated in Figure 35(a). In Jerboa, the syntax is more compact, and the rule scheme shown in Figure 35(b) is of the form L → R. Indeed, the interface graph K can be restricted to L ∩ R and the complete rule L ← K → R can be reconstructed (see [START_REF] Bellet | Geometric modeling: Consistency preservation using two-layered variable substitutions[END_REF]).

In Figure 35(b), the left-hand side matches a node a. The right-hand side looks similar to the matched pattern because there is no topological modification. However, the labels indicate a computation on the exp_pos embedding. As we see at the bottom of the window, the operator calls the weighted barycenter between the node a and the center of the ⟨0⟩-orbit that contains a. This expression is the same as depicted in Figure 35(a). Note that embeddings are implicit in the left-hand side of the rule scheme since we can retrieve the nodes with modified embeddings from an analysis of the right-hand side.

The editor checks the conditions for preserving the topological and the embedding consistency as the rules are being written. When the design of this rule is complete, the editor generates the final code. Then, Jerboa's generic viewer offers an interactive way to visualize the G-map and apply the designed operation. Figure 36 shows this viewer where the G-map encodes a square face. The left picture displays the default geometry of a vertex at a corner of the square face (Figure 36(a)) that forms two consecutive edges. All operations of the modeler are listed on the left of the window. We can apply the operation presented in Figure 35(b) to a node of the vertex, producing the exploded geometry of Figure 36(b). The vertex is exploded, and we see the α 1 -link between the orbit formed by the two darts which compose the vertex.

With this operation, to obtain the complete exploded view of the square, the previous operation is applied to each face's node. Since a face is a ⟨0 1⟩-orbit, its explosion can be realized directly: the transformation is simultaneously applied to each node of the orbit. To retrieve these orbits, Jerboa uses topological variables [START_REF] Bellet | Geometric modeling: Consistency preservation using two-layered variable substitutions[END_REF]. The following section <α0, α1, α2> n0 <α0, α1, α2> exp_pos n0 presents the explosion of volumes in 3D, relying on such variables. The operation is illustrated in Figure 37, where the whole volume is exploded at once. The node n0 is preserved between the left-hand and right-hand sides. As previously, it is labeled with the term exp_pos that calls for a more global computation (not given here), still using the barycenter notion. As a final remark, Jerboa's rule schemes do not support the affectation of an embedding value on the left-hand side. Therefore, if we want to restrict the exploded view's computation to vertices adjacent to a red-colored face, we use application conditions.word

Jerboa

In this section, we briefly discuss the implementation of the rules in the Jerboa platform.

The design and architecture of the Jerboa platform have been presented in [START_REF] Bellet | Designing a topological modeler kernel: a rule-based approach[END_REF][START_REF] Bellet | Geometric modeling: Consistency preservation using two-layered variable substitutions[END_REF]. Jerboa is also available on a website [1]. Figure 38 illustrates exploded views of a nightstand made by an artist. This object has 112 vertices for 152 faces on 14 volumes and corresponds to a small object to be included in a room for architectural purposes. In our structure, this object counts 608 nodes.

The object is encoded in OBJ file format. This file format is widespread in computer graphics and offers additional information such as texture coordinates and materials. Even though this information is not relevant for our work, all these characteristics must be preserved when computing the exploded view, i.e., the topological structure must handle all these elements without modifying their values. Besides, this format may contain topological aberrations. Thus, we use the algorithm developed in [START_REF] Belhaouari | Reconstruction of Volumes from Soup of Faces with a Formal Topological Approach[END_REF] to reconstruct the G-map before applying the explosion operation. Figure 38 Concretely, we made a command-line interface application with the Java version of Jerboa. We designed a modeler for 3-G-maps with the following embeddings:

• pos : ⟨1 2 3⟩ → point_3D stands for the original coordinates from the file.

• exp_f ace : ⟨1 3⟩ → point_3D represents the computed coordinates after face explosion.

• exp_vol : ⟨1 2⟩ → point_3D represents the computed coordinates after volume explosion. • orient : ⟨⟩ → boolean is dedicated to the reconstruction of the topology.

• tex : ⟨1 2 3⟩ → vector_2D memorizes texture coordinates from the file.

• mat : ⟨⟩ → string memorizes materials from the file.

The application takes an OBJ file and various weights and produces a new OBJ file with the exploded geometry. The filename reflects the name of the original file and the given weights. The application is available on the Jerboa website10 .

Other applications

Table 1 summarizes information on some modelers designed using Jerboa and respectively called JerboaArchi, Jermination, Jeolog, and Japhy. Figure 39 gives a brief overview of these tools.

Modeler

JerboaArchi JerboaArchi is a modeler dedicated to architecture (Figure 39(a)), providing basic operations for elevating/extruding a 2D map (done by an architect) into a 3D map, for example, operations to add doors or windows. This modeler has been used to experiment with the reevaluation of rule sequences [START_REF] Cardot | Persistent Naming Based on Graph Transformation Rules to Reevaluate Parametric Specification[END_REF]. It allows the recording of an interactive construction to be reevaluated with new geometric parameters, creating a new model. Jermination follows L-system mechanisms [START_REF] Bohl | Modeling Fruits and Their Internal Structure Using Parametric 3Gmap L-systems[END_REF] appreciated by botanists, who usually write rules reflecting the elementary steps of plant growth. Jermination implements similar rules and allows the display of the growth stages of a plant (Figure 39(b)).

Jeolog is dedicated to geology (Figure 39(c)). Here again, the flexibility of embeddings allows a double representation of geometric points (one at sedimentation times and another at present times) [START_REF] Gauthier | A Topological Approach for Automated Unstructured Meshing of Complex Reservoir[END_REF]. This feature eases the comprehension of Earth layers and fault displacements. Topological cells store data, which simplifies the design of complex operations.

Japhy stands for Jerboa animation-based physics and provides a library for physic simulations (Figure 39(d)). Currently, it supports some physics models such as massspring, finite element method, or mass-tensors among several meshes (triangle, quad, tetrahedron, hexagon). Rules help developers correctly design the location of force interactions [START_REF] Ben Salah | A general physicaltopological framework using rule-based language for physical simulation[END_REF], while runtime verification helps them write correct computations when designing new forces.

To assess the added value of Jerboa, we now briefly comment on metrics provided by Table 1. Rule count gives the number of main rules defined inside the modeler, leaving out operations not issued from the rule application engine. The embedding count indicates the number of considered distinct embeddings. Then we give the average size of objects manipulated with the modeler: geology has the largest object size because of the complexity of the data. The design time gives the average designing time to create all the rules associated with the modeler. This indicator shows that Jerboa can be used either for fast development or step-by-step prototyping.

Conclusion

To cope with the variety of embeddings used in geometric modeling, we introduced a new kind of graph transformation variables, called node variables, dedicated to embedding computations in topology-based geometric modeling. These node variables are equipped with operators that can be extended with user-defined data types, providing a general framework supporting the definition of object transformations for any application domain. Our operators allow the topological structure's traversal without matching the precise configuration of the pattern. The rule instantiation mechanism allows embedding modifications to propagate to the object's corresponding cells. Therefore, embedding computation does not depend on the underlying concrete topology.

The application mechanism presented in Figure 26 is structured in several layers. Graph transformation conditions that guarantee the preservation of the embedding consistency are directly extendable to rule schemes with node variables. A single rule application engine has been implemented to handle any operation, such as the computation of exploded views. Jerboa supports a static verification of the syntactic conditions that ensure the preservation of the object's embedding.

As stated in Section 6, we restricted ourselves to the syntactic equality of terms. However, different terms may have the same value. For instance, consider two nodes a and b in the same ⟨0 1⟩-orbit. These two nodes have the same color but the terms a.col and b.col differ. Besides, user-defined operators may be associative or commutative. For example mix( , ) = mix( , ) = . An interesting yet challenging work could be to study rewriting of terms modulo equivalence induced by the joint use of user-defined operators and dedicated embedding operators.

At first glance, topological conditions defining generalized maps could be expressed with first-order graph formulas, thereof equivalent to nested conditions on graphs. Geometric modeling provides an application field that goes beyond the first order. Indeed, the present paper illustrates an application of graph rewriting requiring monadic second-order formulas. We believe that geometric modeling represents a motivating application domain to promote the definition of a new framework inspired by nested conditions, expressing monadic second-order formulas.

or entity with any financial interest or non-financial interest in the subject matter or materials discussed in this manuscript.

Figure 1 :

 1 Figure 1: Two modeling operations.

Figure 2 :

 2 Figure 2: DPO graph transformation.

Figure 3 :

 3 Figure 3: A relabeling rule.

Figure 5 :

 5 Figure 5: Objects of same topological structure.

Figure 6 :

 6 Figure 6: Object inconsistencies.

Figure 7 :

 7 Figure 7: Topological decomposition of a geometric 2D object.

Figure 8 :

 8 Figure 8: Orbits adjacent to e.

Figure 9 :

 9 Figure 9: Completions.

  Figure 10(b) illustrates the embedded G-map G col = (V, E, s, t, col, α) built on G topo , thus sharing its topological elements with G pos . The embedding operation col maps colors ( and ) to the nodes of V . G pos , a 2-G-map with vertices embedded by 2D positions G col , a 2-G-map with faces embedded by colors

Figure 10 :

 10 Figure 10: Two embedding operations.

  (b) presents the quotient along ⟨0 1⟩-orbits of the 2-G-map of Figure 10(b). Nodes a, b, c, d, e, and f of the triangle face generate the yellow quotient node u while the nodes of the square face produce the blue quotient node v.

Figure 11 :

 11 Figure 11: Quotients of the embedded 2-G-maps given in Figure 10.

Figure 12 :

 12 Figure 12: Two operations on the position embedding.

Figure 13 :

 13 Figure 13: Incoherent translation.

(A )

 ) Embedding consistency: L, K, and R satisfy the embedding consistency constraint (Definition 6).

Figure 14 :

 14 Figure 14: Coherent translation.

Figure 15 :

 15 Figure 15: Two non-consistent rules that break conditions of Theorem 2.

Figure 16 :

 16 Figure 16: Application of the vertex insertion.

  (a)). Nodes are labeled with terms 6 over node variables of L, allowing matching the existing translation t = midpoint (i. pos, k. pos) + w

Figure 17 :

 17 Figure 17: Rule schemes of the operations of Figure 12.

  (b) and uses the .α 2 operator to access adjacent faces. In the term v = mix(e.col, e.α 2 .col) of Figure 19(b), e.α 2 allows the access to the 2-neighbor of e in the transformed object.

Figure 18 :

 18 Figure 18: Face triangulations.

  (e. col, e. α 2 . col) u = mix (b. col, b. α 2 . col) t = mix (a. col, a. α 2 . col)

Figure 19 :

 19 Figure 19: Face triangulations of Figure 18 on a col-embedded G-map.

Figure 20 :

 20 Figure 20: Face triangulation of Figure 18 on a pos-embedded G-map.

Figure 21 :

 21 Figure 21: Evaluation of the multiset of the face positions.

Figure 22 :

 22 Figure 22: Two evaluations of the rule scheme Figure 19.

Figure 23 :

 23 Figure 23: Expected rule scheme of a vertex translation.

Figure 25 :

 25 Figure 25: Rule scheme of the edge removal and its evaluation.

Figure 26 :

 26 Figure 26: Rule scheme evaluation and instantiation.

Figure 27 :

 27 Figure 27: Construction of the topological extension.

Figure 28 :

 28 Figure 28: Quotients for the embedding propagation.

Figure 29 :

 29 Figure 29: Inconsistent edge removal.

Figure 31 :

 31 Figure 31: Edge removal between two faces of same color.

Figure 32 :

 32 Figure 32: Face stretching rule scheme.

Figure 33 :

 33 Figure 33: Consistent face stretching..

Figure 34 :

 34 Figure 34: Inconsistent face stretching..

  (a.pos, coef , center(pos (a), coef. ) s = a. exp_pos s Formal rule scheme (b) Concret rule scheme created with the Jerboa editor

Figure 35 :

 35 Figure 35: Rule scheme to update the exp_pos embedding value of a node.

Figure 36 :

 36 Figure 36: Exploded view of two edges incident to the same vertex in 2D.

Figure 37 :

 37 Figure 37: Rule scheme to compute the exploded view of a whole volume.

  (a) shows a textured nightstand where texture coordinates are preserved during the explosion (Figures 38(b) and 38(c)).

Figure 38 :

 38 Figure 38: Exploded views of a nightstand.

Figure 39 :

 39 Figure 39: Various modelers done with Jerboa.

Table 1 :

 1 Metrics for various modelers made with Jerboa

	Jermination	Jeolog	Japhy

One generally considers standard graph morphisms instead of only considering inclusions.

These conditions, known as the dangling condition, mainly ensure that the removal of nodes does not leave arcs without their node extremities.

Given two sets A and B, a partial function f :A → B is a function from subset A ′ of A to B.The set A ′ is the domain of f and is noted Dom(f ). We say that f (x) is undefined, and write f (x) =⊥, if x is in A -Dom(f ).

Labels of nodes or arcs are either variables of X or expressions built over variables of X.

To agree with the community of geometric modeling, we chose the term "embedded" instead of the term "attributed", most commonly used in the graph transformation community.

Note that terms are detailed on top of the rules for readability purposes.

In accordance with Definition 1, rule nodes must be labeled in L in order to be relabeled.

As sketched previously in the paper, the first two are used with a postfixed notation, while the third is used with a prefixed notation.

Link to website (last consulted on July 4th, 2022): http://xlim-sic.labo.univ-poitiers. fr/jerboa/

(2) r satisfies the conditions of embedding consistency and of labeling of extended embedding orbits of Theorem 2 (conditions (A) and (C)),

(3) and m satisfies the condition of non-overlap of Lemma 3, then the topological extended rule r ⊕m satisfies the following conditions:

(A) Embedding consistency of Theorem 2: L ⊕m , K ⊕m , and R ⊕m satisfy the embedding consistency constraint of Definition 6.

(B') Weak full match of transformed embeddings: if a preserved node v of K ⊕m has a transformed embedding, then R ⊕m ⟨o⟩(v) is a full orbit; i.e., if v is a node of K ⊕m such that π L ⊕m (v) ̸ = π R ⊕m (v), then every node of R ⊕m ⟨o⟩(v) is the source of exactly one i-arc for each i of ⟨o⟩.

(C) Labeling of extended embedding orbits of Theorem 2: if v is a node of K ⊕m and there exits a node w in R ⊕m ⟨o⟩(v) such that w is not in L ⊕m ⟨o⟩(v), then there exist

Proof. Let us show that the three conditions of the Lemma 4 hold.

(A) Embedding consistency Let v and w be two nodes of L ⊕m such that v ≡ L ⊕m ⟨o⟩ w, π L ⊕m (v) ̸ = ⊥, and π L ⊕m (w) ̸ = ⊥. L ⊕m results from the pushout between m ⟨o⟩ : L α → G α ⟨o⟩(m(L α ) α ) and the inclusion L α → L. As nodes of G α ⟨o⟩(m(L α ) α ) are unlabeled, node labels in L ⊕m necessarily come from L. Because of the condition of non-overlap, the antecedent of v and w by m

and m ′-1 (w) are both labeled and L satisfies the embedding consistency constraint, then

The proof is the same for K and R. Therefore, r ⊕m satisfies the embedding consistency condition. (B') Weak full match of transformed embedding.

Let v be a node of K ⊕m such that π L ⊕m (v) ̸ = π R ⊕m (v), Let w be a node in R ⊕m ⟨o⟩(v). We have to consider where w comes from: it can either be a node added by the orbit completion, the image of an added node in R \ K, or the image of a preserved node in K.

Assume w is a node added by the orbit completion, i.e., a node of K ⊕m . Then, because G is a G-map and satisfies the adjacent arc constraint, the topological extension ensures that w is the source of exactly one i-arc per i in ⟨o⟩.

Otherwise w admits a unique antecedent by morphism m

the adjacent arc condition of Theorem 1 on r guarantees that w R is the source of exactly one arc per label in 0..n. In particular, w R is the source of exactly one i-arc for each i of ⟨o⟩.

Finally, consider that w R is a preserved node of K and let i be a label from ⟨o⟩.

• Thanks to the adjacent arc condition of Theorem 1 on r, if w R is the source of an i-arc in L then it is also in R and w is the source of an i-arc in R ⊕m .

• Otherwise, the ⟨o⟩-completion adds an i-arc of source w in L ⊕m . By construction of the topological extension of r along m, this i-arc is also in R ⊕m .

Either way, w is the source of an i-arc in R ⊕m . Because G is a G-map and because m : L → G is an injective morphism, w is not the source of another i-arc in R ⊕m . Therefore, r ⊕m satisfies the weak full match of transformed embedding. (C) Labeling of extended embedding orbits.

Let v be a node of K ⊕m . By construction of the topological extension, there is a node u in K such that the image m K (u) of u in K ⊕m is in the same ⟨o⟩-orbit as v, i.e., m K (u) ≡ L ⊕m ⟨o⟩ v, m K (u) ≡ K ⊕m ⟨o⟩ v, and m K (u) ≡ R ⊕m ⟨o⟩ v. Suppose there is a node w in R ⊕m ⟨o⟩(v) such that w is not in L ⊕m ⟨o⟩(v). The topological extension definition ensures that w has an antecedent by m R . Because r satisfies the labeling of extended embedding orbits, there exists

Therefore, r ⊕m satisfies the labeling of extended embedding orbits.

Let us show that the embedding propagation step, i.e., 3 , restores the original embedding consistency conditions.

Lemma 5 (Embedding consistency preservation of the embedding propagation). Let r : L ← K → R be a rule embedded on π : ⟨o⟩ → τ and m : L α → G a kernel match morphism on a π-embedded G-map G.

If r satisfies the conditions (A), (B ′ ), and (C) of Lemma 4, then the embedding propagated rule r ⊙π satisfies the conditions of embedding consistency preservation of Theorem 2.

Proof. By construction of the embedding propagation, we have L → L ⊙π and L α = L ⊙π α (and the corresponding relations for K and R). Besides, the embedding propagation is well-defined as r satisfies the conditions (A) of embedding consistency of Theorem 2.

Because the embedding propagation does not change the topology, the condition (C) of labeling of extended embedding orbits is preserved.

The π-embedding propagation step propagates each embedding label along the full ⟨o⟩-orbit without changing the topology. Thus, the conditions of embedding consistency (A) are preserved.

Thanks to the π-embedding propagation, every node v such that π R (v) ̸ = ⊥ has it ⟨o⟩-orbit fully embedded in R ⊙π , i.e., for all node v ′ in R ⊙π ⟨o⟩(v), π R ⊙π (v ′ ) ̸ = ⊥. This extends the condition (B ′ ) of weak full match of transformed embeddings to the condition (B) of full match of transformed embeddings.

Therefore, the embedding propagated rule r ⊙π satisfies the conditions of embedding consistency preservation of Theorem 2.

Finally, we can extend this result to the whole rule instantiation and show that it always exists if the following conditions of embedding consistency preservation are satisfied.

Theorem 4 (Embedding consistency preservation of instantiation). Let r(V L ) : L(V L ) ← K(V L ) → R(V L ) be a rule scheme on a user signature Ω π and m : L α → G be a kernel match morphism on a π-embedded G-map G.

The instantiated rule ((r m V ) ⊕m ) ⊙π exists and satisfies the conditions of embedding consistency preservation of Theorem 2 if the following conditions are satisfied:

(1) r(V L ) satisfies the conditions of topological consistency preservation of Theorem 1,

(2) r(V L ) satisfies the conditions of embedding consistency and of labeling of extended embedding orbits of Theorem 2 (conditions (A) and (C)),

(3) and m satisfies the condition of non-overlap of Lemma 3, Before giving the proof, let us point out that, as already indicated in Section 6, rule schemes meet the conditions of Theorems 1and 2 subject to considering the syntactic equality of the terms used for embedding labels.

Proof. As equal terms are evaluated by equal values, if r(V L ) satisfies conditions of Theorem 4, so does the evaluated rule r m V . Then, the extended rule (r m V ) ⊕m satisfies the condition of Lemma 4. Therefore, the propagation ((r m V ) ⊕m ) ⊙π exists. Finally, according to Lemma 5, the instantiated rule ((r m V ) ⊕m ) ⊙π satisfies the conditions of embedding consistency preservation.

Properties of Theorem 4 are sufficient but not necessary to ensure the preservation of the embedding consistency. The main issue is the possibility of several terms having the same evaluation based on semantic information of user-defined functions on embeddings. One solution could be to relax the embedding consistency condition. However, this would lead to inconsistent rules not being discarded. Another solution could be equational unification, as discussed in [START_REF] Baader | Equational Unification[END_REF]. Nevertheless, in this case, the user would have to specify the identities that axiomatize the function properties, which can be challenging. In practice, these properties are similar to compilation warnings provided by code editors. Thus, if a property is unsatisfied because of the algebraic properties of user-defined functions, the user should assess the rule's validity by themselves. In the paper, we avoided the difficulty of assessing term equivalence by minimally labeling graphs of rule schemes. On each orbit, we either put at most one label or the same term for labeling several nodes of an orbit. By noticing that we have carefully labeled all the nodes of an orbit with the same term, rules schemes given in Figure 19(b) and 20(b) meet conditions of Theorem 4.

One common way to ensure consistency preservation is to forbid particular rules' applications, corresponding to Negative Application Conditions [START_REF] Ehrig | Fundamentals of Algebraic Graph Transformation[END_REF]. Nevertheless, NACs rely on morphisms on the left-hand side of the rule to be applied, while embedding constraints concern subgraphs of arbitrary size (depending on the modeled object). In other words, the embedding constraint cannot be verified statically at a local scale at the rule level. NACs have been extended to a nested framework [START_REF] Habel | Correctness of high-level transformation systems relative to nested conditions[END_REF]. Nested conditions are equivalent to first-order graph formulas and have been used to show the correctness

Competing Interests Declaration

The authors did not receive support from any organization for the submitted work. All authors certify that they have no affiliations with or involvement in any organization