# Union Models for Model Families: Efficient Reasoning over Space and Time
## 3 Formalization of Model Families
### Formalization of Model Families and Union Models  
In this paper, we consider model families that consist of an arbitrary set of _homogeneous_ models that conform to the same metamodel. In that sense, we can define a model family as a set of typed attributed graphs that are instances of the same attributed type graph, ATG, and satisfy the constraints of that type graph. **Definition 7**. : _Model Family: A model family is a tuple MF = (\(\{G_{\text{typed}}\}\), type, ATG), where each \(G_{\text{typed}}\in\{G_{\text{typed}}\}\) is in Inst[ATG] and type: \(\{G_{\text{typed}}\}\to ATG\)._  
**Definition 8**. : _Union Model (\(M_{\text{U}}\)): Let MF be a model family with two models such that MF = (\(\{G1\), \(G2\}\), type, ATG), where type: \(G_{1}\), \(G_{2}\to ATG\) (represented as an E-Graph) and where:_  
* \(G1\) _=_ \((N_{\text{G1}}\)_,_ \(N_{\text{D\_G1}}\)_,_ \(E_{\text{G1}}\)_,_ \(E_{\text{NA\_G1}}\)_,_ \(E_{\text{EA\_G1}}\)_,_ \((\text{src}_{j}\)_,_ \(\text{tgt}_{j})\)_, where_ \(j\in\{G\)_, NA, EA\(\}\)_,_ \(\text{type}_{\text{G1}}\)_)_
* \(G2\) _=_ \((N_{\text{G2}}\)_,_ \(N_{\text{D\_G2}}\)_,_ \(E_{\text{G2}}\)_,_ \(E_{\text{NA\_G2}}\)_,_ \(E_{\text{EA\_G2}}\)_,_ \((\text{src}_{j}\)_,_ \(\text{tgt}_{j})\)_, where_ \(j\in\{G\)_, NA, EA\(\}\)_,_ \(\text{type}_{\text{G2}}\)_)_  
_In addition, G1 and G2 satisfy the following conditions:_  
* _Cond._ **1**: _If two nodes have the same name and the same type, then these nodes are considered identical. Note that we assume that each node and each edge has its own unique identifier; for simplicity, we express this identity by means of a unique name._
* _Cond._ **2**: _If two edges have the same name and the same type and if they connect between the same source and target nodes, these edges are considered identical._  
_If the above conditions are satisfied, then the union model that represents MF is a model \(M_{\text{U}}=G1\sqcup G2\) = (\(N_{\text{U}}\), \(E_{\text{U}}\), \(\text{src}_{\text{U}}\), \(\text{tgt}_{\text{U}}\), type\({}_{\text{U}}\)) such that \(N_{\text{U}}\) = \((N_{\text{G1}}\cup N_{\text{G2}}\cup N_{\text{D\_G1}}\cup N_{\text{D\_G2}})\), \(E_{\text{U}}\) = \((E_{\text{G1}}\cup\ E_{\text{G2}}\cup E_{\text{NA\_G1}}\cup E_{\text{NA\_G2}} \cup E_{\text{EA\_G1}}\cup E_{\text{EA\_G2}})\), and the functions \(\text{src}_{\text{U}}\), \(\text{tgt}_{\text{U}}\), and type\({}_{\text{U}}\) are:_  
\[\text{src}_{\text{U}}(e)= \begin{cases}\text{src}_{\text{G1}}(e)&\text{if }e\in E_{\text{G1}}\\ \text{src}_{\text{NA\_G1}}(e)&\text{if }e\in E_{\text{NA\_G1}}\\ \text{src}_{\text{EA\_G1}}(e)&\text{if }e\in E_{\text{EA\_G1}}\\ \text{src}_{\text{G2}}(e)&\text{if }e\in E_{\text{G2}}\\ \text{src}_{\text{NA\_G2}}(e)&\text{if }e\in E_{\text{NA\_G2}}\\ \text{src}_{\text{EA\_G2}}(e)&\text{if }e\in E_{\text{EA\_G2}}\\ \end{cases} \]  
\[\text{tgt}_{\text{U}}(e)= \begin{cases}\text{tgt}_{\text{G1}}(e)&\text{if }e\in E_{\text{G1}}\\ \text{tgt}_{\text{NA\_G1}}(e)&\text{if }e\in E_{\text{NA\_G1}}\\ \text{tgt}_{\text{EA\_G1}}(e)&\text{if }e\in E_{\text{EA\_G1}}\\ \text{tgt}_{\text{G2}}(e)&\text{if }e\in E_{\text{G2}}\\ \text{tgt}_{\text{NA\_G2}}(e)&\text{if }e\in E_{\text{NA\_G2}}\\ \text{tgt}_{\text{EA\_G2}}(e)&\text{if }e\in E_{\text{EA\_G2}}\\ \end{cases} \]  
Figure 12: An instance typed graph ITG of the E-graph EG in Figure 11.  
\[type_{U}(elem)= \begin{cases}type_{G1}(e)&\text{if }elem\in N_{G1}\cup N_{D\_G1} \cup E_{G1}\cup E_{NA\_G1}\ \cup E_{EA\_G1}\\ type_{G2}(e)&\text{if }elem\in N_{G2}\cup N_{D\_G2}\cup E_{G2}\cup E_{NA\_G2}\ \cup E_{EA\_G2}\end{cases} \]  
Provided that conditions Cond. 1 and Cond. 2 in Definition 6 are respected, the union operation can be generalized into an \(MF\) of arbitrary size. That is, given \(MF=(\{G1,G2,\ldots,Gn\},type,ATG)\), its union model is \(M_{U}=G1\sqcup G2\sqcup G3\ldots\sqcup Gn\). The union operation is _incremental_.