11institutetext: Hasso-Plattner Institute at the University of Potsdam
Prof.-Dr.-Helmert-Str. 2-3, D-14482 Potsdam, Germany
11email<EMAIL_ADDRESS>
# Towards Development with Multi-Version Models: Detecting Merge Conflicts and
Checking Well-Formedness††thanks: This work was developed mainly in the course
of the project modular and incremental Global Model Management (project number
336677879) funded by the DFG.
This preprint has not undergone peer review (when applicable) or any post-
submission improvements or corrections. The Version of Record of this
contribution is published in Graph Transformation, 15th International
Conference, Proceedings, and is available online at
https://doi.org/10.1007/978-3-031-09843-7.

Matthias Barkowsky Holger Giese

###### Abstract

Developing complex software requires that multiple views and versions of the
software can be developed in parallel and merged as supported by views and
managed by version control systems. In this context, this paper considers
monitoring merging and related consistency problems permanently at the level
of models and abstract syntax to permit early and frequent conflict detection
while developing in parallel. The presented approach introduces multi-version
models based on typed graphs that permit to store changes and multiple
versions in one graph in a compact form and allow (1) to study well-formedness
for all versions without the need to extract each version individually, (2) to
report all possible merge conflicts without the need to merge all pairs of
versions, and (3) to report all violations of well-formedness conditions that
will result for merges of any two versions independent of any merge decisions
without the need to merge all pairs of versions. The paper defines the related
concepts and algorithms operating on multi-version models, proves their
correctness w.r.t. the usually employed three-way-merge, and reports on
preliminary experiments concerning the scalability.

##  1 Introduction

Developing complex software nowadays requires that multiple views and versions
of the software can be developed in parallel and merged as supported by views
and managed by version control systems [10]. For complex software, living with
inconsistencies at least temporarily is inevitable, as enforcing consistency
may lead to loss of important information [9] and is hence neither always
possible nor desirable. However, working with multiple versions in parallel
and changing each version on its own for longer periods of time can introduce
substantial conflicts that are difficult and expensive to resolve. Therefore,
it is necessary to manage consistency when combining views and versions using
merge approaches [10, 16].

In this context, this paper considers monitoring merging and related
consistency problems permanently at the level of models and abstract syntax.
This aims to permit early and frequent conflict detection while developing in
parallel, as suggested in approaches to detect conflicts early and to enable
collaboration to manage conflicts and their risks [5].

The presented approach therefore introduces multi-version models based on
typed graphs, which permit to store changes and multiple versions in one graph
in a compact form and allow to study the different versions and their merge
combinations. The following capabilities are considered: (1) Study well-
formedness for all versions at once without the need to extract and explicitly
consider each version individually. (2) Report all possible merge conflicts
that may result for merges of any two versions without the need to extract and
explicitly merge all pairs of versions. (3) Report all violations of well-
formedness conditions that will result for merges of any two versions
independent of any merge decisions without the need to extract and explicitly
merge all pairs of versions.

The approach thus promises to support early conflict detection and
collaboration for managing conflicts and their risks, while not having to
decide how to later merge conflicting versions. The technique also aims for a
better scalability in case there are many versions that are considered in
parallel.

Furthermore, the developed multi-version models permit to study the phenomena
of versions, merging, and well-formedness conditions in the unifying framework
of typed graphs. This enables us to (a) formulate algorithms that can obtain
several analysis results without the need to consider a specific version,
merge of a pair of versions, or strategy for conflict resolution and (b) prove
that the algorithms compute the same results as if we would explicitly
consider all specific versions, merges of pairs of versions, or strategies for
conflict resolution.

The paper defines the related concepts and algorithms operating on multi-
version models, proves their correctness w.r.t. the usually employed three-
way-merge, and reports on first experiments concerning the scalability. In
Section 2, we summarize the preliminaries of the presented approach, including
basic definitions for typed graphs, well-formedness conditions, and graph
modifications. Then, as a baseline, single-version models in the form of typed
graphs with well-formedness conditions are defined in Section 3, before multi-
version models are introduced in Section 4. Determining all merge conflicts
and checking well-formedness for all merge results based on multi-version
models is then considered in Section 5. Results of first experiments for our
prototypical implementation of the algorithms are presented in Section 6.
Finally, the conclusions of the paper and an outlook of planned future work
are presented in Section 7. For the submitted review version, more detailed
proofs and the conditions used in the evaluation are in addition presented in
an appendix.

##  2 Preliminaries

We briefly reiterate the basic concepts of graphs, graph modifications, and
well-formedness conditions used in the remainder of the paper.

A graph $G=(V^{G},E^{G},s^{G},t^{G})$ consists of a set of nodes $V^{G}$, a
set of edges $E^{G}$ and two functions $s^{G}:E^{G}\rightarrow V^{G}$ and
$t^{G}:E^{G}\rightarrow V^{G}$ assigning each edge its source and target,
respectively. We assume that graph elements have identities and source and
target of an edge are invariant if an edge is part of multiple graphs, that
is, for two graphs $G$ and $H$ and an edge $e\in E^{G}\cap E^{H}$, it holds
that $s^{G}(e)=s^{H}(e)$ and $t^{G}(e)=t^{H}(e)$. This also implies that, in
the context of this paper, $(V^{G}=V^{H}\wedge E^{G}=E^{H})\rightarrow(G=H)$.

A graph morphism $m:G\rightarrow H$ is given by a pair of functions
$m^{V}:V^{G}\rightarrow V^{H}$ and $m^{E}:E^{G}\rightarrow E^{H}$ that map
elements from $G$ to elements from $H$ such that $s^{H}\circ m^{E}=m^{E}\circ
s^{G}$ and $t^{H}\circ m^{E}=m^{E}\circ t^{G}$ [8].

A graph $G$ can be typed over a type graph $TG$ via a typing morphism
$\mathit{type}:G\rightarrow TG$, forming the typed graph
$G^{T}=(G,\mathit{type}^{G})$. A typed graph morphism between two typed graphs
$G^{T}=(G,\mathit{type}^{G})$ and $H^{T}=(H,\mathit{type}^{H})$ with the same
type graph then denotes a graph morphism $m^{T}:G\rightarrow H$ such that
$\mathit{type}^{G}=\mathit{type}^{H}\circ m^{T}$. A (typed) graph morphism is
a monomorphism iff its functions are both surjective and injective.

Figure 1 shows an example typed graph $M_{1}$ and associated type graph $TM$
from the software development domain. $M_{1}$ represents an abstract syntax
graph for a program written in an object-oriented language that contains four
classes represented by nodes, with edges representing superclass
relationships.

Figure 1: Example graph, type graph, and violation pattern

The structure of a typed graph $G$ can be restricted by a well-formedness
condition $\phi$, which in the context of this paper is characterized by a
typed graph $Q$ typed over the same type graph. $G$ then satisfies the
condition $\phi$, denoted $G\models\phi$, iff there exists no monomorphism
$m:Q\rightarrow G$. We also call such monomorphisms _matches_ and $Q$ the
_violation pattern_ of $\phi$.

Figure 1 shows a violation pattern $Q$ for an example well-formedness
constraint that forbids a class having two outgoing superclass relationships.

A graph modification as defined by Taentzer et al. [20] formalizes the
difference between two graphs $G$ and $H$ and is characterized by an
intermediate graph $K$ and a span of monomorphisms $(G\leftarrow K\rightarrow
H)$. In this paper, we assume that the two morphisms are always partial
identities. The graph $K$ then characterizes the subgraph that is preserved
through the modification, whereas all elements in $G$ that are not in $K$ are
deleted and elements in $H$ but not in $K$ are created.

Figure 2 shows an example graph modification from the graph $M_{1}$ from
Figure 1 to a new graph $M_{2}$, where a superclass edge from class $c_{1}$ to
class $c_{3}$ is created and the class $c_{4}$ is deleted. The morphisms are
implied by node labels.

Figure 2: Example graph modification

Graphs and graph modifications correspond to versions and differences in
conventional, line-based version control systems like Git [2], where versions
of a development artifact and intermediate differences form a directed acyclic
graph.

##  3 Single-Version Models

In this paper, we consider models in the form of typed graphs that are
required to adhere to a set of well-formedness conditions. Effectively, the
combination of type graph and well-formedness conditions then acts as a
metamodel with potential further constraints. Note that attributes, as usually
employed in real-world models, can in this context be modeled as dedicated
nodes [13].

For $\Phi$ the set of well-formedness conditions, a model $M_{i}$ is _well-
formed_ iff $\forall\phi\in\Phi:M_{i}\models\phi.$ We assume
$\mathop{pcheck}(M_{i},\phi)$ to report all violations to property $\phi$ with
violation pattern $Q$ for model $M_{i}$ in the form of matches for $Q$,
essentially realizing $\models$ as $\mathop{pcheck}(M_{i},\phi)=\emptyset\iff
M_{i}\models\phi$. If violations exist, the model $M_{i}$ is also called _ill-
formed_.

For the notion of models as typed graphs, model modifications correspond to
graph modifications as presented in Section 2. We say a model modification
$(M_{i}\leftarrow K\rightarrow M_{j})$ with identity morphisms is _maximally
preserving_ iff it does not delete and recreate identical elements. Formally,
$K=(V^{M_{i}}\cap V^{M_{j}},E^{M_{i}}\cap E^{M_{j}},s^{K},t^{K})$, where
$s^{K}$ and $t^{K}$ are uniquely defined assuming invariant edge sources and
targets. Consequently, for two models $M_{i}$ and $M_{j}$, the maximally
preserving model modification $(M_{i}\leftarrow K\rightarrow M_{j})$ is
uniquely defined.

For a set of model modifications $\Delta^{M_{\\{1,\dots,n\\}}}$ between models
$M_{\\{1,\dots,n\\}}=\\{M_{1},\dots,M_{n}\\}$, with $\forall(G\leftarrow
K\rightarrow H)\in\Delta^{M_{\\{1,\dots,n\\}}}:G\in M_{\\{1,\dots,n\\}}\wedge
H\in M_{\\{1,\dots,n\\}}$, we can define the set of predecessors
$\mathop{pre}(i)\subset M_{\\{1,\dots,n\\}}$ of a version $M_{i}$ as the set
of versions $M_{j}$ such that there exists a sequence of model modifications
$(M_{x_{1}}\leftarrow K_{x_{1}}\rightarrow M_{x_{2}})$, $(M_{x_{2}}\leftarrow
K_{x_{2}}\rightarrow M_{x_{3}})$, …, $(M_{x_{n-1}}\leftarrow
K_{x_{n-1}}\rightarrow M_{x_{n}})$ where $x_{1}=j$, $x_{n}=i$, and
$(M_{x_{k}}\leftarrow K_{x_{k}}\rightarrow
M_{x_{k+1}})\in\Delta^{M_{\\{1,\dots,n\\}}}$ for $1\leq k<n$.

$\Delta^{M_{\\{1,\dots,n\\}}}$ describes a _correct model versioning_ if all
morphisms in the individual model modifications are partial identities, all
model modifications are maximally preserving, the $\mathop{pre}$ relation is
acyclic and there exists a model $M_{\alpha}$ such that
$M_{\alpha}\in\mathop{pre}(i)$ for all models $M_{i}\neq M_{\alpha}$.
Effectively, a correct model versioning describes a directed acyclic graph of
model versions $M_{\\{1,\dots,n\\}}$ that are derived from an original model
$M_{\alpha}$ via the model modifications in $\Delta^{M_{\\{1,\dots,n\\}}}$,
and therefore closely corresponds to the versioning of some development
artifact in a conventional version control system.

Taentzer et al. [20] define a merge operation for model modifications
$m_{1}=(M_{c}\leftarrow K_{i}\rightarrow M_{i})$ and $m_{2}=(M_{c}\leftarrow
K_{j}\rightarrow M_{j})$ with common source $M_{c}$, which unifies $m_{1}$ and
$m_{2}$ into a merged model modification
$m_{m}=\mathop{merge}(m_{1},m_{2})=(M_{c}\leftarrow K_{m}\rightarrow M_{m})$.
We denote the merged model by $M_{m}=\mathop{merge_{G}}(m_{1},m_{2})$. This
merge operation is similar to a three-way-merge in conventional version
control systems[16], since $m_{m}$ in the default case (i) preserves an
element $x\in M_{c}$ iff it is preserved by both $m_{1}$ and $m_{2}$ (ii)
deletes an element $x\in M_{c}$ iff it is deleted by $m_{1}$ or $m_{2}$ (iii)
creates an element $x\in M_{m}$ iff it is created by $m_{1}$ or $m_{2}$.

However, according to [20], model modifications can be in conflict in two
cases: (i) insert-delete conflict and (ii) delete-delete conflict. Taentzer et
al. state that only (i), where one modification creates an edge connected to a
node deleted by the other modification, is an actual conflict, which has to be
resolved to create a correct merge result. In this case, the merge result may
deviate from the default case. Such conflicts will be reported by
$\mathop{mcheck}((M_{c}\leftarrow K_{i}\rightarrow M_{i}),(M_{c}\leftarrow
K_{j}\rightarrow M_{j}))$ in the form $(e,v)$, where $e$ is an edge created by
one of the modifications and $v$ is a node deleted by the other modification.

For a correct model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$, we say that two
sequences of model modifications $M_{c}\Rightarrow^{*}M_{i}$ and
$M_{c}\Rightarrow^{*}M_{j}$ are in conflict iff their corresponding maximally
preserving model modifications $(M_{c}\leftarrow K_{c,i}\rightarrow M_{i})$
and $(M_{c}\leftarrow K_{c,j}\rightarrow M_{j})$ are in conflict. In this
case, we also say that $M_{i}$ and $M_{j}$ are in conflict for the common
predecessor $M_{c}$.

Insert-delete conflicts can be resolved by equipping the $\mathop{merge}$
operation with a manual or automatic strategy for conflict resolution. We
consider such a strategy valid if it decides for each conflict whether to
either revert the edge creation or the node deletion and always produces a
proper merged graph. The approach in [20] effectively proposes an automatic
strategy that favors insertion over deletion in order to preserve as many
model elements as possible. Therefore, it reverts any deletions of nodes that
would lead to insert-delete conflicts.

In contrast, a strategy for conflict resolution may favor deletion over
insertion by reverting any creations of edges that would lead to insert-delete
conflicts. Specifically, for model modifications $m_{1}=(M_{c}\leftarrow
K_{i}\rightarrow M_{i})$ and $m_{2}=(M_{c}\leftarrow K_{j}\rightarrow M_{j})$,
the model modification $m_{min}=\mathop{merge^{min}}(m_{1},m_{2})$, with
$\mathop{merge^{min}}$ a merge operation equipped with this strategy, only
creates an edge created by $m_{1}$ or $m_{2}$ if neither its source nor target
is deleted by the other modification.

If all well-formedness conditions are specified by simple violation patterns,
$m_{min}$ also yields a model where all well-formedness violations are also
present in the merge result for any other conflict resolution strategy:

###### Theorem 3.1

For two model modifications $m_{1}=(M_{c}\leftarrow K_{i}\rightarrow M_{i})$
and $m_{2}=(M_{c}\leftarrow K_{j}\rightarrow M_{j})$ and a well-formedness
constraint $\phi$ with violation pattern $Q$, it holds that

$\mathop{pcheck}(\mathop{merge_{G}^{min}}(m_{1},m_{2}),\phi)=\bigcap_{\mathit{str}\in
S}\mathop{pcheck}(\mathop{merge_{G}^{str}}(m_{1},m_{2}),\phi),$

with $S$ the set of all valid conflict resolution strategies.

###### Proof

(Sketch) Follows directly from the fact that
$\mathop{merge}_{G}^{min}(m_{1},m_{2})$ is the smallest common subgraph of all
graphs produced by the operation $\mathop{merge}$ for any valid conflict
resolution strategy. ∎

If there are no conflicts in the merged model operations, the $\mathop{merge}$
operation produces the same result regardless of the chosen strategy for
conflict resolution.

For a correct model versioning, two model versions $M_{i}$ and $M_{j}$, and
the set of versions $P=\mathop{pre}(i)\cap\mathop{pre}(j)$, we define the
function

$\mathop{pre^{C}}(i,j)=\begin{cases}\emptyset&M_{i}\in\mathop{pre}(j)\vee
M_{j}\in\mathop{pre}(i)\\\ \\{M_{c}\in P\,|\,\forall M_{x}\in
P:M_{c}\notin\mathop{pre}(x)\\}&\textrm{otherwise}\end{cases},$

which returns the set of latest common predecessors of $M_{i}$ and $M_{j}$.
Note that our definition of $\mathit{pre}^{C}$ corresponds to the definition
of a best common ancestor in conventional version control systems such as Git
[2], which is used to compute the base for three-way merges in these systems.

Figure 3 shows an exemplary model versioning based on the graph $M_{1}$ from
Figure 1. The initial graph $M_{\alpha}=M_{1}$ contains four classes. The
modification $m_{1}$ (not to be confused with a morphism) to $M_{2}$ creates a
superclass edge from $c_{1}$ to $c_{3}$ and deletes the node $c_{4}$. The
modification $m_{2}$ to graph $M_{3}$ creates superclass edges from $c_{1}$ to
$c_{2}$ and from $c_{4}$ to $c_{2}$. There is an insert-delete conflict
between the two modifications, since the modification to $M_{2}$ deletes a
node that is needed as the source of an edge created by the modification to
$M_{3}$. Furthermore, the result of the merge of the two modifications would
violate the well-formedness constraint with the violation pattern $Q$ from
Figure 1, since without additional modifications, the node $c_{1}$ would have
two outgoing superclass edges.

Figure 3: Example model versioning

##  4 Multi-Version Models as Typed Graphs

A correct model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$ with model versions
$M_{\\{1,\dots,n\\}}$ conforming to a type graph $TM$ can be represented by a
multi-version model in the form of a single graph that is typed over an
adapted type graph.

The adapted type graph $TM_{mv}$ contains a node for each node and edge in
$TM$. It also contains edges connecting each node in $TM_{mv}$ that represents
an edge in $TM$ to the nodes representing the edge’s source and target in
$TM$. This yields a bijective function $\mathit{corr}_{mv}:V^{TM}\cup
E^{TM}\rightarrow V^{TM_{mv}}$, which maps elements from $TM$ to the
corresponding node in $TM_{mv}$, and two bijective functions
$corr^{s}_{mv},corr^{t}_{mv}:E^{TM}\rightarrow E^{TM_{mv}}$ mapping edges from
$TM$ to the edges in $TM_{mv}$ encoding the source and target relation in
$TM$. In addition, $TM_{mv}$ contains a node $\mathit{version}$, an edge $suc$
with source and target $\mathit{version}$, and two edges $cv_{v}$ and $dv_{v}$
from each other node $v\in V^{TM_{mv}}$ to the $version$ node.

A multi-version model $\mathit{MVM}$ for $\Delta^{M_{\\{1,\dots,n\\}}}$ is
then constructed by an operation $\mathop{comb}$ as follows: A subgraph
$P_{mv}^{M}$ encodes structural information about all model versions and is
constructed by translating $P^{M}=\bigcup_{M_{i}\in M_{\\{1,\dots,n\\}}}M_{i}$
to conform to $TM_{mv}$ using an operation $\mathop{trans_{mv}}$. Since source
and target functions are invariant in a correct model versioning, $P^{M}$ is
well-defined.

For each $v\in v^{P^{M}}$, $\mathop{trans_{mv}}$ creates a node of type
$\mathit{corr}_{mv}(v)$ in $V^{P_{mv}^{M}}$. For each $e\in E^{P^{M}}$, a node
of type $\mathit{corr}_{mv}(e)$ is created. This yields a bijection
$\mathit{origin}:P_{mv}^{M}\rightarrow P^{M}$ mapping translated elements to
their original representation.

In addition, for each edge $e\in E^{P^{M}}$, an edge of type
$corr^{s}_{mv}(e)$ with source $\mathit{origin}^{-1}(e)$ and target
$\mathit{origin}^{-1}(s^{P^{M}}(e))$ and an edge of type $corr^{t}_{mv}(e)$
with source $\mathit{origin}^{-1}(e)$ and target
$\mathit{origin}^{-1}(t^{P^{M}}(e))$ are created in $E^{P^{M}_{mv}}$. Since
edge sources and targets are invariant, the corresponding node
$v_{e}=\mathit{origin}^{-1}(e)$ in the end has exactly one edge of type
$corr^{s}_{mv}(e)$ and one of type $corr^{t}_{mv}(e)$. We thus have two
functions $s_{mv}:\mathit{origin}^{-1}(E^{P^{M}})\rightarrow E^{P^{M}_{mv}}$
respectively $t_{mv}:\mathit{origin}^{-1}(E^{P^{M}})\rightarrow
E^{P^{M}_{mv}}$ encoding these mappings.

Another, distinct subgraph $P_{mv}^{V}$ contains versioning information and is
constructed as follows: For each $M_{i}\in M_{\\{1,\dots,n\\}}$, $P_{mv}^{V}$
contains a corresponding node of type $version$. For each $(M_{i}\leftarrow
K\rightarrow M_{j})\in\Delta^{M_{\\{1,\dots,n\\}}}$, $P_{mv}^{V}$ contains an
edge of type $suc$ from the node representing $M_{i}$ to the node representing
$M_{j}$.

For each modification $(M_{i}\leftarrow K\rightarrow M_{j})$, a $cv$-edge with
the node corresponding to $M_{j}$ as its target is added to all nodes
corresponding to elements created by the modification. A $dv$-edge with the
node corresponding to $M_{j}$ as its target is added to all nodes
corresponding to elements deleted by the modification. Additionally, a $cv$
edge with the node corresponding to the initial version $M_{\alpha}$ as its
target is added to all nodes corresponding to elements in $M_{\alpha}$.

Since attributes can be encoded by dedicated nodes and assignment edges [13],
the construction can be performed analogously for attributed graphs.

For $v\in P_{mv}^{M}$ and $M_{i}\in M_{\\{1,\dots,n\\}}$, we say that $v$ is
_mv-present_ in $M_{i}$, iff for a node $m_{cv}$ connected to $v$ via a $cv$
edge, there exists a path from $m_{cv}$ to the node representing $M_{i}$ via
$suc$ edges that does not go through a node connected to $v$ via a $dv$ edge.
We denote the set of versions where $v$ is mv-present by $p(v)$.

A model version $M_{i}$ can then be derived from $\mathit{MVM}$ via an
operation $\mathop{proj}$ as follows: Collect all nodes $V_{p}=\\{v_{p}\in
V^{P_{mv}^{M}}|M_{i}\in p(v_{p})\\}$, that is, all nodes that are mv-present
in $M_{i}$, and translate the induced subgraph into the single-version model
$M_{i}$ with $V^{M_{i}}=\\{\mathit{origin}(v_{v})|v_{v}\in
V^{MVM}\wedge\mathit{corr}_{mv}^{-1}(type^{MVM}(v_{v}))\in V^{TM}\\}$,
$E^{M_{i}}=\\{\mathit{origin}(v_{e})|v_{e}\in
V^{MVM}\wedge\mathit{corr}_{mv}^{-1}(type^{MVM}(v_{e}))\in E^{TM}\\}$,
$s^{M_{i}}=\mathit{origin}\circ t^{MVM}\circ s_{mv}\circ\mathit{origin}^{-1}$,
and $t^{M_{i}}=\mathit{origin}\circ t^{MVM}\circ
t_{mv}\circ\mathit{origin}^{-1}$.

####  4.0.1 Correctness

###### Theorem 4.1

For a correct model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$ holds concerning
$\mathop{comb}$ and $\mathop{proj}$:

$\forall
i\in\\{1,\dots,n\\}:M_{i}=\mathop{proj}(\mathop{comb}(\Delta^{M_{\\{1,\dots,n\\}}}),i).$

###### Proof

(Sketch) Any element in a version $M_{i}$ has a corresponding node $v$ in
$\mathop{comb}(\Delta^{M_{\\{1,\dots,n\\}}})$. By construction, $v$ is
connected to a node corresponding to some version $M_{j}$ via a $cv$ edge, for
which there exists a path of $\mathit{suc}$ edges to the node corresponding to
$M_{i}$. That path does not go through a node connected to $v$ by a $dv$ edge.
$v$ is thus mv-present in $M_{i}$ and hence contained in the projection.

Inclusion of elements in the opposite direction can be shown analogously.
Because edge sources and targets are invariant over all graphs, the edges in
$\mathop{comb}(M_{1},\dots,M_{n})$ correctly encode the source and target
functions by construction. Thus, $\forall
i\in\\{1,\dots,n\\}:M_{i}=\mathop{proj}(\mathop{comb}(M_{1},\dots,M_{n}),i)$.
∎

A maximally preserving model modification $(M_{i}\leftarrow K\rightarrow
M_{j})$ with $M_{i},M_{j}\in M_{\\{1,\dots,n\\}}$ (and thus any model
modification in $\Delta^{M_{\\{1,\dots,n\\}}}$) can be derived from
$\mathit{MVM}$ via $\mathop{proj^{\Delta}}$ as follows: $M_{i}$ and $M_{j}$
can be derived via the operation $\mathop{proj}$. $K$ is then the graph
containing all elements from $M_{i}\cap M_{j}$, with $s^{K}$ and $t^{K}$
uniquely defined by the corresponding functions from $M_{i}$ and $M_{j}$ and
partial identities as morphisms into $M_{i}$ and $M_{j}$.

###### Theorem 4.2

For a correct model versioning $\Delta^{M}_{\\{1,\dots,n\\}}$, concerning
$\mathop{comb}$ and $\mathop{proj^{\Delta}}$, it holds that:

$\forall M_{i},M_{j}\in
M_{\\{1,\dots,n\\}}:m_{i,j}=\mathop{proj^{\Delta}}(\mathop{comb}(\Delta^{M_{\\{1,\dots,n\\}}}),i,j),$

with $m_{i,j}$ the maximally preserving model modification from $M_{i}$ to
$M_{j}$.

###### Proof

Follows trivially from Theorem 4.1 and the definition of the maximally
preserving model modification $(M_{i}\leftarrow K_{i,j}\rightarrow M_{j})$. ∎

Figure 4 visualizes the multi-version model $MVM$ constructed for the example
versioning in Figure 3 and the associated adapted type graph $TM_{mv}$. $MVM$
contains a node for each node and edge in the models of the example
versioning, one node of type $version$ for each of the graphs $M_{1}$,
$M_{2}$, and $M_{3}$, and appropriate edges as created by $\mathop{comb}$.

Figure 4: Multi-version model and adapted type graph for the versioning in
Figure 3

###  4.1 Directly Checking Well-Formedness for Multi-Version Models

We can use a multi-version model to directly find all well-formedness
violations in all individual versions via an operation $\mathop{pcheck_{mv}}$.
For a multi-version model $\mathit{MVM}$ with a bijective mapping into a union
of original model versions $\mathit{origin}_{M}$ and a well-formedness
constraint $\phi$ with associated violation pattern $Q$,
$\mathop{pcheck_{mv}}(\mathit{MVM},\phi)$ works as follows:

First, the graph $Q$ typed over the original type graph is translated into a
corresponding graph $Q_{mv}$ typed over the adapted type graph using
$\mathop{trans_{mv}}$. This yields a bijective mapping
$\mathit{origin_{Q}}:Q_{mv}\rightarrow Q$.

Then, all matches for $Q_{mv}$ in $\mathit{MVM}$ are found. For each such
match $m_{mv}$, $\mathop{pcheck_{mv}}$ computes all versions for which all
vertices in the image of the match are mv-present by $P=\bigcap_{v\in
V^{Q_{mv}}}p(m_{mv}(v))$. If $P\neq\emptyset$, the match into the original
model versions $m=\mathit{origin_{M}}\circ
m_{mv}\circ\mathit{origin_{Q}^{-1}}$ is constructed and reported as a
violation in all versions in $P$.

####  4.1.1 Correctness

###### Theorem 4.3

For a well-formedness constraint $\phi$ with violation pattern $Q$, a correct
model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$, and
$\mathit{MVM}=\mathop{comb}(\Delta^{M}_{\\{1,\dots,n\\}})$ holds:

$\mathop{pcheck_{mv}}(\mathit{MVM},\phi)=\biguplus_{i\in\\{1,\dots,n\\}}\\{(i,m)|m\in\mathop{pcheck}(\mathop{proj}(\mathit{MVM},i),\phi)\\}.$

###### Proof

(Sketch) A match $m:Q\rightarrow M_{i}$ for any version $M_{i}$ has one
corresponding match $m_{mv}$ with $m=\mathit{origin_{M}}\circ
m_{mv}\circ\mathit{origin_{Q}^{-1}}$, where edges created by
$\mathop{trans}_{mv}$ ensure correct connectivity. $P=\bigcap_{v\in
V^{Q_{mv}}}p(m_{mv}(v))$ contains exactly the versions containing all elements
in $m(Q)$. This yields the stated equality. ∎

####  4.1.2 Complexity

The effort for searching all versions $M_{\\{1,\dots,n\\}}$ of some model
versioning $\Delta^{M_{\\{1,\dots,n\\}}}$ for a pattern $Q$ using
$\mathop{pcheck}$ is in $O(\sum_{M_{i}\in M_{\\{1,\dots,n\\}}}C(M_{i},Q))$,
with $C(M_{i},Q)$ the effort for finding all matches of $Q$ into $M_{i}$.

$P_{mv}^{M}=\mathop{trans}_{mv}(P^{M})$ and $Q_{mv}=\mathop{trans}_{mv}(Q)$
are only different encodings of $P^{M}=\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i}$ and $Q$. Considering computation of the mv-present
predicate, the effort for $\mathop{pcheck_{mv}}$ is hence in
$O(C(\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i},Q)+X\cdot|V^{Q_{mv}}|\cdot|\Delta^{M_{1,\dots,n}}|)$,
with $X$ the number of matches for $Q_{mv}$ into $P_{mv}^{M}$.

####  4.1.3 Discussion

If many elements are shared between individual versions and modifications only
perform few changes, the size of the union of all model versions will be small
compared to the sum of the sizes of all individual versions. If pattern
matching is efficient with respect to the size of the considered model,
pattern matching over the union of all model versions will then likely require
less effort than matching over each individual version. If the number of
matches for violation patterns is low, the associated checks performed by
$\mathop{pcheck_{mv}}$ will likely be more efficient than the pattern matching
over the individual versions.

Overall, $\mathop{pcheck_{mv}}$ will thus likely be more efficient than using
$\mathop{pcheck}$ in scenarios where pattern matching is efficient, the number
of changes between versions is low, and the number of violations in the union
of versions is low.

##  5 Directly Checking Merge Results for Multi-Version Models

We can consider multi-version models to directly detect whether (a) merge
conflicts exist for any valid pair of encoded model modifications via an
operation $\mathop{mcheck_{mv}}$ and (b) any resulting merged model is ill-
formed via an operation $\mathop{pcheck^{m}_{mv}}$, where a pair of model
modifications $(M_{c}\leftarrow K_{i}\rightarrow M_{i})$ and $(M_{c}\leftarrow
K_{j}\rightarrow M_{j})$ is valid iff $M_{c}\in\mathit{pre}^{C}(M_{i},M_{j})$.

###  5.1 Directly Checking for Merge Conflicts

$\mathop{mcheck_{mv}}$ can be realized for a multi-version model
$\mathit{MVM}=\mathop{comb}(\Delta^{M_{\\{1,\dots,n\\}}})$ as follows: First,
the operation collects all nodes in $\mathit{MVM}$ representing edges that are
created by some model modification. This means all nodes $v_{e}\in V^{MVM}$
where $\mathit{corr}_{mv}^{-1}(type^{MVM}(v))\in E^{TM}$ connected to a node
$m_{x}$ via a $cv$ edge, where $m_{x}$ does not correspond to $M_{\alpha}$ and
with $TM$ the original type graph. Then, for each node $v_{e}$, we compute the
set of versions $P=p(v_{e})$ where it is mv-present. If $P\neq p(v_{s})$,
where $v_{s}=s^{\mathit{MVM}}(s_{mv}(v_{e}))$, we then compute a set of
versions $D$ that correspond to nodes reachable via $\mathit{suc}$ edges from
a node connected to $v_{s}$ via a $dv$ edge without going through nodes
connected to $v_{s}$ via a $cv$ edge.

Afterwards, for each pair of versions $M_{i}\in P$ and $M_{j}\in D$, we check
for each latest common predecessor $M_{c}\in\mathit{pre}^{C}(i,j)$ whether
$M_{c}\in p(v_{s})\wedge M_{c}\notin P$. For any triplet of versions $(i,j,c)$
where this is the case, the edge $\mathit{origin}(v_{e})$ is then in an
insert-delete conflict with its source. To facilitate formalization, this
conflict is reported in the normalized form
$(\mathop{min}(i,j),\mathop{max}(i,j),c,(\mathit{origin}(v_{e}),\mathit{origin}(v_{s})))$.
Insert-delete conflicts with the edge’s target are computed analogously.

####  5.1.1 Correctness

###### Theorem 5.1

For a model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$ and the associated
multi-version model $\mathit{MVM}=\mathop{comb}(\Delta^{M}_{\\{1,\dots,n\\}})$
holds:

$\mathop{mcheck_{mv}}(\mathit{MVM})=\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{mcheck}(m_{c,i},m_{c,j})\\},$

where
$Y=\\{(i,j,c)\,|\,i,j\in\\{1,\dots,n\\}:i<j,c\in\\{c|M_{c}\in\mathop{pre^{C}}(i,j)\\}\\}$
and with $m_{c,i}=\mathop{proj^{\Delta}}(\mathit{MVM},c,i)$ and
$m_{c,j}=\mathop{proj^{\Delta}}(\mathit{MVM},c,j)$.

###### Proof

(Sketch) The collected nodes representing edges correspond to a superset of
edges that may be involved in a conflict. The construction of the sets $P$ and
$D$ for a collected node $v_{e}$ ensures that any pair of versions where one
may create $e=\mathit{origin}(v_{e})$ and the other may delete the source (or
target) of $e$ is considered. The condition checked for each common
predecessor of a version pair then yields exactly the triplets of versions
where $e$ is part of an insert-delete conflict. Because of the normalization
of the results of $\mathop{mcheck_{mv}}$, we have the stated equality. ∎

####  5.1.2 Complexity

The function $\mathit{pre}^{C}_{mv}$ can be precomputed in
$O(|M_{\\{1,\dots,n\\}}|^{4})$.

Since information about creation and deletion of elements is not explicitly
available in a naïve representation, finding all insert-delete conflicts
between two model modifications via $\mathop{mcheck}$ has to be done by
checking for each edge in either modification’s resulting model whether it is
created by that modification and its source or target is deleted by the other
modification. Since there may exist up to $O(|M_{\\{1,\dots,n\\}}|^{3})$
possible merges in a model versioning, in the worst case, this implies effort
in $O(|M_{\\{1,\dots,n\\}}|^{4}+|E^{M_{max}}|\cdot|M_{\\{1,\dots,n\\}}|^{3})$,
where $|E^{M_{max}}|$ is the maximum number of edges present in a single model
version.

Created edges can be retrieved efficiently from a multi-version model given
appropriate data structures. Computing and checking the required version sets
takes $O(|M_{\\{1,\dots,n\\}}|^{3})$ steps per edge. Therefore, the overall
computational complexity of $\mathop{mcheck}_{mv}$ is in
$O(|M_{\\{1,\dots,n\\}}|^{4}+\Delta_{+}\cdot|M_{\\{1,\dots,n\\}}|^{3})$, where
$\Delta_{+}$ is the overall number of elements created in the model
versioning.

####  5.1.3 Discussion

The efficiency of $\mathop{mcheck}_{mv}$ compared to using $\mathop{mcheck}$
mostly depends on the number of edges created by some model modification
compared to the number of edges in the individual versions. If most edges are
present in the original model version and are shared between many model
versions, $\mathop{mcheck}_{mv}$ will be more efficient. Otherwise,
$\mathop{mcheck}_{mv}$ will not achieve a significant improvement and might
even perform worse than the operation based on $\mathop{mcheck}$.

Version control systems such as Git typically select a single latest common
predecessor as the base for a three way merge[2]. Using a corresponding
partial function $\mathit{pre}^{C}_{1}:\mathbb{N}\times\mathbb{N}\rightarrow
M_{\\{1,\dots,n\\}}$ with $\mathit{pre}^{C}_{1}(i,j)\in\mathit{pre}^{C}(i,j)$
if $\mathit{pre}^{C}(i,j)\neq\emptyset$ and $\mathit{pre}^{C}_{1}(i,j)=\perp$
to select a single latest common predecessor of two versions $i$ and $j$
rather than $\mathit{pre}^{C}$ in $\mathop{mcheck_{mv}}$, by the same logic as
used in the proof of correctness, we instead have an analogous equality for
$\mathit{pre}^{C}_{1}$. Disregarding the computational effort for precomputing
$\mathit{pre}^{C}_{1}$, replacing $\mathit{pre}^{C}$ by $\mathit{pre}^{C}_{1}$
reduces the remaining computational complexity of $\mathop{mcheck_{mv}}$ to
$O(\Delta_{+}\cdot|M_{\\{1,\dots,n\\}}|^{2})$.

###  5.2 Directly Checking Well-Formedness for Merge Results

To find all violations of a well-formedness constraint $\phi$ characterized by
a pattern $Q$ via $\mathop{pcheck^{m}_{mv}}$ in merge results of a multi-
version model $MVM$, we first translate $Q$ into $Q_{mv}=\mathop{trans}_{mv}$.
We then find all matches for $Q_{mv}$ in $MVM$.

For a match $m_{mv}$ for $Q_{mv}$, we determine the set of versions
$P_{v}=p(v)$ for each $v\in m_{mv}(V^{Q_{mv}})$. For each pair of versions
$M_{i}\in\operatorname*{arg\,min}_{P\in\\{p(v)|v\in m_{mv}(V^{Q_{mv}}\\}}|P|$
and $M_{j}\in\bigcup_{v\in V^{Q_{mv}}}p(v)$, we check whether $\forall v\in
m_{mv}(V^{Q_{mv}}):M_{i}\in p(v)\vee M_{j}\in p(v)$. We then check for each
latest common predecessor $M_{c}\in\mathit{pre}^{C}(i,j)$ if for all $v\in
V^{Q_{mv}}$, it holds that $v\in V^{M_{c}}\rightarrow(v\in V^{M_{i}}\wedge
v\in V^{M_{j}})$, that is, $v$ is not deleted in $M_{i}$ or $M_{j}$. If this
is the case, the match $m$ into $\bigcup_{M_{x}\in M_{\\{1,\dots,n\\}}}M_{x}$
corresponding to $m_{mv}$ represents a violation in
$\mathop{merge}^{min}((M_{c}\leftarrow K_{i}\rightarrow
M_{i}),(M_{c}\leftarrow K_{j}\rightarrow M_{j}))$. We report results in the
normalized form $(\mathop{min}(i,j),\mathop{max}(i,j),c,m)$.

####  5.2.1 Correctness

###### Theorem 5.2

For a well-formedness constraint $\phi$, a correct model versioning
$\Delta^{M_{\\{1,\dots,n\\}}}$, and the multi-version model
$\mathit{MVM}=\mathop{comb}(\Delta^{M}_{\\{1,\dots,n\\}})$ holds:

$\mathop{pcheck^{m}_{mv}}(\mathit{MVM},\phi)=\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{pcheck}(M^{min}_{i,j,c},\phi)\\},$

where
$Y=\\{(i,j,c)\,|\,i,j\in\\{1,\dots,n\\}:i<j,c\in\\{c|M_{c}\in\mathop{pre^{C}}(i,j)\\}\\}$
and
$M^{min}_{i,j,c}=\mathop{merge_{G}^{min}}(\mathop{proj^{\Delta}}(\mathit{MVM},c,i),\mathop{proj^{\Delta}}(\mathit{MVM},c,j))$.

###### Proof

(Sketch) For two versions $M_{i},M_{j}$ with latest common predecessor
$M_{c}$, a match
$m:Q\rightarrow\mathop{merge_{G}^{min}}(\mathop{proj^{\Delta}}(\mathit{MVM},c,i),\mathop{proj^{\Delta}}(\mathit{MVM},c,j))$
has one corresponding match
$m_{mv}:\mathop{trans}_{mv}(Q)\rightarrow\mathit{MVM}$ by construction, where
the edges created by $\mathop{trans}_{mv}$ ensure the correct connectivity.
The set of version pairs considered by $\mathop{pcheck^{m}_{mv}}$ contains all
version pairs such that each matched element is contained in at least one of
the versions. The condition checked for every latest common predecessor
ensures that only version triplets are reported where the merge result also
contains all matched elements if there are no merge conflicts. Since
$\mathop{merge^{min}}$ resolves conflicts by prioritizing deletion and, as
ensured by the check, no matched node is deleted by the merge, conflict
resolution cannot invalidate the match or create new matches. We thus have the
stated equality. ∎

By Theorem 3.1 and Theorem 5.2, we also have that $\mathop{pcheck^{m}_{mv}}$
yields the set of violations that cannot be avoided by any conflict resolution
strategy:

###### Corollary 1

For a well-formedness constraint $\phi$, a correct model versioning
$\Delta^{M_{\\{1,\dots,n\\}}}$, and the multi-version model
$\mathit{MVM}=\mathop{comb}(\Delta^{M_{\\{1,\dots,n\\}}})$ holds:

$\mathop{pcheck^{m}_{mv}}(\mathit{MVM},\phi)=\biguplus_{(i,j,c)\in
Y}\bigcap_{\mathit{str}\in
S}\\{(i,j,c,m)|m\in\mathop{mcheck}(M^{str}_{i,j,c},\phi)\\},$

where
$Y=\\{(i,j,c)\,|\,i,j\in\\{1,\dots,n\\}:i<j,c\in\\{c|M_{c}\in\mathop{pre^{C}}(i,j)\\}\\}$
and
$M^{str}_{i,j,c}=\mathop{merge_{G}^{str}}(\mathop{proj^{\Delta}}(\mathit{MVM},c,i),\mathop{proj^{\Delta}}(\mathit{MVM},c,j))$,
and with $S$ the set of all valid conflict resolution strategies.

####  5.2.2 Complexity

The function $\mathit{pre}^{C}_{mv}$ can be precomputed in
$O(|M_{\\{1,\dots,n\\}}|^{4})$.

With $C(M_{i},Q)$ the effort for finding all matches of $Q$ into $M_{i}$,
finding violations characterized by a pattern $Q$ in all results of a set of
possible merges $Y$ using $\mathop{pcheck}$ takes effort in
$O(O(|M_{\\{1,\dots,n\\}}|^{4}+\sum_{(m_{1},m_{2})\in
Y}C(\mathop{merge^{min}_{G}}(m_{1},m_{2}),Q))$.

The computation and checking of version triplets for a match in
$\mathop{pcheck^{m}_{mv}}$ takes effort in $O(|M_{\\{1,\dots,n\\}}|^{3})$. For
$X$ matches for $Q_{mv}$, the effort for $\mathop{pcheck^{m}_{mv}}$ is thus in
$O(|M_{\\{1,\dots,n\\}}|^{4}+C(\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i},Q)+X\cdot|V^{Q_{mv}}|\cdot|M_{\\{1,\dots,n\\}}|^{3})$.

####  5.2.3 Discussion

By the same argumentation as for $\mathop{pcheck_{mv}}$,
$\mathop{pcheck^{m}_{mv}}$ will likely be more efficient than the
corresponding operation using $\mathop{pcheck}$ in scenarios where pattern
matching is efficient, the number of changes between versions is low, and the
number of violations in the union of model versions is low.

Using some partial function
$\mathit{pre}^{C}_{1}:\mathbb{N}\times\mathbb{N}\rightarrow
M_{\\{1,\dots,n\\}}$ to select a single latest common predecessor rather than
$\mathit{pre}^{C}$ in $\mathop{pcheck^{m}_{mv}}$, by the same logic as in the
proof of correctness, we have an analogous equality for
$\mathit{pre}^{C}_{1}$. Disregarding the effort for precomputing
$\mathit{pre}^{C}_{1}$, replacing $\mathit{pre}^{C}$ by $\mathit{pre}^{C}_{1}$
reduces the remaining complexity of $\mathop{pcheck^{m}_{mv}}$ to
$O(C(\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i},Q)+X\cdot|V^{Q_{mv}}|\cdot|M_{\\{1,\dots,n\\}}|^{2})$.

##  6 Evaluation

For an initial empirical evaluation of the performance and scalability of the
presented operations, we experiment with an application scenario from the
software development domain. Therefore, we extract abstract syntax graphs from
a small previous research project (rete) and a larger open source project
(henshin [3]) written in Java using the EMF-based [1] MoDisco tool [6]. We
store the extracted models in a graph format and fold each of the projects
into a multi-version model, using a mapping strategy based on hierarchy and
element names.

We then run implementations of the presented operations for conflict detection
and well-formedness checking based on multi-version models (MVM) and baseline
implementations using corresponding single-version models (SVM).111All
experiments were executed on a Linux SMP Debian 4.19.67-2 machine with Intel
Xeon E5-2630 CPU (2.3 GHz clock rate) and 386 GB system memory running OpenJDK
version 1.8.0_242. Reported execution times correspond to the arithmetic mean
of at least five runs of the respective experiment. Our implementation and
datasets are available under https://github.com/hpi-sam/multi-version-models
We consider three well-formedness constraints: uniqueness of a class’s
superclass, uniqueness of a method’s return type, and consistency of an
overriden method’s return type. We employ our own EMF-based tool [11] for
pattern matching.

Figure 5 shows the measured execution times for the operations
$\mathop{pcheck_{mv}}$, $\mathop{mcheck_{mv}}$, and $\mathop{pcheck^{m}_{mv}}$
and related single-version-model-based operations over the example models. The
execution times for $\mathop{pcheck_{mv}}$ and $\mathop{pcheck^{m}_{mv}}$
correspond to the combined pattern matching time for all considered well-
formedness constraints. All reported times exclude the time for computing any
merge results required by SVM and the time required to precompute the
$\mathit{pre}^{C}$ function, since it is required by both the MVM and the SVM
implementation. Precomputing $\mathit{pre}^{C}$ took about 5 ms for the
smaller project and about 3.5 s for the larger project.

Figure 5: Measurement results for $\mathop{pcheck_{mv}}$,
$\mathop{mcheck_{mv}}$, and $\mathop{pcheck^{m}_{mv}}$

For the tasks related to well-formedness checking, the MVM variant performs
better (up to factor 50) than SVM. Since there are only few to no matches for
the violation patterns of the considered constraints, the MVM implementation
only performs few of the potentially expensive checks over the version graph,
while avoiding most of the redundancy in the pattern matching of SVM.

For conflict detection, MVM performs better than SVM for the smaller project
(factor 5), but has a substantially higher execution time for the larger
project (factor 10). The reason for the bad performance is that most edges are
not present in the initial model version. In fact, the number of edges created
throughout the model versioning is much higher than the number of edges in any
individual version. Furthermore, in contrast to the solution using
$\mathop{mcheck}$, the operation $\mathop{mcheck}_{mv}$ considers versions
where the source or target of an edge is _not_ present. Due to the high number
of versions in the project and because many elements are only present in few
versions, this leads to the processing of large version sets, which
deteriorates the performance of MVM in this scenario.

####  6.0.1 Threats to Validity

Unexpected JVM behavior poses a threat to internal validity, which we tried to
mitigate by performing multiple runs of each experiment and profiling time
spent on garbage collection. To address threats to external validity, we used
real-world data and well-formedness constraints in our experiments. While we
used our own tool for pattern matching, said tool has already been used in our
previous works and has shown adequate performance [11].

However, the example constraints are not representative and the folding of
individual model versions extracted from source code may yield a larger-than-
necessary multi-version model. Our results are thus not necessarily
generalizable, but instead constitute an early conceptual evaluation of the
presented approach.

##  7 Related Work

While most practical version control systems operate on text documents [16],
versioning and merging of models has also been subject to extensive research.

There already exist several formal and semi-formal approaches to model
merging, which compute the result of a three-way-merge of model modifications
[21, 20]. Notably, the approach by Taentzer et al. [20] represents a formally
defined solution that works on the level of graphs, which is why for our
approach, we build on their notion of model merging. In their work, Taentzer
et al. also consider checking of well-formedness constraints by constructing a
tentative merge result over which the check is executed. While this allows
their approach to handle arbitrary constraints rather than just simple graph
patterns, the check has to be executed for each individual merge.

Some approaches consider detection of merge conflicts [15] or model
inconsistencies [4] based on the analysis of sequences of primitive changes.
However, these approaches do not consider the case of multiple versions and
pairwise merges and naturally do not employ a graph-based definition of
inconsistencies.

For the more general problem of model versioning, both formal solutions [18,
7] and tool implementations [17, 14] have been introduced. Similar to our
approach, some of these techniques are based on a joint representation of
multiple model versions [17, 18]. However, to the best of our knowledge, joint
conflict detection or well-formedness checking for all merges at once is not
considered.

Westfechtel and Greiner [22] present a solution to configuration management
for product lines, where several configurations are represented in a unified
feature model. Information about the presence of elements in certain
configurations is encoded in logic formulas and propagated along model
transformations. While this approach bears some similarity to the encoding of
different versions and collective well-formedness checking in our solution,
the technique in [22] focuses on the definition of product lines and hence
does not consider merging.

Folding and joint querying of the temporal evolution of graphs has been
studied in previous work of our group [12, 19]. However, the aim of these
solutions is the development of a temporal logic for graphs. The presented
concepts are hence specific to sequences of graph modifications and do not
consider merging.

##  8 Conclusion

In this paper, we have presented an approach for encoding a model versioning
as a single typed graph. Based on this representation, we have introduced
operations for finding merge conflicts and violations of well-formedness
conditions in the form of graph patterns in the entire versioning and related
merge results. We have conducted an initial empirical evaluation, which
demonstrates potential benefits of the approach, but also highlights
shortcomings in unfavorable scenarios.

In future work, we plan to address these shortcomings by studying how to
compress the version graph or restrict the set of considered versions to those
most relevant to users. We want to investigate how to lift our notion of well-
formedness constraints to more expressive formalisms such as nested graph
conditions and develop an incremental version of the approach. Finally, we
will extend our empirical evaluation to better characterize our technique’s
performance.

## References

  * [1] EMF. https://www.eclipse.org/modeling/emf/, last accessed 23 February 2022
  * [2] Git. https://git-scm.com/, last accessed 23 February 2022
  * [3] Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: International Conference on Model Driven Engineering Languages and Systems. Springer (2010)
  * [4] Blanc, X., Mougenot, A., Mounier, I., Mens, T.: Incremental detection of model inconsistencies based on model operations. In: International Conference on Advanced Information Systems Engineering. pp. 32–46. Springer (2009)
  * [5] Brun, Y., Holmes, R., Ernst, M.D., Notkin, D.: Early Detection of Collaboration Conflicts and Risks. IEEE Transactions on Software Engineering 39(10)
  * [6] Bruneliere, H., Cabot, J., Jouault, F., Madiot, F.: MoDisco: a generic and extensible framework for model driven reverse engineering. In: Proceedings of the IEEE/ACM international conference on Automated software engineering
  * [7] Diskin, Z., Czarnecki, K., Antkiewicz, M.: Model-versioning-in-the-large: Algebraic foundations and the tile notation. In: 2009 ICSE Workshop on Comparison and Versioning of Software Models. pp. 7–12. IEEE (2009)
  * [8] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer (2006)
  * [9] Finkelstein, A.C.W., Gabbay, D., Hunter, A., Kramer, J., Nuseibeh, B.: Inconsistency Handling in Multiperspective Specifications. IEEE Transactions on Software Engineering 20(8), 569–578 (August 1994)
  * [10] Frühauf, K., Zeller, A.: Software configuration management: State of the art, state of the practice. In: International Symposium on Software Configuration Management. pp. 217–227. Springer (1999)
  * [11] Giese, H., Hildebrandt, S., Seibel, A.: Improved flexibility and scalability by interpreting story diagrams. Electronic Communications of the EASST 18 (2009)
  * [12] Giese, H., Maximova, M., Sakizloglou, L., Schneider, S.: Metric temporal graph logic over typed attributed graphs. In: International Conference on Fundamental Approaches to Software Engineering. pp. 282–298. Springer, Cham (2019)
  * [13] Heckel, R., Küster, J.M., Taentzer, G.: Confluence of Typed Attributed Graph Transformation Systems. In: Graph Transformation (2002)
  * [14] Koegel, M., Helming, J.: Emfstore: a model repository for emf models. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 2. pp. 307–308 (2010)
  * [15] Küster, J.M., Gerth, C., Engels, G.: Dependent and conflicting change operations of process models. In: European Conference on Model Driven Architecture-Foundations and Applications. pp. 158–173. Springer (2009)
  * [16] Mens, T.: A State-of-the-Art Survey on Software Merging. IEEE Trans. Softw. Eng. 28(5), 449–462 (2002)
  * [17] Murta, L., Corrêa, C., Prudêncio, J.G., Werner, C.: Towards odyssey-vcs 2: Improvements over a uml-based version control system. In: Proceedings of the 2008 international workshop on Comparison and versioning of software models (2008)
  * [18] Rutle, A., Rossini, A., Lamo, Y., Wolter, U.: A category-theoretical approach to the formalisation of version control in MDE. In: International Conference on Fundamental Approaches to Software Engineering. pp. 64–78. Springer (2009)
  * [19] Sakizloglou, L., Ghahremani, S., Barkowsky, M., Giese, H.: Incremental execution of temporal graph queries over runtime models with history and its applications. Software and Systems Modeling pp. 1–41 (2021)
  * [20] Taentzer, G., Ermel, C., Langer, P., Wimmer, M.: A fundamental approach to model versioning based on graph modifications: from theory to implementation. Software & Systems Modeling 13(1), 239–272 (2014)
  * [21] Westfechtel, B.: A formal approach to three-way merging of emf models. In: Proceedings of the 1st International Workshop on Model Comparison in Practice
  * [22] Westfechtel, B., Greiner, S.: Extending single-to multi-variant model transformations by trace-based propagation of variability annotations. Software and Systems Modeling 19(4), 853–888 (2020)

##  Appendix 0.A Technical Details

###### Theorem 0.A.1

For a correct model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$ holds concerning
$\mathop{comb}$ and $\mathop{proj}$:

$\forall
i\in\\{1,\dots,n\\}:M_{i}=\mathop{proj}(\mathop{comb}(\Delta^{M_{\\{1,\dots,n\\}}}),i).$

###### Proof

For any version $M_{i}$ and any element $x\in M_{i}$, there is a version
$M_{j}$, such that $x\in M_{j}$ with $M_{j}=M_{\alpha}$ or
$\exists(M_{x}\leftarrow K\rightarrow
M_{j})\in\Delta^{M_{\\{1,\dots,n\\}}}:x\notin M_{x}\wedge x\in M_{j}$, that
is, $(M_{x}\leftarrow K\rightarrow M_{j})$ creates $x$, and there exists a
(potentially empty) sequence of model modifications
$M_{j}\Rightarrow^{*}M_{i}$ that does not delete $x$ again.

Thus, by the construction of $\mathop{comb}$, there exists an element
$x_{mv}\in\mathit{MVM}$, where
$\mathit{MVM}=\mathop{comb}(M_{1},\dots,M_{n})$, which is connected to the
node $m_{j}\in MVM$ that corresponds to $M_{j}$ via a $cv$ edge.

Because there exists a sequence of model modifications
$M_{j}\Rightarrow^{*}M_{i}$ where $x$ is not deleted, there exists a path of
$suc$ edges from $m_{j}$ to the node representing $M_{i}$ that does not go
through any node connected to $x_{mv}$ via a $dv$ edge. Therefore, $x_{mv}$ is
mv-present in $M_{i}$ for $\mathit{MVM}$. Hence,
$x\in\mathop{proj}(\mathop{comb}(M_{1},\dots,M_{n}),i)$.

Since all implications used for deductions are equivalences, we have that
$x\in\mathop{proj}(\mathop{comb}(M_{1},\dots,M_{n}),i)\Leftrightarrow x\in
M_{i}$ for any element $x$ and model version $M_{i}$ and therefore the
equality of vertex and edge sets of $M_{i}$ and the projection.

Because edge sources and targets are invariant over multiple graphs, the edges
in $\mathop{comb}(M_{1},\dots,M_{n})$ correctly encode the source and target
functions by construction. Thus, $\forall
i\in\\{1,\dots,n\\}:M_{i}=\mathop{proj}(\mathop{comb}(M_{1},\dots,M_{n}),i)$.
∎

###### Theorem 0.A.2

For a well-formedness constraint $\phi$, a correct model versioning
$\Delta^{M_{\\{1,\dots,n\\}}}$, and associated multi-version model
$\mathit{MVM}=\mathop{comb}(\Delta^{M}_{\\{1,\dots,n\\}})$ holds:

$\mathop{pcheck_{mv}}(\mathit{MVM},\phi)=\biguplus_{i\in\\{1,\dots,n\\}}\\{(i,m)|m\in\mathop{pcheck}(\mathop{proj}(\mathit{MVM},i),\phi)\\}.$

###### Proof

For a tuple $(i,m)$ with match $m:Q\rightarrow\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i}$ to be reported in the result of
$\mathop{pcheck_{mv}}(M_{\\{1,\dots,n\\}},\phi)$, there has to exist a match
$m_{mv}:Q_{mv}\rightarrow\mathit{MVM}$, where $Q_{mv}=\mathop{trans}_{mv}(Q)$,
such that $m=\mathop{trans_{mv}}^{m}(m_{mv})$ and $\bigcap_{v\in
V^{Q_{mv}}}p(m_{mv}(v))\neq\emptyset$.

There hence exists some version $M_{i}\in M_{\\{1,\dots,n\\}}$ such that
$\forall v\in V^{Q_{mv}}:M_{i}\in p(m_{mv}(v))$. Therefore, $\forall v\in
V^{Q_{mv}}:\mathit{origin_{M}}(m_{mv}(v))\in\mathop{proj}(M_{\\{1,\dots,n\\}},i)$.

Then, $m$ is a valid monomorphism into
$M_{i}=\mathop{proj}(M_{\\{1,\dots,n\\}},i)$, since (i) all required elements
are present and (ii) by construction of $\mathit{MVM}$, $Q_{mv}$, the edges in
$Q_{mv}$ ensure that $\forall e\in E^{Q}:s^{M_{i}}(m(e))=m(s^{Q}(e))\wedge
t^{M_{i}}(m(e))=m(t^{Q}(e))$, and the $\mathit{origin}$ function is bijective.
Therefore, it holds that
$(i,m)\in\biguplus_{i\in\\{1,\dots,n\\}}\mathop{pcheck}(\mathop{proj}(M_{\\{1,\dots,n\\}},i),\phi)$.

Thus, we have:

$\mathop{pcheck_{mv}}(\mathit{MVM},\phi)\subseteq\biguplus_{i\in\\{1,\dots,n\\}}\\{(i,m)|m\in\mathop{pcheck}(\mathop{proj}(\mathit{MVM},i),\phi)\\}$

Any match $m:Q\rightarrow M_{i}$, where
$M_{i}=\mathop{proj}(M_{\\{1,\dots,n\\}},i)$ is also structurally present in
$\biguplus_{M_{i}\in M_{\\{1,\dots,n\\}}}M_{i}$. Since $\mathop{trans}_{mv}$
creates isomorphic graphs for $Q$ and the image of $Q$ under $m$, there exists
a match $m_{mv}=\mathop{trans_{mv}}^{m}(m_{mv})$ for
$Q_{mv}=\mathop{trans}_{mv}(Q)$ into $\mathit{MVM}$.

For $m$ to be reported by
$\mathop{pcheck}(\mathop{proj}(M_{\\{1,\dots,n\\}},i),\phi)$, all elements in
the image of $m$ have to be present in $M_{i}$. Hence, by the semantics of
$\mathop{proj}$, we have that $\forall x\in Q:M_{i}\in
p(\mathit{origin}_{M}^{-1}(m(x)))$ and hence, $\forall v\in
V^{Q_{mv}}:M_{i}\in p(m_{mv}(v))$. Therefore, $\bigcap_{v\in
V^{Q_{mv}}}p(m_{mv}(v))\neq\emptyset$, so
$(i,m)\in\mathop{pcheck_{mv}}(M_{\\{1,\dots,n\\}},\phi)$.

Thus, we have:

$\mathop{pcheck_{mv}}(\mathit{MVM},\phi)\supseteq\biguplus_{i\in\\{1,\dots,n\\}}\\{(i,m)|m\in\mathop{pcheck}(\mathop{proj}(\mathit{MVM},i),\phi)\\}$

From the two subset-relations follows the equality. ∎

###### Theorem 0.A.3

For a model versioning $\Delta^{M_{\\{1,\dots,n\\}}}$ and the associated
multi-version model $\mathit{MVM}=\mathop{comb}(\Delta^{M}_{\\{1,\dots,n\\}})$
holds:

$\mathop{mcheck_{mv}}(\mathit{MVM})=\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{mcheck}(m_{c,i},m_{c,j})\\},$

where
$Y=\\{(i,j,c)\,|\,i,j\in\\{1,\dots,n\\}:i<j,c\in\\{c|M_{c}\in\mathop{pre^{C}}(i,j)\\}\\}$
and with $m_{c,i}=\mathop{proj^{\Delta}}(\mathit{MVM},c,i)$ and
$m_{c,j}=\mathop{proj^{\Delta}}(\mathit{MVM},c,j)$.

###### Proof

For $e$ an edge and its invariant source $s$ reported for versions $M_{i}$ and
$M_{j}$ and common predecessor $M_{c}\in\mathit{pre}^{C}(i,j)$ by
$\mathop{mcheck}_{mv}$, by the normalization and the fact that
$\mathit{pre}^{C}\neq\emptyset\rightarrow i\neq j$, we have that $i<j$.
Because $M_{c}\notin p(v_{e})$, we also have that $e\notin E^{M_{c}}$.
Furthermore, we either have that $M_{i}\in p(\mathit{origin}^{-1}(e))$ and
therefore $e\in E^{M_{i}}$ by Theorem 4.1 (case 1) or $M_{j}\in
p(\mathit{origin}^{-1}(e))$ and therefore $e\in E^{M_{j}}$ (case 2). Since,
$M_{c}\in\mathit{pre}(M_{i})$, we therefore have a sequence of model
modifications $M_{c}\Rightarrow^{*}M_{i}$ (case 1) or
$M_{c}\Rightarrow^{*}M_{j}$ (case 2) that creates $e$.

We also know that, in case 1, the node in the multi-version model
corresponding to $M_{j}$ lies on a path corresponding to a sequence of model
modifications that deletes but does not recreate $s$. Hence, $M_{j}\notin
p(\mathit{origin}^{-1}(s))$, since $M_{j}$ being in
$p(\mathit{origin}^{-1}(s))$ would contradict the consistency of the model
versioning. Furthermore, we know that $M_{c}\in p(\mathit{origin}^{-1}(s))$.
This means there exists a sequence of model modifications
$M_{c}\Rightarrow^{*}M_{j}$ that deletes $s$, but not $e$, since $e\notin
E^{M_{c}}$. In case 2, by the same logic, there exists a sequence of model
modifications $M_{c}\Rightarrow^{*}M_{i}$ that deletes $s$ but not $e$. Thus,
there is an insert-delete conflict between $e$ and $s$ for $M_{i}$ and $M_{j}$
in either case.

The same is true for the target of an edge.

Thus, we have:

$\mathop{mcheck_{mv}}(\mathit{MVM})\subseteq\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{mcheck}(m_{c,i},m_{c,j})\\},$

If there exists an insert-delete conflict for an edge $e$ and its source $s$
between two versions $M_{i}=\mathop{proj}(M_{\\{1,\dots,n\\}},i)$ and
$M_{j}=\mathop{proj}(M_{\\{1,\dots,n\\}},j)$ for a common predecessor
$M_{c}\in\mathit{pre}^{C}(i,j)$, this means that there exist a sequence of
model modifications $S_{i}=M_{c}\Rightarrow^{*}M_{i}$ and at least one
sequence $S_{j}=M_{c}\Rightarrow^{*}M_{j}$, where one sequence deletes $s$ and
does not delete $e$ and the other sequence creates $e$. Therefore, $s\in
V^{M_{c}}$ and $e\notin E^{M_{c}}$.

In the case where $S_{i}$ is the sequence that creates $e$, it follows that
$e\in E^{M_{i}}$. By Theoreme 4.1, it then follows that $M_{i}\in p(v_{e})$
and $M_{c}\notin p(v_{e})$, with $v_{e}=\mathit{origin}^{-1}(e)$. Because
$S_{j}$ then deletes and does not recreate $s$, it follows that there exists a
path from a node connected to $v_{s}$ via a $dv$ edge to the node
corresponding to $M_{j}$ that does not go through a node connected to $v_{s}$
via a $cv$ edge, with $v_{s}=\mathit{origin}^{-1}(s)$.

By the same logic, we can derive mirrored statements for the case where
$S_{j}$ is the sequence that creates $e$.

From the existence of a sequence of model modifications that creates $e$, it
also follows that $v_{e}$ is connected to some node $m_{x}$ via a $cv$ edge
that does not correspond to $M_{\alpha}$. From the fact that one sequence
deletes $e$ but not $s$, it follows that $p(v_{e})\neq p(v_{s})$.

Thus, $e$ and $v$ would be reported as an insert-delete conflict for versions
$M_{i}$ and $M_{j}$ with predecessor $M_{c}$ in its normalized format by
$\mathop{mcheck}_{mv}$.

The same is true for the target of an edge.

Thus, we have:

$\mathop{mcheck_{mv}}(\mathit{MVM})\supseteq\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{mcheck}(m_{c,i},m_{c,j})\\},$

By the two inclusions, we also have the equality. ∎

###### Theorem 0.A.4

For a well-formedness constraint $\phi$, a correct model versioning
$\Delta^{M_{\\{1,\dots,n\\}}}$ and the associated multi-version model
$\mathit{MVM}=\mathop{comb}(\Delta^{M}_{\\{1,\dots,n\\}})$ holds:

$\mathop{pcheck^{m}_{mv}}(\mathit{MVM},\phi)=\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{pcheck}(M^{min}_{i,j,c},\phi)\\},$

where
$Y=\\{(i,j,c)\,|\,i,j\in\\{1,\dots,n\\}:i<j,c\in\\{c|M_{c}\in\mathop{pre^{C}}(i,j)\\}\\}$
and
$M^{min}_{i,j,c}=\mathop{merge_{G}^{min}}(\mathop{proj^{\Delta}}(\mathit{MVM},c,i),\mathop{proj^{\Delta}}(\mathit{MVM},c,j))$.

###### Proof

For a match $m$ for $Q$ into $\bigcup_{M_{i}\in M_{\\{1,\dots,n\\}}}M_{i}$ to
be reported as a violation in the merge of versions $M_{i}$ and $M_{j}$ with
latest common predecessor $M_{c}$ by $\mathop{pcheck^{m}_{mv}}$, there has to
exist a corresponding match
$m_{mv}:\mathop{trans}_{mv}(Q)\rightarrow\mathit{MVM}$. We know that, because
$M_{c}\in\mathit{pre}^{C}(M_{i},M_{j})$, there are sequences of model
modifications $S_{i}=M_{c}\Rightarrow^{*}M_{i}$ and
$S_{j}=M_{c}\Rightarrow^{*}M_{j}$. Furthermore $m_{mv}$, we know that $\forall
v\in m_{mv}(Q_{mv}):M_{i}\in p(v)\vee M_{j}\in p(v)$ and $\forall v\in
m_{mv}(Q_{mv}):M_{c}\in p(v)\rightarrow(M_{i}\in p(v)\wedge M_{j}\in p(v))$.

Hence, every element $x\in m(Q)$ is either present in $M_{c}$ or created by
$S_{i}$ or $S_{j}$, and none of these elements are deleted by either
modification sequence. The resolution of merge conflicts by
$\mathop{merge^{min}}$ may delete an edge created by one modification
sequence, if its source or target is deleted by the other modification
sequence. However, since $Q$ is a proper graph, meaning that for any edge
$e\in E^{Q}:s^{Q}(e)\in V^{Q}\wedge t^{Q}(e)\in V^{Q}$, and no node $v\in
m(V^{Q})$ is deleted by either modification sequence, it follows that no edge
$e\in m(E^{Q})$ can be deleted in the process of resolving merge conflicts.

Hence, all elements $x\in m(Q)$ are present in
$\mathop{merge_{G}^{min}}(S_{i},S_{j})$. By the construction of $MVM$, we also
know that source and target functions of edges are preserved by
$\mathop{trans}_{mv}^{m}(m_{mv})$. This makes $m$ a violation of $\phi$ in the
merge. Therefore,
$(i,j,c,m)\in\mathop{pcheck}(\mathop{merge_{G}^{min}}(\mathop{proj}(M_{\\{1,\dots,n\\}},i),\mathop{proj}(M_{\\{1,\dots,n\\}},j)),\phi)$.

Since we know that $i<j$, we have:

$\mathop{pcheck^{m}_{mv}}(\mathit{MVM},\phi)\subseteq\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{pcheck}(M^{min}_{i,j,c},\phi)\\},$

For two versions $M_{i}$ and $M_{j}$ with common predecessor
$M_{c}=\mathit{pre}^{C}(M_{i},M_{j})$, a match
$m\in\mathop{pcheck}(\mathop{merge_{G}^{min}}(\mathop{proj}(M_{\\{1,\dots,n\\}},i),\mathop{proj}(M_{\\{1,\dots,n\\}},j)),\phi)$
is also a valid match into $\bigcup_{M_{i}\in M_{\\{1,\dots,n\\}}}M_{i}$.
There hence exists a corresponding match
$m_{mv}:Q_{mv}\rightarrow\mathit{MVM}$ with
$m=\mathop{trans}_{mv}^{m}(m_{mv})$.

Furthermore, in order to be present in the merge result, each element in the
image of $m$ needs to be contained in $M_{i}$ or $M_{j}$ and, therefore,
$\forall x\in m(\phi):x\in M_{i}\cup M_{j}$. We also know that none of the
elements are deleted by the modification sequence $M_{c}\Rightarrow^{*}M_{i}$
or $M_{c}\Rightarrow^{*}M_{i}$, which means that $\forall x\in m(Q):x\in
M_{c}\rightarrow(x\in M_{i}\wedge x\in M_{j})$. We thus also have that
$\forall v\in m_{mv}(V^{Q_{mv}}):M_{i}\in p(v)\vee M_{j}\in p(v)$ and $\forall
v\in m_{mv}(V^{Q_{mv}}):M_{c}\in p(v)\rightarrow(M_{i}\in p(v)\wedge M_{j}\in
p(v))$. Thereby, it must also hold that
$M_{i}\in\operatorname*{arg\,min}_{P\in\\{p(v)|v\in
m_{mv}(V^{Q_{mv}}\\}}|P|\vee
M_{j}\in\operatorname*{arg\,min}_{P\in\\{p(v)|v\in m_{mv}(V^{Q_{mv}}\\}}|P|$.
Because $i<j$, it follows that
$(i,j,c,m)\in\mathop{pcheck^{m}_{mv}}(M_{\\{1,\dots,n\\}},\phi)$.

Thus, we have:

$\mathop{pcheck^{m}_{mv}}(\mathit{MVM},\phi)\supseteq\biguplus_{(i,j,c)\in
Y}\\{(i,j,c,m)|m\in\mathop{pcheck}(M^{min}_{i,j,c},\phi)\\},$

By the two inclusions, we also have the equality. ∎

####  0.A.0.1 Complexity of $\mathop{pcheck_{mv}}$

Effectively, the graphs $P_{mv}^{M}=\mathop{trans}_{mv}(P^{M})$ and
$Q_{mv}=\mathop{trans}_{mv}(Q)$ are only a different encoding of
$P^{M}=\bigcup_{M_{i}\in M_{\\{1,\dots,n\\}}}M_{i}$ and $Q$, where edges are
replaced by nodes with a single incoming and outgoing edge. Since these newly
introduced nodes only cause a constant-factor overhead in pattern matching
using an appropriate matching strategy and the size of the two graphs
increases only by a constant factor, the effort for finding all matches for
$Q_{mv}$ into $P_{mv}^{M}$ is in $O(C(\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i},Q))$.

The set $p(v_{x})$ for each individual element $x$ with
$v_{x}=\mathit{origin}^{-1}(x)$ can be computed via breadth-first searches
starting in each node connected to $v_{x}$ via a $cv$ edge over $P^{V}_{mv}$
and stopping at nodes that are either connected to $v_{x}$ via a $dv$ edge or
that have already been visited by a previous search. Since this ensures that
the breadth-first searches do not perform redundant searches, the combined
effort is in $O(|\Delta^{M_{1,\dots,n}}|)$. Given appropriate data structures,
the effort for a single intersection of two version sets is in
$O(|M_{\\{1,\dots,n\\}}|)$. Hence, computing $P=\bigcap_{v\in
V^{Q_{mv}}}p(m_{mv}(v))$ for a single match $m_{mv}$ takes effort in
$O(|V^{Q_{mv}}|\cdot|\Delta^{M_{1,\dots,n}}|)$.

For a number of matches $X$ for $Q_{mv}$ into $P_{mv}^{M}$, the effort for
$\mathop{pcheck_{mv}}$ is then in $O(C(\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i},Q)+X\cdot|V^{Q_{mv}}|\cdot|\Delta^{M_{1,\dots,n}}|)$.

####  0.A.0.2 Complexity of $\mathop{mcheck_{mv}}$

We can precompute the latest common predecessors for any pair of versions
$M_{i}$ and $M_{j}$ according to the definition in
$O(|P^{V}_{mv}\cdot|M_{\\{1,\dots,n\\}}|+|M_{\\{1,\dots,n\\}}|^{4})$ via
breadth-first search for finding all predecessors for every version and basic
set operations. Since the maximally preserving model modification between two
versions along identity morphisms is uniquely defined and therefore
$|E^{P^{V}_{mv}}|\leq|M_{\\{1,\dots,n\\}}|^{2}$, the complexity is in
$O(|M_{\\{1,\dots,n\\}}|^{4})$. This computation allows an efficient
enumeration of the set of model modification pairs representing possible
merges.

Since information about creation and deletion of elements is not explicitly
available in a model-modification-based representation of a versioning,
finding all insert-delete conflicts between two model modifications via
$\mathop{mcheck}$ can be done by checking for each edge in either
modification’s resulting model whether it is created by that modification and
its source or target is deleted by the other modification. Given appropriate
data structures for storing the individual model versions, the check for one
edge can be performed in constant time thanks to the requirement of partial
identity morphisms. This yields a computational complexity in
$O(|M_{\\{1,\dots,n\\}}|^{4}+\sum_{((M_{c}\leftarrow K_{i}\rightarrow
M_{i}),(M_{c}\leftarrow K_{j}\rightarrow M_{j}))\in
Y}|E^{M_{i}}|+|E^{M_{j}}|)$ for checking an entire model versioning with $Y$
the set of possible merges represented by pairs of model modifications. Note
that, in the worst case, there may exist up to $O(|M_{\\{1,\dots,n\\}}|^{3})$
possible merges in a model versioning, so in the worst case, this implies
effort in
$O(|M_{\\{1,\dots,n\\}}|^{4}+|E^{M_{max}}|\cdot|M_{\\{1,\dots,n\\}}|^{3})$,
where $|E^{M_{max}}|$ is the maximum number of edges present in a single model
version.

The computation of $P=p(v_{e})$ and $D$ for every node $v_{e}\in V^{MVM}$,
where $\mathit{corr}_{mv}^{-1}(type^{MVM}(v_{e}))\in E^{TM}$ and $v_{e}$ has a
$cv$ edge to a node representing another version than $M_{\alpha}$, and the
edge source $v_{s}=s^{M}(\mathit{origin}(v_{e}))$ can be performed in
$O(\Delta_{+}\cdot|P^{V}_{mv}|)$, where $P^{V}_{mv}$ is the version graph and
$\Delta_{+}$ is the overall number of elements created by the model
versioning. Checking whether $p(v_{e})=p(v_{s})$ only takes effort in
$O(|M_{\\{1,\dots,n\\}}|)$.

For a node $v_{e}$ and versions $M_{i}\in P$ and $M_{j}\in D$, we can then
determine all latest predecessors for which $M_{i}$ and $M_{j}$ are in
conflict in $O(|M_{\\{1,\dots,n\\}}|)$. Since there are at most
$|M_{\\{1,\dots,n\\}}|^{2}$ pairs of versions in $P\times D$, the overall
complexity of $\mathop{mcheck}_{mv}$ considering the effort for precomputing
latest common predecessors is in
$O(|M_{\\{1,\dots,n\\}}|^{4}+\Delta_{+}\cdot|M_{\\{1,\dots,n\\}}|^{3})$, which
simplifies to $O(|\Delta_{+}\cdot|M_{\\{1,\dots,n\\}}|^{3})$ if
$|M_{\\{1,\dots,n\\}}|\leq\Delta_{+}$. The computation for edge targets works
analogously and thus does not change the complexity.

####  0.A.0.3 Complexity of $\mathop{pcheck^{m}_{mv}}$

We denote the effort for finding all matches for a pattern $Q$ in a model
$M_{m}$ by $C(M_{m},Q)$. A possible merge in a model versioning is
characterized by two model modifications, that is, two model versions $M_{i}$
and $M_{j}$ and a latest common predecessor $M_{c}$. Disregarding the effort
for computing a merge itself, the effort for finding all violations of a well-
formedness condition characterized by $Q$ in a model versioning with $Y$ the
set of possible merges via computing all merges and searching for $Q$ in the
results is then given by $O(\sum_{(m_{1},m_{2})\in
Y}C(\mathop{merge^{min}_{G}}(m_{1},m_{2}),Q))$. Potentially, there are up to
$O(|M_{\\{1,\dots,n\\}}|^{3})$ possible merges in a model versioning with
versions $M_{\\{1,\dots,n\\}}$, which can be computed in
$O(|M_{\\{1,\dots,n\\}}|^{4})$. This results in a complexity for computing and
checking all these merges via $\mathop{pcheck}$ in
$O(|M_{\\{1,\dots,n\\}}|^{4}+\sum_{(m_{1},m_{2})\in
Y}C(\mathop{merge^{min}_{G}}(m_{1},m_{2}),Q))$.

Finding all violations characterized by a pattern $Q$ in a model versioning by
$\mathop{pcheck^{m}_{mv}}$ requires a search for $Q_{mv}$ over the
corresponding multi-version model. As discussed in Section 4.1.2, this
requires effort in $O(C(\bigcup_{M_{i}\in M_{\\{1,\dots,n\\}}}M_{i},Q))$.
Then, for each structural match that is found, the set $P_{v}=p(v)$ has to be
computed for each $v\in V^{Q_{mv}}$, which takes
$O(|V^{Q_{mv}}|\cdot|P^{V}_{mv}|)$ computational steps. Finding all
complementary versions $M_{j}$ regarding $Q_{mv}$ for a version $M_{i}$
requires $O(|V^{Q_{mv}}|\cdot|M_{\\{1,\dots,n\\}}|)$ steps.

The number of candidates of complementary versions is in
$O(|M_{\\{1,\dots,n\\}}|^{2})$. Latest common predecessors for all version
pairs can be computed and cached upfront in $O(|M_{\\{1,\dots,n\\}}|^{4})$.
For each latest common predecessor, the remaining checks can be performed in
$O(|V^{Q_{mv}}|)$ given appropriate data structures. Since any pair of
versions has at most $|M_{\\{1,\dots,n\\}}|$ common predecessors, we thus have
effort in $O(|V^{Q_{mv}}|\cdot|M_{\\{1,\dots,n\\}}|^{3})$ for each match.

For $X$ matches for $Q_{mv}$ into $\mathit{MVM}$, the overall computational
effort is thus in $O(|M_{\\{1,\dots,n\\}}|^{4}+C(\bigcup_{M_{i}\in
M_{\\{1,\dots,n\\}}}M_{i},Q)+X\cdot|V^{Q_{mv}}|\cdot|M_{\\{1,\dots,n\\}}|^{3})$.

##  Appendix 0.B Violation Patterns of Considered Well-Formedness Constraints

Figure 6: Violation pattern for the constraint “unique superclass” Figure 7:
Violation pattern for the constraint “unique return type” Figure 8: Violation
pattern for the constraint “consistent override”


# Instructions for ACL 2019 Proceedings

First Author
Affiliation / Address line 1
Affiliation / Address line 2
Affiliation / Address line 3
email@domain
Second Author
Affiliation / Address line 1
Affiliation / Address line 2
Affiliation / Address line 3
email@domain

###### Abstract

This document contains the instructions for preparing a camera-ready
manuscript for the proceedings of ACL 2019. The document itself conforms to
its own specifications, and is therefore an example of what your manuscript
should look like. These instructions should be used for both papers submitted
for review and for final versions of accepted papers. Authors are asked to
conform to all the directions reported in this document.

##  1 Credits

This document has been adapted from the instructions for earlier ACL and NAACL
proceedings, including those for NAACL 2019 by Stephanie Lukin and Alla
Roskovskaya, ACL 2018 by Shay Cohen, Kevin Gimpel, and Wei Lu, NAACL 2018 by
Margaret Michell and Stephanie Lukin, 2017/2018 (NA)ACL bibtex suggestions
from Jason Eisner, ACL 2017 by Dan Gildea and Min-Yen Kan, NAACL 2017 by
Margaret Mitchell, ACL 2012 by Maggie Li and Michael White, those from ACL
2010 by Jing-Shing Chang and Philipp Koehn, those for ACL 2008 by JohannaD.
Moore, Simone Teufel, James Allan, and Sadaoki Furui, those for ACL 2005 by
Hwee Tou Ng and Kemal Oflazer, those for ACL 2002 by Eugene Charniak and
Dekang Lin, and earlier ACL and EACL formats. Those versions were written by
several people, including John Chen, Henry S. Thompson and Donald Walker.
Additional elements were taken from the formatting instructions of the
_International Joint Conference on Artificial Intelligence_ and the
_Conference on Computer Vision and Pattern Recognition_.

##  2 Introduction

The following instructions are directed to authors of papers submitted to ACL
2019 or accepted for publication in its proceedings. All authors are required
to adhere to these specifications. Authors are required to provide a Portable
Document Format (PDF) version of their papers. The proceedings are designed
for printing on A4 paper.

##  3 General Instructions

Manuscripts must be in two-column format. Exceptions to the two-column format
include the title, authors’ names and complete addresses, which must be
centered at the top of the first page, and any full-width figures or tables
(see the guidelines in Subsection 3.6). Type single-spaced. Start all pages
directly under the top margin. See the guidelines later regarding formatting
the first page. The manuscript should be printed single-sided and its length
should not exceed the maximum page limit described in Section 5. Pages are
numbered for initial submission. However, do not number the pages in the
camera-ready version.

By uncommenting `\aclfinalcopy` at the top of this document, it will compile
to produce an example of the camera-ready formatting; by leaving it commented
out, the document will be anonymized for initial submission. When you first
create your submission on softconf, please fill in your submitted paper ID
where `***` appears in the `\def\aclpaperid{***}` definition at the top.

The review process is double-blind, so do not include any author information
(names, addresses) when submitting a paper for review. However, you should
maintain space for names and addresses so that they will fit in the final
(accepted) version. The ACL 2019 LaTeX style will create a titlebox space of
2.5in for you when `\aclfinalcopy` is commented out.

###  3.1 The Ruler

The ACL 2019 style defines a printed ruler which should be presented in the
version submitted for review. The ruler is provided in order that reviewers
may comment on particular lines in the paper without circumlocution. If you
are preparing a document without the provided style files, please arrange for
an equivalent ruler to appear on the final output pages. The presence or
absence of the ruler should not change the appearance of any other content on
the page. The camera ready copy should not contain a ruler. (LaTeX users may
uncomment the `\aclfinalcopy` command in the document preamble.)

Reviewers: note that the ruler measurements do not align well with lines in
the paper – this turns out to be very difficult to do well when the paper
contains many figures and equations, and, when done, looks ugly. In most cases
one would expect that the approximate location will be adequate, although you
can also use fractional references (_e.g._ , the first paragraph on this page
ends at mark $108.5$).

###  3.2 Electronically-available resources

ACL provides this description in LaTeX2e (acl2019.tex) and PDF format
(acl2019.pdf), along with the LaTeX2e style file used to format it
(acl2019.sty) and an ACL bibliography style (acl_natbib.bst) and example
bibliography (acl2019.bib). These files are all available at
http://acl2019.org/downloads/ acl2019-latex.zip. We strongly recommend the use
of these style files, which have been appropriately tailored for the ACL 2019
proceedings.

###  3.3 Format of Electronic Manuscript

For the production of the electronic manuscript you must use Adobe’s Portable
Document Format (PDF). PDF files are usually produced from LaTeX using the
pdflatex command. If your version of LaTeX produces Postscript files, you can
convert these into PDF using ps2pdf or dvipdf. On Windows, you can also use
Adobe Distiller to generate PDF.

Please make sure that your PDF file includes all the necessary fonts
(especially tree diagrams, symbols, and fonts with Asian characters). When you
print or create the PDF file, there is usually an option in your printer setup
to include none, all or just non-standard fonts. Please make sure that you
select the option of including ALL the fonts. Before sending it, test your PDF
by printing it from a computer different from the one where it was created.
Moreover, some word processors may generate very large PDF files, where each
page is rendered as an image. Such images may reproduce poorly. In this case,
try alternative ways to obtain the PDF. One way on some systems is to install
a driver for a postscript printer, send your document to the printer
specifying “Output to a file”, then convert the file to PDF.

It is of utmost importance to specify the A4 format (21 cm x 29.7 cm) when
formatting the paper. When working with dvips, for instance, one should
specify -t a4. Or using the command `\special{papersize=210mm,297mm}` in the
latex preamble (directly below the `\usepackage` commands). Then using dvipdf
and/or pdflatex which would make it easier for some.

Print-outs of the PDF file on A4 paper should be identical to the hardcopy
version. If you cannot meet the above requirements about the production of
your electronic submission, please contact the publication chairs as soon as
possible.

###  3.4 Layout

Format manuscripts two columns to a page, in the manner these instructions are
formatted. The exact dimensions for a page on A4 paper are:

  * •

Left and right margins: 2.5 cm

  * •

Top margin: 2.5 cm

  * •

Bottom margin: 2.5 cm

  * •

Column width: 7.7 cm

  * •

Column height: 24.7 cm

  * •

Gap between columns: 0.6 cm

Papers should not be submitted on any other paper size. If you cannot meet the
above requirements about the production of your electronic submission, please
contact the publication chairs above as soon as possible.

###  3.5 Fonts

For reasons of uniformity, Adobe’s Times Roman font should be used. In LaTeX2e
this is accomplished by putting

>
>     \usepackage{times}
>     \usepackage{latexsym}
>

in the preamble. If Times Roman is unavailable, use Computer Modern Roman
(LaTeX2e’s default). Note that the latter is about 10% less dense than Adobe’s
Times Roman font.

Type of Text | Font Size | Style
---|---|---
paper title | 15 pt | bold
author names | 12 pt | bold
author affiliation | 12 pt |
the word “Abstract” | 12 pt | bold
section titles | 12 pt | bold
subsection titles | 11 pt | bold
document text | 11 pt |
captions | 10 pt |
abstract text | 10 pt |
bibliography | 10 pt |
footnotes | 9 pt |
Table 1:  Font guide.

###  3.6 The First Page

Center the title, author’s name(s) and affiliation(s) across both columns. Do
not use footnotes for affiliations. Do not include the paper ID number
assigned during the submission process. Use the two-column format only when
you begin the abstract.

Title: Place the title centered at the top of the first page, in a 15-point
bold font. (For a complete guide to font sizes and styles, see Table 1) Long
titles should be typed on two lines without a blank line intervening.
Approximately, put the title at 2.5 cm from the top of the page, followed by a
blank line, then the author’s names(s), and the affiliation on the following
line. Do not use only initials for given names (middle initials are allowed).
Do not format surnames in all capitals (_e.g._ , use “Mitchell” not
“MITCHELL”). Do not format title and section headings in all capitals as well
except for proper names (such as “BLEU”) that are conventionally in all
capitals. The affiliation should contain the author’s complete address, and if
possible, an electronic mail address. Start the body of the first page 7.5 cm
from the top of the page.

The title, author names and addresses should be completely identical to those
entered to the electronical paper submission website in order to maintain the
consistency of author information among all publications of the conference. If
they are different, the publication chairs may resolve the difference without
consulting with you; so it is in your own interest to double-check that the
information is consistent.

Abstract: Type the abstract at the beginning of the first column. The width of
the abstract text should be smaller than the width of the columns for the text
in the body of the paper by about 0.6 cm on each side. Center the word
Abstract in a 12 point bold font above the body of the abstract. The abstract
should be a concise summary of the general thesis and conclusions of the
paper. It should be no longer than 200 words. The abstract text should be in
10 point font.

Text: Begin typing the main body of the text immediately after the abstract,
observing the two-column format as shown in the present document. Do not
include page numbers.

Indent: Indent when starting a new paragraph, about 0.4 cm. Use 11 points for
text and subsection headings, 12 points for section headings and 15 points for
the title.

| Command | Output
---|---
`{\"a}` | ä
`{\^e}` | ê
`{\‘i}` | ì
`{\.I}` | İ
`{\o}` | ø
`{\’u}` | ú
`{\aa}` | å
| Command | Output
---|---
`{\c c}` | ç
`{\u g}` | ğ
`{\l}` | ł
`{\~n}` | ñ
`{\H o}` | ő
`{\v r}` | ř
`{\ss}` | ß
Table 2: Example commands for accented characters, to be used in, _e.g._ ,
BibTeX names.

###  3.7 Sections

Headings: Type and label section and subsection headings in the style shown on
the present document. Use numbered sections (Arabic numerals) in order to
facilitate cross references. Number subsections with the section number and
the subsection number separated by a dot, in Arabic numerals. Do not number
subsubsections.

output | natbib | previous ACL style files
---|---|---
(Gusfield:97) | `\citep` | `\cite`
Gusfield:97 | `\citet` | `\newcite`
(Gusfield:97) | `\citeyearpar` | `\shortcite`
Table 3: Citation commands supported by the style file. The citation style is
based on the natbib package and supports all natbib citation commands. It also
supports commands defined in previous ACL style files for compatibility.

Citations: Citations within the text appear in parentheses as Gusfield:97 or,
if the author’s name appears in the text itself, as Gusfield Gusfield:97.
Using the provided LaTeX style, the former is accomplished using `\cite` and
the latter with `\shortcite` or `\newcite`. Collapse multiple citations as in
Gusfield:97; Aho:72; this is accomplished with the provided style using commas
within the `\cite` command, _e.g._ , `\cite{Gusfield:97,Aho:72}`. Append
lowercase letters to the year in cases of ambiguities. Treat double authors as
in Aho:72, but write as in Chandra:81 when more than two authors are involved.
Collapse multiple citations as in Gusfield:97; Aho:72. Also refrain from using
full citations as sentence constituents.

We suggest that instead of

> “Gusfield:97 showed that …”

you use

> “Gusfield Gusfield:97 showed that …”

If you are using the provided LaTeX and BibTeX style files, you can use the
command `\citet` (cite in text) to get “author (year)” citations.

You can use the command `\citealp` (alternative cite without parentheses) to
get “author year” citations (which is useful for using citations within
parentheses, as in Gusfield:97).

If the BibTeX file contains DOI fields, the paper title in the references
section will appear as a hyperlink to the DOI, using the hyperref LaTeX
package. To disable the hyperref package, load the style file with the
`nohyperref` option:
`\usepackage[nohyperref]{acl2019}`

Compilation Issues: Some of you might encounter the following error during
compilation:

“`\pdfendlink` ended up in different nesting level than `\pdfstartlink`.”

This happens when `pdflatex` is used and a citation splits across a page
boundary. To fix this, the style file contains a patch consisting of the
following two lines: (1) `\RequirePackage{etoolbox}` (line 454 in
acl2019.sty), and (2) A long line below (line 455 in acl2019.sty).

If you still encounter compilation issues even with the patch enabled, disable
the patch by commenting the two lines, and then disable the `hyperref` package
(see above), recompile and see the problematic citation. Next rewrite that
sentence containing the citation. (See, e.g., http://tug.org/errors.html)

Digital Object Identifiers: As part of our work to make ACL materials more
widely used and cited outside of our discipline, ACL has registered as a
CrossRef member, as a registrant of Digital Object Identifiers (DOIs), the
standard for registering permanent URNs for referencing scholarly materials.
As of 2017, we are requiring all camera-ready references to contain the
appropriate DOIs (or as a second resort, the hyperlinked ACL Anthology
Identifier) to all cited works. Thus, please ensure that you use BibTeX
records that contain DOI or URLs for any of the ACL materials that you
reference. Appropriate records should be found for most materials in the
current ACL Anthology at http://aclanthology.info/.

As examples, we cite P16-1001 to show you how papers with a DOI will appear in
the bibliography. We cite C14-1001 to show how papers without a DOI but with
an ACL Anthology Identifier will appear in the bibliography.

As reviewing will be double-blind, the submitted version of the papers should
not include the authors’ names and affiliations. Furthermore, self-references
that reveal the author’s identity, _e.g._ ,

> “We previously showed Gusfield:97 …”

should be avoided. Instead, use citations such as

> “Gusfield:97 Gusfield:97 previously showed … ”

Any preliminary non-archival versions of submitted papers should be listed in
the submission form but not in the review version of the paper. ACL 2019
reviewers are generally aware that authors may present preliminary versions of
their work in other venues, but will not be provided the list of previous
presentations from the submission form.

Please do not use anonymous citations and do not include when submitting your
papers. Papers that do not conform to these requirements may be rejected
without review.

References: Gather the full set of references together under the heading
References; place the section before any Appendices. Arrange the references
alphabetically by first author, rather than by order of occurrence in the
text. By using a .bib file, as in this template, this will be automatically
handled for you. See the `\bibliography` commands near the end for more.

Provide as complete a citation as possible, using a consistent format, such as
the one for _Computational Linguistics_ or the one in the _Publication Manual
of the American Psychological Association_ APA:83. Use of full names for
authors rather than initials is preferred. A list of abbreviations for common
computer science journals can be found in the ACM _Computing Reviews_ ACM:83.

The LaTeX and BibTeX style files provided roughly fit the American
Psychological Association format, allowing regular citations, short citations
and multiple citations as described above.

  * •

Example citing an arxiv paper: rasooli-tetrault-2015.

  * •

Example article in journal citation: Ando2005.

  * •

Example article in proceedings, with location: borsch2011.

  * •

Example article in proceedings, without location: andrew2007scalable.

See corresponding .bib file for further details.

Submissions should accurately reference prior and related work, including code
and data. If a piece of prior work appeared in multiple venues, the version
that appeared in a refereed, archival venue should be referenced. If multiple
versions of a piece of prior work exist, the one used by the authors should be
referenced. Authors should not rely on automated citation indices to provide
accurate references for prior and related work.

Appendices: Appendices, if any, directly follow the text and the references
(but see above). Letter them in sequence and provide an informative title:
Appendix A. Title of Appendix.

###  3.8 Footnotes

Footnotes: Put footnotes at the bottom of the page and use 9 point font. They
may be numbered or referred to by asterisks or other symbols.111This is how a
footnote should appear. Footnotes should be separated from the text by a
line.222Note the line separating the footnotes from the text.

###  3.9 Graphics

Illustrations: Place figures, tables, and photographs in the paper near where
they are first discussed, rather than at the end, if possible. Wide
illustrations may run across both columns. Color illustrations are
discouraged, unless you have verified that they will be understandable when
printed in black ink.

Captions: Provide a caption for every illustration; number each one
sequentially in the form: “Figure 1. Caption of the Figure.” “Table 1. Caption
of the Table.” Type the captions of the figures and tables below the body,
using 10 point text. Captions should be placed below illustrations. Captions
that are one line are centered (see Table 1). Captions longer than one line
are left-aligned (see Table 2). Do not overwrite the default caption sizes.
The acl2019.sty file is compatible with the caption and subcaption packages;
do not add optional arguments.

###  3.10 Accessibility

In an effort to accommodate people who are color-blind (as well as those
printing to paper), grayscale readability for all accepted papers will be
encouraged. Color is not forbidden, but authors should ensure that tables and
figures do not rely solely on color to convey critical distinctions. A simple
criterion: All curves and points in your figures should be clearly
distinguishable without color.

##  4 Translation of non-English Terms

It is also advised to supplement non-English characters and terms with
appropriate transliterations and/or translations since not all readers
understand all such characters and terms. Inline transliteration or
translation can be represented in the order of: original-form transliteration
“translation”.

##  5 Length of Submission

The ACL 2019 main conference accepts submissions of long papers and short
papers. Long papers may consist of up to eight (8) pages of content plus
unlimited pages for references. Upon acceptance, final versions of long papers
will be given one additional page – up to nine (9) pages of content plus
unlimited pages for references – so that reviewers’ comments can be taken into
account. Short papers may consist of up to four (4) pages of content, plus
unlimited pages for references. Upon acceptance, short papers will be given
five (5) pages in the proceedings and unlimited pages for references. For both
long and short papers, all illustrations and tables that are part of the main
text must be accommodated within these page limits, observing the formatting
instructions given in the present document. Papers that do not conform to the
specified length and formatting requirements are subject to be rejected
without review.

ACL 2019 does encourage the submission of additional material that is relevant
to the reviewers but not an integral part of the paper. There are two such
types of material: appendices, which can be read, and non-readable
supplementary materials, often data or code. Do not include this additional
material in the same document as your main paper. Additional material must be
submitted as one or more separate files, and must adhere to the same anonymity
guidelines as the main paper. The paper must be self-contained: it is optional
for reviewers to look at the supplementary material. Papers should not refer,
for further detail, to documents, code or data resources that are not
available to the reviewers. Refer to Appendix A and Appendix B for further
information.

Workshop chairs may have different rules for allowed length and whether
supplemental material is welcome. As always, the respective call for papers is
the authoritative source.

## Acknowledgments

The acknowledgments should go immediately before the references. Do not number
the acknowledgments section. Do not include this section when submitting your
paper for review.

Preparing References:
Include your own bib file like this: `\bibliographystyle{acl_natbib}`
`\bibliography{acl2019}`

where `acl2019` corresponds to a acl2019.bib file.

##  Appendix A Appendices

Appendices are material that can be read, and include lemmas, formulas,
proofs, and tables that are not critical to the reading and understanding of
the paper. Appendices should be uploaded as supplementary material when
submitting the paper for review. Upon acceptance, the appendices come after
the references, as shown here. Use `\appendix` before any appendix section to
switch the section numbering over to letters.

##  Appendix B Supplemental Material

Submissions may include non-readable supplementary material used in the work
and described in the paper. Any accompanying software and/or data should
include licenses and documentation of research review as appropriate.
Supplementary material may report preprocessing decisions, model parameters,
and other details necessary for the replication of the experiments reported in
the paper. Seemingly small preprocessing decisions can sometimes make a large
difference in performance, so it is crucial to record such decisions to
precisely characterize state-of-the-art methods.

Nonetheless, supplementary material should be supplementary (rather than
central) to the paper. Submissions that misuse the supplementary material may
be rejected without review. Supplementary material may include explanations or
details of proofs or derivations that do not fit into the paper, lists of
features or feature templates, sample inputs and outputs for a system, pseudo-
code or source code, and data. (Source code and data should be separate
uploads, rather than part of the paper).

The paper should not rely on the supplementary material: while the paper may
refer to and cite the supplementary material and the supplementary material
will be available to the reviewers, they will not be asked to review the
supplementary material.