# Formalism-Driven Development: Concepts, Taxonomy, and Practice +
## 2 Preliminaries
### Integration Stage
#### 3.4.1. Increment  
An increment has two types: horizontal increment and vertical increment. A **horizontal increment** is to embed a system graph into another one. Formally, embedding is defined as follows.  
**Definition 15** (Embedding).: _Let \(\mathfrak{S}_{i}=\langle D_{i},\mathcal{N}_{i},A_{i},\hookrightarrow_{i},i_{i},g _{0,i},F_{i},P_{i},\mathcal{L}_{i}\rangle,i\in[1,2]\) be two system graphs over \((\text{Var},\text{Chan})\). System graph \(\mathfrak{S}\) of embedding \(\mathfrak{S}_{1}\) into \(\mathfrak{S}_{2}\) in the place of state declarator \(d_{2}\in D_{2}\) is the tuple_  
\[\langle D,\mathcal{N},A,\hookrightarrow,i,g_{0},F,P,\mathcal{L}\rangle\]  
_where_  
* \(D=D_{1}\uplus D_{2}\)_,_ \(A=A_{1}\uplus A_{2}\)_,_ \(P=P_{1}\uplus P_{2}\)_;_
* \(\forall d\in D_{i}:\mathcal{N}(d)=\mathcal{N}_{i}(d)\)_;_
* \(\hookrightarrow=\hookrightarrow_{1}\uplus\hookrightarrow_{2}\setminus\hookrightarrow_{ d_{2}}\uplus\hookrightarrow_{d_{2}}^{\prime}\)_;_
* \(i=\begin{cases}i_{1}&d_{2}=i_{2}\\ i_{2}&d_{2}\
eq i_{2}\end{cases}\)_;_
* \(F=\begin{cases}F_{2}\setminus d_{2}\uplus F_{1}&d_{2}\in F_{2}\\ F_{2}&d_{2}\
otin F_{2}\end{cases}\)_;_
* \(\forall s\in S_{i}:\mathcal{L}(s)=\mathcal{L}_{i}(s)\)_._ \(\hookrightarrow_{d_{2}}\in\hookrightarrow_{2}\) _is a set of transition relations such that_  
1. \(\forall(d_{2},g,a,d_{2}^{\prime})\in\hookrightarrow_{2}:d_{2}\xrightarrow{g \uplus a}d_{2}^{\prime}\in\hookrightarrow_{d_{2}}\)_; and_
2. \(\forall(d_{2}^{\prime},g,a,d_{2})\in\hookrightarrow_{2}:d_{2}^{\prime} \xrightarrow{g\uplus a}d_{2}\in\hookrightarrow_{d_{2}}\)_._ \(\hookrightarrow_{d_{2}}^{\prime}\) _is a set of transition relations such that_  
1. \(\forall(d,g,a,d_{2})\in\hookrightarrow_{2}:d\xrightarrow{g_{0}\uplus a}i_{1} \in\hookrightarrow_{d_{2}}^{\prime}\)_; and_
2. \(\forall f\in F_{1}(\forall(d_{2},g,a,d)\in\hookrightarrow_{2}:f\xrightarrow{g \uplus a}d)\)_._  
**Remark 7** (Module).: _In Definition 15, if \(\mathfrak{S}_{1}\) shares state declarators, actions, propositions, naming, and labeling functions with \(\mathfrak{S}_{2}\), i.e., \(D_{1}\subseteq D_{2},A_{1}\subseteq A_{2},P_{1}\subseteq P_{2},\forall d\in D _{1}:\mathcal{N}_{1}(d)=\mathcal{N}_{2}(d),\forall s\in S_{1}:\mathcal{L}_{1}( s)=\mathcal{L}_{2}(s)\), then \(\mathfrak{S}_{1}\) is a module of \(\mathfrak{S}_{2}\)._  
_While embedding \(\mathfrak{S}_{1}\) into \(\mathfrak{S}_{2}\), if \(\mathfrak{S}_{1}\) is a module of \(\mathfrak{S}_{2}\), \(\uplus\) relation is changed to \(\cup\)._  
A **vertical increment** is an integration of a system graph into another one through parallelisms or communications, i.e., the current system graph is regarded as a subsystem that is parallel with or communicates with other subsystems in a higher-level system.  
**Example 10** (Increment in Transaction Client).: _In fact, system graph \(\mathfrak{S}_{tx}\) of the transaction client in Example 1 is a considerably high-level model. Each component encapsulates either ahorizontal increment or a vertical increment. So does an increment. For a simple but clear instance, pending integrates a system graph depicted in Figure 4 where the rounded dashed box denotes the terminal state declarator._  
_Clearly, this increment is a module of \(\mathfrak{S}_{tx}\). According to Remark 7, we can visualize modularized \(\mathfrak{S}_{tx}\) in Figure 5._