# Formalism-Driven Development: Concepts, Taxonomy, and Practice +
## 2 Preliminaries
### Abstraction Stage
#### 3.1.1 Origin Stage  
The _Origin Stage_ creates a system graph as a design model. A system graph is built on top of a channel system defined in Definition 7. Although they have equivalent expressiveness, a system graph cuts down the details that describe individual states by using a naming function to describe a group of states. Individual states are inferred from concrete contexts. This keeps a system graph succinct to model complex systems such as decentralized systems. **Definition 11** (System Graph). : _A system graph \(\mathfrak{S}\) over \((Var,Chan)\) is a tuple_  
\[\mathfrak{S}\triangleq\langle D,\mathcal{N},A,\hookrightarrow,i,g_{0},F,P, \mathcal{L}\rangle\]  
_where_  
* \(D=N\times[\widehat{Var}],\widehat{Var}\subseteq Var\) _is a set of state declarators with names in_ \(N\)_;_
* \(\mathcal{N}:D\mapsto\varphi([Var])\) _is a naming function;_
* \(A\supseteq Com\) _is a set of actions;_
* \(\hookrightarrow\subset D\times\|Var\|\times A\times D\) _is the conditional transition relation;_
* \(i\in D\) _is the initial state declarator;_
* \(g_{0}\in\|Var\|\) _is the initial guard;_
* \(F\subseteq D\) _is a set of terminal state declarators;_
* \(P\supseteq\|Var\|\) _is a set of propositions; and_
* \(\mathcal{L}:[Var]\mapsto\varphi(P)\) _is a labeling function._  
Notably, a system graph uses state declarators to describe state sets and infer individual states instead of identifying each state explicitly. A state declarator \(d\in D\) introduces a kind of state with a given name into a system by identifying interesting state variables that are essential to show features of this kind of state. The name of a state declarator is unique, i.e.,  
\[\forall\langle n,\widehat{\mathcal{V}}\rangle\in D(\
exists\langle n^{\prime },\widehat{\mathcal{V}}^{\prime}\rangle\in D:\widehat{\mathcal{V}}=\widehat{ \mathcal{V}}^{\prime}\wedge n\
eq n^{\prime}).\]  
Figure 1: Stage transition graph of an iteration. The naming function \(\mathcal{N}\) relates a set \(\mathcal{N}(d)\in\wp([\underline{Var}])\) of variable evaluations, i.e., states, to any state declarator \(d=\langle n,\widehat{\mathcal{V}}\rangle\) such that  
* \(\forall\mathcal{V}\in[\underline{Var}](\exists\dagger\widehat{\mathcal{V}}\in[ \overline{Var}]:\mathcal{V}\in\mathcal{N}(d))\); and
* \(\forall x\in Dom(\widehat{\mathcal{V}}):\widehat{\mathcal{V}}(x)=\mathcal{V}(x ),\mathcal{V}\in[\underline{Var}],Dom(\widehat{\mathcal{V}})\subseteq Dom( \mathcal{V})\). The conditional transition relation is on top of state declarators. Only one initial state declarator exists in a system graph. A system graph is nonterminal if \(F=\emptyset\). Propositions are well-formed propositional formulae in propositional logic and constructed from atomic propositions by logical connectives. A set of propositions are related to any variable evaluation, i.e., state, by the labeling function \(\mathcal{L}\). By using the state declarator, it enables describing a system in a succinct form. We are only concerned about the most critical features of states identified by interesting state variables. The evaluation of other state variables is inferred from the preceding state. **Example 1** (Transaction Client). : _We use a simplified transaction client in our developed demonstration as an example to illustrate core concepts in this paper. The complete demonstration fully developed by FDD is a prototype of Ethereum including the client-side and server-side systems._  
_A visualized system graph \(\mathfrak{S}_{tx}\) of the simplified transaction client is shown in Figure 2._  
_Each box is a state declarator consisting of two parts. The big box is also an increment (illustrated in Section 3.4). The above part is a name, while the below part is a set of state variable evaluations. State variable status has type Integer and paid has type Boolean. A one-way arrow pointing from a state declarator to another is a transition relation with a guard and an action.