Bidirectional graph transformation is expected to play an important role in model-driven software engineering where artifacts are often refined through compositions of model transformations, by propagating changes in the artifacts over transformations bidirectionally. However, it is often difficult to understand the correspondence among elements of the artifacts. The connections view elements have among each other and with source elements, which lead to restrictions of view editability, and parts of the transformation which are responsible for these relations, are not apparent to the user of a bidirectional transformation program. These issues are critical for more complex transformations. In this paper, we propose an approach to analyzing the above correspondence as well as to classifying edges according to their editability on the target, in a compositional framework of bidirectional graph transformation where the target of a graph transformation can be the source of another graph transformation. These are achieved by augmenting the forward semantics of the transformations with explicit correspondence traces. By leveraging this approach, it is possible to solve the above issues, without executing the entire backward transformation.
Bidirectional transformations has been attracting interdisciplinary studies [
A bidirectional transformation consists of forward (F ) and backward (B)
transformations [
GS
F
GV
edit
whIenthemraanyv,iewespeedcgiealhlyasciotsmoprliegxintirnanasfpoarrmtiactuiloanrs,souitrcies endogte oi mrampedairatt(efloyr aexpapmarpelnet, G′S B G′V
operators or variables) in the transformation, and what that part is. Thus, it is not
easy to tell where edits to the view edge are propagated back to. Moreover, in a setting in which usual strong
well-behaved properties like PutGet [
Our bidirectional transformation framework called GRoundTram (Graph Roundtrip Transformation for
Models) [
There are some existing work with similar objectives. Traceability is studied enthusiastically in model-driven
engineering [
The rest of the paper is organized as follows: Section 2 overviews our motivation and goal with a running
example. More involved examples can be found on our project website at http://www.prg.nii.ac.jp/projects/
gtcontrib/cmpbx/. Section 3 summarizes the semantics of our underlying graph data model, core graph
language UnCAL [
1In this case, the constant in the transformation is pointed out so that user can consider changing it in the transformation directly. country name people name 25 lcaonngtuinaegnet 19 language 3 continent 9 language 1 name people
Japan Japanese
Asia Germany Europe German Austria people {&} country 15 continent 26 country 12 ethnicGroup 11
German {&} 0 result 13 result 14 language located ethnic language located ethnic 3 7 4 8 10 12
German 1 5 9 2 6 11 ethnicGroup select { result: { ethnic: $e, language: $lang, located: $cont } where { country: { name:$g, people: { ethnicGroup: $e} , language: $lang, continent: $cont} in $db, { $l :$Any} in $cont , $l = Europe
S1: In the view graph (Fig. 2), three edges have identical labels “German” (3 , German, 1), (4, German, 2) and (12, German, 11), but have different origins in the source graph and are produced by different parts in the transformation. For example, the edge ζ = (3, German, 1) is the language of Germany and is a copy of the edge (1, German, 0) of the source graph (Fig. 1). On the other hand, ζ has nothing to do with the edge (11, German, 10) of the source graph despite identical labels. This later edge denotes the ethnic group instead. In addition, ζ is copied by the graph variable $lang in the select part of the transformation. Other graph variables and edge constructors do not participate in creating ζ. It would be much easier for the user to understand, if the system visually highlights corresponding elements between source graph, view graph and transformation to increase comprehensibility.
S2: In this example, the non-leaf edges of the view graph (“result”, “located”, “language” and “ethnic”) are constant edges in the sense that they cannot be modified by the user in the view. Ideally, the system should make such constant edges easily recognizable to prevent the edits in the view and guide the user to make an edit to the constant in the transformation instead.
S3: In another scenario, the user decides that the language of Germany should better be called “German (Germany)” and the language of Austria be called “Austrian German” and thus rename the view edges (3 , German, 1) and (4, German, 2) to (3, German (Germany), 1) and (4, Austrian German, 2) accordingly. However, the backward transformation rejects this modification because these two view edges originate from the language “German” in a single edge of the source graph. The backward propagation of two edits would conflict at the source edge. Ideally, the system would highlight groups of edges that could cause the conflict, and would prohibit triggering the backward transformation in that case.
S4: Finally, suppose both of the edges labeled “Europe” in the view graph are edited to “Eurasia”. Although this time these updates would be propagated to the same originating source edge (3, Europe, 2) without conflict, since the transformation depends on the label of this edge, changing it would lead to the selection of another conditional path in the transformation in a subsequent forward transformation. The renaming would cause an empty view after a round-trip of backward and forward transformation. To prevent this, such edits are rejected in our system. Changes in the control flow are very difficult or impossible to predict if the transformation is too complex. We can assist the prediction by highlighting the conditional branches involved.
Formal property As a remark, our editability checking is sound in the sense that the edits that passed the checking always succeed. We provide a proof sketch in Section 5.
Using this property and analysis, additional interesting observations can be made. In the Class2RDB example on our project website, there is no edge in the view for which the above last warning is caused. Thus, the transformation is ”fully polymorphic” in the sense that all edges that come from source graph are free from label inspection in the transformation. Note that this editability property may not be fully determined by just looking at the transformation. Non-polymorphic transformations may still produce views that avoid the warning. For example, select $g where { a:$g} in $db is not polymorphic, but the edits on edges in the view never cause condition expressions to be changed, because they are not inspected (they are inspected by bulk semantics explained in the next section but left unreachable). Tracing mechanism Though the editability analysis is powerful enough to, for example, cope with complex interactions between graph variables and label variables, the underlying idea is simple. For the analysis of a chain of transformations, if an edge ζ is related to ζ0 in the first transformation and ζ0 is related to ζ00 in the second transformation, then trace information allows to relate ζ and ζ00, possibly with the occurrence information of the language constructs in the transformation that created these edges. The variable binding environment is extended to cope with this analysis.
Support of editing operations other than edge renaming As another remark, this paper focuses on
updates on edge labels, and trace information is designed as such. However, we can relatively easily extend the
data structure of the trace to cope with edge deletion. The data structure already supports node tracing, so
insertion operation can be supported by highlighting the node in the source on which a graph will be inserted.
Support of permissive bidirectional transformation The bidirectional transformation we are dealing with
under relaxed notion of consistency, i.e., WeakPutGet as mentioned in the introduction, in fact is permissive
in users edits. For example, in the above scenario S3, if the user edits only one of the view edge, then the
backward transformation successfully propagates the changes to the source edge, though the updated view graph
on the whole is not perfectly consistent if we define source s and view v to be consistent if and only if get s = v
where get is the forward transformation, because another forward transformation from the updated source would
propagate the new edge label to the other copy edge in the view graph. The perfectly consistent view graph
would have been the one which all the edges originating from a common source edge are updated to the same
value. However, it might be hard for the users to identify all these copies. Therefore, our system accepts updates
in which only one copy is updated in the view. Borrowing the notion of degree of consistency by Stevens [
We use the UnCAL (Unstructured CALculus) query language [
UnCAL Graph Data Model
UnCAL graphs are multi-rooted and edge-labeled with all information stored in edge labels ranging over Label ∪
{ ε} (Label ε), node labels are only used as identifiers. There is no order between outgoing edges of a node.
The notion of graph equivalence is defined by bisimulation; so equivalence between the graphs is efficiently
determined [
Fig. 3 shows examples of our graphs. We represent a graph by a quadruple (V, E, I, O). V is the set of nodes,
E the set of edges ranging over the set Edgeε, where an edge is represented by a triple of source node, label and
destination node. I : Marker → V is a function that identifies the roots (called input nodes) of a graph. Here,
Marker is the set of markers of which element is denoted by &x . We may call a marker in dom(I) (domain of I) an
input marker. A special marker & is called the default marker. O ⊆ V ×Marker assigns nodes with markers called
output markers. If (v, &m) ∈ O, v is called an output node. Intuitively output nodes serve as ”exit points” where
Graphs can be created in the UnCAL query language [
There are three nullary constructors. () constructs a graph without any nodes or edges, so F [[()]] ∈ DB ∅, where F [[e]] denotes the (forward) evaluation of expression e. The constructor } { constructs a graph with a node with default input marker (&) and no edges, so F [[} { ]] ∈ DB . &y constructs a graph similar to } { with additional output marker &y associated with the node, i.e., F [[&y]] ∈ DB { &y} .
The edge constructor { : } takes a label l and a graph g ∈ DB Y , constructs a new root with the default input marker with an edge labeled l from the new root to g.I(&); thus { l : g} ∈ DB Y . The union g1 ∪ g2 of &x1...&xm
g1 &x1′…&x m′′ &z1... &zk &x1′…&x m′′ &z1′…&zk′′
g2 &y1 ... &yn &x1...&xm g1 g2 ε ... ε &y1 ... &yn {} & &y & &y
() ∅ &y1... &ym &x g1 &x.&y1...&x.&ym :=
g &z1 ... &zn andThreetuinrpnustangordaephrenwahmosineginoppuetramtoarrk:=erstaakreesparempeanrdkeerd &bxy a&nxd, athgursa(p&hx g:=∈ gD)B∈Y DwBit&hx.YY w=h e{r&ey 1t,h.e. .d,o&ty m“.” } , Z
Z concatenates markers and forms a monoid with & , i.e., &.&x = &x .& = &x for any marker &x ∈ Marker , and &x .Y = { &x .&y 1, . . . , &x .&y m} for Y = { &y 1, . . . , &y m} . In particular, when Y = { &} , the := operator just assigns a new name to the root of the operand, i.e., (&x := g) ∈ DB {Y&x } for g ∈ DB Y .
The disjoint union g1 ⊕ g2 of two graphs g1 ∈ DB XX 0 and g2 ∈ DB YY0 with X ∩ Y = ∅, the resultant graph inherits all the markers, edges and nodes from the operands, thus g1 ⊕ g2 ∈ DB X ∪Y .
X 0∪Y0
The remaining two constructors connect output and input nodes with matching markers by ε-edges. g1 @ g2 appends g1 ∈ DB XX 0∪Z and g2 ∈ DB X 0∪Z0 by connecting the output and input nodes with a matching subset
Y of markers X 0, and discards the rest of the markers, thus g1 @ g2 ∈ DB X . An idiom &x 0@g2 projects (selects) Y one input marker &x 0 and renames it to default (&), while discarding the rest of the input markers (making them unreachable). The cycle construction cycle(g) for g ∈ DB X X ∪Y with X ∩ Y = ∅ works similarly to @ but in an intra-graph instead of inter-graph manner, by connecting output and input nodes of g with matching markers X , and constructs copies of input nodes of g, each connected with the original input node by an ε-edge. The output markers in Y are left as is.
It is worth noting that any graph in the data model can be expressed by using these UnCAL constructors (up
to bisimilarity), where the notion of bisimilarity is extended to ε-edges [
The semantics of conditionals is standard, but the condition is restricted to label equivalence comparison.
There are two kinds of variables: label variables and graph variables. Label variables, denoted $l , $l1 etc., bind
labels while graph variables denoted $g , $g1 etc., bind graphs. They are introduced by structural recursion
operator rec, whose semantics is explained below by example. The variable binders let and llet having standard
meanings are our extensions used for optimization by rewriting [
We take a look at the following concrete transformation in UnCAL that replaces every label a by d and contracts edges labeled c.
rec(λ($l , $g ). if $l = a then { d : &1} 2 else if $l = c then { ε : &3} 4 else { $l : &5} 6)($db)7 If the graph variable $db is bound to the graph in Fig. 3 (a), the result of the transformation will be the one in Fig. 3 (b). We call the first operand of rec the body expression and the second operand the argument expression. In the above transformation, the body is an if conditional, while the argument is the variable reference $db. We use $db as a special global variable to represent the input of the graph transformation. For the sake of bidirectional evaluation (and also used in our tracing in this paper), we superscribe UnCAL expressions with their code position p ∈ Pos where Pos is the set of position numbers. For instance, in the example above, the numbers 1 and 2 in { d : &1} 2 denote the code positions of the graph constructors & and { d : &} , respectively.
Fig. 6 shows the bulk semantics of rec for the example. It is “bulk” because the body of rec can be evaluated in parallel for each edge and the subgraph reachable from the target node of the edge (which are correspondingly bound to variables $l and $g in the body).
In the bulk semantics, the node identifier carries some information which has the following structure [
Code Pos Marker RecN Pos StrID Marker
RecE Pos StrID Edge, where the base case (SrcID ) represents the node identifier in the input graph, Code p &x denotes the nodes constructed by } { , { : } , &y , ∪ and cycle where &x is the marker of the corresponding input node of the operand(s) of the constructor. Except for ∪, the marker is always default and thus omitted. RecN p v &z denotes the node created by rec at position p for node v of the graph resulting from evaluating the argument expression. For example, in Fig. 6, the node RN 7 1 , originating from node 1, is created by rec at position 7 RN 7 1
& RE 7 (C 2) (1,a,2) RE 7 (C 6) (1,b,3) RE 7 (C 6) (1,b,4)
d b b RE 7 (C 1) (1,a,2) RE 7 (C 5) (1,b,3) RE 7 (C 5) (1,b,4)
RN 7 2
RN 7 3
RN 7 4 RE 7 (C 2) (2,a,5) RE 7 (C 2) (3,a,5)
d d RE 7 (C 1) (2,a,5) RE 7 (C 1) (3,a,5)
RE 7 (C 4) (6,c,3)
ε
RE 7 (C 3) (6,c,3) RN 7 5
RE 7 (C 6) (5,d,6)
d
RE 7 (C 5) (5,d,6) RN 7 6 (RecN is abbreviated to RN in the figure for simplicity, and similarly Code to C and RecE to RE). We have six such nodes, one for each in the input graph. Then we evaluate the body expression for each binding of $l and $g . For the edge (1, a, 2), the result will be ({ (C 2), (C 1)} , { (C 2, d, C 1)} , { & 7→ C 2} , { (C 2, &)} ), with the nodes C 2 and C 1 constructed by { : } and &, respectively. For the shortcut edges, an ε-edge is generated similarly. Then each node v of such results for edge ζ is wrapped with the trace information RE like RE p v ζ for rec at position p. These results are surrounded by round squares drawn with dashed lines in Fig. 6. They are then connected together according to the original shape of the graph as depicted in Fig. 6. For example, the input node RE 7 (C 2) (1, a, 2) is connected with RN 7 1 . After removing the ε-edges and flattening the node IDs, we obtain the result graph in Fig. 3 (b).
Our bidirectional transformation in UnCAL is based on its bidirectional evaluation, whose semantics is given by F [[ ]] and B[[ ]] as follows. F [[e]]ρ = G is the forward semantics applied to UnCAL query e with source variable environment ρ, which includes a global variable binding $db the input graph. B[[e]](ρ, G0) = ρ0 produces the updated source ρ0 given the updated view graph G0 and the original source ρ.
Bidirectional transformations need to satisfy round-trip properties [
F JeKρ = GV BJeK(ρ, GV ) = ρ (GetPut)
BJeK(ρ, G0V ) = ρ0 F JeKρ0 = G0V0 (WPutGet)
BJeK(ρ, G0V0 ) = ρ0
where GetPut says that when the view is not updated after forward transformation, the result of the following
backward transformation agrees with the original source, and W(Weak)PutGet (a.k.a. weak invertibility [
In the backward evaluation of rec, the final ε-elimination to hide them from the user is reversed to restore the shape of Fig. 6, and then the graph is decomposed with the help of the structured IDs, and then the decomposed graph is used for the backward evaluation of each body expression. The backward evaluation produces the updated variable bindings (in this body expression we get the bindings for $l , $g and $db and merge them to get the final binding of $ db). For example, the update of the edge label of (1, b, 3) in the view to x is propagated via the backward evaluation of the body { $l : &} , which produces the binding of $l updated with x and is reflected to the source graph with edge (1, b, 3), replaced by (1, x, 3).
UnQL as a Textual Surface Syntax of Bidirectional Graph Transformation
We use the surface language UnQL [
This section describes the forward semantics of UnCAL augmented with explicit correspondence traces. In the trace, every view edge and node is mapped to a corresponding source edge or node or a part of the transformation. The path taken in the transformation is also recorded in the trace for the view elements.
The trace information is utilized for (1) correspondence analysis, where a selected source element is contrasted with its corresponding view element(s) by highlighting them, and likewise, a selected view element is contrasted with its corresponding parts in source and transformation, and for (2) editability analysis, classifying edges by origins to (2-1) pre-reject the editing of edges that map to the transformation, (2-2) pre-reject the conflicting editing of view edges whose edit would be propagated to the same source edge, (2-3) warn the edit that could violate WPutGet by changing branching behavior of if by highlighting the branch conditions that are affected by the edit.
The augmented forward evaluation F [[ ]] : Expr → Env → Graph × Trace takes an UnCAL expression and an environment as arguments, and produces a target graph and trace. The shaded part represents the augmented part and we apply the same shading in the following. The trace maps an edge ∈ Edge (resp. a node ∈ Node) to a source edge (resp. source node) or a code position, preceded by zero or more code positions that represent the corresponding language constructs involved in the transformation that produced the edge (resp. the node). The preceding parts are used for the warning in (2-3) above. Thus
Trace = Edge ∪ Node → TraceE ∪ TraceV TraceE ::= Pos : TraceE | [Edge | Pos] TraceV ::= Pos : TraceV | [Node | Pos]
The environment Env represents bindings of graph variables and label variables. Each graph variable is mapped to a graph with a trace, while each label variable is mapped to a label with a trace that contains only edge mapping. Thus
Env = Var → (Graph × Trace) ∪ (Label × TraceE).
Given source graph gs, the top level environment ρ0 is initialized as follows.
ρ0 = { $db 7→ (gs, { ζ 7→ [ζ] | ζ ∈ gs.E} ∪ { v 7→ [v] | v ∈ gs.V} )} (InitEnv) As idioms used in the following, we introduce two auxiliary functions of type Trace → Trace: prepp to prepend code position p ∈ Pos to traces, and recep,ζ to “wrap” the nodes in the domain of traces with RecE constructor to adjust to bulk semantics.
prepp t = { x 7→ p:τ | (x 7→ τ ) ∈ t} recep,ζ t = { (f x) 7→ τ | (x 7→ τ ) ∈ t}
{ (RecE p u ζ, l, RecE p v ζ) if x = (u, l, v) ∈ Edge where f x = RecE p x ζ if x ∈ Node
Now we describe the semantics F [[ ]]. The graph component returned by the semantics is the same as that
of [
F [[} { p]]ρ = (G} { p, { G.I(&) 7→ [p]} ) F [[e1 ∪p e2]]ρ = (G(g1 ∪p g2), (t1 ∪ t2 ∪ { v 7→ [p] | (&x 7→ v) ∈ G.I} ))
where ((g1, t1), (g2, t2)) = (F [[e1]]ρ, F [[e2]]ρ) F [[{ eL : e} p]]ρ = (G{ l : g} p, { (G.I(&), l, g.I(&)) 7→ τ, G.I(&) 7→ [p]} ∪ t) where ((l, τ), (g, t)) = (FL[[eL]]ρ, F [[e]]ρ) (T-emp) (Uni) (Edg) (Lcnst) (Lvar) (Llet) (Let) (Var) (If) For the constructor } { , the trace maps the only node (G.I(&)) created, to the code position p of the constructor (T-emp). The binary graph constructors ∪, ⊕ and @ returns the traces of both subexpressions, in addition to the trace created by themselves. The graph union’s trace maps newly created input nodes to the code position (Uni). For the edge-constructor (Edg), the correspondence between the created edge and its trace created by the label expression eL is established, while the newly created node is mapped to the code position of the constructor.
For label expression evaluation FL[[ ]] : Expr L → Env → Label × TraceE, the trace that associates the label to the corresponding edge or code position is accompanied with the resultant label value.
FL[[ap]]ρ = (a, [p]) FL[[$l p]]ρ = (l, p : τ)
where (l, τ) = ρ($l ) Label literal expressions (Lcnst) record their code positions, while label variable reference expressions (Lvar) add their code positions to the traces that are registered in the environment.
The label variable binding expression (Llet) registers the trace to the environment and passes it to the forward evaluation of the body expression e. Graph variable binding expression (Let) is treated similarly, except it handles graphs and their traces. Graph variable reference (Var) retrieves traces from the environment and add the code position of the variable reference to it.
F [[lletp $l = eL in e]]ρ = F [[e]]ρ∪{ $l7→(l,p : τ)}
where (l, τ) = FL[[eL]]ρ F [[letp $g = e1 in e2]]ρ = F [[e2]]ρ∪{ $g7→(g,prepp t)}
where (g, t) = F [[e1]]ρ F [[$gp]]ρ = (g, prepp t)
where (g, t) = ρ($g) [ [ if p(eL = e0L) then etru e] ] F else efalse ρ = (g, prepp t) where ((l, ), (l0, )) = (FL[[eL]], FL[[e0L]])
b = (l = l0) (g, t) = F [[eb]]ρ
Structural recursion rec (Rec) introduces a new environment for the label ($l ) and graph ($g) variable that includes traces inherited from the traces generated by the argument expression ea, augmented with the code position p of rec. gv denotes the subgraph of graph g that is reachable from node v. tv denotes a trace that are restricted to the subgraph reachable from node v. The function M : Edge → (Graph × Trace) takes an edge and returns the pair of the graph created by the body expression eb for the edge, and the trace associated with the graph. tζ is the trace generated by adjusting the trace returned by M with the node structure introduced by rec. composerpec is the bulk semantics explained in Sect. 3.2 using Fig. 6, for the input graph g and the input/output marker Z of eb, where VRecN denotes the nodes with structured ID RecN. where (g, t) = F [[ea]]ρ
M = { ζ 7→ F [[eb]]ρ0 | ζ ∈ g.E, ζ 6= ε, (u, l, v) = ζ,
ρ0 = ρ ∪ { $l 7→ (l, p : t(ζ)), $g 7→ (gv, prepp tv)} } g0 = (VRecN ∪ . . . , , , ) = composerpec(M, g, Z) t0V = { v 7→ [p] | v ∈ VRecN} tζ = recep,ζ (prepp π2(M (ζ))) (Rec)
The above semantics collects all the necessary trace information whose utilization is described in the next section. Even though the tracing mechanisms are defined for UnCAL, they also work straightforwardly for UnQL, based on the observation that when an UnQL query is translated into UnCAL, all edge constructors and graph variables in the UnQL query creating edges in the view graph are preserved in the UnCAL query. One limitation is: in our system, the bidirectional interpreter of UnCAL optionally rewrites expressions for efficiency. However, due to reorganization of expressions during the rewriting, we currently support neither tracing UnCAL nor tracing UnQL if the rewriting is activated. 5
This section elaborates utilization of the traces defined in Sect. 4 for the correspondence and editability analysis motivated in Sect. 2. Soundness of this analysis is discussed at the end of this section.
Given transformation e, environment ρ0 (defined by InitEnv), and the corresponding trace t for (g, t) = F [[e]]ρ0 through semantics given in Sect. 4, the trace (represented as a list) for view edge ζ has the following form t(ζ) = p1 : p2 : . . . : pn : [x] (n ≥ 0) where x is the origin, and x = ζ0 ∈ Edge if ζ is a copy of ζ0 in the source graph, or x = p ∈ Pos if the label of ζ is a copy of the label constant at position p in the transformation. p1, p2, . . . , pn represent code positions of variable definitions/references and conditionals that conveyed ζ.
For view graph g and trace t, define the function origin : Edge → Edge ∪ Pos and its inverse: origin ζ = last(t(ζ)) origin−1 x = { ζ | ζ ∈ g.E, origin ζ = x} Correspondence is then the relation between the domain and image of trace t, and various individual correspondence can be derived, the most generic one being R : Edge ∪ Node ∪ Pos × Edge ∪ Node = { (x0, x) | (x 7→ τ ) ∈ t, x0 ∈ τ } , meaning that x0 and x is related if (x0, x) ∈ R. Source-target correspondence being { (x0, x) | (x 7→ τ ) ∈ t, x0 = last τ, x0 ∈ (Node ∪ Edge)} . Using origin and origin−1, corresponding source, transformation and view elements can be identified in both directions. When a view element such as the edge ζ = (4, German, 2) in Fig. 2 is given, we can find the corresponding source edge origin(ζ) = (1, German, 0), which will be updated if we change ζ. In contrast, given the view edge (14, language, 4), the code position of the label constant lang in { lang : $e} of the select part in Listing 1 is obtained. Given the view edge ζ = (3, German, 1), the code positions of the graph variables $lang of the select part and $db in Listing 1 are obtained, utilizing code positions in p1, . . . , pn, because t ζ includes such positions. These graph variables copy the source edge origin(ζ) = (1, German, 0) to the view graph.
In the following, although the trace t can be used for both nodes and edges, we only focus on edges instead of nodes, and edge renamings as the update operations. However, the node trace can be used to support insertion operation by highlighting the node in the source on which a graph corresponding to the graph to be inserted in the view will be attached. For the deletion operation, we can relatively easily extend the data structure of the trace defined in the previous section to be tree-structured, being able to trace multiple sources, and extend rule (Rec) to associate each edge created by the body expression with the trace of the edge bound to the label variable.
For editability analysis, the following notion of equivalence is used. Given the partial function originE : Edge → Edge defined by originE ζ = origin(ζ) if origin(ζ) ∈ Edge, or undefined otherwise. Then, view edges ζ1 and ζ2 are equivalent, denoted by ζ1 ∼ ζ2, if and only if originE ζ1 = originE ζ2. All edges for which originE is undefined are considered equivalent. The equivalence class for edge ζ is denoted by [ζ]∼. We define our updates as upd : Upd where Upd = Edge → Label , an expression and its environment at position p as expr : Pos → Expr × Env , and update propagation along trace t as prop : Env → Upd → Env . Then, our editability analysis is defined as follows.
Definition 1 (Editability checking). Given (g, t) = F [[e]]ρ0 and update upd on g, editability checking succeeds if all the following three conditions are satisfied.
1. For all updated edges ζ, other view edges in [ζ]∼ are unchanged or consistently updated, i.e., ∀ζ ∈ dom(upd).∀ζ0 ∈ [ζ]∼.ζ0 ∈/ dom(upd) ∨ upd(ζ) = upd(ζ0). 2. For every if eB . . . expression in the backward evaluation path, applying the edit to the binding does not change the condition, i.e., ∀p ∈ {∪ [p | p ∈ t(ζ), p ∈ Pos] | ζ ∈ dom(upd)} , expr(p) = (if eB . . . , ρ), F [[eB]]ρ = F [[eB]]prop(ρ,upd). For the case of label variables, this interference can be checked by $l ∈ F V(eB), ρ0($l ) = ( , τ ), last(τ ) = ζ0 for ζ0 = originE ζ. Weakened version for graph variables is: ∀$g ∈ F V(eB).(g0, t0) = ρ0($g ), ∀ζ00 ∈ g0.E. last(t0((ζ00)) 6= originE(ζ) for all ζ ∈ dom(upd).
3. No edited edge trace to code position, i.e., ∀ζ ∈ dom(upd). origin(ζ) ∈/ Pos.
Further, we recap all the three run-time errors to reject updates [
Lemma 1. Condition 1 in Def. 1 is false iff error (1) occurs.
Lemma 2. Error (2) implies condition 2 in Def. 1 is false.
Lemma 3. Condition 3 in Def. 1 is false iff error (3) occurs.
Theorem 1 (Soundness of editability analysis). Given forward transformation (g, t) = F [[e]]ρ0 and update upd on g to g0, success of editability checking in Def. 1 implies B[[e]](ρ0, g0) defined and results in prop(ρ0, upd). Thus edit on the view edge ζ with ζ0 = originE ζ defined is propagable to ζ0 in the source graph by B[[]], when the checking in Def. 1 succeeds. An edit on the view edge ζ with origin(ζ) = p ∈ Pos is not propagable to the source by Lemma 3. Editing label constant at p in the transformation would achieve the edits, with possible side effects through other copies of the label constant.
Consider the example in Listing 1 with the source graph of Fig. 1 and view graph of Fig. 2. We get four equivalence classes, one each for the source edges (1, German, 0), (3, Europe, 2), (5, Austrian, 4) and (11, German, 10), as well as the class that violate condition 3. For view edge ζ = (3, German, 1), we have (4, German, 2) ∈ [ζ]∼ via originE ζ = (1, German, 0), so these equivalent edges can be selected simultaneously, inconsistent edits on which can be prevented (Lem. 1). Direct edits of the view edge ζ = (0, result, 14) are suppressed since origin ζ ∈ Pos (Lem. 3). On condition 2, when the view edge ζ = (7, Europe, 5) is given, all the code positions in t ζ00 for ζ00 ∈ originE−1(originE ζ) are checked if the positions represent conditionals that refer variables, change of those binding would change the conditions and would be rejected by B. We obtain the position for variable reference $l in the condition ($l = Europe) for warning.
Cases in which completeness is lost: Note that system may choose the weakened version of condition 2, and just issue warning (i.e., whenever the edge being updated has common source edge with any variable reference occurring free in any of the conditional expressions along the execution path), because when condition includes not only the simple label comparison expressions but also graph emptiness checking by isEmpty, the cost of fully checking the change of the condition may amount to re-executing the most part of the forward transformation. If this warning-only strategy is chosen, backward transformation may succeed despite this warning, because the warning does not necessarily mean condition value changes. Therefore, the checking is not complete (may warn some safe updates). We argue that this “false alarm” is not so problematic in practice, with the following reasons. The argument of isEmpty usually includes select to test an existence of certain graph pattern. So we further analyze conditions in select down to simple label equivalence check. If the argument is a bare graph variable reference, then we analyze its binder. If the graph variable is $db (the entire input graph), then any changes cause false alarms. This predicate may be used only for debugging purpose to exclude empty source graphs, but otherwise we don’t think we frequently encounter this situation.
Now we provide a proof sketch. First, we prove Lemma 3. We do this by parallel case analysis on augmented
forward semantics and backward semantics [
Base case No edit is possible for } { , () and &y that produce no edge. For a transformation { a : e0} p and the view graph as v a /G, since a is a constant, augmented forward semantics generates code position p as trace, which violates condition 3 when a is being updated. Backward semantics rejects with error (3). Inductive case
Transformation { $l : e0} p and the view graph as v l G/: Update on l to l0 will be handled by the backward semantics of $l , which updates its reference. Suppose it is introduced by an expression llet $l = a in { $l : e0} . . .. Then binding $l 7→ l0 is generated and it is passed to the backward evaluation of label expression a, which is constant. So no value other than a is allowed. So backward transformation fails with error (3). The trace generates code position of label constant a, which also signals violation of condition 3. If $l is bound by rec(λ($l , ).{ $l : e1} )(e2), then the update is also translated to the argument expression e2, so if corresponding part in e2 originates from a label constant, then the condition is violated and backward transformation fails similarly. e1 ∪ e2, e1 ⊕ e2, e1 @ e2 : We reduce the backward transformation to that of subexpressions, assuming decomposition operation for each operator. So assuming Lemma 3 for these subexpressions, Lemma 3 holds for entire expression. Similar argument applies for cycle(e), & := e and if then e1 else e2. rec(e1)(e2): What is produced as a trace depends on e1 and e2. Assuming the decomposition of target graph, the backward evaluation is reduced to those of e1 and e2. The only interesting case is a graph variable reference as (sub) expression. The update on the target graph that was produced by the variable reference is reduced to updated graph variable bindings, and the bound graph is aggregated for each edge in the input graph that was produced by e2, and passed to the backward evaluation of e2. The trace, on the other hand, is produced by e2 and combined with the trace by e1. If e1 is a graph variable reference, then the (sub) trace induced from the trace from e2 is used, so the edge that trace back to constant is inherited in the trace of the result of rec, so attempt to update an edge that traces back to the constant produced by e2 and carried by the graph variable reference is signaled with condition 3. So, assuming Lemma 3 on e2 by induction hypothesis, Lemma 3 holds for the entire expression.
Thus conclude the proof for Lemma 3.
Next we prove Lemma 1. When violation of 1 is signaled, multiple edge labels with the same equivalence class is updated to different values. The proof can be conducted similarly to the case for Lemma 3, except that we focus on multiple edge labels generated by different subexpressions of the transformation. { $l : $g } : Suppose bindings $l 7→ a and $g 7→ { b : G} are generated by updates on the target graph. Further, suppose these bindings are generated by rec(λ($l 0, ). rec(λ($l , $g ).{ $l : $g } )({ $l 0 : { $l 0 : } { ))($db) as the inner body expression of rec and $db is bound to graph { x : } { . Then, backward evaluation of the argument expression in the inner rec, i.e., { $l 0 : { $l 0 : } { will produce the bindings $l 0 7→ a and $l 0 7→ b for the first label expression $l 0 and the label construction expression { $l 0 : } { , respectively, and merge these bindings by ] operator relative to original binding $l 0 7→ x. Then backward transformation fails because of the conflicting bindings. In this case, the augmented forward semantics also allocate the top and the following edge the same origin edge, so the update signals violation of condition 1. So violation of condition 1 coincides failed backward transformation. Similar situation can be observed for graph constructors ∪, ⊕ and @ that unifies the graphs, when conflicting updates are attempted to edges originated from identical edges. The merge phase for the subexpressions in the backward transformation causes the failure. Note that the duplicate is propagated through variable bindings, so conflicting updates can be detected within the target graph created by a single graph variable reference, like let $g 0 = rec(λ($l 0, ). rec(λ($l , $g ).{ $l : $g } )({ $l 0 : { $l 0 : } { ))($db) in $g 0. The failure takes place in the let expression in this case. We omit the detailed case analysis here.
For the Lemma 2, its proof is straightforward by the warning algorithm in the long version. Note that if we exclude the update on target that causes violation of condition 2, we have soundness and completeness. In general, we only have soundness. This concludes the proof sketch. 6
Our novelty is to analyze editability using traces in compositional bidirectional graph transformations.
Tracing mechanism. Traceability is studied enthusiastically in model-driven engineering (MDE) [
Our own previous work [
Triple Graph Grammars (TGG) [
Xiong et al. [32]’s traces are editing operations (including deletion, insertion and replacement) embedded in model elements. They are translated along with transformation (in ATL bytecode). They check control flow changes in these embedded operations after finishing backward transformations and reject updates when these changes are detected. ATL level trace could have been computed using our approach for correspondence analysis.
Target Element Classification and Editability Analysis. Model element classification has been studied
in the context of Precedence Triple Graph Grammars [
Another well-studied bidirectional transformation framework called semantic bidirectionalization [
Hu et al. [
In this paper, we proposed, within a compositional bidirectional graph transformation framework based on structural recursion, a technique for analyzing the correspondence between source, transformation and target as well as to classifying edges according to their editability. We achieve this by augmenting the forward semantics with explicit correspondence traces. The incorporation of this technique into the GUI enables the user to clearly visualize the correspondence. Moreover, prohibited edits such as changing a constant edge and updating a group of edges inconsistently are disabled. This allows the user to predict violated updates and thus do not attempt them at the first place. In this paper we only focused on edge-reaming as edit operation but the proposed framework can also support edge-deletion by slight extension, while insertion handling can be supported by the present node tracing.
As a future work, we would like to utilize the proposed framework to optimize the performance of edge deletion and subgraph insertion using the backward transformation semantics for in-place update semantics, because we currently handle these update operations by different algorithms. In particular, insertions use a general inversion strategy which is costly. We already have limited support in this direction, however we are still to establish formal bidirectional properties for complex expressions. Leveraging the traces in the forward semantics indicating which edge is involved in the branching behavior, we could safely determine the part that accepts the insertion or deletion of that part reusing the in-place update semantics, thus achieving “cheap backward transformation”. The proposed mechanism can be used for any other trace-based approaches, unidirectional or bidirectional, as we discussed in Section 6, and we would like to pursue this direction as well.
Acknowledgments The authors would like to thank Zhenjiang Hu, Hiroyuki Kato and other IPL members, and AtlanMod team for their valuable comments. We also thank the reviewers for their constructive feedbacks. The project was supported by the International Internship Program of the National Institute of Informatics.
ACM Trans. Database